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.

To make this work with the current module ordering, I needed to wire in the
definition of `IsLtNat` into `SAWCoreScaffolding`, which proves
straightforward.

Fixes #1784.

Author: RyanGlScott

heapster-saw/examples/mbox_proofs.v

@@ -6,6 +6,7 @@ From CryptolToCoq Require Import SAWCoreScaffolding.
 From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
 From CryptolToCoq Require Import SAWCoreBitvectors.
 From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import SAWCorePreludeExtra.
 From CryptolToCoq Require Import SpecMExtra.
 From EnTree       Require Import Automation.
 Import SAWCorePrelude.

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

@@ -1,10 +1,15 @@
+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.
 
 Fixpoint Nat_cases2_match a f1 f2 f3 (x y : nat) : a :=
@@ -68,6 +73,60 @@ Proof.
   intro n. 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.
+
+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 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 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.

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

@@ -224,6 +224,11 @@ Definition IsLeNat__rec
             | le_S _ m H => Hstep m H (rec m H)
             end.
 
+(* We could have SAW autogenerate this definition in SAWCorePrelude, but it is
+   convenient to place it here so that it can be used in
+   SAWCoreVectorsAsCoqVectors.v, which cannot import SAWCorePrelude. *)
+Definition IsLtNat := @lt.
+
 (* Definition minNat := Nat.min. *)
 
 Definition uncurry (a b c : Type) (f : a -> b -> c) (p : a * (b * unit)) : c  :=

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

@@ -1,8 +1,10 @@
 From Bits Require Import operations.
 From Bits Require Import spec.
 
+From Coq Require Import FunctionalExtensionality.
 From Coq Require Import Lists.List.
 From Coq Require        Numbers.NatInt.NZLog.
+From Coq Require Import Peano_dec.
 From Coq Require Import PeanoNat.
 From Coq Require Import Strings.String.
 From Coq Require Import Vectors.Vector.
@@ -36,6 +38,27 @@ Constraint Vec.u1 <= mkrel.u0.
 Constraint Vec.u1 <= mkapp.u0.
 Constraint Vec.u1 <= mkapp.u1.
 
+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.
+
 Fixpoint gen (n : nat) (a : Type) (f : nat -> a) {struct n} : Vec n a.
   refine (
       match n with
@@ -115,6 +138,15 @@ Fixpoint atWithDefault (n : nat) (a : Type) (default : a) (v : Vec n a) (index :
   ).
 Defined.
 
+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.
+
 Definition map (a b : Type) (f : a -> b) (n : nat) (xs : Vec n a) :=
   VectorDef.map f xs.
 
@@ -175,6 +207,15 @@ Proof.
   }
 Qed.
 
+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.
+
 (* NOTE: This version of `zip` accepts two vectors of different size, unlike the
  * one in `CoqVectorsExtra.v` *)
 Fixpoint zipFunctional (a b : sort 0) (m n : nat) (xs : Vec m a) (ys : Vec n b)
@@ -199,6 +240,41 @@ Definition zipWithFunctional
            (a b c : Type) (f : a -> b -> c) (n : nat) (xs : Vec n a) (ys : Vec n b) :=
   VectorDef.map (fun p => f (fst p) (snd p)) (zipFunctional _ _ _ _ xs ys).
 
+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.
+
 Notation bitvector n := (Vec n bool).
 
 (* NOTE BITS are stored in reverse order than bitvector *)

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

@@ -337,12 +337,13 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("Refl",    mapsToExpl logicModule "eq_refl")
   ]
 
-  -- Nat le
+  -- Nat le/lt
   ++
   [ ("IsLeNat"     , mapsTo sawDefinitionsModule "IsLeNat")
   , ("IsLeNat__rec", mapsTo sawDefinitionsModule "IsLeNat__rec")
   , ("IsLeNat_base", mapsTo sawDefinitionsModule "IsLeNat_base")
   , ("IsLeNat_succ", mapsTo sawDefinitionsModule "IsLeNat_succ")
+  , ("IsLtNat"     , mapsTo sawDefinitionsModule "IsLtNat")
   ]
 
   -- Strings
@@ -370,7 +371,9 @@ 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")
+  , ("atWithProof",   mapsTo vectorsModule "atWithProof")
   , ("at_single",     skip) -- is boring, could be proved on the Coq side
   , ("bvAdd",         mapsTo vectorsModule "bvAdd")
   , ("bvLg2",         mapsTo vectorsModule "bvLg2")
@@ -394,6 +397,8 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("eq_Vec",        skip)
   , ("foldr",         mapsTo vectorsModule "foldr")
   , ("foldl",         mapsTo vectorsModule "foldl")
+  , ("gen_at_BVVec",  mapsTo preludeExtraModule "gen_at_BVVec")
+  , ("genWithProof",  mapsTo vectorsModule "genWithProof")
   , ("scanl",         mapsTo vectorsModule "scanl")
   , ("gen",           mapsTo vectorsModule "gen")
   , ("rotateL",       mapsTo vectorsModule "rotateL")