Remove glue admits in Toplevel1

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
20m47.54s | Total                                                                | 20m48.81s || -0m01.26s | -0.10%
--------------------------------------------------------------------------------------------------------------------
3m14.11s  | p384_32.c                                                            | 3m19.20s  || -0m05.08s | -2.55%
6m18.53s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo                | 6m14.62s  || +0m03.90s | +1.04%
4m38.90s  | Experiments/NewPipeline/Toplevel1.vo                                 | 4m37.97s  || +0m00.92s | +0.33%
1m36.44s  | Experiments/NewPipeline/Toplevel2.vo                                 | 1m36.23s  || +0m00.21s | +0.21%
0m44.38s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m44.09s  || +0m00.28s | +0.65%
0m39.93s  | p521_32.c                                                            | 0m40.58s  || -0m00.64s | -1.60%
0m32.86s  | p521_64.c                                                            | 0m33.84s  || -0m00.98s | -2.89%
0m29.52s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m29.66s  || -0m00.14s | -0.47%
0m22.76s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m22.88s  || -0m00.11s | -0.52%
0m16.76s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m16.66s  || +0m00.10s | +0.60%
0m14.01s  | secp256k1_32.c                                                       | 0m14.03s  || -0m00.01s | -0.14%
0m13.88s  | p256_32.c                                                            | 0m13.79s  || +0m00.09s | +0.65%
0m10.63s  | p384_64.c                                                            | 0m10.67s  || -0m00.03s | -0.37%
0m10.16s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m10.07s  || +0m00.08s | +0.89%
0m09.76s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m09.92s  || -0m00.16s | -1.61%
0m07.83s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m07.65s  || +0m00.17s | +2.35%
0m06.60s  | p224_32.c                                                            | 0m06.35s  || +0m00.25s | +3.93%
0m06.54s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m06.48s  || +0m00.05s | +0.92%
0m06.42s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.40s  || +0m00.01s | +0.31%
0m04.99s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m04.94s  || +0m00.04s | +1.01%
0m04.92s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.96s  || -0m00.04s | -0.80%
0m04.12s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m04.06s  || +0m00.06s | +1.47%
0m02.40s  | curve25519_32.c                                                      | 0m02.40s  || +0m00.00s | +0.00%
0m01.90s  | p224_64.c                                                            | 0m02.02s  || -0m00.12s | -5.94%
0m01.84s  | p256_64.c                                                            | 0m01.83s  || +0m00.01s | +0.54%
0m01.84s  | secp256k1_64.c                                                       | 0m01.84s  || +0m00.00s | +0.00%
0m01.48s  | Experiments/NewPipeline/CLI.vo                                       | 0m01.48s  || +0m00.00s | +0.00%
0m01.48s  | curve25519_64.c                                                      | 0m01.63s  || -0m00.14s | -9.20%
0m01.28s  | Experiments/NewPipeline/StandaloneHaskellMain.vo                     | 0m01.24s  || +0m00.04s | +3.22%
0m01.28s  | Experiments/NewPipeline/StandaloneOCamlMain.vo                       | 0m01.32s  || -0m00.04s | -3.03%

1 files changed, 145 insertions, 84 deletions

diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index cd55a4472..957264d3f 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -545,6 +545,8 @@ Module Pipeline.
   | Value_not_leZ (descr : string) (lhs rhs : Z)
   | Value_not_leQ (descr : string) (lhs rhs : Q)
   | Value_not_ltZ (descr : string) (lhs rhs : Z)
+  | Value_not_lt_listZ (descr : string) (lhs rhs : list Z)
+  | Value_not_le_listZ (descr : string) (lhs rhs : list Z)
   | Values_not_provably_distinctZ (descr : string) (lhs rhs : Z)
   | Values_not_provably_equalZ (descr : string) (lhs rhs : Z)
   | Values_not_provably_equal_listZ (descr : string) (lhs rhs : list Z)
@@ -650,6 +652,10 @@ Module Pipeline.
                 => ["Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs]
               | Value_not_ltZ descr lhs rhs
                 => ["Value not < (" ++ descr ++ ") : expected " ++ show false lhs ++ " < " ++ show false rhs]
+              | Value_not_lt_listZ descr lhs rhs
+                => ["Value not < (" ++ descr ++ ") : expected " ++ show false lhs ++ " < " ++ show false rhs]
+              | Value_not_le_listZ descr lhs rhs
+                => ["Value not ≤ (" ++ descr ++ ") : expected " ++ show false lhs ++ " ≤ " ++ show false rhs]
               | Values_not_provably_distinctZ descr lhs rhs
                 => ["Values not provably distinct (" ++ descr ++ ") : expected " ++ show true lhs ++ " ≠ " ++ show true rhs]
               | Values_not_provably_equalZ descr lhs rhs
@@ -1300,9 +1306,44 @@ Hint Extern 1 (_ = cmovznz _ _ _ _) => simple apply (proj1 cmovznz_gen_correct)
 Hint Immediate (proj2 cmovznz_gen_correct) : wf_gen_cache.
 
 
-Axiom admit_pf : False.
-Notation admit := (match admit_pf with end).
-
+(** XXX TODO MOVE ME *)
+Module Import HelperLemmas.
+  Lemma eval_is_bounded_by wt n' bounds bounds' f
+        (H : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) bounds f = true)
+        (Hb : bounds = Some (List.map (@Some _) bounds'))
+        (Hblen : length bounds' = n')
+        (Hwt : forall i, List.In i (seq 0 n') -> 0 <= wt i)
+  : eval wt n' (List.map lower bounds') <= eval wt n' f <= eval wt n' (List.map upper bounds').
+  Proof.
+    clear -H Hb Hblen Hwt.
+    setoid_rewrite in_seq in Hwt.
+    subst bounds.
+    pose proof H as H'; apply fold_andb_map_length in H'.
+    revert dependent bounds'; intro bounds'.
+    revert dependent f; intro f.
+    rewrite <- (List.rev_involutive bounds'), <- (List.rev_involutive f);
+      generalize (List.rev bounds') (List.rev f); clear bounds' f; intros bounds f; revert bounds f.
+    induction n' as [|n IHn], bounds as [|b bounds], f as [|f fs]; intros;
+      cbn [length rev map] in *; distr_length.
+    { rewrite !map_app in *; cbn [map] in *.
+      erewrite !eval_snoc by (distr_length; eauto).
+      cbn [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by] in *.
+      cbv [is_bounded_by_bool] in *.
+      specialize_by (intros; auto with omega).
+      specialize (Hwt n); specialize_by omega.
+      repeat first [ progress Bool.split_andb
+                   | rewrite Nat.add_1_r in *
+                   | rewrite fold_andb_map_snoc in *
+                   | rewrite Nat.succ_inj_wd in *
+                   | progress Z.ltb_to_lt
+                   | progress cbn [In seq] in *
+                   | match goal with
+                     | [ H : length _ = ?v |- _ ] => rewrite H in *
+                     | [ H : ?v = length _ |- _ ] => rewrite <- H in *
+                     end ].
+      split; apply Z.add_le_mono; try apply IHn; auto; distr_length; nia. }
+  Qed.
+End HelperLemmas.
 
 (** XXX TODO: Translate Jade's python script *)
 Module Import UnsaturatedSolinas.
@@ -1371,7 +1412,10 @@ Module Import UnsaturatedSolinas.
                (negb (list_beq _ Z.eqb v1 v2), Pipeline.Values_not_provably_equal_listZ "map mask m_enc ≠ m_enc (needed for to_bytes)" v1 v2));
               (let v1 := eval (weight (Qnum limbwidth) (QDen limbwidth)) n m_enc in
                let v2 := s - Associational.eval c in
-               (negb (v1 =? v2)%Z, Pipeline.Values_not_provably_equalZ "eval m_enc ≠ s - Associational.eval c (needed for to_bytes)" v1 v2))].
+               (negb (v1 =? v2)%Z, Pipeline.Values_not_provably_equalZ "eval m_enc ≠ s - Associational.eval c (needed for to_bytes)" v1 v2));
+              (let v1 := eval (weight (Qnum limbwidth) (QDen limbwidth)) n tight_upperbounds in
+               let v2 := 2 * eval (weight (Qnum limbwidth) (QDen limbwidth)) n m_enc in
+               (negb (v1 <? v2)%Z, Pipeline.Value_not_ltZ "2 * eval m_enc ≤ eval tight_upperbounds (needed for to_bytes)" v1 v2))].
 
     Notation type_of_strip_3arrow := ((fun (d : Prop) (_ : forall A B C, d) => d) _).
 
@@ -1731,7 +1775,8 @@ Module Import UnsaturatedSolinas.
                      | solve [ auto ] ].
 
       Lemma use_curve_good
-        : Z.pos m = s - Associational.eval c
+        : let eval := eval (weight (Qnum limbwidth) (QDen limbwidth)) n in
+          Z.pos m = s - Associational.eval c
           /\ Z.pos m <> 0
           /\ s - Associational.eval c <> 0
           /\ s <> 0
@@ -1742,9 +1787,10 @@ Module Import UnsaturatedSolinas.
           /\ 0 < Qden limbwidth <= Qnum limbwidth
           /\ s = weight (Qnum limbwidth) (QDen limbwidth) n
           /\ map (Z.land (Z.ones machine_wordsize)) m_enc = m_enc
-          /\ eval (weight (Qnum limbwidth) (QDen limbwidth)) n m_enc = s - Associational.eval c
+          /\ eval m_enc = s - Associational.eval c
           /\ Datatypes.length m_enc = n
-          /\ 0 < Associational.eval c < s.
+          /\ 0 < Associational.eval c < s
+          /\ eval tight_upperbounds < 2 * eval m_enc.
       Proof.
         clear -curve_good.
         cbv [check_args fold_right] in curve_good.
@@ -1779,9 +1825,10 @@ Module Import UnsaturatedSolinas.
         { use_curve_good_t. }
         { use_curve_good_t. }
         { use_curve_good_t. }
+        { use_curve_good_t. }
       Qed.
 
-      (** TODO: Find a better place to put the spec for [to_bytes] *)
+      (** TODO: Find a better place to put the spec for [to_bytes] and [from_bytes] *)
       Definition GoodT : Prop
         := @Ring.GoodT
              (Qnum limbwidth)
@@ -1803,48 +1850,19 @@ Module Import UnsaturatedSolinas.
                  ((ZRange.type.base.option.is_bounded_by prime_bytes_bounds (type.app_curried (Interp rto_bytesv) f) = true
                    /\ (forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rto_bytesv) f
                                                = type.app_curried (t:=to_bytesT) (freeze_to_bytesmod (Qnum limbwidth) (Z.pos (Qden limbwidth)) n machine_wordsize m_enc) f))
-                  /\ (Positional.eval (weight 8 1) n_bytes (type.app_curried (t:=to_bytesT) (freeze_to_bytesmod (Qnum limbwidth) (Z.pos (Qden limbwidth)) n machine_wordsize m_enc) f)) = (Positional.eval (weight (Qnum limbwidth) (Z.pos (Qden limbwidth))) n (fst f) mod m))).
-
-      (** XXX TODO MOVE ME? *)
-      Lemma eval_is_bounded_by wt n' bounds bounds' f
-            (H : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) bounds f = true)
-            (Hb : bounds = Some (List.map (@Some _) bounds'))
-            (Hblen : length bounds' = n')
-            (Hwt : forall i, List.In i (seq 0 n') -> 0 <= wt i)
-        : eval wt n' (List.map lower bounds') <= eval wt n' f <= eval wt n' (List.map upper bounds').
-      Proof.
-        clear -H Hb Hblen Hwt.
-        setoid_rewrite in_seq in Hwt.
-        subst bounds.
-        pose proof H as H'; apply fold_andb_map_length in H'.
-        revert dependent bounds'; intro bounds'.
-        revert dependent f; intro f.
-        rewrite <- (List.rev_involutive bounds'), <- (List.rev_involutive f);
-          generalize (List.rev bounds') (List.rev f); clear bounds' f; intros bounds f; revert bounds f.
-        induction n' as [|n IHn], bounds as [|b bounds], f as [|f fs]; intros;
-          cbn [length rev map] in *; distr_length.
-        { rewrite !map_app in *; cbn [map] in *.
-          erewrite !eval_snoc by (distr_length; eauto).
-          cbn [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by] in *.
-          cbv [is_bounded_by_bool] in *.
-          specialize_by (intros; auto with omega).
-          specialize (Hwt n); specialize_by omega.
-          repeat first [ progress Bool.split_andb
-                       | rewrite Nat.add_1_r in *
-                       | rewrite fold_andb_map_snoc in *
-                       | rewrite Nat.succ_inj_wd in *
-                       | progress Z.ltb_to_lt
-                       | progress cbn [In seq] in *
-                       | match goal with
-                         | [ H : length _ = ?v |- _ ] => rewrite H in *
-                         | [ H : ?v = length _ |- _ ] => rewrite <- H in *
-                         end ].
-          split; apply Z.add_le_mono; try apply IHn; auto; distr_length; nia. }
-      Qed.
+                  /\ (Positional.eval (weight 8 1) n_bytes (type.app_curried (t:=to_bytesT) (freeze_to_bytesmod (Qnum limbwidth) (Z.pos (Qden limbwidth)) n machine_wordsize m_enc) f)) = (Positional.eval (weight (Qnum limbwidth) (Z.pos (Qden limbwidth))) n (fst f) mod m)))
+           /\ (let from_bytesT := (base.type.list base.type.Z -> base.type.list base.type.Z)%etype in
+               forall f
+                      (Hf : type.andb_bool_for_each_lhs_of_arrow (t:=from_bytesT) (@ZRange.type.option.is_bounded_by) (prime_bytes_bounds, tt) f = true),
+                 ((ZRange.type.base.option.is_bounded_by (t:=base.type.list (base.type.type_base base.type.Z)) (Some tight_bounds) (type.app_curried (Interp rfrom_bytesv) f) = true
+                   /\ (forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rfrom_bytesv) f
+                                                     = type.app_curried (t:=from_bytesT) (from_bytesmod (Qnum limbwidth) (Z.pos (Qden limbwidth)) n) f))
+                  /\ (Positional.eval (weight (Qnum limbwidth) (Z.pos (Qden limbwidth))) n (type.app_curried (t:=from_bytesT) (from_bytesmod (Qnum limbwidth) (Z.pos (Qden limbwidth)) n) f)) = (Positional.eval (weight 8 1) n_bytes (fst f)))).
+
       Theorem Good : GoodT.
       Proof.
-        pose proof use_curve_good; destruct_head'_and; destruct_head_hnf' ex.
-        split.
+        pose proof use_curve_good; cbv zeta in *; destruct_head'_and; destruct_head_hnf' ex.
+        split; [ | split ].
         { eapply Ring.Good;
             lazymatch goal with
             | [ H : ?P ?rop |- context[expr.Interp _ ?rop] ]
@@ -1873,29 +1891,32 @@ Module Import UnsaturatedSolinas.
             { lazymatch goal with
               | [ H : eval _ _ _ = ?x |- _ <= _ < 2 * ?x ] => rewrite <- H
               end.
-              cbv [m_enc tight_bounds tight_upperbounds prime_upperbound_list] in H15 |- *.
-              eapply eval_is_bounded_by with (wt:=weight (Qnum limbwidth) (QDen limbwidth)) in H15.
-              2:rewrite <- (map_map _ (@Some _)); reflexivity.
-              2:distr_length; reflexivity.
-              rewrite ?map_map in *.
+              let H := match goal with H : ZRange.type.base.option.is_bounded_by _ _ = true |- _ => H end in
+              cbv [m_enc tight_bounds tight_upperbounds prime_upperbound_list] in H |- *;
+                eapply eval_is_bounded_by with (wt:=weight (Qnum limbwidth) (QDen limbwidth)) in H;
+                [
+                | rewrite <- (map_map _ (@Some _)); reflexivity
+                | autorewrite with distr_length; reflexivity
+                | intros; apply Z.lt_le_incl, weight_positive, wprops; lia ].
+              progress rewrite ?map_map in *.
               cbn [lower upper] in *.
               split.
-              { etransitivity; [ erewrite <- eval_zeros | apply H15 ].
+              { destruct_head'_and.
+                etransitivity; [ erewrite <- eval_zeros | eassumption ].
                 apply Z.eq_le_incl; f_equal.
-                repeat match goal with H : _ |- _ => revert H end; exact admit. }
-              { eapply Z.le_lt_trans; [ apply H15 | ].
-                assert (Hlen : length (encode (weight (Qnum limbwidth) (QDen limbwidth)) n s c (s - 1)) = n) by distr_length.
-                revert Hlen.
-                generalize ((encode (weight (Qnum limbwidth) (QDen limbwidth)) n s c (s - 1))).
-                intro ls.
-                clear.
-                revert ls.
-                clearbody limbwidth.
-                induction n as [|n' IHn'], ls as [|l ls]; cbn [length]; intros; try omega.
-                repeat match goal with H : _ |- _ => revert H end; exact admit.
-                cbn [map].
-                repeat match goal with H : _ |- _ => revert H end; exact admit. }
-              repeat match goal with H : _ |- _ => revert H end; exact admit. } } }
+                erewrite zeros_ext_map; [ reflexivity | now autorewrite with distr_length ]. }
+              { destruct_head'_and.
+                eapply Z.le_lt_trans; [ eassumption | ].
+                assumption. } } } }
+        { cbv zeta; intros f Hf; split.
+          { apply Hfrom_bytesv; solve [ assumption | repeat split ]. }
+          { cbn [type.for_each_lhs_of_arrow type_base type.andb_bool_for_each_lhs_of_arrow ZRange.type.option.is_bounded_by fst snd] in *.
+            rewrite Bool.andb_true_iff in *; split_and'.
+            etransitivity; [ apply eval_from_bytesmod | reflexivity ];
+              auto; try omega.
+            { cbv [ZRange.type.base.option.is_bounded_by prime_bytes_bounds prime_bytes_upperbound_list n_bytes] in *.
+              erewrite Ring.length_is_bounded_by by eassumption.
+              autorewrite with distr_length; reflexivity. } } }
       Qed.
     End make_ring.
 
@@ -2525,8 +2546,10 @@ Module WordByWordMontgomery.
       := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list).
     Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z))
       := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list).
+    Definition saturated_upper_bounds : list Z
+      := List.repeat (2^machine_wordsize-1)%Z n.
     Definition saturated_bounds : ZRange.type.option.interp (base.type.list (base.type.Z))
-      := Some (List.repeat (Some r[0 ~> 2^machine_wordsize-1]%zrange) n).
+      := Some (List.map (fun u => Some r[0 ~> u]%zrange) saturated_upper_bounds).
 
     Definition m_enc : list Z
       := encode (UniformWeight.uweight machine_wordsize) n s c (s-Associational.eval c).
@@ -2862,7 +2885,6 @@ Module WordByWordMontgomery.
           /\ 0 < machine_wordsize
           /\ n <> 0%nat
           /\ List.length bounds = n
-          /\ List.length bounds = n
           /\ 0 < 1 <= machine_wordsize
           /\ 0 < Associational.eval c < s
           /\ (r * r') mod m = 1
@@ -2873,7 +2895,7 @@ Module WordByWordMontgomery.
       Proof.
         clear -curve_good.
         cbv [check_args fold_right] in curve_good.
-        cbv [bounds prime_bound m_enc prime_bounds] in *.
+        cbv [bounds prime_bound m_enc prime_bounds saturated_upper_bounds saturated_bounds] in *.
         break_innermost_match_hyps; try discriminate.
         rewrite negb_false_iff in *.
         Z.ltb_to_lt.
@@ -2903,10 +2925,9 @@ Module WordByWordMontgomery.
         { use_curve_good_t. }
         { use_curve_good_t. }
         { use_curve_good_t. }
-        { use_curve_good_t. }
       Qed.
 
-      (** TODO: Find a better place to put the spec for [to_bytes] *)
+      (** TODO: Find a better place to put the spec for [to_bytes] and [from_bytes] *)
       Definition GoodT : Prop
         := @MontgomeryStyleRing.GoodT
              machine_wordsize 1
@@ -2927,16 +2948,55 @@ Module WordByWordMontgomery.
                 ((ZRange.type.base.option.is_bounded_by prime_bytes_bounds (type.app_curried (Interp rto_bytesv) f) = true
                   /\ (forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rto_bytesv) f
                                                     = type.app_curried (t:=to_bytesT) (to_bytesmod machine_wordsize n) f))
-                 /\ (Positional.eval (weight 8 1) n_bytes (type.app_curried (t:=to_bytesT) (to_bytesmod machine_wordsize n) f)) = (Positional.eval (weight machine_wordsize 1) n (fst f) mod m)))
+                 (*/\ (Positional.eval (weight 8 1) n_bytes (type.app_curried (t:=to_bytesT) (to_bytesmod machine_wordsize n) f)) = (Positional.eval (weight machine_wordsize 1) n (fst f) mod m)*) (* duplicate from Arithmetic, except without validity *)))
+           /\ (let from_bytesT := (base.type.list base.type.Z -> base.type.list base.type.Z)%etype in
+               forall f
+                      (Hf : type.andb_bool_for_each_lhs_of_arrow (t:=from_bytesT) (@ZRange.type.option.is_bounded_by) (prime_bytes_bounds, tt) f = true),
+                 ((ZRange.type.base.option.is_bounded_by (t:=base.type.list (base.type.type_base base.type.Z)) prime_bounds (type.app_curried (Interp rfrom_bytesv) f) = true
+                   /\ (forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) rfrom_bytesv) f
+                                                     = type.app_curried (t:=from_bytesT) (from_bytesmod machine_wordsize 1 n) f))
+                  /\ (Positional.eval (weight machine_wordsize 1) n (type.app_curried (t:=from_bytesT) (from_bytesmod machine_wordsize 1 n) f)) = (Positional.eval (weight 8 1) n_bytes (fst f))))
            /\ (forall f
-                 (Hf : type.andb_bool_for_each_lhs_of_arrow (t:=(base.type.list base.type.Z -> base.type.Z)%etype) (@ZRange.type.option.is_bounded_by) (Some bounds, tt) f = true), (Interp rnonzerov (fst f) = 0) <-> ((@eval machine_wordsize n (from_montgomery_mod machine_wordsize n m m' (fst f))) mod m = 0)).
+                 (Hf : type.andb_bool_for_each_lhs_of_arrow (t:=(base.type.list base.type.Z -> base.type.Z)%etype) (@ZRange.type.option.is_bounded_by) (Some bounds, tt) f = true) (Hfvalid : valid machine_wordsize n m (fst f)), (Interp rnonzerov (fst f) = 0) <-> ((@eval machine_wordsize n (from_montgomery_mod machine_wordsize n m m' (fst f))) mod m = 0)).
+
+      (** XXX TODO: MOVE ME *)
+      Lemma is_bounded_by_repeat_In_iff {rg n'} {ls : list Z}
+            (H : @ZRange.type.base.option.is_bounded_by (base.type.list (base.type.type_base base.type.Z)) (Some (List.repeat (Some rg) n')) ls = true)
+        : forall x, List.In x ls -> lower rg <= x <= upper rg.
+      Proof using Type.
+        clear -H.
+        cbn [ZRange.type.base.option.is_bounded_by] in *.
+        rewrite fold_andb_map_iff in H.
+        destruct H as [H' H].
+        intros x H''; specialize (H (Some rg, x)).
+        repeat first [ progress subst
+                     | progress cbn [fst snd] in *
+                     | progress cbv [ZRange.type.base.is_bounded_by is_bounded_by_bool] in *
+                     | progress autorewrite with distr_length in *
+                     | progress rewrite combine_same in *
+                     | progress rewrite in_map_iff in *
+                     | progress specialize_by_assumption
+                     | progress Bool.split_andb
+                     | progress Z.ltb_to_lt
+                     | solve [ auto ]
+                     | match goal with
+                       | [ H : context[List.In _ (combine (repeat _ _) _)] |- _ ]
+                         => rewrite <- map_const, combine_map_l, in_map_iff in H
+                       | [ H : (exists x, _ = _ /\ _) -> _ |- _ ]
+                         => specialize (fun x0 pf => H (ex_intro _ (x0, _) (conj eq_refl pf)))
+                       | [ H : (exists x, _ = _ /\ _) -> _ |- _ ]
+                         => specialize (fun pf => H (ex_intro _ _ (conj eq_refl pf)))
+                       | [ H : forall x, List.In (x, ?y) _ -> _ |- _ ]
+                         => specialize (H y)
+                       end ].
+      Qed.
 
       (** XXX TODO MOVE ME *)
       Local Opaque valid addmod submod oppmod encodemod mulmod from_montgomery_mod nonzeromod.
       Theorem Good : GoodT.
       Proof.
         pose proof use_curve_good; destruct_head'_and; destruct_head_hnf' ex.
-        split; [ | split ].
+        split; [ | repeat apply conj ].
         { eapply MontgomeryStyleRing.Good;
             lazymatch goal with
             | [ H : ?P ?rop |- context[expr.Interp _ ?rop] ]
@@ -2957,21 +3017,22 @@ Module WordByWordMontgomery.
                          | eapply nonzeromod_correct
                          | intros; apply conj
                          | omega ]. }
+        { cbv zeta; intros f Hf.
+          apply Hto_bytesv; solve [ assumption | repeat split ]. }
         { cbv zeta; intros f Hf; split.
-          { apply Hto_bytesv; solve [ assumption | repeat split ]. }
+          { apply Hfrom_bytesv; solve [ assumption | repeat split ]. }
           { cbn [type.for_each_lhs_of_arrow type_base type.andb_bool_for_each_lhs_of_arrow ZRange.type.option.is_bounded_by fst snd] in *.
             rewrite Bool.andb_true_iff in *; split_and'.
-            apply to_bytesmod_correct; eauto; [].
-            split; cbv [small].
-            repeat match goal with H : _ |- _ => revert H end; exact admit.
-            repeat match goal with H : _ |- _ => revert H end; exact admit. } }
+            etransitivity; [ apply eval_from_bytesmod | reflexivity ];
+              auto; try omega.
+            { cbv [ZRange.type.base.option.is_bounded_by prime_bytes_bounds prime_bytes_upperbound_list n_bytes] in *.
+              erewrite Ring.length_is_bounded_by by eassumption.
+              autorewrite with distr_length; reflexivity. } } }
         { intros.
           split; [ intro H'; eapply nonzeromod_correct;
                    [ .. | rewrite <- H'; symmetry; eapply Hrnonzerov ]
                  | etransitivity; [ apply Hrnonzerov | eapply nonzeromod_correct; [ .. | eassumption ] ] ];
-          try solve [ eassumption | repeat split ].
-          repeat match goal with H : _ |- _ => revert H end; exact admit.
-          repeat match goal with H : _ |- _ => revert H end; exact admit. }
+          try solve [ eassumption | repeat split ]. }
       Qed.
     End make_ring.