From a204ed31fdda33129513d421d7f746ef9974f1c0 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 15 Apr 2021 08:28:14 -0400
Subject: [PATCH] Don't ask for needless `32 <= Semantics.width`

As Jade pointed out in
https://github.com/mit-plv/fiat-crypto/pull/929#issuecomment-820375339,
it's not needed.
---
 src/Bedrock/Field/Interface/Representation.v | 5 ++---
 src/Bedrock/Field/Synthesis/Generic/Bignum.v | 9 ++++++---
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/Bedrock/Field/Interface/Representation.v b/src/Bedrock/Field/Interface/Representation.v
index 941dd3b82e..8e20060557 100644
--- a/src/Bedrock/Field/Interface/Representation.v
+++ b/src/Bedrock/Field/Interface/Representation.v
@@ -18,8 +18,7 @@ Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
 
 Section Representation.
   Context {p : Types.parameters} {field_parameters : FieldParameters}
-          {p_ok : Types.ok}
-          (width_ge_32 : 32 <= Semantics.width).
+          {p_ok : Types.ok}.
   Context (n : nat) (weight : nat -> Z)
           (loose_bounds tight_bounds : list (option zrange))
           (relax_bounds :
@@ -74,7 +73,7 @@ Section Representation.
       { match goal with
           | H : Array.array _ _ _ _ _ |- _ =>
             eapply Bignum_of_bytes with (n0:=n) in H;
-              [ destruct H | nia.. ]
+              [ destruct H | (idtac + destruct Semantics.width_cases); nia.. ]
         end.
         eexists; eauto. }
       {
diff --git a/src/Bedrock/Field/Synthesis/Generic/Bignum.v b/src/Bedrock/Field/Synthesis/Generic/Bignum.v
index c95486866b..f67999d721 100644
--- a/src/Bedrock/Field/Synthesis/Generic/Bignum.v
+++ b/src/Bedrock/Field/Synthesis/Generic/Bignum.v
@@ -30,8 +30,7 @@ Section Bignum.
     sep (emp (length x = n_bytes)) (array ptsto (word.of_Z 1) px x).
 
   Section Proofs.
-    Context {ok : Types.ok}
-            (width_ge_32 : 32 <= Semantics.width).
+    Context {ok : Types.ok}.
     Existing Instance semantics_ok.
 
     (* TODO: factor this proof into a more general form that says if subarrays
@@ -51,7 +50,11 @@ Section Bignum.
         cbn [array length] in *. sepsimpl; eauto. }
       { rewrite <-(firstn_skipn (Z.to_nat word_size_in_bytes) bs).
         rewrite array_append.
-        rewrite Scalars.scalar_of_bytes with (l:=List.firstn _ _); try assumption.
+        rewrite Scalars.scalar_of_bytes with (l:=List.firstn _ _);
+          lazymatch goal with
+          | [ |- _ <= Semantics.width ] => destruct Semantics.width_cases; lia
+          | _ => idtac
+          end.
         2:{
           rewrite word_size_in_bytes_eq in *.
           etransitivity;