fact: Definition P_i (i : pid) (b : bool): package (P_i_locs i) Sigma1_I P_i_E := [package #def #[ INIT ] (_ : 'unit) : 'public_key { #import {sig #[ Sigma1.Sigma.RUN ] : chRelation1 → chTranscript1} as ZKP ;; #import {sig #[ Sigma1.Sigma.VERIFY ] : chTranscript1 → 'bool} as VER ;; x ← sample uniform i_secret ;; #put (skey_loc i) := x ;; let y := (fto (g ^+ (otf x))) : public in zkp ← ZKP (y, x) ;; ret (y, zkp) } ; #def #[ CONSTRUCT ] (m : 'public_keys) : 'unit { #import {sig #[ Sigma1.Sigma.VERIFY ] : chTranscript1 → 'bool} as VER ;; #assert (size (domm m) == n) ;; let key := fto (compute_key m i) in #put (ckey_loc i) := key ;; @ret 'unit Datatypes.tt } ; #def #[ VOTE ] (v : 'bool) : 'public { skey ← get (skey_loc i) ;; ckey ← get (ckey_loc i) ;; if b then let vote := (otf ckey ^+ skey * g ^+ v) in @ret 'public (fto vote) else let vote := (otf ckey ^+ skey * g ^+ (negb v)) in @ret 'public (fto vote) } ].
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_composition Package Prelude SigmaProtocol Schnorr DDH) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)