WIP Extractor definition

AU-COBRA · May 16, 2024 · 0774662 · 0774662
1 parent 57730b9
commit 0774662
Show file tree

Hide file tree

Showing 3 changed files with 302 additions and 44 deletions.
diff --git a/theories/hacspec/Hacspec_ovn_Ovn_traits.v b/theories/hacspec/Hacspec_ovn_Ovn_traits.v
@@ -33,6 +33,7 @@ Class t_Field (v_Self : _) `{ t_Copy v_Self} `{ t_PartialEq v_Self v_Self} `{ t_
   f_opp : (both v_Self -> both v_Self) ;
   f_sub : (both v_Self -> both v_Self -> both v_Self) ;
   f_mul : (both v_Self -> both v_Self -> both v_Self) ;
+  f_inv : (both v_Self -> both v_Self) ;
 }.
 
 Class t_Group (v_Self : _) `{ t_Copy v_Self} `{ t_PartialEq v_Self v_Self} `{ t_Eq v_Self} `{ t_Clone v_Self} `{ t_Serialize v_Self} := {
@@ -51,7 +52,7 @@ Class t_Group (v_Self : _) `{ t_Copy v_Self} `{ t_PartialEq v_Self v_Self} `{ t_
   f_pow : (both v_Self -> both f_Z -> both v_Self) ;
   f_group_one : (both v_Self) ;
   f_prod : (both v_Self -> both v_Self -> both v_Self) ;
-  f_inv : (both v_Self -> both v_Self) ;
+  f_group_inv : (both v_Self -> both v_Self) ;
   f_div : (both v_Self -> both v_Self -> both v_Self) ;
   f_hash : (both (t_Vec v_Self t_Global) -> both f_Z) ;
 }.
diff --git a/theories/hacspec/Hacspec_ovn_Ovn_z_89_.v b/theories/hacspec/Hacspec_ovn_Ovn_z_89_.v
@@ -107,7 +107,7 @@ Hint Unfold t_z_89__t_Field.
       solve_lift (f_prod result g) : (both t_g_z_89_))) result in
   solve_lift result : both t_g_z_89_ in
   let f_g_pow := fun  (x : both t_z_89_) => solve_lift (f_pow f_g x) : both t_g_z_89_ in
-  let f_inv := fun  (x : both t_g_z_89_) => solve_lift (run (letb _ := foldi_both_list (f_into_iter (Build_t_Range (f_start := ret_both (0 : int8)) (f_end := ret_both (89 : int8)))) (fun j =>
+  let f_group_inv := fun  (x : both t_g_z_89_) => solve_lift (run (letb _ := foldi_both_list (f_into_iter (Build_t_Range (f_start := ret_both (0 : int8)) (f_end := ret_both (89 : int8)))) (fun j =>
     ssp (fun _ =>
       letb g_value := Build_t_g_z_89_ (f_g_val := j) in
       solve_lift (ifb (f_prod x g_value) =.? f_group_one
@@ -119,15 +119,15 @@ 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_inv y)) : 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_inv := (@f_inv);
+  f_group_inv := (@f_inv);
   f_div := (@f_div)|}.
 Fail Next Obligation.
 Hint Unfold t_g_z_89__t_Group.