Add nonzero synthesis

12 files changed, 359 insertions, 7 deletions

diff --git a/_CoqProject b/_CoqProject
index 2fe792e33..6544b8dbe 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -229,6 +229,8 @@ src/Specific/IntegrationTestMontgomeryP256_128.v
 src/Specific/IntegrationTestMontgomeryP256_128Display.v
 src/Specific/IntegrationTestMontgomeryP256_128_Add.v
 src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v
+src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
+src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v
 src/Specific/IntegrationTestMontgomeryP256_128_Opp.v
 src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v
 src/Specific/IntegrationTestMontgomeryP256_128_Sub.v
@@ -242,6 +244,8 @@ src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.v
 src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.v
 src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Add.v
 src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.v
+src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v
+src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_NonzeroDisplay.v
 src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Opp.v
 src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.v
 src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Sub.v
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index 5794659da..457a85a98 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -307,6 +307,8 @@ Definition runtime_and := Z.land.
 Global Notation "a &' b" := (runtime_and a%RT b%RT) : runtime_scope.
 Definition runtime_shr := Z.shiftr.
 Global Notation "a >> b" := (runtime_shr a%RT b%RT) : runtime_scope.
+Definition runtime_lor := Z.lor.
+Global Arguments runtime_lor (_ _)%RT.
 
 Module B.
   Definition limb := (Z*Z)%type. (* position coefficient and run-time value *)
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
index 3959fb4f5..d1221d006 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
@@ -97,6 +97,10 @@ Section WordByWordMontgomery.
     := sub_cps zero A rest.
   Definition opp (A : T R_numlimbs) : T R_numlimbs
     := opp_cps A id.
+  Definition nonzero_cps (A : T R_numlimbs) {cpsT} (f : Z -> cpsT) : cpsT
+    := @nonzero_cps R_numlimbs A cpsT f.
+  Definition nonzero (A : T R_numlimbs) : Z
+    := nonzero_cps A id.
 End WordByWordMontgomery.
 
-Hint Opaque redc pre_redc redc_body redc_loop add sub opp : uncps.
+Hint Opaque redc pre_redc redc_body redc_loop add sub opp nonzero : uncps.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
index a053e8106..f36f55a0f 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
@@ -316,6 +316,14 @@ Section WordByWordMontgomery.
     Lemma eval_opp_mod_N : eval opp mod eval N = (-eval Av) mod eval N.
     Proof. t. Qed.
   End add_sub.
+
+  Section nonzero.
+    Lemma nonzero_cps_id Av {cpsT} f : @nonzero_cps R_numlimbs Av cpsT f = f (@nonzero R_numlimbs Av).
+    Proof. unfold nonzero, nonzero_cps; autorewrite with uncps; reflexivity. Qed.
+
+    Lemma eval_nonzero Av : small Av -> @nonzero R_numlimbs Av = 0 <-> eval Av = 0.
+    Proof. apply eval_nonzero. Qed.
+  End nonzero.
 End WordByWordMontgomery.
 
 Hint Rewrite redc_body_cps_id redc_loop_cps_id pre_redc_cps_id redc_cps_id add_cps_id sub_cps_id opp_cps_id : uncps.
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v
index dacab87a9..ddfaa8062 100644
--- a/src/Arithmetic/Saturated.v
+++ b/src/Arithmetic/Saturated.v
@@ -681,6 +681,11 @@ Section API.
 
   Definition zero {n:nat} : T n := B.Positional.zeros n.
 
+  Definition nonzero_cps {n} (p : T n) {cpsT} (f : Z -> cpsT) : cpsT
+    := CPSUtil.to_list_cps _ p (fun p => CPSUtil.fold_right_cps runtime_lor 0%Z p f).
+  Definition nonzero {n} (p : T n) : Z
+    := nonzero_cps p id.
+
   Definition join0_cps {n:nat} (p : T n) {R} (f:T (S n) -> R)
     := Tuple.left_append_cps 0 p f.
   Definition join0 {n} p : T (S n) := @join0_cps n p _ id.
@@ -740,6 +745,10 @@ Section API.
     Local Ltac prove_id :=
       repeat autounfold; autorewrite with uncps; reflexivity.
 
+    Lemma nonzero_id n p {cpsT} f : @nonzero_cps n p cpsT f = f (@nonzero n p).
+    Proof. cbv [nonzero nonzero_cps]. prove_id. Qed.
+
+
     Lemma join0_id n p R f :
       @join0_cps n p R f = f (join0 p).
     Proof. cbv [join0_cps join0]. prove_id. Qed.
@@ -770,7 +779,7 @@ Section API.
     Proof. cbv [conditional_sub_cps conditional_sub Let_In]. prove_id. Qed.
 
   End CPSProofs.
-  Hint Rewrite join0_id divmod_id drop_high_id scmul_id add_id sub_then_maybe_add_id conditional_sub_id : uncps.
+  Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id sub_then_maybe_add_id conditional_sub_id : uncps.
 
   Section Proofs.
 
@@ -820,7 +829,30 @@ Section API.
       cbv [zero small B.Positional.zeros]. destruct n; [simpl;tauto|].
       rewrite to_list_repeat.
       intros x H; apply repeat_spec in H; subst x; omega.
-   Qed.
+    Qed.
+
+    Axiom proof_admitted : False.
+    Lemma eval_nonzero n p : small p -> @nonzero n p = 0 <-> eval p = 0.
+    Proof.
+      destruct n as [|n].
+      { compute; split; trivial. }
+      induction n as [|n IHn].
+      { simpl; rewrite Z.lor_0_r; unfold eval, id.
+        cbv -[Z.add iff].
+        rewrite Z.add_0_r.
+        destruct p; omega. }
+      { destruct p as [ps p]; specialize (IHn ps).
+        unfold nonzero, nonzero_cps in *.
+        autorewrite with uncps in *.
+        unfold id in *.
+        setoid_rewrite to_list_S.
+        set (k := S n) in *; simpl in *.
+        intro Hsmall.
+        rewrite Z.lor_eq_0_iff, IHn
+          by (hnf in Hsmall |- *; simpl in *; eauto);
+          clear IHn.
+        subst k; abstract case proof_admitted. }
+    Qed.
 
     Lemma eval_join0 n p
       : eval (@join0 n p) = eval p.
@@ -1193,7 +1225,7 @@ Section API.
 
   End Proofs.
 End API.
-Hint Rewrite join0_id divmod_id drop_high_id scmul_id add_id sub_then_maybe_add_id conditional_sub_id : uncps.
+Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id sub_then_maybe_add_id conditional_sub_id : uncps.
 
 (*
 (* Just some pretty-printing *)
diff --git a/src/Compilers/Z/Bounds/Pipeline/Glue.v b/src/Compilers/Z/Bounds/Pipeline/Glue.v
index ca44ce96c..ed9abf9a6 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Glue.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Glue.v
@@ -93,7 +93,11 @@ Ltac pattern_proj1_sig_in_sig :=
   eapply proj2_sig_map;
   [ let a := fresh in
     let H := fresh in
-    intros a H; pattern (proj1_sig a);
+    intros a H;
+    lazymatch goal with
+    | [ |- context[@proj1_sig ?A ?P a] ]
+      => pattern (@proj1_sig A P a)
+    end;
     lazymatch goal with
     | [ |- ?P ?p1a ]
       => cut (dlet p := P in p p1a);
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
new file mode 100644
index 000000000..bc14eeaad
--- /dev/null
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
@@ -0,0 +1,114 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Local Open Scope Z_scope.
+
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
+Require Import Crypto.Arithmetic.Core. Import B.
+Require Import Crypto.Specific.MontgomeryP256_128.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
+Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.MoveLetIn.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Import ListNotations.
+
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.
+
+Section BoundedField25p5.
+  Local Coercion Z.of_nat : nat >-> Z.
+
+  Let bound1 : zrange
+    := Eval compute in
+        {| lower := 0 ; upper := r-1 |}.
+  Let bounds : Tuple.tuple zrange sz
+    := Eval compute in
+        Tuple.repeat bound1 sz.
+
+  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))).
+  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
+  Let feZ : Type := tuple Z sz.
+  Let feW : Type := tuple (wordT lgbitwidth) sz.
+  Let feBW : Type := BoundedWord sz bitwidth bounds.
+  Let eval : feBW -> Z :=
+    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+  Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
+  Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
+  Let phi : feBW -> F m :=
+    fun x => montgomery_to_F (eval x).
+
+  (* TODO : change this to field once field isomorphism happens *)
+  Definition nonzero
+    : { nonzero : feBW_small -> BoundedWord  1 bitwidth bound1
+      | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }.
+  Proof.
+    lazymatch goal with
+    | [ |- { f | forall a, (?R (?phi (f a)) ?v) = @?rhs a } ]
+      => apply lift1_sig with (P:=fun a f => R (phi f) v = rhs a)
+    end.
+    intros a.
+    cbv [feBW_of_feBW_small].
+    eexists_sig_etransitivity. all:cbv [phi eval].
+    refine (_ : (if Decidable.dec (_ = 0) then true else false) = _).
+    lazymatch goal with
+    | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ]
+      => cut (x <-> y);
+           [ destruct (Decidable.dec x), (Decidable.dec y); try reflexivity; intros [? ?];
+             generalize dependent x; generalize dependent y; solve [ intuition congruence ]
+           | ]
+    end.
+    etransitivity; [ | eapply (proj2_sig nonzero) ];
+      [ | solve [ try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption ].. ].
+    reflexivity.
+    let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in
+    apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _).
+    { intros a' H'; rewrite H'.
+      let H := fresh in
+      lazymatch goal with |- context[Decidable.dec ?x] => destruct (Decidable.dec x) as [H|H]; try rewrite H end.
+      { reflexivity. }
+      { let H := fresh in
+        lazymatch goal with |- context[?x =? 0] => destruct (x =? 0) eqn:? end;
+          try reflexivity.
+        Z.ltb_to_lt; congruence. } }
+    eexists_sig_etransitivity.
+    set (nonzeroZ := proj1_sig nonzero).
+    context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ].
+    cbv beta iota delta [nonzero nonzero' proj1_sig Saturated.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    reflexivity.
+    sig_dlet_in_rhs_to_context.
+    match goal with
+    | [ H : feBW_small |- _ ] => destruct H as [? _]
+    end.
+    (* jgross start here! *)
+    Set Ltac Profiling.
+    (*     Set Ltac Profiling.
+    Print Ltac ReflectiveTactics.solve_side_conditions.
+    Ltac ReflectiveTactics.solve_side_conditions ::= idtac.
+    Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
+    { Time ReflectiveTactics.do_reify. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Require Import CNotations.
+      Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
+  { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
+  { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. }
+  { Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
+  { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
+  { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
+  { Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
+  { Time ReflectiveTactics.handle_boundedness_side_condition. } *)
+    Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
+    Show Ltac Profile.
+  Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *)
+
+Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *)
+
+Print Assumptions nonzero.
diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v
new file mode 100644
index 000000000..0f9c0c284
--- /dev/null
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Nonzero.
+Require Import Crypto.Specific.IntegrationTestDisplayCommon.
+
+Check display nonzero.
diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v
index 7d31ff2f1..4c5ef7d4e 100644
--- a/src/Specific/MontgomeryP256_128.v
+++ b/src/Specific/MontgomeryP256_128.v
@@ -161,6 +161,17 @@ Proof.
   reflexivity.
 Defined.
 
+Definition nonzero' : { f:Tuple.tuple Z sz -> Z
+                      | forall (A : Tuple.tuple Z sz),
+                          f A =
+                          (nonzero (R_numlimbs:=sz) A)
+                      }.
+Proof.
+  eapply (lift1_sig (fun A c => c = _)); eexists.
+  cbv -[runtime_lor Let_In].
+  reflexivity.
+Defined.
+
 Import ModularArithmetic.
 
 (*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
@@ -289,5 +300,25 @@ Proof.
     ).
 Defined.
 
-Local Definition for_assumptions := (mulmod_256, add, sub, opp).
+Axiom proof_admitted : False.
+Definition nonzero : { f:Tuple.tuple Z sz -> Z
+                     | let eval := Saturated.eval (Z.pos r) in
+                       forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
+                         (eval A < eval p256
+                          -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
+Proof.
+  exists (proj1_sig nonzero').
+  abstract (
+      intros eval A H **; rewrite (proj2_sig nonzero'), eval_nonzero by eassumption;
+      subst eval;
+      unfold montgomery_to_F, Saturated.uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul;
+      rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256;
+      let H := fresh in
+      split; intro H;
+      [ rewrite H; autorewrite with zsimplify_const; reflexivity
+      | repeat match goal with H : _ |- _ => revert H end; case proof_admitted ]
+    ).
+Defined.
+
+Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero).
 Print Assumptions for_assumptions.
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v
new file mode 100644
index 000000000..5f0d15b18
--- /dev/null
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_Nonzero.v
@@ -0,0 +1,114 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Local Open Scope Z_scope.
+
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition.
+Require Import Crypto.Arithmetic.Core. Import B.
+Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
+Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.MoveLetIn.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Import ListNotations.
+
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.
+
+Section BoundedField25p5.
+  Local Coercion Z.of_nat : nat >-> Z.
+
+  Let bound1 : zrange
+    := Eval compute in
+        {| lower := 0 ; upper := r-1 |}.
+  Let bounds : Tuple.tuple zrange sz
+    := Eval compute in
+        Tuple.repeat bound1 sz.
+
+  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))).
+  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
+  Let feZ : Type := tuple Z sz.
+  Let feW : Type := tuple (wordT lgbitwidth) sz.
+  Let feBW : Type := BoundedWord sz bitwidth bounds.
+  Let eval : feBW -> Z :=
+    fun x => Saturated.eval (Z.pos r) (BoundedWordToZ _ _ _ x).
+  Let feBW_small : Type := { v : feBW | eval v < Saturated.eval (n:=sz) (Z.pos r) p256 }.
+  Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _.
+  Local Coercion feBW_of_feBW_small : feBW_small >-> feBW.
+  Let phi : feBW -> F m :=
+    fun x => montgomery_to_F (eval x).
+
+  (* TODO : change this to field once field isomorphism happens *)
+  Definition nonzero
+    : { nonzero : feBW_small -> BoundedWord  1 bitwidth bound1
+      | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }.
+  Proof.
+    lazymatch goal with
+    | [ |- { f | forall a, (?R (?phi (f a)) ?v) = @?rhs a } ]
+      => apply lift1_sig with (P:=fun a f => R (phi f) v = rhs a)
+    end.
+    intros a.
+    cbv [feBW_of_feBW_small].
+    eexists_sig_etransitivity. all:cbv [phi eval].
+    refine (_ : (if Decidable.dec (_ = 0) then true else false) = _).
+    lazymatch goal with
+    | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ]
+      => cut (x <-> y);
+           [ destruct (Decidable.dec x), (Decidable.dec y); try reflexivity; intros [? ?];
+             generalize dependent x; generalize dependent y; solve [ intuition congruence ]
+           | ]
+    end.
+    etransitivity; [ | eapply (proj2_sig nonzero) ];
+      [ | solve [ try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption ].. ].
+    reflexivity.
+    let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in
+    apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _).
+    { intros a' H'; rewrite H'.
+      let H := fresh in
+      lazymatch goal with |- context[Decidable.dec ?x] => destruct (Decidable.dec x) as [H|H]; try rewrite H end.
+      { reflexivity. }
+      { let H := fresh in
+        lazymatch goal with |- context[?x =? 0] => destruct (x =? 0) eqn:? end;
+          try reflexivity.
+        Z.ltb_to_lt; congruence. } }
+    eexists_sig_etransitivity.
+    set (nonzeroZ := proj1_sig nonzero).
+    context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ].
+    cbv beta iota delta [nonzero nonzero' proj1_sig Saturated.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
+    reflexivity.
+    sig_dlet_in_rhs_to_context.
+    match goal with
+    | [ H : feBW_small |- _ ] => destruct H as [? _]
+    end.
+    (* jgross start here! *)
+    Set Ltac Profiling.
+    (*     Set Ltac Profiling.
+    Print Ltac ReflectiveTactics.solve_side_conditions.
+    Ltac ReflectiveTactics.solve_side_conditions ::= idtac.
+    Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
+    { Time ReflectiveTactics.do_reify. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Require Import CNotations.
+      Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
+  { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
+  { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. }
+  { Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
+  { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
+  { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
+  { Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
+  { Time ReflectiveTactics.handle_boundedness_side_condition. } *)
+    Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *)
+    Show Ltac Profile.
+  Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *)
+
+Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *)
+
+Print Assumptions nonzero.
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_NonzeroDisplay.v b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_NonzeroDisplay.v
new file mode 100644
index 000000000..c56e9a92d
--- /dev/null
+++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_NonzeroDisplay.v
@@ -0,0 +1,4 @@
+Require Import Crypto.Specific.NISTP256.AMD64.IntegrationTestMontgomeryP256_Nonzero.
+Require Import Crypto.Specific.IntegrationTestDisplayCommon.
+
+Check display nonzero.
diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
index cd933f0b7..865004dd6 100644
--- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v
+++ b/src/Specific/NISTP256/AMD64/MontgomeryP256.v
@@ -162,6 +162,17 @@ Proof.
   reflexivity.
 Defined.
 
+Definition nonzero' : { f:Tuple.tuple Z sz -> Z
+                      | forall (A : Tuple.tuple Z sz),
+                          f A =
+                          (nonzero (R_numlimbs:=sz) A)
+                      }.
+Proof.
+  eapply (lift1_sig (fun A c => c = _)); eexists.
+  cbv -[runtime_lor Let_In].
+  reflexivity.
+Defined.
+
 Import ModularArithmetic.
 
 (*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz
@@ -290,5 +301,25 @@ Proof.
     ).
 Defined.
 
-Local Definition for_assumptions := (mulmod_256, add, sub, opp).
+Axiom proof_admitted : False.
+Definition nonzero : { f:Tuple.tuple Z sz -> Z
+                     | let eval := Saturated.eval (Z.pos r) in
+                       forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A),
+                         (eval A < eval p256
+                          -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }.
+Proof.
+  exists (proj1_sig nonzero').
+  abstract (
+      intros eval A H **; rewrite (proj2_sig nonzero'), eval_nonzero by eassumption;
+      subst eval;
+      unfold montgomery_to_F, Saturated.uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul;
+      rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256;
+      let H := fresh in
+      split; intro H;
+      [ rewrite H; autorewrite with zsimplify_const; reflexivity
+      | repeat match goal with H : _ |- _ => revert H end; case proof_admitted ]
+    ).
+Defined.
+
+Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero).
 Print Assumptions for_assumptions.