Showed that the constrained state property is decidable for ELMO

theories/Core/Equivocation.v

@@ -79,6 +79,12 @@ Proof.
   by apply sum_weights_subseteq.
 Qed.
 
+#[export] Instance not_heavy_dec
+   `{BasicEquivocation st validator Cv threshold}
+   `{!DecidableReachableThreshold validator Cv threshold} :
+   forall (s : st), Decision (not_heavy s).
+Proof. by intros s; apply rt_dec. Qed.
+
 (** *** State-message oracles and endowing states with history
 
   Our first step is to define some useful concepts in the context of a single VLSM.

theories/Core/ReachableThreshold.v

@@ -20,6 +20,11 @@ Class ReachableThreshold V Cv (threshold : R) `{Hm : Measurable V} `{FinSet V Cv
 
 #[global] Hint Mode ReachableThreshold - - - ! ! ! ! ! ! ! ! ! ! : typeclass_instances.
 
+Class DecidableReachableThreshold V Cv (threshold : R) `{ReachableThreshold V Cv threshold} :=
+  rt_dec :> forall (vs : Cv), Decision (sum_weights vs <= threshold)%R.
+
+#[global] Hint Mode DecidableReachableThreshold - - - ! ! ! ! ! ! ! ! ! ! ! : typeclass_instances.
+
 Section sec_reachable_threshold_props.
 
 Context