Update saw-core-coq to include changes relating to foldl.

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

@@ -657,7 +657,7 @@ Definition ecParmap : forall (a : Type), forall (b : Type), forall (n : @Num), @
   fun (a : Type) (b : Type) (n : @Num) (pb : RecordTypeCons "eq" (b -> b -> @SAWCoreScaffolding.Bool) RecordTypeNil) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : @Num) => (a -> b) -> @seq n1 a -> @seq n1 b) (fun (n1 : @SAWCoreScaffolding.Nat) (f : a -> b) (xs : @SAWCoreVectorsAsCoqVectors.Vec n1 a) => @SAWCorePrelude.map a b f n1 xs) (fun (f : a -> b) (xs : @SAWCorePrelude.Stream a) => @SAWCoreScaffolding.error (@SAWCorePrelude.Stream b) "Unexpected infinite stream in parmap"%string) n.
 
 Definition ecFoldl : forall (n : @Num), forall (a : Type), forall (b : Type), (a -> b -> a) -> a -> @seq n b -> a :=
-  fun (n : @Num) (a : Type) (b : Type) (f : a -> b -> a) (z : a) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : @Num) => @seq n1 b -> a) (fun (n1 : @SAWCoreScaffolding.Nat) (xs : @SAWCoreVectorsAsCoqVectors.Vec n1 b) => @SAWCoreVectorsAsCoqVectors.foldr b a n1 (fun (y : b) (x : a) => f x y) z (@SAWCorePrelude.reverse n1 b xs)) (fun (xs : @SAWCorePrelude.Stream b) => @SAWCoreScaffolding.error a "Unexpected infinite stream in foldl"%string) n.
+  fun (n : @Num) (a : Type) (b : Type) (f : a -> b -> a) (z : a) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : @Num) => @seq n1 b -> a) (fun (n1 : @SAWCoreScaffolding.Nat) (xs : @SAWCoreVectorsAsCoqVectors.Vec n1 b) => @SAWCoreVectorsAsCoqVectors.foldl b a n1 f z xs) (fun (xs : @SAWCorePrelude.Stream b) => @SAWCoreScaffolding.error a "Unexpected infinite stream in foldl"%string) n.
 
 Definition ecFoldlPrime : forall (n : @Num), forall (a : Type), forall (b : Type), @PEq a -> (a -> b -> a) -> a -> @seq n b -> a :=
   fun (n : @Num) (a : Type) (b : Type) (pa : RecordTypeCons "eq" (a -> a -> @SAWCoreScaffolding.Bool) RecordTypeNil) => @ecFoldl n a b.

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

@@ -507,6 +507,8 @@ Fixpoint zip (a b : sort 0) (m n : Nat) (xs : Vec m a) (ys : Vec n b)
 
 (* Prelude.foldr was skipped *)
 
+(* Prelude.foldl was skipped *)
+
 Definition reverse : forall (n : @SAWCoreScaffolding.Nat), forall (a : Type), @SAWCoreVectorsAsCoqVectors.Vec n a -> @SAWCoreVectorsAsCoqVectors.Vec n a :=
   fun (n : @SAWCoreScaffolding.Nat) (a : Type) (xs : @SAWCoreVectorsAsCoqVectors.Vec n a) => @SAWCoreVectorsAsCoqVectors.gen n a (fun (i : @SAWCoreScaffolding.Nat) => @SAWCorePrelude.sawAt n a xs (@subNat (@subNat n 1) i)).
 

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

@@ -108,6 +108,12 @@ Fixpoint foldr (a b : Type) (n : Nat) (f : a -> b -> b) (base : b) (v : Vec n a)
   | Vector.cons hd _ tl => f hd (foldr _ _ _ f base tl)
   end.
 
+Fixpoint foldl (a b : Type) (n : Nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : b :=
+  match v with
+  | Vector.nil => acc
+  | Vector.cons hd _ tl => foldl _ _ _ f (f acc hd) tl
+  end.
+
 Fixpoint foldl_dep (a : Type) (b : Nat -> Type) (n : Nat)
          (f : forall n, b n -> a -> b (S n)) (base : b O) (v : Vec n a) : b n :=
   match v with

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

@@ -318,6 +318,7 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("coerceVec",     mapsTo vectorsModule "coerceVec")
   , ("eq_Vec",        skip)
   , ("foldr",         mapsTo vectorsModule "foldr")
+  , ("foldl",         mapsTo vectorsModule "foldl")
   , ("gen",           mapsTo vectorsModule "gen")
   , ("rotateL",       mapsTo vectorsModule "rotateL")
   , ("rotateR",       mapsTo vectorsModule "rotateR")