WIP (new module structure is slow)

_CoqProject

@@ -2,13 +2,16 @@
 
 theories/hacspec/Hacspec_helpers.v
 theories/hacspec/Hacspec_ovn_Ovn_traits.v
-#theories/hacspec/Hacspec_ovn_Ovn_z_89_.v
+theories/hacspec/Hacspec_ovn_Ovn_z_89_.v
 theories/hacspec/Hacspec_ovn.v
 theories/hacspec/Hacspec_ovn_group_and_field.v
+
 theories/hacspec/Hacspec_ovn_sigma_setup.v
 theories/hacspec/Hacspec_ovn_schnorr.v
 theories/hacspec/Hacspec_ovn_or.v
-theories/hacspec/Hacspec_ovn_total_proof.v
+
+# theories/hacspec/Hacspec_ovn_total_proof.v
+# theories/hacspec/Hacspec_ovn_proof_z_89.v
 
 # -R theories/hacspec Examples
 # -arg -w

theories/hacspec/Hacspec_helpers.v

@@ -434,8 +434,23 @@ Ltac pattern_rhs pat :=
 Ltac pattern_rhs_f f pat :=
   match goal with | |- context [ f ?lhs = f ?rhs ] => let H_rhs := fresh in set (H_rhs := rhs) ; pattern pat in H_rhs ; subst H_rhs end.
 
-Axiom hacspec_function_guarantees : forall {A B} (f : both A -> both B) (x : both A),
+Lemma hacspec_function_guarantees : forall {A B} (f : both A -> both B) (x : both A),
     is_pure (f x) = is_pure (f (ret_both (is_pure x))).
+Proof.
+  intros.
+
+  f_equal.
+  f_equal.
+  f_equal.
+
+  apply both_eq.
+
+  destruct x as [[] [] ?].
+  now inversion is_valid_both ; subst.
+Qed.
+
+(* Axiom hacspec_function_guarantees : forall {A B} (f : both A -> both B) (x : both A), *)
+(*     is_pure (f x) = is_pure (f (ret_both (is_pure x))). *)
 
 Corollary hacspec_function_guarantees2 : forall {A B C} (f : both A -> both B -> both C) (x : both A) (y : both B),
     is_pure (f x y) = is_pure (f (ret_both (is_pure x)) (ret_both (is_pure y))).

theories/hacspec/Hacspec_ovn.v

@@ -56,35 +56,40 @@ Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
 
 From OVN Require Import Hacspec_ovn_Ovn_traits.
 Export Hacspec_ovn_Ovn_traits.
-Module HacspecOVN.
-(** Move arguments to context *)
-Parameter (v_G : choice_type).
 
-(* TODO: Cannot find instance in hacspec lib? *)
-#[global] Instance v_G_t_copy : t_Copy v_G := copy.
-#[global] Instance v_G_t_partial_eq : t_PartialEq v_G v_G := partial_eq.
-#[global] Instance v_G_t_eq : t_Eq v_G := is_eq.
-#[global] Instance v_G_t_clone : t_Clone v_G := clone.
-#[global] Instance v_G_t_serialize : t_Serialize v_G := serialize.
+Module Type HacspecOvnParameter.
+  (** Move arguments to context *)
+  Parameter (v_G : choice_type).
 
-Parameter (v_G_t_Group : t_Group v_G).
-Instance v_G_t_Group_temp : t_Group v_G := v_G_t_Group.
+  Parameter (v_G_t_Group : t_Group v_G).
 
-Parameter (v_A : choice_type).
-Parameter (v_A_t_Sized : t_Sized v_A).
-Instance v_A_t_Sized_temp : t_Sized v_A := v_A_t_Sized.
+  Parameter (v_A : choice_type).
+  Parameter (v_A_t_Sized : t_Sized v_A).
 
-Parameter (v_A_t_HasActions : t_HasActions v_A).
-Instance v_A_t_HasActions_temp : t_HasActions v_A := v_A_t_HasActions.
+  Parameter (v_A_t_HasActions : t_HasActions v_A).
 
-Parameter (n : both uint_size).
+  Parameter (n : both uint_size).
 
-(* Extra from code *)
-Parameter (v_G_t_Sized : t_Sized v_G).
-Instance v_G_t_Sized_temp : t_Sized v_G := v_G_t_Sized.
+  (* Extra from code *)
+  Parameter (v_G_t_Sized : t_Sized v_G).
 
-Notation "'v_Z'" := f_Z : hacspec_scope.
+  Notation "'v_Z'" := f_Z : hacspec_scope.
+End HacspecOvnParameter.
 
+Module HacspecOvn (HOP : HacspecOvnParameter).
+  Include HOP.
+
+  Instance v_G_t_Group_temp : t_Group v_G := v_G_t_Group.
+  Instance v_A_t_Sized_temp : t_Sized v_A := v_A_t_Sized.
+  Instance v_A_t_HasActions_temp : t_HasActions v_A := v_A_t_HasActions.
+  Instance v_G_t_Sized_temp : t_Sized v_G := v_G_t_Sized.
+
+  (* TODO: Cannot find instance in hacspec lib? *)
+  #[global] Instance v_G_t_copy : t_Copy v_G := copy.
+  #[global] Instance v_G_t_partial_eq : t_PartialEq v_G v_G := partial_eq.
+  #[global] Instance v_G_t_eq : t_Eq v_G := is_eq.
+  #[global] Instance v_G_t_clone : t_Clone v_G := clone.
+  #[global] Instance v_G_t_serialize : t_Serialize v_G := serialize.
 (** * Generated code *)
 
 Equations sub (x : both v_Z) (y : both v_Z) : both v_Z :=
@@ -654,4 +659,4 @@ Fail Next Obligation.
 
 Definition contract_OVN  : @Contract _ (state_OVN) (Msg_OVN) (state_OVN) (t_ParseError) state_OVN_Serializable Msg_OVN_Serializable state_OVN_Serializable _ :=
   build_contract init_OVN receive_OVN.
-End HacspecOVN.
+End HacspecOvn.

theories/hacspec/Hacspec_ovn_Ovn_z_89_.v

@@ -55,10 +55,10 @@ Equations Build_t_z_89_ {f_z_val : both int8} : both (t_z_89_) :=
 Fail Next Obligation.
 Notation "'Build_t_z_89_' '[' x ']' '(' 'f_z_val' ':=' y ')'" := (Build_t_z_89_ (f_z_val := y)).
 
-Instance t_z_89_t_Copy : t_Copy t_z_89_. Admitted.
-Instance t_z_89_t_PartialEq : t_PartialEq t_z_89_ t_z_89_. Admitted.
-Instance t_z_89_t_Clone : t_Clone t_z_89_. Admitted.
-Instance t_z_89_t_Serialize : t_Serialize t_z_89_. Admitted.
+Instance t_z_89_t_Copy : t_Copy t_z_89_ := _.
+Instance t_z_89_t_PartialEq : t_PartialEq t_z_89_ t_z_89_ := _.
+Instance t_z_89_t_Clone : t_Clone t_z_89_ := _.
+Instance t_z_89_t_Serialize : t_Serialize t_z_89_ := _.
 
 #[global] Program Instance t_z_89__t_Field : t_Field t_z_89_ :=
   let f_q := solve_lift (Build_t_z_89_ (f_z_val := ret_both (89 : int8))) : both t_z_89_ in
@@ -72,7 +72,6 @@ Instance t_z_89_t_Serialize : t_Serialize t_z_89_. Admitted.
   let f_opp := fun  (x : both t_z_89_) => letb q___ := (f_z_val f_q) .- (ret_both (1 : int8)) in
   letb x___ := (f_z_val x) .% q___ in
   solve_lift (Build_t_z_89_ (f_z_val := q___ .- x___)) : both t_z_89_ in
-  let f_sub := fun  (x : both t_z_89_) (y : both t_z_89_) => solve_lift (f_add x (f_opp y)) : both t_z_89_ in
   let f_mul := fun  (x : both t_z_89_) (y : both t_z_89_) => letb q___ := (f_z_val f_q) .- (ret_both (1 : int8)) in
   letb (x___ : both int16) := cast_int (WS2 := _) ((f_z_val x) .% q___) in
   letb (y___ : both int16) := cast_int (WS2 := _) ((f_z_val y) .% q___) in
@@ -83,7 +82,6 @@ Instance t_z_89_t_Serialize : t_Serialize t_z_89_. Admitted.
   f_field_one := (@f_field_one);
   f_add := (@f_add);
   f_opp := (@f_opp);
-  f_sub := (@f_sub);
   f_mul := (@f_mul)|}.
 Fail Next Obligation.
 Hint Unfold t_z_89__t_Field.
@@ -119,15 +117,13 @@ Hint Unfold t_z_89__t_Field.
   (* else ret_both (tt : 'unit) in *)
   letm[choice_typeMonad.result_bind_code t_g_z_89_] hoist30 := v_Break x in
   ControlFlow_Continue (never_to_any hoist30))) : both t_g_z_89_ in
-  let f_div := fun  (x : both t_g_z_89_) (y : both t_g_z_89_) => solve_lift (f_prod x (f_group_inv y)) : both t_g_z_89_ in
   {| f_Z := (@f_Z);
   f_g := (@f_g);
   f_hash := (@f_hash);
   f_g_pow := (@f_g_pow);
   f_pow := (@f_pow);
   f_group_one := (@f_group_one);
   f_prod := (@f_prod);
-  f_group_inv := (@f_group_inv);
-  f_div := (@f_div)|}.
+  f_group_inv := (@f_group_inv)|}.
 Fail Next Obligation.
 Hint Unfold t_g_z_89__t_Group.

theories/hacspec/Hacspec_ovn_group_and_field.v

@@ -415,8 +415,11 @@ HB.mixin Record is_setoid_field_properties (V : Type) of field_op V & eqR V :=
 
     (* One is not zero *)
     sf_one_not_zero : ¬ (@eq_relation V sf_one sf_zero) ;
+    (* sf_zero_is_zero : U  *)
 
     sf_mulV : forall x, ¬ (@eq_relation V x sf_zero)  -> @eq_relation V (sf_mul (sf_inv x) x) sf_one ;
+
+    (* zero_to_zero : forall x, (@eq_relation V x sf_zero) -> F x = F sf_zero *)
   }.
 
 (* Given setoid lower relation and a setoid with field-like structure, we can lower to a field *)
@@ -485,9 +488,6 @@ HB.instance Definition _  (SG : lowerToField) :=
   GRing.Nmodule_isZmodule.Build  (T (s := SG)) (setoid_lower_left_inverse sf_addN).
 
 (* begin details : we lower mul inverse *)
-(* Property of equality for fields ! *)
-Parameter zero_to_zero : forall (SG : lowerToField), forall x, (@eq_relation _ (U (s := SG) x) sf_zero) -> x = setoid_lower0 sf_zero.
-
 (* field has mul inverse *)
 Lemma setoid_lower_mulVr :
   forall {G : lowerToField},
@@ -502,7 +502,8 @@ Proof.
   apply (H (U x)).
   red ; intros.
   apply (ssrbool.elimN eqP Hneq) ; clear Hneq.
-  now apply zero_to_zero.
+  rewrite <- F_U_cancel.
+  now apply lower_to_eq.
 Qed.
 
 Definition f_lower_mulVr_subproof {G : lowerToField} : _ :=

theories/hacspec/Hacspec_ovn_or.v

@@ -78,10 +78,10 @@ Import PackageNotation.
 (** * OR protocol *)
 (* Setup and definitions for the OR protocol *)
 (* This allows us to instantiate the SigmaProtocol library *)
-Module OVN_or_proof_preconditions (HGPA : HacspecGroupParamAxiom).
+Module OVN_or_proof_preconditions (HOP : HacspecOvnParameter) (HOGaFP : HacspecOvnGroupAndFieldParameter HOP) (HOGaFE : HacspecOvnGroupAndFieldExtra HOP HOGaFP) (HGPA : HacspecGroupParamAxiom HOP HOGaFP HOGaFE).
   Include HGPA.
   Export HGPA.
-
+  
   Module MyParam <: SigmaProtocolParams.
 
     Definition Witness : finType := prod (prod (Finite.clone _ 'Z_q) (Finite.clone _ 'bool)) gT.
@@ -276,21 +276,17 @@ End OVN_or_proof_preconditions.
 (** * OR protocol proofs *)
 (* Shows equality between above code and Hax generated code.   *)
 (* Then proofs SHVZK and extractor correctness for OR protocol *)
-Module OVN_or_proof (HGPA : HacspecGroupParamAxiom).
-  Module proof_args := OVN_or_proof_preconditions HGPA.
-
-  Import HGPA.
-  Import proof_args.
+Module OVN_or_proof (HOP : HacspecOvnParameter) (HOGaFP : HacspecOvnGroupAndFieldParameter HOP) (HOGaFE : HacspecOvnGroupAndFieldExtra HOP HOGaFP) (HGPA : HacspecGroupParamAxiom HOP HOGaFP HOGaFE).
+  Module proof_args := OVN_or_proof_preconditions HOP HOGaFP HOGaFE HGPA.
+  Include proof_args.
+  Export proof_args.
 
   Import MyParam.
   Import MyAlg.
 
   Import Sigma.Oracle.
   Import Sigma.
 
-  Include proof_args.
-  Export proof_args.
-
   Transparent zkp_one_out_of_two.
 
   (* Mapping between d2, r2 and w, d for sampled randomness *)
@@ -642,8 +638,7 @@ Module OVN_or_proof (HGPA : HacspecGroupParamAxiom).
         rewrite mulg1 in H.
         rewrite mulVg in H.
 
-        fold g.
-        rewrite <- H.
+        setoid_rewrite <- H.
         reflexivity.
       }
 
@@ -744,8 +739,8 @@ Module OVN_or_proof (HGPA : HacspecGroupParamAxiom).
         unfold Sigma_locs in H0 ; rewrite <- fset1E in H0 ; rewrite in_fset1 in H0.
         now rewrite <- get_heap_set_heap.
     }
-    (* Qed. *)
-    (* Fail Timeout 5 *) Qed. (* Admitted. *) (* SLOW: 525.61 sec *)
+    Qed.
+    (* Fail Timeout 5 Qed. Admitted. (* SLOW: 525.61 sec *) *)
 
   (* The packaged version for running the hacspec code *)
   Program Definition hacspec_or_run :