saw-core-coq: Explicitly define atWithProof, genWithProof, and friends

This provides explicit Coq definitions for SAWCore's `atWithProof` and
`genWithProof` functions, which allow them to compute. It also proves the
auxiliary `at_gen_BVVec` and `gen_at_BVVec` lemmas, a feat which is now possible
thanks to the aforementioned computability.

Fixes #1784.

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

@@ -1,11 +1,17 @@
+From Coq          Require Import Arith.Peano_dec.
+From Coq          Require Import Arith.PeanoNat.
 From Coq          Require Import Lists.List.
+From Coq          Require Import Logic.Eqdep_dec.
 From Coq          Require Import Logic.FunctionalExtensionality.
 Import ListNotations.
 From Coq          Require Import String.
 From Coq          Require Import Vectors.Vector.
+From CryptolToCoq Require Import SAWCoreBitvectors.
 From CryptolToCoq Require Import SAWCoreScaffolding.
 From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
 Import SAWCorePrelude.
+Import VectorNotations.
 
 Fixpoint Nat_cases2_match a f1 f2 f3 (x y : nat) : a :=
   match (x, y) with
@@ -68,6 +74,116 @@ Proof.
   intro n. reflexivity.
 Qed.
 
+Lemma Vec_0_nil :
+  forall (a : Type) (v : Vec 0 a),
+  v = [].
+Proof.
+  intros a v.
+  apply (case0 (fun v' => v' = [])).
+  reflexivity.
+Qed.
+
+Lemma Vec_S_cons :
+  forall (n : nat) (a : Type) (v : Vec (S n) a),
+  exists (x : a) (xs : Vec n a),
+  v = x::xs.
+Proof.
+  intros n a v.
+  apply (caseS (fun n' v' => exists (x : a) (xs : Vec n' a), v' = x::xs)).
+  intros x m xs.
+  exists x. exists xs.
+  reflexivity.
+Qed.
+
+Lemma bvToNat_bvNat (w n : nat) :
+  n < 2^w -> bvToNat w (bvNat w n) = n.
+Admitted.
+
+Lemma bvToNat_bounds (w : nat) (x : bitvector w) :
+  bvToNat w x < 2^w.
+Proof.
+  holds_for_bits_up_to_3; try repeat constructor.
+Qed.
+
+Lemma at_gen_Vec :
+  forall (n : nat) (a : Type)
+         (f : forall i : nat, IsLtNat i n -> a)
+         (ix : nat) (pf : IsLtNat ix n),
+  atWithProof n a (genWithProof n a f) ix pf = f ix pf.
+Proof.
+  intros n a f.
+  induction n; intros ix pf.
+  - destruct (Nat.nlt_0_r ix pf).
+  - induction ix.
+    + simpl.
+      rewrite (le_unique _ _ (le_n_S 0 n (le_0_n n)) pf).
+      reflexivity.
+    + simpl.
+      rewrite IHn.
+      rewrite (le_unique _ _ (le_n_S (Succ ix) n (le_S_n (S ix) n pf)) pf).
+      reflexivity.
+Qed.
+
+Lemma gen_at_Vec :
+  forall (n : nat) (a : Type) (x : Vec n a),
+  genWithProof n a (atWithProof n a x) = x.
+Proof.
+  intros n a x.
+  induction n.
+  - rewrite (Vec_0_nil a x). reflexivity.
+  - destruct (Vec_S_cons n a x) as [y [ys Yeq]].
+    subst x. simpl.
+    rewrite <- (IHn ys) at 1.
+    do 2 f_equal.
+    extensionality i. extensionality prf.
+    rewrite (le_unique _ _ (le_S_n (S i) n (le_n_S (Succ i) n prf)) prf).
+    reflexivity.
+Qed.
+
+Theorem at_gen_BVVec :
+  forall (n : nat) (len : bitvector n) (a : Type)
+         (f : forall i : bitvector n, is_bvult n i len -> a)
+         (ix : bitvector n) (pf : is_bvult n ix len),
+  atBVVec n len a (genBVVec n len a f) ix pf = f ix pf.
+Proof.
+  intros n len a f ix pf.
+  unfold atBVVec, genBVVec.
+  rewrite at_gen_Vec.
+  generalize (IsLtNat_to_bvult n len (bvToNat n ix)
+               (bvult_to_IsLtNat n len (bvToNat n ix)
+                 (trans bool (bvult n (bvNat n (bvToNat n ix)) len) (bvult n ix len) 1%bool
+                   (eq_cong (bitvector n) (bvNat n (bvToNat n ix)) ix (bvNat_bvToNat_id n ix) bool
+                     (fun y : bitvector n => bvult n y len)) pf))) as pf2.
+  rewrite (bvNat_bvToNat n ix).
+  intros pf2.
+  rewrite (UIP_dec Bool.bool_dec pf2 pf).
+  reflexivity.
+Qed.
+
+Lemma gen_at_BVVec :
+  forall (n : nat) (len : bitvector n) (a : Type) (x : BVVec n len a),
+  genBVVec n len a (atBVVec n len a x) = x.
+Proof.
+  intros n len a x.
+  unfold genBVVec, atBVVec.
+  rewrite <- (gen_at_Vec _ _ x) at 1.
+  f_equal. extensionality i. extensionality pf.
+  generalize (bvult_to_IsLtNat n len (bvToNat n (bvNat n i))
+               (trans bool (bvult n (bvNat n (bvToNat n (bvNat n i))) len) (bvult n (bvNat n i) len) 1%bool
+                 (eq_cong (bitvector n) (bvNat n (bvToNat n (bvNat n i))) (bvNat n i)
+                   (bvNat_bvToNat_id n (bvNat n i)) bool (fun y : bitvector n => bvult n y len))
+                     (IsLtNat_to_bvult n len i pf))) as pf2.
+  assert (X : bvToNat n (bvNat n i) = i).
+  { apply bvToNat_bvNat.
+    transitivity (bvToNat n len).
+    - exact pf.
+    - apply bvToNat_bounds.
+  }
+  rewrite X. intros pf2.
+  rewrite (le_unique _ _ pf2 pf).
+  reflexivity.
+Qed.
+
 
 Theorem fold_unfold_IRT As Ds D : forall x, foldIRT As Ds D (unfoldIRT As Ds D x) = x.
 Proof.
@@ -91,4 +207,4 @@ Proof.
      and the fact that genBVVec and atBVVec define an isomorphism *)
   etransitivity; [ | apply gen_at_BVVec ].
   f_equal; repeat (apply functional_extensionality_dep; intro); eauto.
-Qed.
+Qed.

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

@@ -97,6 +97,7 @@ text = pretty
 preamble :: TranslationConfiguration -> Doc ann
 preamble (TranslationConfiguration { vectorModule, postPreamble }) = text [i|
 (** Mandatory imports from saw-core-coq *)
+From Coq Require Import Arith.PeanoNat.
 From Coq Require Import Lists.List.
 From Coq Require Import String.
 From Coq Require Import Vectors.Vector.

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

@@ -370,6 +370,7 @@ sawCorePreludeSpecialTreatmentMap configuration =
   ++
   [ ("EmptyVec",      mapsTo vectorsModule "EmptyVec")
   , ("at",            rename "sawAt") -- `at` is a reserved keyword in Coq
+  , ("at_gen_BVVec",  mapsTo preludeExtraModule "at_gen_BVVec")
   , ("atWithDefault", mapsTo vectorsModule "atWithDefault")
   , ("at_single",     skip) -- is boring, could be proved on the Coq side
   , ("bvAdd",         mapsTo vectorsModule "bvAdd")
@@ -394,6 +395,7 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("eq_Vec",        skip)
   , ("foldr",         mapsTo vectorsModule "foldr")
   , ("foldl",         mapsTo vectorsModule "foldl")
+  , ("gen_at_BVVec",  mapsTo preludeExtraModule "gen_at_BVVec")
   , ("scanl",         mapsTo vectorsModule "scanl")
   , ("gen",           mapsTo vectorsModule "gen")
   , ("rotateL",       mapsTo vectorsModule "rotateL")
@@ -405,6 +407,10 @@ sawCorePreludeSpecialTreatmentMap configuration =
   -- used by other definitions in the same file, so it can neither be pre- nor
   -- post-defined.
   , ("zip",           realize zipSnippet)
+  -- Similarly for {at,gen}WithProof, as they depend on IsLtNat (generated in
+  -- SAWCorePrelude) and is used by {at,gen}BVVec (defined in SAWCorePrelude).
+  , ("atWithProof",   realize atWithProofSnippet)
+  , ("genWithProof",  realize genWithProofSnippet)
   -- cannot map directly to Vector.t because arguments are in a different order
   , ("Vec",           mapsTo vectorsModule "Vec")
   ]
@@ -604,3 +610,27 @@ Fixpoint zip (a b : sort 0) (m n : nat) (xs : Vec m a) (ys : Vec n b)
   end
 .
 |]
+
+atWithProofSnippet :: String
+atWithProofSnippet = [i|
+Fixpoint atWithProof (n : nat) (a : Type) (v : Vec n a) (i : nat) :
+    IsLtNat i n -> a :=
+  match i as i', n as n' return Vec n' a -> IsLtNat i' n' -> a with
+  | _,   O   => fun _ prf =>
+                match Nat.nlt_0_r _ prf with end
+  | O,   S y => fun v' prf => Vector.hd v'
+  | S x, S y => fun v' prf => atWithProof y a (Vector.tl v') x (le_S_n _ _ prf)
+  end v.
+|]
+
+genWithProofSnippet :: String
+genWithProofSnippet = [i|
+Fixpoint genWithProof (n : nat) (a : Type) :
+    (forall (i : nat), IsLtNat i n -> a) -> Vec n a :=
+  match n as n' return (forall (i : nat), IsLtNat i n' -> a) -> Vec n' a with
+  | O   => fun _ => Vector.nil a
+  | S m => fun f => Vector.cons a (f 0 (le_n_S _ _ (le_0_n _)))
+                                m (genWithProof m a
+                                               (fun i prf => f (S i) (le_n_S _ _ prf)))
+  end.
+|]