Merge pull request #1511 from GaloisInc/coq-primitives

Make scanl a SAWCore primitive

Author: robdockins

cryptol-saw-core/saw/Cryptol.sawcore

@@ -403,6 +403,16 @@ seqZip a b m n =
        n)
     m;
 
+zipSame : (a b : isort 0) -> (n : Nat) -> Vec n a -> Vec n b -> Vec n (a * b);
+zipSame a b n x y = gen n (a*b) (\ (i : Nat) -> (at n a x i, at n b y i));
+
+seqZipSame : (a b : isort 0) -> (n : Num) -> seq n a -> seq n b -> seq n (a * b);
+seqZipSame a b n =
+  Num#rec
+    (\ (n : Num) -> seq n a -> seq n b -> seq n (a * b))
+    (\ (n : Nat) -> zipSame a b n)
+    (streamMap2 a b (a*b) (\ (x:a) -> \ (y:b) -> (x,y)))
+    n;
 
 --------------------------------------------------------------------------------
 -- Ring and Logic functions
@@ -1560,6 +1570,15 @@ ecFoldlPrime :
   (n : Num) -> (a : sort 0) -> (b : isort 0) -> PEq a -> (a -> b -> a) -> a -> seq n b -> a;
 ecFoldlPrime n a b pa = ecFoldl n a b;
 
+-- scanl : {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a
+ecScanl :
+  (n : Num) -> (a : sort 0) -> (b : sort 0) -> (a -> b -> a) -> a -> seq n b -> seq (tcAdd (TCNum 1) n) a;
+ecScanl n a b f z =
+  Num#rec (\ (n : Num) -> seq n b -> seq (tcAdd (TCNum 1) n) a)
+    (\ (n:Nat) -> \ (xs : Vec n b) -> scanl b a n f z xs)
+    (\ (xs : Stream b) -> streamScanl b a f z xs)
+    n;
+
 --------------------------------------------------------------------------------
 -- Floating point primitives (TODO)
 

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -812,7 +812,7 @@ prelPrims =
   , ("parmap",       flip scGlobalDef "Cryptol.ecParmap")      -- {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b
   , ("foldl",        flip scGlobalDef "Cryptol.ecFoldl")       -- {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
   , ("foldl'",       flip scGlobalDef "Cryptol.ecFoldlPrime")  -- {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
-
+  , ("scanl",        flip scGlobalDef "Cryptol.ecScanl")       -- {n, a, b}  (a -> b -> a) -> a -> [n]b -> [1+n]a
   , ("error",        flip scGlobalDef "Cryptol.ecError")       -- {at,len} (fin len) => [len][8] -> at -- Run-time error
   , ("random",       flip scGlobalDef "Cryptol.ecRandom")      -- {a} => [32] -> a -- Random values
   , ("trace",        flip scGlobalDef "Cryptol.ecTrace")       -- {n,a,b} [n][8] -> a -> b -> b
@@ -1483,10 +1483,14 @@ importComp sc env lenT elemT expr mss =
               m <- importType sc env len
               a <- importType sc env ty
               (ys, n, b, argss, len') <- zipAll branches
-              zs <- scGlobalApply sc "Cryptol.seqZip" [a, b, m, n, xs, ys]
-              mn <- scGlobalApply sc "Cryptol.tcMin" [m, n]
               ab <- scTupleType sc [a, b]
-              return (zs, mn, ab, args : argss, C.tMin len len')
+              if len == len' then
+                do zs <- scGlobalApply sc "Cryptol.seqZipSame" [a, b, m, xs, ys]
+                   return (zs, m, ab, args : argss, len)
+              else
+                do zs <- scGlobalApply sc "Cryptol.seqZip" [a, b, m, n, xs, ys]
+                   mn <- scGlobalApply sc "Cryptol.tcMin" [m, n]
+                   return (zs, mn, ab, args : argss, C.tMin len len')
      (xs, n, a, argss, lenT') <- zipAll mss
      f <- lambdaTuples sc env elemT expr argss
      b <- importType sc env elemT

deps/cryptol

@@ -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 *)
@@ -185,6 +186,12 @@ Definition mlet : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabite
 Definition seqZip : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (m : Num), forall (n : Num), seq m a -> seq n b -> seq (tcMin m n) (prod a b) :=
   fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (b : Type) {Inh_b : SAWCoreScaffolding.Inhabited b} (m : Num) (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (m1 : Num) => seq m1 a -> seq n b -> seq (tcMin m1 n) (prod a b)) (fun (m1 : SAWCoreScaffolding.Nat) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => SAWCoreVectorsAsCoqVectors.Vec m1 a -> seq n1 b -> seq (tcMin (TCNum m1) n1) (prod a b)) (fun (n1 : SAWCoreScaffolding.Nat) => SAWCorePrelude.zip a b m1 n1) (fun (xs : SAWCoreVectorsAsCoqVectors.Vec m1 a) (ys : SAWCorePrelude.Stream b) => SAWCoreVectorsAsCoqVectors.gen m1 (prod a b) (fun (i : SAWCoreScaffolding.Nat) => pair (SAWCorePrelude.sawAt m1 a xs i) (SAWCorePrelude.streamGet b ys i))) n) (CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => SAWCorePrelude.Stream a -> seq n1 b -> seq (tcMin TCInf n1) (prod a b)) (fun (n1 : SAWCoreScaffolding.Nat) (xs : SAWCorePrelude.Stream a) (ys : SAWCoreVectorsAsCoqVectors.Vec n1 b) => SAWCoreVectorsAsCoqVectors.gen n1 (prod a b) (fun (i : SAWCoreScaffolding.Nat) => pair (SAWCorePrelude.streamGet a xs i) (SAWCorePrelude.sawAt n1 b ys i))) (SAWCorePrelude.streamMap2 a b (prod a b) (fun (x : a) (y : b) => pair x y)) n) m.
 
+Definition zipSame : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (n : SAWCoreScaffolding.Nat), SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreVectorsAsCoqVectors.Vec n b -> SAWCoreVectorsAsCoqVectors.Vec n (prod a b) :=
+  fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (b : Type) {Inh_b : SAWCoreScaffolding.Inhabited b} (n : SAWCoreScaffolding.Nat) (x : SAWCoreVectorsAsCoqVectors.Vec n a) (y : SAWCoreVectorsAsCoqVectors.Vec n b) => SAWCoreVectorsAsCoqVectors.gen n (prod a b) (fun (i : SAWCoreScaffolding.Nat) => pair (SAWCorePrelude.sawAt n a x i) (SAWCorePrelude.sawAt n b y i)).
+
+Definition seqZipSame : forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, forall (n : Num), seq n a -> seq n b -> seq n (prod a b) :=
+  fun (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (b : Type) {Inh_b : SAWCoreScaffolding.Inhabited b} (n : Num) => CryptolPrimitivesForSAWCore.Num_rect (fun (n1 : Num) => seq n1 a -> seq n1 b -> seq n1 (prod a b)) (fun (n1 : SAWCoreScaffolding.Nat) => zipSame a b n1) (SAWCorePrelude.streamMap2 a b (prod a b) (fun (x : a) (y : b) => pair x y)) n.
+
 Definition seqBinary : forall (n : Num), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, (a -> a -> a) -> seq n a -> seq n a -> seq n a :=
   fun (num : Num) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (f : a -> a -> a) => CryptolPrimitivesForSAWCore.Num_rect (fun (n : Num) => seq n a -> seq n a -> seq n a) (fun (n : SAWCoreScaffolding.Nat) => SAWCorePrelude.zipWith a a a f n) (SAWCorePrelude.streamMap2 a a a f) num.
 
@@ -677,6 +684,9 @@ Definition ecFoldl : forall (n : Num), forall (a : Type), forall (b : Type), for
 Definition ecFoldlPrime : forall (n : Num), forall (a : Type), forall (b : Type), forall {Inh_b : SAWCoreScaffolding.Inhabited b}, PEq a -> (a -> b -> a) -> a -> seq n b -> a :=
   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) => 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/CryptolPrimitivesForSAWCore.v

@@ -582,6 +582,8 @@ Fixpoint zip (a b : sort 0) (m n : Nat) (xs : Vec m a) (ys : Vec n b)
 
 (* Prelude.foldl was skipped *)
 
+(* Prelude.scanl was skipped *)
+
 Definition reverse : forall (n : SAWCoreScaffolding.Nat), forall (a : Type), forall {Inh_a : SAWCoreScaffolding.Inhabited a}, SAWCoreVectorsAsCoqVectors.Vec n a -> SAWCoreVectorsAsCoqVectors.Vec n a :=
   fun (n : SAWCoreScaffolding.Nat) (a : Type) {Inh_a : SAWCoreScaffolding.Inhabited a} (xs : SAWCoreVectorsAsCoqVectors.Vec n a) => SAWCoreVectorsAsCoqVectors.gen n a (fun (i : SAWCoreScaffolding.Nat) => SAWCorePrelude.sawAt n a xs (subNat (subNat n 1) i)).
 
@@ -828,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 *)
@@ -950,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/generated/CryptolToCoq/SAWCorePrelude.v

@@ -25,19 +25,24 @@ Coercion natToNat : nat >-> Nat.
 Theorem Eq_TCNum a b : a = b -> Eq _ (TCNum a) (TCNum b).
 Proof.
   intros EQ.
-  rewrite EQ.
-  reflexivity.
-Qed.
+  apply f_equal.
+  apply EQ.
+Defined.
 
 Theorem min_nSn n : min n (S n) = n.
 Proof.
   induction n; simpl; auto.
-Qed.
+Defined.
 
 Theorem min_Snn n : min (S n) n = n.
 Proof.
   induction n; simpl; auto.
-Qed.
+Defined.
+
+Theorem min_nn n : min n n = n.
+Proof.
+  induction n; simpl; auto.
+Defined.
 
 Ltac solveUnsafeAssertStep :=
   match goal with
@@ -50,12 +55,21 @@ Ltac solveUnsafeAssertStep :=
   | [ n : Num |- _ ] => destruct n
   | [ |- Eq Num (TCNum _) (TCNum _) ] => apply Eq_TCNum
   | [ |- Eq Num _ _ ] => reflexivity
+  | [ |- min ?n ?n = _ ] => rewrite (min_nn n)
   | [ |- min ?n (S ?n) = _ ] => rewrite (min_nSn n)
   | [ |- min (S ?n) ?n = _ ] => rewrite (min_Snn n)
   end.
 
-Ltac solveUnsafeAssert := repeat (solveUnsafeAssertStep; simpl; try lia); trivial.
+Ltac unfoldLets :=
+  repeat
+  match goal with
+    [ X := _ |- _ ] => progress (cbv delta [X])
+  end.
 
+Ltac solveUnsafeAssert :=
+  try (unfoldLets;
+       repeat (repeat solveUnsafeAssertStep; simpl; try reflexivity; try lia);
+       trivial).
 
 Fixpoint iterNat {a : Type} (n : nat) (f : a -> a) : a -> a :=
   match n with

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

@@ -18,35 +18,57 @@ Theorem Nat_cases2_match_spec a f1 f2 f3 : forall x y,
   Nat_cases2 a f1 f2 f3 x y = Nat_cases2_match a f1 f2 f3 x y.
 Proof.
   induction x; induction y; simpl; congruence.
-Qed.
+Defined.
 
 Theorem minNat_min : forall x y, minNat x y = min x y.
 Proof.
   induction x; induction y; simpl; auto.
-Qed.
+Defined.
 
 Theorem maxNat_max : forall x y, maxNat x y = max x y.
 Proof.
   induction x; induction y; simpl; auto.
-Qed.
+Defined.
 
 Theorem addNat_add : forall x y, addNat x y = x + y.
 Proof.
   induction x; simpl; auto.
-Qed.
+Defined.
 
 Theorem subNat_sub : forall x y, subNat x y = x - y.
 Proof.
   induction x; induction y; simpl; auto.
-Qed.
+Defined.
 
 Theorem mulNat_mul : forall x y, mulNat x y = x * y.
 Proof.
   induction x; simpl; intros; auto.
   rewrite IHx.
   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/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v

@@ -118,6 +118,12 @@ Fixpoint foldl (a b : Type) (n : Nat) (f : b -> a -> b) (acc : b) (v : Vec n a)
   | Vector.cons hd _ tl => foldl _ _ _ f (f acc hd) tl
   end.
 
+Fixpoint scanl (a b : Type) (n : Nat) (f : b -> a -> b) (acc : b) (v : Vec n a) : Vec (S n) b :=
+  match v in VectorDef.t _ n return Vec (S n) b with
+  | Vector.nil => [ acc ]
+  | Vector.cons h n' tl => Vector.cons b acc (S n') (scanl a b n' f (f acc h) 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/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v

@@ -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 $ []
 
@@ -344,6 +347,7 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("eq_Vec",        skip)
   , ("foldr",         mapsTo vectorsModule "foldr")
   , ("foldl",         mapsTo vectorsModule "foldl")
+  , ("scanl",         mapsTo vectorsModule "scanl")
   , ("gen",           mapsTo vectorsModule "gen")
   , ("rotateL",       mapsTo vectorsModule "rotateL")
   , ("rotateR",       mapsTo vectorsModule "rotateR")
@@ -358,6 +362,11 @@ sawCorePreludeSpecialTreatmentMap configuration =
   , ("Vec",           mapsTo vectorsModule "Vec")
   ]
 
+  -- Streams
+  ++
+  [ ("streamScanl",   mapsTo preludeExtraModule "streamScanl")
+  ]
+
   -- Integers
   ++
   [ ("Integer",  mapsTo sawDefinitionsModule "Integer")

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

@@ -959,6 +959,7 @@ primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minN
 
 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;
+primitive scanl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> Vec (addNat 1 n) b;
 
 reverse : (n : Nat) -> (a : isort 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));
@@ -1336,6 +1337,28 @@ streamShiftL a xs i = streamDrop a i xs;
 streamShiftR : (a : sort 0) -> a -> Stream a -> Nat -> Stream a;
 streamShiftR a z xs i = streamAppend a i (replicate i a z) xs;
 
+-- TODO "streamScanl" should probably be a primitive.  However, stream
+-- primitives are complicated to implement because the backends have different
+-- implementations for streams, and there is no uniform place to implement them.
+--
+-- We explicitly use "fix" here to implement sharing in the stream.  A naive
+-- 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)
+    (\ (bs : Stream b) -> MkStream b
+      (natCase (\ (n : Nat) -> b)
+         -- zero case
+         z
+	 -- successor case
+	 (\ (n : Nat) -> f (streamGet b bs n) (streamGet a as n)))
+    );
+
 --------------------------------------------------------------------------------
 -- Integer values
 --   integer values of unbounded precision
@@ -1643,7 +1666,7 @@ genBVVec : (n : Nat) -> (len : Vec n Bool) -> (a : sort 0) ->
            BVVec n len a;
 genBVVec n len a f =
   genWithProof (bvToNat n len) a
-    (\(i:Nat) (pf:IsLtNat i (bvToNat n len)) -> 
+    (\(i:Nat) (pf:IsLtNat i (bvToNat n len)) ->
       f (bvNat n i) (IsLtNat_to_bvult n len i pf));
 
 -- Generate a BVVec from the elements of an existing vector, using a default

saw-core/prelude/Prelude.sawcore

@@ -354,6 +354,7 @@ constMap bp = Map.fromList
   , ("Prelude.zip", vZipOp (bpUnpack bp))
   , ("Prelude.foldr", foldrOp (bpUnpack bp))
   , ("Prelude.foldl", foldlOp (bpUnpack bp))
+  , ("Prelude.scanl", scanlOp (bpUnpack bp))
   , ("Prelude.rotateL", rotateLOp bp)
   , ("Prelude.rotateR", rotateROp bp)
   , ("Prelude.shiftL", shiftLOp bp)
@@ -521,7 +522,7 @@ coerceOp =
 
 -- | Return the number of bits necessary to represent the given value,
 -- which should be a value of type Nat.
-natSize :: BasePrims l -> Value l -> Natural
+natSize :: HasCallStack => BasePrims l -> Value l -> Natural
 natSize _bp val =
   case val of
     VNat n -> widthNat n
@@ -1074,6 +1075,24 @@ foldlOp unpack =
     xv <- toVector unpack xs
     lift (V.foldl g (force z) xv)
 
+-- scanl : (a b : sort 0) -> (n : Nat) -> (b -> a -> b) -> b -> Vec n a -> Vec (addNat n 1) b;
+scanlOp :: forall l. (VMonadLazy l, Show (Extra l)) => Unpack l -> Prim l
+scanlOp unpack =
+  constFun $ -- a
+  constFun $ -- b
+  constFun $ -- n
+  strictFun $ \f ->
+  primFun $ \z ->
+  strictFun $ \xs ->
+  PrimExcept $ do
+    let g :: Vector (Thunk l) ->
+             Thunk l ->
+             EvalM l (Vector (Thunk l))
+        g bs v = do b <- delay (applyAll f [V.last bs, v])
+                    return (V.snoc bs b)
+    xv <- toVector unpack xs
+    lift (VVector <$> V.foldM g (V.singleton z) xv)
+
 -- op :: Integer -> Integer;
 intUnOp :: VMonad l => (VInt l -> MInt l) -> Prim l
 intUnOp f =
@@ -1377,4 +1396,3 @@ arrayRangeEqOp bp =
        j' <- toWord (bpPack bp) j
        l' <- toWord (bpPack bp) l
        VBool <$> (bpArrayRangeEq bp) f' i' g' j' l'
-