-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
7 changed files
with
951 additions
and
107 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -5,7 +5,7 @@ authors = ["Lasse Letager Hanse <[email protected]>"] | |
| edition = "2018" | ||
|
|
||
| [lib] | ||
| path = "src/ovn_group.rs" | ||
| path = "src/ovn_no_group.rs" | ||
|
|
||
| [dependencies] | ||
| hacspec-lib = { git = "https://github.com/hacspec/hacspec.git" } | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,140 @@ | ||
| (* File automatically generated by Hacspec *) | ||
| Set Warnings "-notation-overridden,-ambiguous-paths". | ||
| From Crypt Require Import choice_type Package Prelude. | ||
| Import PackageNotation. | ||
| From extructures Require Import ord fset. | ||
| From mathcomp Require Import word_ssrZ word. | ||
| From Jasmin Require Import word. | ||
|
|
||
| From Coq Require Import ZArith. | ||
| From Coq Require Import Strings.String. | ||
| Import List.ListNotations. | ||
| Open Scope list_scope. | ||
| Open Scope Z_scope. | ||
| Open Scope bool_scope. | ||
|
|
||
| From Hacspec Require Import ChoiceEquality. | ||
| From Hacspec Require Import LocationUtility. | ||
| From Hacspec Require Import Hacspec_Lib_Comparable. | ||
| From Hacspec Require Import Hacspec_Lib_Pre. | ||
| From Hacspec Require Import Hacspec_Lib. | ||
|
|
||
| Open Scope hacspec_scope. | ||
| Import choice.Choice.Exports. | ||
|
|
||
| Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. | ||
|
|
||
| Require Import Hacspec_ovn_Ovn_traits. | ||
| Export Hacspec_ovn_Ovn_traits. | ||
|
|
||
| Definition t_g_z_89_ : choice_type := | ||
| 'unit. | ||
| Equations Build_t_g_z_89_ : both (fset []) (fset []) (t_g_z_89_) := | ||
| Build_t_g_z_89_ := | ||
| solve_lift (ret_both (tt (* Empty tuple *) : (t_g_z_89_))) : both (fset []) (fset []) (t_g_z_89_). | ||
| Fail Next Obligation. | ||
|
|
||
| Definition t_z_89_ : choice_type := | ||
| 'unit. | ||
| Equations Build_t_z_89_ : both (fset []) (fset []) (t_z_89_) := | ||
| Build_t_z_89_ := | ||
| solve_lift (ret_both (tt (* Empty tuple *) : (t_z_89_))) : both (fset []) (fset []) (t_z_89_). | ||
| Fail Next Obligation. | ||
|
|
||
| #[global] Program Instance t_z_89__t_Z_Field : t_Z_Field t_z_89_ := _. | ||
| Next Obligation. | ||
| refine ( | ||
| let f_field_type := int32 : choice_type in | ||
| let f_q := fun {L : {fset Location}} {I : Interface} => solve_lift (ret_both (89 : int32)) : both (L :|: fset []) I int32 in | ||
| let f_random_field_elem := fun {L1 : {fset Location}} {I1 : Interface} (random : both L1 I1 int32) => solve_lift (random .% ((f_q ) .- (ret_both (1 : int32)))) : both (L1 :|: fset []) I1 int32 in | ||
| let f_field_zero := fun {L : {fset Location}} {I : Interface} => solve_lift (ret_both (0 : int32)) : both (L :|: fset []) I int32 in | ||
| let f_field_one := fun {L : {fset Location}} {I : Interface} => solve_lift (ret_both (1 : int32)) : both (L :|: fset []) I int32 in | ||
| let f_add := fun {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) => solve_lift ((x .+ y) .% ((f_q ) .- (ret_both (1 : int32)))) : both (L1 :|: L2 :|: fset []) (I1 :|: I2) int32 in | ||
| let f_sub := fun {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) => solve_lift (((x .+ ((f_q ) .- (ret_both (1 : int32)))) .- y) .% ((f_q ) .- (ret_both (1 : int32)))) : both (L1 :|: L2 :|: fset []) (I1 :|: I2) int32 in | ||
| let f_mul := fun {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) => solve_lift ((x .* y) .% ((f_q ) .- (ret_both (1 : int32)))) : both (L1 :|: L2 :|: fset []) (I1 :|: I2) int32 in | ||
| {| f_field_type := (@f_field_type); | ||
| f_q_loc := (fset [] : {fset Location}); | ||
| f_q := (@f_q); | ||
| f_random_field_elem_loc := (fset [] : {fset Location}); | ||
| f_random_field_elem := (@f_random_field_elem); | ||
| f_field_zero_loc := (fset [] : {fset Location}); | ||
| f_field_zero := (@f_field_zero); | ||
| f_field_one_loc := (fset [] : {fset Location}); | ||
| f_field_one := (@f_field_one); | ||
| f_add_loc := (fset [] : {fset Location}); | ||
| f_add := (@f_add); | ||
| f_sub_loc := (fset [] : {fset Location}); | ||
| f_sub := (@f_sub); | ||
| f_mul_loc := (fset [] : {fset Location}); | ||
| f_mul := (@f_mul)|} | ||
| ). | ||
| easy. | ||
| easy. | ||
| easy. | ||
| easy. | ||
| easy. | ||
| exact int_eqdec. | ||
| easy. | ||
| easy. | ||
| Unshelve. | ||
| all: try normalize_fset. | ||
| all: try solve_single_fset_fsubset. | ||
|
|
||
| unfold f_parameter_cursor_loc. | ||
|
|
||
| Next Obligation. | ||
| unfold t_z_89__t_Z_Field_obligation_4. | ||
| Fail Next Obligation. | ||
| Hint Unfold t_z_89__t_Z_Field. | ||
|
|
||
| Definition res_loc : Location := | ||
| (int32;0%nat). | ||
| Definition result_loc : Location := | ||
| (int32;1%nat). | ||
| #[global] Program Instance t_g_z_89__t_Group : t_Group t_g_z_89_ t_z_89_ := | ||
| let f_group_type := int32 : choice_type in | ||
| let f_g := fun {L : {fset Location}} {I : Interface} => solve_lift (ret_both (3 : int32)) : both (L :|: fset []) I int32 in | ||
| let f_hash := fun {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Vec int32 t_Global)) => letb res loc(res_loc) := f_field_one (ret_both (tt : 'unit)) in | ||
| letb _ := foldi_both_list (f_into_iter x) (fun y => | ||
| ssp (fun _ => | ||
| assign todo(term) : (both (*1*)(L1:|:fset [res_loc]) (I1) 'unit))) (ret_both (tt : 'unit)) in | ||
| solve_lift res : both (L1 :|: fset [res_loc]) I1 int32 in | ||
| let f_g_pow := fun {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) => solve_lift (f_pow (f_g (ret_both (tt : 'unit))) x) : both (L1 :|: fset []) I1 int32 in | ||
| let f_pow := fun {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (g : both L1 I1 int32) (x : both L2 I2 int32) => letb result loc(result_loc) := f_group_one (ret_both (tt : 'unit)) in | ||
| letb _ := foldi_both_list (f_into_iter (Build_t_Range (f_start := ret_both (0 : int32)) (f_end := x .% ((f_q (ret_both (tt : 'unit))) .- (ret_both (1 : int32)))))) (fun i => | ||
| ssp (fun _ => | ||
| assign todo(term) : (both (*1*)(L1:|:L2:|:fset [result_loc]) (I1:|:I2) 'unit))) (ret_both (tt : 'unit)) in | ||
| solve_lift result : both (L1 :|: L2 :|: fset [result_loc]) (I1 :|: I2) int32 in | ||
| let f_group_one := fun {L : {fset Location}} {I : Interface} => solve_lift (ret_both (1 : int32)) : both (L :|: fset []) I int32 in | ||
| let f_prod := fun {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) => solve_lift (((x .% (f_q (ret_both (tt : 'unit)))) .* (y .% (f_q (ret_both (tt : 'unit))))) .% (f_q (ret_both (tt : 'unit)))) : both (L1 :|: L2 :|: fset []) (I1 :|: I2) int32 in | ||
| let f_inv := fun {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) => solve_lift (run (letb _ := foldi_both_list (f_into_iter (Build_t_Range (f_start := ret_both (0 : int32)) (f_end := ret_both (89 : int32)))) (fun j => | ||
| ssp (fun _ => | ||
| solve_lift (ifb (f_prod x j) =.? (f_group_one (ret_both (tt : 'unit))) | ||
| then letm[choice_typeMonad.result_bind_code int32] hoist1 := v_Break j in | ||
| ControlFlow_Continue (never_to_any hoist1) | ||
| else ()) : (both (*0*)(L1:|:fset []) (I1) (t_ControlFlow int32 'unit)))) (ret_both (tt : 'unit)) in | ||
| letb _ := ifb not (ret_both (false : 'bool)) | ||
| then never_to_any (panic (ret_both (assertion failed: false : chString))) | ||
| else () in | ||
| letm[choice_typeMonad.result_bind_code int32] hoist2 := v_Break x in | ||
| ControlFlow_Continue (never_to_any hoist2))) : both (L1 :|: fset []) I1 int32 in | ||
| let f_div := fun {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) => solve_lift (f_prod x (f_inv y)) : both (L1 :|: L2 :|: fset []) (I1 :|: I2) int32 in | ||
| {| f_group_type := (@f_group_type); | ||
| f_g_loc := (fset [] : {fset Location}); | ||
| f_g := (@f_g); | ||
| f_hash_loc := (fset [res_loc] : {fset Location}); | ||
| f_hash := (@f_hash); | ||
| f_g_pow_loc := (fset [] : {fset Location}); | ||
| f_g_pow := (@f_g_pow); | ||
| f_pow_loc := (fset [result_loc] : {fset Location}); | ||
| f_pow := (@f_pow); | ||
| f_group_one_loc := (fset [] : {fset Location}); | ||
| f_group_one := (@f_group_one); | ||
| f_prod_loc := (fset [] : {fset Location}); | ||
| f_prod := (@f_prod); | ||
| f_inv_loc := (fset [] : {fset Location}); | ||
| f_inv := (@f_inv); | ||
| f_div_loc := (fset [] : {fset Location}); | ||
| f_div := (@f_div)|}. | ||
| Fail Next Obligation. | ||
| Hint Unfold t_g_z_89__t_Group. |
Oops, something went wrong.