fact: Definition Exec_i (i j : pid) (m : chMap pid (chProd public choiceTranscript1)): package fset0 EXEC_i_I (Exec_i_E i) := [package #def #[ Exec i ] (v : 'bool) : 'public { #import {sig #[ INIT ] : 'unit → 'public_key} as Init ;; #import {sig #[ CONSTRUCT ] : 'public_keys → 'unit} as Construct ;; #import {sig #[ VOTE ] : 'bool → 'public} as Vote ;; #import {sig #[ Sigma1.Sigma.RUN ] : chRelation1 → chTranscript1} as ZKP ;; pk ← Init Datatypes.tt ;; x ← sample uniform i_secret ;; let y := (fto (g ^+ (otf x))) : public in zkp ← ZKP (y, x) ;; let m' := setm (setm m j (y, zkp)) i pk in Construct m' ;; vote ← Vote v ;; @ret 'public 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)