diff --git a/heapster-saw/examples/mbox_proofs.v b/heapster-saw/examples/mbox_proofs.v index 69f1a11a66..c964cf4bc1 100644 --- a/heapster-saw/examples/mbox_proofs.v +++ b/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. diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v index eeef4d8fc7..e98b772b2e 100644 --- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v +++ b/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). diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v index 86e41a5d22..c9921e60b5 100644 --- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v +++ b/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. diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v index 26f31c1f9f..605a50c663 100644 --- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreScaffolding.v +++ b/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 := diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v index b656f8a52c..7a03a6fb7b 100644 --- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v +++ b/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 *) diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs index 6c22eac36d..717df91833 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs +++ b/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) diff --git a/saw-core/prelude/Prelude.sawcore b/saw-core/prelude/Prelude.sawcore index b2b884dea8..1fac5dbd14 100644 --- a/saw-core/prelude/Prelude.sawcore +++ b/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))