Merge pull request #1786 from GaloisInc/atGenWithProof

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

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.
@@ -28,16 +29,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 +195,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 +289,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 +442,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 +501,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 +1132,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/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

@@ -211,9 +211,6 @@ sawVectorDefinitionsModule (TranslationConfiguration {..}) =
 cryptolPrimitivesModule :: ModuleName
 cryptolPrimitivesModule = mkModuleName ["CryptolPrimitivesForSAWCore"]
 
-sawCoreScaffoldingModule :: ModuleName
-sawCoreScaffoldingModule = mkModuleName ["SAWCoreScaffolding"]
-
 preludeExtraModule :: ModuleName
 preludeExtraModule = mkModuleName ["SAWCorePreludeExtra"]
 
@@ -246,7 +243,7 @@ sawCorePreludeSpecialTreatmentMap configuration =
   Map.fromList $
 
   -- sawLet
-  [ ("sawLet", mapsTo sawCoreScaffoldingModule "sawLet_def") ]
+  [ ("sawLet", mapsTo sawDefinitionsModule "sawLet_def") ]
 
   -- Unsafe SAW features
   ++
@@ -337,12 +334,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
@@ -362,15 +360,17 @@ sawCorePreludeSpecialTreatmentMap configuration =
   [ ("divModNat", mapsTo sawDefinitionsModule "divModNat")
   , ("Nat",       mapsTo datatypesModule "nat")
   , ("widthNat",  mapsTo sawDefinitionsModule "widthNat")
-  , ("Zero",      mapsTo sawCoreScaffoldingModule   "Zero")
-  , ("Succ",      mapsTo sawCoreScaffoldingModule   "Succ")
+  , ("Zero",      mapsTo sawDefinitionsModule "Zero")
+  , ("Succ",      mapsTo sawDefinitionsModule "Succ")
   ]
 
   -- Vectors
   ++
   [ ("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 +394,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")
@@ -472,7 +474,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,8 +1218,8 @@ 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;
+axiom bvNat_bvToNat : (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;
@@ -1946,7 +1946,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
@@ -3153,12 +3153,6 @@ axiom bveq_same2 : (n : Nat)
                  (bvEq n (bvAdd n x y) (bvAdd n x z))
                  (bvEq n y z);
 
-axiom bvNat_bvToNat : (n : Nat)
-              -> (x : Vec n Bool)
-              -> Eq (Vec n Bool)
-                    (bvNat n (bvToNat n x))
-                    x;
-
 axiom ite_split_cong : (b : Bool) -> (x : Vec 384 Bool) -> (y : Vec 384 Bool)
                -> Eq (Vec 12 (Vec 32 Bool))
                      (split 12 32 Bool (ite (Vec 384 Bool) b x y))