Timings for p224_64_new.v
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev/./src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.timing
- /home/gitlab-runner/builds/gGKko-aj/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev/./src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.timing
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Arithmetic.PrimeFieldTheorems.
Require Import Crypto.Bedrock.Field.Interface.Representation.
Require Import Crypto.Bedrock.Field.Synthesis.New.ComputedOp.
Require Import Crypto.Bedrock.Field.Synthesis.New.WordByWordMontgomery.
Require Import Crypto.Bedrock.Field.Translation.Parameters.Defaults32.
Require Import Crypto.Bedrock.Specs.Field.
Require Import bedrock2.WeakestPreconditionProperties.
Require Import bedrock2.WeakestPrecondition.
Require Import bedrock2.ProgramLogic.
Require Import bedrock2.Map.Separation.
Require Import bedrock2.Map.SeparationLogic.
Require Import bedrock2.Syntax.
Local Open Scope string_scope.
Local Infix "*" := sep : sep_scope.
Delimit Scope sep_scope with sep.
Local Notation function_t := ((String.string * (list String.string * list String.string * Syntax.cmd.cmd))%type).
Local Notation functions_t := (list function_t).
Local Open Scope sep_scope.
(* Parameters for p224 field. *)
Definition m : Z := (2^224 - 2^96 + 1)%Z.
Existing Instances Defaults32.default_parameters
Defaults32.default_parameters_ok.
Definition prefix : string := "p224_"%string.
Instance field_parameters : FieldParameters.
let M := (eval vm_compute in (Z.to_pos (m))) in
(* curve 'A' parameter *)
let a := constr:(F.of_Z M (m - 3)) in
let prefix := constr:("p224_felem_"%string) in
eapply
(field_parameters_prefixed
M ((a - F.of_Z _ 2) / F.of_Z _ 4)%F prefix).
Definition to_mont_string := prefix ++ "to_mont".
Definition from_mont_string := prefix ++ "from_mont".
(* Call fiat-crypto pipeline on all field operations *)
Instance p224_ops : @word_by_word_Montgomery_ops from_mont_string to_mont_string _ _ _ _ _ _ _ _ _ _ (WordByWordMontgomery.n m machine_wordsize) m.
Time constructor; make_computed_op.
(**** Translate each field operation into bedrock2 and apply bedrock2 backend
field pipeline proofs to prove the bedrock2 functions are correct. ****)
Local Ltac begin_derive_bedrock2_func :=
lazymatch goal with
| |- context [spec_of_BinOp bin_mul] => eapply mul_func_correct
| |- context [spec_of_UnOp un_square] => eapply square_func_correct
| |- context [spec_of_BinOp bin_add] => eapply add_func_correct
| |- context [spec_of_BinOp bin_sub] => eapply sub_func_correct
| |- context [spec_of_UnOp un_opp] => eapply opp_func_correct
(* | |- context [spec_of_UnOp un_scmula24] => eapply scmula24_func_correct *)
| |- context [spec_of_from_bytes] => eapply from_bytes_func_correct
| |- context [spec_of_to_bytes] => eapply to_bytes_func_correct
end.
Ltac epair :=
lazymatch goal with
| f := _ : string * Syntax.func |- _ =>
let p := open_constr:((_, _)) in
unify f p;
subst f
end.
Ltac derive_bedrock2_func op :=
epair;
begin_derive_bedrock2_func;
(* this goal fills in the evar, so do it first for [abstract] to be happy *)
try lazymatch goal with
| |- _ = b2_func _ => vm_compute; reflexivity
end;
(* solve all the remaining goals *)
lazymatch goal with
| |- _ = @ErrorT.Success ?ErrT unit tt =>
abstract (vm_cast_no_check (@eq_refl _ (@ErrorT.Success ErrT unit tt)))
| |- Func.valid_func _ =>
eapply Func.valid_func_bool_iff;
abstract vm_cast_no_check (eq_refl true)
| |- (_ = _)%Z => vm_compute; reflexivity
end.
Local Notation functions_contain functions f :=
(Interface.map.get functions (fst f) = Some (snd f)).
Derive p224_from_bytes
SuchThat (forall functions,
functions_contain functions p224_from_bytes ->
spec_of_from_bytes
(field_representation:=field_representation_raw m)
functions)
As p224_from_bytes_correct.
Time derive_bedrock2_func from_bytes_op.
Derive p224_to_bytes
SuchThat (forall functions,
functions_contain functions p224_to_bytes ->
spec_of_to_bytes
(field_representation:=field_representation_raw m)
functions)
As p224_to_bytes_correct.
Time derive_bedrock2_func to_bytes_op.
Derive p224_mul
SuchThat (forall functions,
functions_contain functions p224_mul ->
spec_of_BinOp bin_mul
(field_representation:=field_representation m)
functions)
As p224_mul_correct.
Time derive_bedrock2_func mul_op.
Derive p224_square
SuchThat (forall functions,
functions_contain functions p224_square ->
spec_of_UnOp un_square
(field_representation:=field_representation m)
functions)
As p224_square_correct.
Time derive_bedrock2_func square_op.
Derive p224_add
SuchThat (forall functions,
functions_contain functions p224_add ->
spec_of_BinOp bin_add
(field_representation:=field_representation m)
functions)
As p224_add_correct.
Time derive_bedrock2_func add_op.
Derive p224_sub
SuchThat (forall functions,
functions_contain functions p224_sub ->
spec_of_BinOp bin_sub
(field_representation:=field_representation m)
functions)
As p224_sub_correct.
Time derive_bedrock2_func sub_op.
(*TODO: adapt derive_bedrock2_func to also derive the remaining functions.*)
Derive p224_from_mont
SuchThat (forall functions,
functions_contain functions p224_from_mont ->
spec_of_UnOp un_from_mont
(field_representation:=field_representation m)
functions)
As p224_from_mont_correct.
eapply (from_mont_func_correct _ _ _ from_mont_string to_mont_string).
eapply Func.valid_func_bool_iff.
abstract vm_cast_no_check (eq_refl true).
Derive p224_to_mont
SuchThat (forall functions,
functions_contain functions p224_to_mont ->
spec_of_UnOp un_to_mont
(field_representation:=field_representation m)
functions)
As to_from_mont_correct.
eapply (to_mont_func_correct _ _ _ from_mont_string to_mont_string).
eapply Func.valid_func_bool_iff.
abstract vm_cast_no_check (eq_refl true).
Derive p224_select_znz
SuchThat (forall functions,
functions_contain functions p224_select_znz ->
spec_of_selectznz
(field_representation:=field_representation m)
functions)
As select_znz_correct.
eapply select_znz_func_correct.
eapply Func.valid_func_bool_iff.
abstract vm_cast_no_check (eq_refl true).