Make foldl on vectors its own primitive instead of encoding it as

a reversed `foldr`.

cryptol-saw-core/saw/Cryptol.sawcore

@@ -1533,7 +1533,7 @@ ecParmap a b n pb =
 ecFoldl : (n : Num) -> (a : sort 0) -> (b : sort 0) -> (a -> b -> a) -> a -> seq n b -> a;
 ecFoldl n a b f z =
   Num#rec (\ (n : Num) -> seq n b -> a)
-    (\ (n : Nat) -> \ (xs : Vec n b) -> foldr b a n (\ (y : b) -> \ (x : a) -> f x y) z (reverse n b xs))
+    (\ (n : Nat) -> \ (xs : Vec n b) -> foldl b a n f z xs)
     (\ (xs : Stream b) -> error a "Unexpected infinite stream in foldl" )
     n;
 

saw-core/prelude/Prelude.sawcore

@@ -951,6 +951,7 @@ axiom at_single : (a : sort 0) -> (x : a) -> (i : Nat) -> Eq a (at 1 a (single a
 primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);
 
 primitive foldr : (a b : sort 0) -> (n : Nat) -> (a -> b -> b) -> b -> Vec n a -> b;
+primitive foldl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> b;
 
 reverse : (n : Nat) -> (a : sort 0) -> Vec n a -> Vec n a;
 reverse n a xs = gen n a (\ (i : Nat) -> at n a xs (subNat (subNat n 1) i));

saw-core/src/Verifier/SAW/Simulator/Prims.hs

@@ -349,6 +349,7 @@ constMap bp = Map.fromList
   , ("Prelude.split", splitOp bp)
   , ("Prelude.zip", vZipOp (bpUnpack bp))
   , ("Prelude.foldr", foldrOp (bpUnpack bp))
+  , ("Prelude.foldl", foldlOp (bpUnpack bp))
   , ("Prelude.rotateL", rotateLOp bp)
   , ("Prelude.rotateR", rotateROp bp)
   , ("Prelude.shiftL", shiftLOp bp)
@@ -1051,6 +1052,21 @@ foldrOp unpack =
     xv <- toVector unpack xs
     lift (V.foldr g (force z) xv)
 
+-- foldl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> b;
+foldlOp :: (VMonadLazy l, Show (Extra l)) => Unpack l -> Prim l
+foldlOp unpack =
+  constFun $
+  constFun $
+  constFun $
+  strictFun $ \f ->
+  primFun $ \z ->
+  strictFun $ \xs ->
+  PrimExcept $ do
+    let g m x = do f1 <- apply f =<< delay m
+                   apply f1 x
+    xv <- toVector unpack xs
+    lift (V.foldl g (force z) xv)
+
 -- op :: Integer -> Integer;
 intUnOp :: VMonad l => (VInt l -> MInt l) -> Prim l
 intUnOp f =