From 496271f86e9dc6df1b23a189d6b8fd2a82db33aa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 30 Jan 2019 19:13:27 -0500 Subject: Add autogenerated docstrings to synthesized code We now stringify the correctness conditions to generate docstrings for the synthesized code. Closes #512 Time commitment: about 6 hours --- src/PushButtonSynthesis/BarrettReduction.v | 5 +- src/PushButtonSynthesis/MontgomeryReduction.v | 5 +- src/PushButtonSynthesis/Primitives.v | 472 ++++++++++++++++++++++++- src/PushButtonSynthesis/SaturatedSolinas.v | 18 +- src/PushButtonSynthesis/SmallExamples.v | 18 +- src/PushButtonSynthesis/UnsaturatedSolinas.v | 95 ++++- src/PushButtonSynthesis/WordByWordMontgomery.v | 123 ++++++- 7 files changed, 680 insertions(+), 56 deletions(-) (limited to 'src/PushButtonSynthesis') diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index 3e3e4e105..bc525412a 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -91,7 +91,10 @@ Section rbarrett_red. Definition sbarrett_red (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "barrett_red" barrett_red. + := Eval cbv beta in + FromPipelineToString + prefix "barrett_red" barrett_red + (fun _ _ _ => @nil string). (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like << diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v index 2b7841ac0..a452a047c 100644 --- a/src/PushButtonSynthesis/MontgomeryReduction.v +++ b/src/PushButtonSynthesis/MontgomeryReduction.v @@ -82,7 +82,10 @@ Section rmontred. Definition smontred (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "montred" montred. + := Eval cbv beta in + FromPipelineToString + prefix "montred" montred + (fun _ _ _ => @nil string). (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like << diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index f36f4cb9c..e45940369 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -133,19 +133,7 @@ Local Notation out_bounds_of_pipeline result (only parsing). Notation FromPipelineToString prefix name result - := (((prefix ++ name)%string, - match result with - | Success E' - => let E := ToString.C.ToFunctionLines - true true (* static *) prefix (prefix ++ name)%string [] E' None - (arg_bounds_of_pipeline result) - (out_bounds_of_pipeline result) in - match E with - | inl E => Success E - | inr err => Error (Pipeline.Stringification_failed E' err) - end - | Error err => Error err - end)). + := (Pipeline.FromPipelineToString prefix name result). Ltac prove_correctness use_curve_good := let Hres := match goal with H : _ = Success _ |- _ => H end in @@ -175,6 +163,419 @@ Ltac prove_correctness use_curve_good := | progress autorewrite with distr_length in * ] | .. ]. +Module CorrectnessStringification. + Module dyn_context. + Inductive list := + | nil + | cons {T1 T2} (k : T1) (v : T2) (ctx : list). + End dyn_context. + + Ltac strip_bounds_info correctness := + lazymatch correctness with + | (fun x : ?T => ?f) + => let fx := fresh in + constr:(fun x : T => match f return _ with + | fx => ltac:(let fx := (eval cbv [fx] in fx) in + let v := strip_bounds_info fx in + exact v) + end) + | ((lower ?r <=? ?v) && (?v <=? upper ?r))%bool%Z = true -> ?T + => strip_bounds_info T + | list_Z_bounded_by _ _ -> ?T + => strip_bounds_info T + | ?T /\ list_Z_bounded_by _ _ + => T + | ?T /\ (match _ with pair _ _ => _ end = true) + => T + | ?T /\ ((lower ?r <=? ?v) && (?v <=? upper ?r))%bool%Z = true + => T + | iff _ _ + => correctness + | _ = _ /\ (_ = _ /\ (_ <= _ < _)) + => correctness + | _ = _ :> list Z + => correctness + | forall x : ?T, ?f + => let fx := fresh in + constr:(forall x : T, match f return _ with + | fx => ltac:(let fx := (eval cbv [fx] in fx) in + let v := strip_bounds_info fx in + exact v) + end) + | ?T + => let __ := match goal with _ => idtac "Unrecognized bounds component:" T end in + constr:(I : I) + end. + + Ltac with_assoc_list ctx correctness arg_var_names out_var_names cont := + lazymatch correctness with + | (fun x : ?T => ?f) + => let fx := fresh in + constr:(fun x : T + => match f return _ with + | fx + => ltac:(let fx' := (eval cbv delta [fx] in fx) in + clear fx; + let ret := with_assoc_list + (dyn_context.cons x out_var_names ctx) + fx' + arg_var_names + () + cont in + exact ret) + end) + | _ + => let T := type of arg_var_names in + lazymatch (eval hnf in T) with + | prod _ _ + => lazymatch correctness with + | (forall x : ?T, ?f) + => let fx := fresh in + constr:(fun x : T + => match f return _ with + | fx + => ltac:(let fx' := (eval cbv delta [fx] in fx) in + clear fx; + let ret := with_assoc_list + (dyn_context.cons x (fst arg_var_names) ctx) + fx' + (snd arg_var_names) + out_var_names + cont in + exact ret) + end) + | ?T + => cont ctx T + end + | _ => cont ctx correctness + end + end. + + Ltac maybe_parenthesize str natural cur_lvl := + let should_paren := (eval cbv in (Z.ltb cur_lvl natural)) in + lazymatch should_paren with + | true => constr:(("(" ++ str ++ ")")%string) + | false => str + end. + + Ltac find_head_in_ctx' ctx x cont := + let h := head x in + lazymatch ctx with + | context[dyn_context.cons h ?name _] => cont name + | context[dyn_context.cons x ?name _] => cont name + | _ => lazymatch x with + | fst ?x + => find_head_in_ctx' ctx x ltac:(fun x => cont (fst x)) + | snd ?x + => find_head_in_ctx' ctx x ltac:(fun x => cont (snd x)) + | _ => constr:(@None string) + end + end. + Ltac find_head_in_ctx ctx x := + find_head_in_ctx' ctx x ltac:(fun x => constr:(Some x)). + + Ltac find_in_ctx' ctx x cont := + lazymatch ctx with + | context[dyn_context.cons x ?name _] => cont name + | _ => lazymatch x with + | fst ?x + => find_in_ctx' ctx x ltac:(fun x => cont (fst x)) + | snd ?x + => find_in_ctx' ctx x ltac:(fun x => cont (snd x)) + | _ => constr:(@None string) + end + end. + Ltac find_in_ctx ctx x := + find_in_ctx' ctx x ltac:(fun x => constr:(Some x)). + + Ltac test_is_var v := + constr:(ltac:(tryif is_var v then exact true else exact false)). + + Local Open Scope string_scope. + + Ltac fresh_from' ctx check_list start_val := + lazymatch check_list with + | cons ?n ?check_list + => lazymatch ctx with + | context[dyn_context.cons _ n] + => fresh_from' ctx check_list start_val + | _ => n + end + | _ + => let n := (eval cbv in ("x" ++ decimal_string_of_Z start_val)) in + lazymatch ctx with + | context[dyn_context.cons _ n] + => fresh_from' ctx check_list (Z.succ start_val) + | _ => n + end + end. + + Ltac fresh_from ctx := fresh_from' ctx ["x"; "y"; "z"] 0%Z. + + Ltac stringify_function_binders ctx correctness stringify_body := + lazymatch correctness with + | (fun x : ?T => ?f) + => let fx := fresh in + let xn := fresh_from ctx in + lazymatch + constr:( + fun x : T + => match f return string with + | fx + => ltac:( + let fx' := (eval cbv delta [fx] in fx) in + clear fx; + let res := stringify_function_binders + (dyn_context.cons x xn ctx) + fx' + stringify_body in + exact (" " ++ xn ++ res)) + end) with + | fun _ => ?f => f + | ?F => let __ := match goal with _ => idtac "Failed to eliminate functional dependencies in" F end in + constr:(I : I) + end + | ?v => let res := stringify_body ctx v in + constr:(", " ++ res) + end. + + Ltac is_literal x := + lazymatch x with + | O => true + | S ?x => is_literal x + | _ => false + end. + + Ltac stringify_rec0 evalf ctx correctness lvl := + let recurse v lvl := stringify_rec0 evalf ctx v lvl in + let name_of_var := find_head_in_ctx ctx correctness in + let weightf := lazymatch evalf with eval ?weightf _ => weightf | _ => I end in + let stringify_if testv t f := + let stest := recurse testv 200 in + let st := recurse t 200 in + let sf := recurse f 200 in + maybe_parenthesize (("if " ++ stest ++ " then " ++ st ++ " else " ++ sf)%string) 200 lvl in + let show_Z _ := + maybe_parenthesize (Show.Decimal.show_Z false correctness) 1 lvl in + let show_nat _ := + maybe_parenthesize (Show.Decimal.show_nat false correctness) 1 lvl in + let stringify_prefix f natural arg_lvl := + lazymatch correctness with + | ?F ?x + => let sx := recurse x arg_lvl in + maybe_parenthesize (f ++ sx)%string natural lvl + end in + let stringify_postfix f natural arg_lvl := + lazymatch correctness with + | ?F ?x + => let sx := recurse x arg_lvl in + maybe_parenthesize (sx ++ f)%string natural lvl + end in + let stringify_infix' lvl space f natural l_lvl r_lvl := + lazymatch correctness with + | ?F ?x ?y + => let sx := recurse x l_lvl in + let sy := recurse y r_lvl in + maybe_parenthesize (sx ++ space ++ f ++ space ++ sy)%string natural lvl + end in + let stringify_infix := stringify_infix' lvl " " in + let stringify_infix_without_space := stringify_infix' lvl "" in + let stringify_infix2 f1 f2 natural l_lvl c_lvl r_lvl := + lazymatch correctness with + | and (?F1 ?x ?y) (?F2 ?y ?z) + => let sx := recurse x l_lvl in + let sy := recurse y c_lvl in + let sz := recurse z r_lvl in + maybe_parenthesize (sx ++ " " ++ f1 ++ " " ++ sy ++ " " ++ f2 ++ " " ++ sz)%string natural lvl + end in + let name_of_fun := + lazymatch correctness with + | ?f ?x => find_in_ctx ctx f + | _ => constr:(@None string) + end in + lazymatch constr:((name_of_var, name_of_fun)) with + | (Some ?name, _) + => maybe_parenthesize name 1 lvl + | (None, Some ?name) + => lazymatch correctness with + | ?f ?x + => let sx := recurse x 9 in + maybe_parenthesize ((name ++ " " ++ sx)%string) 10 lvl + end + | (None, None) + => lazymatch correctness with + | ?x = ?y :> ?T + => lazymatch (eval cbv in T) with + | Z => let sx := recurse x 69 in + let sy := recurse y 69 in + maybe_parenthesize ((sx ++ " = " ++ sy)%string) 70 lvl + | list Z + => let sx := recurse x 69 in + let sy := recurse y 69 in + maybe_parenthesize ((sx ++ " = " ++ sy)%string) 70 lvl + | prod ?A ?B + => let v := (eval cbn [fst snd] in (fst x = fst y /\ snd x = snd y)) in + recurse v lvl + | ?T' => let __ := match goal with _ => idtac "Error: Unrecognized type for equality:" T' end in + constr:(I : I) + end + | evalf ?v + => let sv := recurse v 9 in + maybe_parenthesize (("eval " ++ sv)%string) 10 lvl + | weightf ?v + => let sv := recurse v 9 in + maybe_parenthesize (("weight " ++ sv)%string) 10 lvl + | eval (weight 8 1) _ ?v + => let sv := recurse v 9 in + maybe_parenthesize (("bytes_eval " ++ sv)%string) 10 lvl + | UniformWeight.uweight ?machine_wordsize ?v + => recurse (2^(machine_wordsize * Z.of_nat v)) lvl + | weight 8 1 ?i + => recurse (2^(8 * Z.of_nat i)) lvl + | List.map ?x ?y + => let sx := recurse x 9 in + let sy := recurse y 9 in + maybe_parenthesize (("map " ++ sx ++ " " ++ sy)%string) 10 lvl + | match ?testv with true => ?t | false => ?f end + => stringify_if testv t f + | match ?testv with or_introl _ => ?t | or_intror _ => ?f end + => stringify_if testv t f + | match ?testv with left _ => ?t | right _ => ?f end + => stringify_if testv t f + | Decidable.dec ?p + => recurse p lvl + | Z0 => show_Z () + | Zpos _ => show_Z () + | Zneg _ => show_Z () + | O => show_nat () + | S ?x + => let is_lit := is_literal x in + lazymatch is_lit with + | true => show_nat () + | false => recurse (x + 1)%nat lvl + end + | Z.of_nat ?x => recurse x lvl + | ?x <= ?y < ?z => stringify_infix2 "≤" "<" 70 69 69 69 + | ?x <= ?y <= ?z => stringify_infix2 "≤" "≤" 70 69 69 69 + | ?x < ?y <= ?z => stringify_infix2 "<" "≤" 70 69 69 69 + | ?x < ?y < ?z => stringify_infix2 "<" "<" 70 69 69 69 + | iff _ _ => stringify_infix "↔" 95 94 94 + | and _ _ => stringify_infix "∧" 80 80 80 + | Z.modulo _ _ => stringify_infix "mod" 40 39 39 + | Z.mul _ _ => stringify_infix "*" 40 40 39 + | Z.pow _ _ => stringify_infix_without_space "^" 30 29 30 + | Z.add _ _ => stringify_infix "+" 50 50 49 + | Z.sub _ _ => stringify_infix "-" 50 50 49 + | Z.opp _ => stringify_prefix "-" 35 35 + | Z.le _ _ => stringify_infix "≤" 70 69 69 + | Z.lt _ _ => stringify_infix "<" 70 69 69 + | Nat.mul _ _ => stringify_infix "*" 40 40 39 + | Nat.pow _ _ => stringify_infix "^" 30 29 30 + | Nat.add _ _ => stringify_infix "+" 50 50 49 + | Nat.sub _ _ => stringify_infix "-ℕ" 50 50 49 + | Z.div _ _ + => let res := stringify_infix' 69 " " "/" 40 40 39 in + maybe_parenthesize ("⌊" ++ res ++ "⌋") 9 lvl + | List.seq ?x ?y + => let sx := recurse x 9 in + let sy := recurse (pred y) 9 in + constr:("[" ++ sx ++ ".." ++ sy ++ "]") + | pred ?n + => let iv := test_is_var n in + let il := is_literal n in + lazymatch (eval cbv in (orb il iv)) with + | true => show_nat () + | false + => recurse (n - 1)%nat lvl + end + | fun x : ?T => ?f + => let slam := stringify_function_binders ctx correctness ltac:(fun ctx body => stringify_rec0 evalf ctx body 200) in + maybe_parenthesize ("λ" ++ slam) 200 lvl + | ?v + => let iv := test_is_var v in + lazymatch iv with + | true + => let T := type of v in + lazymatch (eval hnf in T) with + | Z => show_Z () + | nat => show_nat () + | _ + => let __ := match goal with _ => idtac "Error: Unrecognized var:" v " in " ctx end in + constr:(I : I) + end + | false + => let __ := match goal with _ => idtac "Error: Unrecognized term:" v " in " ctx end in + constr:(I : I) + end + end + end. + + Ltac stringify_rec prefix evalf ctx correctness lvl := + let recurse' prefix v lvl := stringify_rec prefix evalf ctx v lvl in + let recurse := recurse' "" in + let default _ := let v := stringify_rec0 evalf ctx correctness lvl in + constr:((prefix ++ v)::nil) in + lazymatch correctness with + | ?A -> ?B + => let sA := stringify_rec0 evalf ctx A 98 in + let sB := recurse B 200 in + constr:((prefix ++ sA ++ " →")%string :: sB) + | _ <= _ < _ => default () + | _ <= _ <= _ => default () + | _ < _ <= _ => default () + | _ < _ < _ => default () + | and ?A ?B + => let sA := recurse' prefix A 80 in + let sB := recurse' "∧ " B 80 in + constr:(List.app sA sB) + | ?x = ?y :> prod ?A ?B + => let v := (eval cbn [fst snd] in (fst x = fst y /\ snd x = snd y)) in + recurse' prefix v lvl + | _ + => default () + end. + + Ltac strip_lambdas v := + lazymatch v with + | fun _ => ?f => strip_lambdas f + | ?v => v + end. + + Ltac stringify ctx correctness evalf fname arg_var_data out_var_data := + let G := match goal with |- ?G => G end in + let correctness := (eval hnf in correctness) in + let correctness := (eval cbv [Partition.partition Arithmetic.WordByWordMontgomery.valid Arithmetic.WordByWordMontgomery.small] in correctness) in + let correctness := strip_bounds_info correctness in + let arg_var_names := constr:(type.map_for_each_lhs_of_arrow (@ToString.C.OfPHOAS.names_of_var_data) arg_var_data) in + let out_var_names := constr:(ToString.C.OfPHOAS.names_of_base_var_data out_var_data) in + let res := with_assoc_list + ctx + correctness + arg_var_names + out_var_names + ltac:( + fun ctx T + => let v := stringify_rec "" evalf ctx T 200 in refine v + ) in + let res := strip_lambdas res in + res. + + Notation stringify_correctness_with_ctx ctx evalf pre_extra correctness + := (fun fname arg_var_data out_var_data + => ltac:(let res := stringify ctx correctness evalf fname arg_var_data out_var_data in + refine (List.app (pre_extra fname) res))) (only parsing). + Notation stringify_correctness evalf pre_extra correctness + := (match dyn_context.nil with + | ctx' => stringify_correctness_with_ctx ctx' evalf pre_extra correctness + end) + (only parsing). +End CorrectnessStringification. + +Notation stringify_correctness_with_ctx ctx evalf pre_extra correctness + := (CorrectnessStringification.stringify_correctness_with_ctx ctx evalf pre_extra correctness) (only parsing). +Notation stringify_correctness evalf pre_extra correctness + := (CorrectnessStringification.stringify_correctness evalf pre_extra correctness) (only parsing). + Section __. Context (n : nat) (machine_wordsize : Z). @@ -199,6 +600,9 @@ Section __. Proof using Type. cbv [saturated_bounds_list]; now autorewrite with distr_length. Qed. Hint Rewrite length_saturated_bounds_list : distr_length. + Local Notation dummy_weight := (weight 0 0). + Local Notation evalf := (eval dummy_weight n). + Definition selectznz := Pipeline.BoundsPipeline false (* subst01 *) @@ -210,7 +614,13 @@ Section __. Definition sselectznz (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "selectznz" selectznz. + := Eval cbv beta in + FromPipelineToString + prefix "selectznz" selectznz + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is a multi-limb conditional select."]%string) + (selectznz_correct dummy_weight n saturated_bounds_list)). Definition mulx (s : Z) := Pipeline.BoundsPipeline @@ -224,7 +634,13 @@ Section __. Definition smulx (prefix : string) (s : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s). + := Eval cbv beta in + FromPipelineToString + prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s) + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is an extended multiplication."]%string) + (mulx_correct s)). Definition addcarryx (s : Z) := Pipeline.BoundsPipeline @@ -236,9 +652,16 @@ Section __. (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange (Some r[0~>2^s-1], Some r[0~>1])%zrange. + Definition saddcarryx (prefix : string) (s : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s). + := Eval cbv beta in + FromPipelineToString + prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s) + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is an add with carry."]%string) + (addcarryx_correct s)). Definition subborrowx (s : Z) := Pipeline.BoundsPipeline @@ -252,7 +675,14 @@ Section __. Definition ssubborrowx (prefix : string) (s : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s). + := Eval cbv beta in + FromPipelineToString + prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s) + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is a sub with borrow."]%string) + (subborrowx_correct s)). + Definition cmovznz (s : Z) := Pipeline.BoundsPipeline @@ -266,7 +696,13 @@ Section __. Definition scmovznz (prefix : string) (s : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s). + := Eval cbv beta in + FromPipelineToString + prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s) + (stringify_correctness + evalf + (fun fname : string => ["The function " ++ fname ++ " is a single-word conditional move."]%string) + (cmovznz_correct s)). Local Ltac solve_extra_bounds_side_conditions := cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 334c2a475..7ff799c80 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -135,6 +135,17 @@ Section __. { use_curve_good_t. } Qed. + Local Notation weightf := (weight machine_wordsize 1). + Local Notation evalf := (eval weightf n). + Local Notation initial_ctx := (CorrectnessStringification.dyn_context.nil). + Local Notation stringify_correctness pre_extra correctness + := (stringify_correctness_with_ctx + initial_ctx + evalf + pre_extra + correctness) + (only parsing). + Definition mul := Pipeline.BoundsPipeline false (* subst01 *) @@ -147,7 +158,12 @@ Section __. Definition smul (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "mul" mul. + := Eval cbv beta in + FromPipelineToString + prefix "mul" mul + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (mul_correct weightf n m boundsn)). Local Ltac solve_extra_bounds_side_conditions := cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. diff --git a/src/PushButtonSynthesis/SmallExamples.v b/src/PushButtonSynthesis/SmallExamples.v index 09f361356..daa50c9e9 100644 --- a/src/PushButtonSynthesis/SmallExamples.v +++ b/src/PushButtonSynthesis/SmallExamples.v @@ -43,53 +43,59 @@ Compute Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_mulx_u64" [] + true "fiat_" "fiat_mulx_u64" true None [64; 128] ltac:(let r := Reify (Arithmetic.mulx 64) in exact r) + (fun _ _ => []) (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt))%zrange (Some r[0~>2^64-1], Some r[0~>2^64-1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_addcarryx_u64" [] + true "fiat_" "fiat_addcarryx_u64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.addcarryx 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_addcarryx_u51" [] + true "fiat_" "fiat_addcarryx_u51" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.addcarryx 51) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange (Some r[0~>2^51-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_subborrowx_u64" [] + true "fiat_" "fiat_subborrowx_u64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.subborrowx 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_subborrowx_u51" [] + true "fiat_" "fiat_subborrowx_u51" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.subborrowx 51) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange (Some r[0~>2^51-1], Some r[0~>1])%zrange). Compute (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_cmovznz64" [] + true "fiat_" "fiat_cmovznz64" true None [1; 64; 128] ltac:(let r := Reify (Arithmetic.cmovznz 64) in exact r) + (fun _ _ => []) (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange (Some r[0~>2^64-1])%zrange). diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index 8923aa10e..75e430a24 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -258,6 +258,17 @@ else: { use_curve_good_t. } Qed. + Local Notation weightf := (weight (Qnum limbwidth) (QDen limbwidth)). + Local Notation evalf := (eval weightf n). + Local Notation initial_ctx := (CorrectnessStringification.dyn_context.cons m "m"%string CorrectnessStringification.dyn_context.nil). + Local Notation stringify_correctness pre_extra correctness + := (stringify_correctness_with_ctx + initial_ctx + evalf + pre_extra + correctness) + (only parsing). + Definition carry_mul := Pipeline.BoundsPipeline false (* subst01 *) @@ -270,7 +281,12 @@ else: Definition scarry_mul (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry_mul" carry_mul. + := Eval cbv beta in + FromPipelineToString + prefix "carry_mul" carry_mul + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (carry_mul_correct weightf n m tight_bounds loose_bounds)). Definition carry_square := Pipeline.BoundsPipeline @@ -284,7 +300,12 @@ else: Definition scarry_square (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry_square" carry_square. + := Eval cbv beta in + FromPipelineToString + prefix "carry_square" carry_square + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (carry_square_correct weightf n m tight_bounds loose_bounds)). Definition carry_scmul_const (x : Z) := Pipeline.BoundsPipeline @@ -298,7 +319,12 @@ else: Definition scarry_scmul_const (prefix : string) (x : Z) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x). + := Eval cbv beta in + FromPipelineToString + prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x) + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (carry_scmul_const_correct weightf n m tight_bounds loose_bounds x)). Definition carry := Pipeline.BoundsPipeline @@ -312,7 +338,12 @@ else: Definition scarry (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry" carry. + := Eval cbv beta in + FromPipelineToString + prefix "carry" carry + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (carry_correct weightf n m tight_bounds loose_bounds)). Definition add := Pipeline.BoundsPipeline @@ -326,7 +357,12 @@ else: Definition sadd (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "add" add. + := Eval cbv beta in + FromPipelineToString + prefix "add" add + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (add_correct weightf n m tight_bounds loose_bounds)). Definition sub := Pipeline.BoundsPipeline @@ -340,7 +376,12 @@ else: Definition ssub (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "sub" sub. + := Eval cbv beta in + FromPipelineToString + prefix "sub" sub + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (sub_correct weightf n m tight_bounds loose_bounds)). Definition opp := Pipeline.BoundsPipeline @@ -354,7 +395,12 @@ else: Definition sopp (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "opp" opp. + := Eval cbv beta in + FromPipelineToString + prefix "opp" opp + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (opp_correct weightf n m tight_bounds loose_bounds)). Definition to_bytes := Pipeline.BoundsPipeline @@ -368,7 +414,12 @@ else: Definition sto_bytes (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. + := Eval cbv beta in + FromPipelineToString + prefix "to_bytes" to_bytes + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (to_bytes_correct weightf n n_bytes m tight_bounds)). Definition from_bytes := Pipeline.BoundsPipeline @@ -382,7 +433,12 @@ else: Definition sfrom_bytes (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. + := Eval cbv beta in + FromPipelineToString + prefix "from_bytes" from_bytes + (stringify_correctness + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (from_bytes_correct weightf n n_bytes m s tight_bounds)). Definition encode := Pipeline.BoundsPipeline @@ -396,7 +452,12 @@ else: Definition sencode (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "encode" encode. + := Eval cbv beta in + FromPipelineToString + prefix "encode" encode + (stringify_correctness + (fun fname : string => [fname ++ ":"]%string) + (encode_correct weightf n m tight_bounds)). Definition zero := Pipeline.BoundsPipeline @@ -410,7 +471,12 @@ else: Definition szero (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "zero" zero. + := Eval cbv beta in + FromPipelineToString + prefix "zero" zero + (stringify_correctness + (fun fname : string => @nil string) + (zero_correct weightf n m tight_bounds)). Definition one := Pipeline.BoundsPipeline @@ -424,7 +490,12 @@ else: Definition sone (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "one" one. + := Eval cbv beta in + FromPipelineToString + prefix "one" one + (stringify_correctness + (fun fname : string => @nil string) + (one_correct weightf n m tight_bounds)). Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. Definition sselectznz (prefix : string) diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index a97c829e2..f64e4a8c3 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -223,6 +223,28 @@ Section __. Qed. + Local Notation valid := (Arithmetic.WordByWordMontgomery.valid machine_wordsize n m). + Local Notation bytes_valid := (Arithmetic.WordByWordMontgomery.valid 8 n_bytes m). + + Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). + + Local Notation evalf := (@eval machine_wordsize n). + Local Notation initial_ctx prefix + := (CorrectnessStringification.dyn_context.cons + m "m"%string + (CorrectnessStringification.dyn_context.cons + from_montgomery_res (prefix ++ "from_montgomery")%string + (CorrectnessStringification.dyn_context.cons + (@eval 8 n_bytes) "bytes_eval"%string + CorrectnessStringification.dyn_context.nil))). + Local Notation stringify_correctness prefix pre_extra correctness + := (stringify_correctness_with_ctx + (initial_ctx prefix) + evalf + pre_extra + correctness) + (only parsing). + Definition mul := Pipeline.BoundsPipeline false (* subst01 *) @@ -235,7 +257,13 @@ Section __. Definition smul (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "mul" mul. + := Eval cbv beta in + FromPipelineToString + prefix "mul" mul + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (mul_correct machine_wordsize n m valid from_montgomery_res)). Definition square := Pipeline.BoundsPipeline @@ -249,7 +277,13 @@ Section __. Definition ssquare (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "square" square. + := Eval cbv beta in + FromPipelineToString + prefix "square" square + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (square_correct machine_wordsize n m valid from_montgomery_res)). Definition add := Pipeline.BoundsPipeline @@ -263,7 +297,13 @@ Section __. Definition sadd (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "add" add. + := Eval cbv beta in + FromPipelineToString + prefix "add" add + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (add_correct machine_wordsize n m valid from_montgomery_res)). Definition sub := Pipeline.BoundsPipeline @@ -277,7 +317,13 @@ Section __. Definition ssub (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "sub" sub. + := Eval cbv beta in + FromPipelineToString + prefix "sub" sub + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (sub_correct machine_wordsize n m valid from_montgomery_res)). Definition opp := Pipeline.BoundsPipeline @@ -291,7 +337,13 @@ Section __. Definition sopp (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "opp" opp. + := Eval cbv beta in + FromPipelineToString + prefix "opp" opp + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (opp_correct machine_wordsize n m valid from_montgomery_res)). Definition from_montgomery := Pipeline.BoundsPipeline @@ -305,7 +357,13 @@ Section __. Definition sfrom_montgomery (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_montgomery" from_montgomery. + := Eval cbv beta in + FromPipelineToString + prefix "from_montgomery" from_montgomery + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (from_montgomery_correct machine_wordsize n m r' valid)). Definition nonzero := Pipeline.BoundsPipeline @@ -318,7 +376,13 @@ Section __. Definition snonzero (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "nonzero" nonzero. + := Eval cbv beta in + FromPipelineToString + prefix "nonzero" nonzero + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (nonzero_correct machine_wordsize n m valid from_montgomery_res)). Definition to_bytes := Pipeline.BoundsPipeline @@ -332,7 +396,13 @@ Section __. Definition sto_bytes (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. + := Eval cbv beta in + FromPipelineToString + prefix "to_bytes" to_bytes + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (to_bytes_correct machine_wordsize n n_bytes m valid)). Definition from_bytes := Pipeline.BoundsPipeline @@ -346,7 +416,13 @@ Section __. Definition sfrom_bytes (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. + := Eval cbv beta in + FromPipelineToString + prefix "from_bytes" from_bytes + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (from_bytes_correct machine_wordsize n n_bytes m valid bytes_valid)). Definition encode := Pipeline.BoundsPipeline @@ -360,7 +436,13 @@ Section __. Definition sencode (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "encode" encode. + := Eval cbv beta in + FromPipelineToString + prefix "encode" encode + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (encode_correct machine_wordsize n m valid from_montgomery_res)). Definition zero := Pipeline.BoundsPipeline @@ -374,7 +456,13 @@ Section __. Definition szero (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "zero" zero. + := Eval cbv beta in + FromPipelineToString + prefix "zero" zero + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (zero_correct machine_wordsize n m valid from_montgomery_res)). Definition one := Pipeline.BoundsPipeline @@ -388,16 +476,19 @@ Section __. Definition sone (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "one" one. + := Eval cbv beta in + FromPipelineToString + prefix "one" one + (stringify_correctness + prefix + (fun fname : string => ["The function " ++ fname ++ " does stuff."]%string) + (one_correct machine_wordsize n m valid from_montgomery_res)). Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. Definition sselectznz (prefix : string) : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) := Primitives.sselectznz n machine_wordsize prefix. - Local Notation valid := (Arithmetic.WordByWordMontgomery.valid machine_wordsize n m). - Local Notation bytes_valid := (Arithmetic.WordByWordMontgomery.valid 8 n_bytes m). - Lemma bounded_by_of_valid x (H : valid x) : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some bounds) x = true. @@ -618,8 +709,6 @@ Section __. reified_from_montgomery` (the post-pipeline version), and take in success of the pipeline on `from_montgomery` as well? *) - Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). - Lemma mul_correct res (Hres : mul = Success res) : mul_correct machine_wordsize n m valid from_montgomery_res (Interp res). -- cgit v1.2.3