saw-core: Use bvNat_bvToNat over bvNat_bvToNat_id

To avoid unnecessary breakage in the Coq support libraries, we keep
`bvNat_bvToNat_id` around as a deprecated alias for `bvNat_bvToNat`.

Fixes #1785.

Author: RyanGlScott

heapster-saw/examples/mbox_proofs.v

@@ -28,16 +28,16 @@ Import mbox.
 
 (* QOL: nicer names for bitvector and mbox arguments *)
 #[local] Hint Extern 901 (IntroArg Any (bitvector _) _) =>
-  let e := fresh "x" in IntroArg_intro e : refines prepostcond. 
+  let e := fresh "x" in IntroArg_intro e : refines prepostcond.
 #[local] Hint Extern 901 (IntroArg Any Mbox _) =>
-  let e := fresh "m" in IntroArg_intro e : refines prepostcond. 
+  let e := fresh "m" in IntroArg_intro e : refines prepostcond.
 #[local] Hint Extern 901 (IntroArg Any Mbox_def _) =>
   let e := fresh "m" in IntroArg_intro e : refines prepostcond.
 
 #[local] Hint Extern 901 (IntroArg RetAny (bitvector _) _) =>
-  let e := fresh "r_x" in IntroArg_intro e : refines prepostcond. 
+  let e := fresh "r_x" in IntroArg_intro e : refines prepostcond.
 #[local] Hint Extern 901 (IntroArg RetAny Mbox _) =>
-  let e := fresh "r_m" in IntroArg_intro e : refines prepostcond. 
+  let e := fresh "r_m" in IntroArg_intro e : refines prepostcond.
 #[local] Hint Extern 901 (IntroArg RetAny Mbox_def _) =>
   let e := fresh "r_m" in IntroArg_intro e : refines prepostcond.
 
@@ -194,7 +194,7 @@ Polymorphic Lemma bvuleWithProof_not_IntroArg n w a b goal :
   IntroArg n (~ (isBvule w a b)) (fun _ => goal) ->
   IntroArg n (bvuleWithProof w a b = Nothing _) (fun _ => goal).
 Proof. intros H eq; apply H; apply bvuleWithProof_not; eauto. Qed.
- 
+
 #[local] Hint Extern 101 (IntroArg _ (bvuleWithProof _ _ _ = Nothing _) _) =>
   simple apply bvuleWithProof_not_IntroArg || shelve : refines.
 
@@ -288,9 +288,9 @@ Global Instance QuantType_bitvector {w} : QuantType (bitvector w) :=
   { quantEnc := QEnc_nat;
     quantEnum := bvNat w;
     quantEnumInv := bvToNat w;
-    quantEnumSurjective := bvNat_bvToNat_id w }.
+    quantEnumSurjective := bvNat_bvToNat w }.
 
-Lemma gen_sawAt_eq n a v `{Inhabited a} : 
+Lemma gen_sawAt_eq n a v `{Inhabited a} :
   gen n a (sawAt n a v) = v.
 Proof. dependent induction v; simpl; f_equal. apply IHv. Qed.
 
@@ -441,7 +441,7 @@ Tactic Notation "rewrite_transMbox_Mbox_nil_r_dep" "in" ident(H1) ident(H2) :=
 Tactic Notation "rewrite_transMbox_Mbox_nil_r_dep" "in" ident(H1) ident(H2) ident(H3) :=
   revert H1 H2 H3; rewrite transMbox_Mbox_nil_r; intros H1 H2 H3.
 
-Definition mbox_chain_length := 
+Definition mbox_chain_length :=
   Mbox_rect (fun _ => nat) O (fun _ _ _ rec _ => S rec).
 
 Lemma mbox_chain_length_transMbox m1 m2 :
@@ -500,7 +500,7 @@ Time Qed.
 
 Lemma mbox_rect_identity m :
   Mbox_rect _ Mbox_nil (fun strt len _ rec d => Mbox_cons strt len rec d) m = m.
-Proof. induction m; simpl; try f_equal; eauto. Qed. 
+Proof. induction m; simpl; try f_equal; eauto. Qed.
 
 Definition mbox_concat_chains_spec (m1 m2 : Mbox) : Mbox :=
   if mbox_chain_length m1 =? 0 then Mbox_nil else transMbox m1 m2.
@@ -1131,7 +1131,7 @@ Proof.
     Ltac busywork a e_assert := simpl in *;
       repeat rewrite_transMbox_Mbox_nil_r_dep in a e_assert.
     + unshelve instantiate (1 := _).
-      { busywork a e_assert. apply a. } 
+      { busywork a e_assert. apply a. }
       busywork a e_assert.
       rewrite -> e_assert.
       reflexivity.

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v

@@ -241,6 +241,13 @@ Definition isBvult_to_bvEq_false w a b : isBvult w a b -> bvEq w a b = false.
 Proof. holds_for_bits_up_to_3. Qed.
 
 
+(** Other lemmas about bitvector equalities **)
+
+(** DEPRECATED: Use [bvNat_bvToNat] instead. *)
+Definition bvNat_bvToNat_id w a : bvNat w (bvToNat w a) = a :=
+  bvNat_bvToNat w a.
+
+
 (** Other lemmas about bitvector inequalities **)
 
 Definition not_isBvslt_bvsmin w a : ~ isBvslt w a (bvsmin w).

saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs

@@ -472,7 +472,6 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("bveq_sameL",           skip)
   , ("bveq_sameR",           skip)
   , ("bveq_same2",           skip)
-  , ("bvNat_bvToNat",        skip)
   , ("ite_split_cong",       skip)
   , ("ite_join_cong",        skip)
   , ("map_map",              skip)

saw-core/prelude/Prelude.sawcore

@@ -1218,9 +1218,6 @@ primitive bvNat : (n : Nat) -> Nat -> Vec n Bool;
 -- | Satisfies @bvNat n (bvToNat n x) = x@.
 primitive bvToNat : (n : Nat) -> Vec n Bool -> Nat;
 
-axiom bvNat_bvToNat_id : (n : Nat) -> (x : Vec n Bool) ->
-                         Eq (Vec n Bool) (bvNat n (bvToNat n x)) x;
-
 bvAt : (n : Nat) -> (a : isort 0) -> (w : Nat) -> Vec n a -> Vec w Bool
      -> a;
 bvAt n a w xs i = at n a xs (bvToNat w i);
@@ -1946,7 +1943,7 @@ atBVVec n len a x ix pf =
     (bvult_to_IsLtNat n len (bvToNat n ix)
       (trans Bool (bvult n (bvNat n (bvToNat n ix)) len) (bvult n ix len) True
         (eq_cong (Vec n Bool) (bvNat n (bvToNat n ix)) ix
-          (bvNat_bvToNat_id n ix) Bool (\ (y:Vec n Bool) -> bvult n y len))
+          (bvNat_bvToNat n ix) Bool (\ (y:Vec n Bool) -> bvult n y len))
         pf));
 
 -- Indexing a generated BVVec just returns the generating function