Implement streamScanl in Coq, and set up the translation to use

it instead of the SAWCore implementation.

Author: robdockins

saw-core-coq/coq/generated/CryptolToCoq/CryptolPrimitivesForSAWCore.v

@@ -10,6 +10,7 @@ Import ListNotations.
 (** Post-preamble section specified by you *)
 From CryptolToCoq Require Import SAWCorePrelude.
 Import SAWCorePrelude.
+From CryptolToCoq Require Import SAWCorePreludeExtra.
 
 
 (** Code generated by saw-core-coq *)
@@ -684,7 +685,7 @@ Definition ecFoldlPrime : forall (n : Num), forall (a : Type), forall (b : Type)
   fun (n : Num) (a : Type) (b : Type) {Inh_b : SAWCoreScaffolding.Inhabited b} (pa : RecordTypeCons "eq" (a -> a -> SAWCoreScaffolding.Bool) RecordTypeNil) => ecFoldl n a b.
 
 Definition ecScanl : forall (n : Num), forall (a : Type), forall (b : Type), (a -> b -> a) -> a -> seq n b -> seq (tcAdd (TCNum 1) n) a :=
-  fun (n : Num) (a : Type) (b : Type) (f : a -> b -> a) (z : a) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => seq n1 b -> seq (tcAdd (TCNum 1) n1) a) (fun (n1 : SAWCoreScaffolding.Nat) (xs : SAWCoreVectorsAsCoqVectors.Vec n1 b) => SAWCoreVectorsAsCoqVectors.scanl b a n1 f z xs) (fun (xs : SAWCorePrelude.Stream b) => SAWCorePrelude.MkStream a (SAWCorePrelude.Nat__rec (fun (i : SAWCoreScaffolding.Nat) => a) z (fun (i : SAWCoreScaffolding.Nat) (x : a) => f x (SAWCorePrelude.streamGet b xs i)))) n.
+  fun (n : Num) (a : Type) (b : Type) (f : a -> b -> a) (z : a) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => seq n1 b -> seq (tcAdd (TCNum 1) n1) a) (fun (n1 : SAWCoreScaffolding.Nat) (xs : SAWCoreVectorsAsCoqVectors.Vec n1 b) => SAWCoreVectorsAsCoqVectors.scanl b a n1 f z xs) (fun (xs : SAWCorePrelude.Stream b) => SAWCorePreludeExtra.streamScanl b a f z xs) n.
 
 Definition TCFloat : Num -> Num -> Type :=
   fun (_1 : Num) (_2 : Num) => unit : Type.

saw-core-coq/coq/generated/CryptolToCoq/SAWCorePrelude.v

@@ -830,6 +830,8 @@ Definition streamShiftL : forall (a : Type), Stream a -> SAWCoreScaffolding.Nat
 Definition streamShiftR : forall (a : Type), a -> Stream a -> SAWCoreScaffolding.Nat -> Stream a :=
   fun (a : Type) (z : a) (xs : Stream a) (i : SAWCoreScaffolding.Nat) => streamAppend a i (replicate i a z) xs.
 
+(* Prelude.streamScanl was skipped *)
+
 (* Prelude.Integer was skipped *)
 
 (* Prelude.intAdd was skipped *)
@@ -952,6 +954,10 @@ Definition foldW64List : unfoldedW64List -> W64List :=
   either (unit : Type) (prod (@sigT (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (_1 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => unit : Type)) (prod W64List (unit : Type))) W64List (fun (_1 : unit : Type) => W64Nil) (fun (bv_l : prod (@sigT (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (_1 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => unit : Type)) (prod W64List (unit : Type))) => let var__0   := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in
   W64Cons (@projT1 var__0 (fun (_1 : var__0) => unit : Type) (SAWCoreScaffolding.fst bv_l)) (SAWCoreScaffolding.fst (SAWCoreScaffolding.snd bv_l))).
 
+(* Prelude.unsafeAssertBVULt was skipped *)
+
+(* Prelude.unsafeAssertBVULe was skipped *)
+
 Axiom bvEqWithProof : forall (n : SAWCoreScaffolding.Nat), forall (v1 : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool), forall (v2 : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool), Maybe (SAWCoreScaffolding.Eq (SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool) v1 v2) .
 
 Definition bvultWithProof : forall (n : SAWCoreScaffolding.Nat), forall (v1 : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool), forall (v2 : SAWCoreVectorsAsCoqVectors.Vec n SAWCoreScaffolding.Bool), Maybe (SAWCoreScaffolding.Eq SAWCoreScaffolding.Bool (SAWCoreVectorsAsCoqVectors.bvult n v1 v2) SAWCoreScaffolding.true) :=

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

@@ -47,6 +47,28 @@ Proof.
   apply addNat_add.
 Defined.
 
+Definition streamScanl (a b : sort 0) (f : b -> a -> b) (z:b) (xs:Stream a) : Stream b :=
+  MkStream b
+    (fix strm (n:nat) : b :=
+       match n with
+       | O => z
+       | S n' => f (strm n') (streamGet a xs n')
+       end).
+
+Lemma streamScanl_zero a b f z xs : streamGet b (streamScanl a b f z xs) 0 = z.
+Proof.
+  reflexivity.
+Qed.
+
+Lemma streamScanl_succ a b f z xs : forall n,
+  streamGet b (streamScanl a b f z xs) (S n) =
+  f (streamGet b (streamScanl a b f z xs) n)
+    (streamGet a xs n).
+Proof.
+  intro n. reflexivity.
+Qed.
+
+
 Theorem fold_unfold_IRT As Ds D : forall x, foldIRT As Ds D (unfoldIRT As Ds D x) = x.
 Proof.
   induction x; simpl; unfold uncurry; f_equal; try easy.

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

@@ -179,6 +179,9 @@ cryptolPrimitivesModule = mkModuleName ["CryptolPrimitivesForSAWCore"]
 sawCoreScaffoldingModule :: ModuleName
 sawCoreScaffoldingModule = mkModuleName ["SAWCoreScaffolding"]
 
+preludeExtraModule :: ModuleName
+preludeExtraModule = mkModuleName ["SAWCorePreludeExtra"]
+
 cryptolPreludeSpecialTreatmentMap :: Map.Map String IdentSpecialTreatment
 cryptolPreludeSpecialTreatmentMap = Map.fromList $ []
 
@@ -359,6 +362,11 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("Vec",           mapsTo vectorsModule "Vec")
   ]
 
+  -- Streams
+  ++
+  [ ("streamScanl",   mapsTo preludeExtraModule "streamScanl")
+  ]
+
   -- Integers
   ++
   [ ("Integer",  mapsTo sawDefinitionsModule "Integer")

saw-core/prelude/Prelude.sawcore

@@ -1345,6 +1345,9 @@ streamShiftR a z xs i = streamAppend a i (replicate i a z) xs;
 -- implementation that just iterates "f" separate for each index would waste work.
 -- The fixpoint is well founded because each element only refers to elements with
 -- smaller indices.
+--
+-- For Coq support, this definition is replaced with a naive implementation
+-- that performs independent iterations for each location.
 streamScanl : (a b : sort 0) -> (b -> a -> b) -> b -> Stream a -> Stream b;
 streamScanl a b f z as =
   fix (Stream b)

src/SAWScript/Prover/Exporter.hs

@@ -410,6 +410,14 @@ withImportSAWCorePrelude config@(Coq.TranslationConfiguration { Coq.postPreamble
    ]
   }
 
+withImportSAWCorePreludeExtra :: Coq.TranslationConfiguration  -> Coq.TranslationConfiguration
+withImportSAWCorePreludeExtra config@(Coq.TranslationConfiguration { Coq.postPreamble }) =
+  config { Coq.postPreamble = postPreamble ++ unlines
+   [ "From CryptolToCoq Require Import SAWCorePreludeExtra."
+   ]
+  }
+
+
 withImportCryptolPrimitivesForSAWCore ::
   Coq.TranslationConfiguration  -> Coq.TranslationConfiguration
 withImportCryptolPrimitivesForSAWCore config@(Coq.TranslationConfiguration { Coq.postPreamble }) =
@@ -478,6 +486,7 @@ writeCoqCryptolModule inputFile outputFile notations skips = io $ do
   let configuration =
         withImportCryptolPrimitivesForSAWCoreExtra $
         withImportCryptolPrimitivesForSAWCore $
+        withImportSAWCorePreludeExtra $
         withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
   let nm = takeBaseName inputFile
@@ -518,6 +527,7 @@ writeCoqCryptolPrimitivesForSAWCore outputFile notations skips = do
   () <- scLoadModule sc (emptyModule (mkModuleName ["CryptolPrimitivesForSAWCore"]))
   m  <- scFindModule sc nameOfCryptolPrimitivesForSAWCoreModule
   let configuration =
+        withImportSAWCorePreludeExtra $
         withImportSAWCorePrelude $
         coqTranslationConfiguration notations skips
   let doc = Coq.translateSAWModule configuration m