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

7 files changed, 680 insertions, 56 deletions

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).