proposition: Lemma code_pkg_equiv m i j (vote : 'bool): ⊢ ⦃ λ '(h₀, h₁), h₀ = h₁ ⦄ get_op_default (Exec_i_realised true m i j) ((Exec i), ('bool, 'public)) vote ≈ Exec_i_realised_code m i j vote ⦃ eq ⦄.
proof: Proof. unfold Exec_i_realised. rewrite get_op_default_link. erewrite get_op_default_spec. 2: { cbn. rewrite eqnE eq_refl. done. } ssprove_code_simpl. simpl. repeat choice_type_eqP_handle. rewrite !cast_fun_K. ssprove_code_simpl. simpl. ssprove_code_simpl. ssprove_code_simpl_more. simpl. ssprove_sync_eq=>x. simpl. ssprove_code_simpl_more. ssprove_sync_eq. ssprove_sync_eq=>rel1. ssprove_sync_eq=>r1. ssprove_sync_eq. ssprove_code_simpl. ssprove_contract_put_get_lhs. ssprove_contract_put_get_rhs. ssprove_sync_eq. simpl. ssprove_code_simpl. ssprove_sync_eq=>a. ssprove_sync_eq. ssprove_sync_eq=>v. apply r_uniform_bij with (f := (fun (x : Arit (@uniform i_secret Sigma1.MyParam.Witness_pos)) => (x : Arit (@uniform i_secret Secret_pos)))). 1: exact (inv_bij (fun x => erefl)). intros. match goal with | |- context [⊢ ⦃ _ ⦄ bind (assertD ?v ?z) ?y ≈ ?x ⦃ _ ⦄] => set (temp1 := x) ; set (temp2 := y) ; set (temp3 := z) ; set (temp4 := v) in * end. apply (r_transL (@assertD _ temp4 (fun z => x ← temp3 z ;; temp2 x))). 1:{ eapply r_transR. 1:{ apply r_bind_assertD_sym. } apply rreflexivity_rule. } subst temp1 temp2 temp3 temp4. apply (@r_assertD_same (chFin (mkpos #|gT|)) _). intros. simpl. ssprove_sync_eq=>a0. ssprove_sync_eq. ssprove_contract_put_get_lhs. ssprove_contract_put_get_rhs. ssprove_sync_eq. simpl. ssprove_sync_eq=>a1. ssprove_sync_eq. ssprove_sync_eq=>a2. match goal with | |- context [⊢ ⦃ _ ⦄ bind (assertD ?v ?z) ?y ≈ ?x ⦃ _ ⦄] => set (temp1 := x) ; set (temp2 := y) ; set (temp3 := z) ; set (temp4 := v) in * end. apply (r_transL (@assertD _ temp4 (fun z => x ← temp3 z ;; temp2 x))). 1:{ eapply r_transR. 1:{ apply r_bind_assertD_sym. } apply rreflexivity_rule. } subst temp1 temp2 temp3 temp4. hnf. apply r_assertD_same. intros. ssprove_sync_eq. ssprove_sync_eq=>a3. ssprove_sync_eq=>a4. apply r_ret. intros. subst. reflexivity. Qed.
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)