diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/BoundsPipeline.v | 47 | ||||
-rw-r--r-- | src/CStringification.v | 44 | ||||
-rw-r--r-- | src/PushButtonSynthesis/BarrettReduction.v | 5 | ||||
-rw-r--r-- | src/PushButtonSynthesis/MontgomeryReduction.v | 5 | ||||
-rw-r--r-- | src/PushButtonSynthesis/Primitives.v | 472 | ||||
-rw-r--r-- | src/PushButtonSynthesis/SaturatedSolinas.v | 18 | ||||
-rw-r--r-- | src/PushButtonSynthesis/SmallExamples.v | 18 | ||||
-rw-r--r-- | src/PushButtonSynthesis/UnsaturatedSolinas.v | 95 | ||||
-rw-r--r-- | src/PushButtonSynthesis/WordByWordMontgomery.v | 123 | ||||
-rw-r--r-- | src/SlowPrimeSynthesisExamples.v | 2 |
10 files changed, 746 insertions, 83 deletions
diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index 2b74545f3..0299f2e9e 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -211,7 +211,7 @@ Module Pipeline. => ((["Computed bounds " ++ show true computed_bounds ++ " are not tight enough (expected bounds not looser than " ++ show true expected_bounds ++ ")."]%string) ++ [explain_too_loose_bounds (t:=type.base _) computed_bounds expected_bounds] ++ match ToString.C.ToFunctionLines - false (* do extra bounds check *) false (* static *) "" "f" nil syntax_tree None arg_bounds ZRange.type.base.option.None with + false (* do extra bounds check *) false (* static *) "" "f" syntax_tree (fun _ _ => nil) None arg_bounds ZRange.type.base.option.None with | inl (E_lines, types_used) => ["When doing bounds analysis on the syntax tree:"] ++ E_lines ++ [""] @@ -322,13 +322,13 @@ Module Pipeline. (static : bool) (type_prefix : string) (name : string) - (comment : list string) (with_dead_code_elimination : bool := true) (with_subst01 : bool) (translate_to_fancy : option to_fancy_args) (possible_values : list Z) {t} (E : Expr t) + (comment : type.for_each_lhs_of_arrow ToString.C.OfPHOAS.var_data t -> ToString.C.OfPHOAS.var_data (type.final_codomain t) -> list string) arg_bounds out_bounds : ErrorT (list string * ToString.C.ident_infos) @@ -340,7 +340,7 @@ Module Pipeline. E arg_bounds out_bounds in match E with | Success E' => let E := ToString.C.ToFunctionLines - true static type_prefix name comment E' None arg_bounds out_bounds in + true static type_prefix name E' comment None arg_bounds out_bounds in match E with | inl E => Success E | inr err => Error (Stringification_failed E' err) @@ -352,50 +352,53 @@ Module Pipeline. (static : bool) (type_prefix : string) (name : string) - (comment : list string) (with_dead_code_elimination : bool := true) (with_subst01 : bool) (translate_to_fancy : option to_fancy_args) relax_zrange {t} (E : Expr t) + (comment : type.for_each_lhs_of_arrow ToString.C.OfPHOAS.var_data t -> ToString.C.OfPHOAS.var_data (type.final_codomain t) -> list string) arg_bounds out_bounds : ErrorT (string * ToString.C.ident_infos) := let E := BoundsPipelineToStrings - static type_prefix name comment + static type_prefix name (*with_dead_code_elimination*) with_subst01 translate_to_fancy relax_zrange - E arg_bounds out_bounds in + E comment arg_bounds out_bounds in match E with | Success (E, types_used) => Success (ToString.C.LinesToString E, types_used) | Error err => Error err end. Local Notation arg_bounds_of_pipeline result - := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl) + := ((fun a b c t E arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c t E arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl) (only parsing). Local Notation out_bounds_of_pipeline result - := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl) + := ((fun a b c t E arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c t E arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl) (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)). - + := (fun comment + => ((prefix ++ name)%string, + match result with + | Success E' + => let E := ToString.C.ToFunctionLines + true true (* static *) prefix (prefix ++ name)%string + E' + (comment (prefix ++ name)%string) + 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)). Local Ltac wf_interp_t := repeat first [ progress destruct_head'_and diff --git a/src/CStringification.v b/src/CStringification.v index 5c73b8e26..d31fa55e8 100644 --- a/src/CStringification.v +++ b/src/CStringification.v @@ -784,6 +784,40 @@ Module Compilers. | type.arrow s d => Empty_set end. + Fixpoint base_var_names (t : base.type) : Set + := match t with + | base.type.unit + => unit + | base.type.nat + | base.type.bool + => Empty_set + | base.type.Z => string + | base.type.prod A B => base_var_names A * base_var_names B + | base.type.list A => string + end. + Definition var_names (t : Compilers.type.type base.type) : Set + := match t with + | type.base t => base_var_names t + | type.arrow s d => Empty_set + end. + + Fixpoint names_of_base_var_data {t} : base_var_data t -> base_var_names t + := match t return base_var_data t -> base_var_names t with + | base.type.unit + | base.type.nat + | base.type.bool + => fun x => x + | base.type.Z => @fst _ _ + | base.type.prod A B + => fun xy => (@names_of_base_var_data A (fst xy), @names_of_base_var_data B (snd xy)) + | base.type.list A => fun x => fst (fst x) + end. + Definition names_of_var_data {t} : var_data t -> var_names t + := match t with + | type.base t => names_of_base_var_data + | type.arrow _ _ => fun x => x + end. + Fixpoint arith_expr_for_base (t : base.type) : Set := match t with | base.type.Z @@ -2167,9 +2201,10 @@ Module Compilers. :: (List.map (fun s => " " ++ s)%string (to_strings prefix body))) ++ ["}"])%list. - Definition ToFunctionLines (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) (comment : list string) + Definition ToFunctionLines (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) {t} (e : @Compilers.expr.Expr base.type ident.ident t) + (comment : type.for_each_lhs_of_arrow var_data t -> var_data (type.final_codomain t) -> list string) (name_list : option (list string)) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (outbounds : ZRange.type.base.option.interp (type.final_codomain t)) @@ -2177,7 +2212,7 @@ Module Compilers. := match ExprOfPHOAS do_bounds_check e name_list inbounds with | inl (indata, outdata, f) => inl ((["/*"] - ++ (List.map (fun s => " * " ++ s)%string comment) + ++ (List.map (fun s => " * " ++ s)%string (comment indata outdata)) ++ [" * Input Bounds:"] ++ List.map (fun v => " * " ++ v)%string (input_bounds_to_string indata inbounds) ++ [" * Output Bounds:"] @@ -2197,14 +2232,15 @@ Module Compilers. : string := String.concat String.NewLine lines. - Definition ToFunctionString (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) (comment : list string) + Definition ToFunctionString (do_bounds_check : bool) (static : bool) (prefix : string) (name : string) {t} (e : @Compilers.expr.Expr base.type ident.ident t) + (comment : type.for_each_lhs_of_arrow var_data t -> var_data (type.final_codomain t) -> list string) (name_list : option (list string)) (inbounds : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (outbounds : ZRange.type.option.interp (type.final_codomain t)) : (string * ident_infos) + string - := match ToFunctionLines do_bounds_check static prefix name comment e name_list inbounds outbounds with + := match ToFunctionLines do_bounds_check static prefix name e comment name_list inbounds outbounds with | inl (ls, used_types) => inl (LinesToString ls, used_types) | inr err => inr err end. 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). diff --git a/src/SlowPrimeSynthesisExamples.v b/src/SlowPrimeSynthesisExamples.v index a84455a6c..9bac61295 100644 --- a/src/SlowPrimeSynthesisExamples.v +++ b/src/SlowPrimeSynthesisExamples.v @@ -73,12 +73,12 @@ Section debugging_p448. true (* static *) "" (* prefix *) "mul" - [] (* comment *) false (* subst01 *) None (* fancy *) possible_values ltac:(let r := Reify ((carry_mulmod limbwidth_num limbwidth_den s c n [3; 7; 4; 0; 5; 1; 6; 2; 7; 3; 4; 0]%nat)) in exact r) + (fun _ _ => []) (* comment *) (Some loose_bounds, (Some loose_bounds, tt)) (Some tight_bounds). |