diff --git a/cryptol-saw-core/saw/Cryptol.sawcore b/cryptol-saw-core/saw/Cryptol.sawcore
index a45e322a6e..8b5401f6f8 100644
--- a/cryptol-saw-core/saw/Cryptol.sawcore
+++ b/cryptol-saw-core/saw/Cryptol.sawcore
@@ -128,7 +128,6 @@ tcDiv =
                (\ (y:Nat) -> TCInf)
                -- infinity / infinity = 1
                (TCNum 1);
-
 tcMod : Num -> Num -> Num;
 tcMod =
   binaryNumFun (\ (x:Nat) -> \ (y:Nat) -> modNat x y)
@@ -170,7 +169,7 @@ tcCeilDiv =
 
 tcCeilMod : Num -> Num -> Num;
 tcCeilMod =
-  binaryNumFun ceilModNat (\ (x:Nat) -> TCNum 0) (\ (y:Nat) -> TCInf) TCInf;
+  binaryNumFun ceilModNat (\ (x:Nat) -> TCNum 0) (\ (y:Nat) -> TCNum 0) TCInf;
 
 tcLenFromThenTo_Nat : Nat -> Nat -> Nat -> Nat;
 tcLenFromThenTo_Nat x y z =
@@ -848,9 +847,9 @@ PIntegral a =
    , toInt : a -> Integer
    , posNegCases :
         (r : sort 0) ->
-	(Nat -> r) ->
-	(Nat -> r) ->
-	a -> r
+        (Nat -> r) ->
+        (Nat -> r) ->
+        a -> r
    };
 
 PIntegralInteger : PIntegral Integer;
@@ -879,7 +878,7 @@ PIntegralSeqBool n =
   Num#rec (\ (n:Num) -> PIntegral (seq n Bool))
           (\ (n:Nat) -> PIntegralWord n)
           (error (PIntegral (Stream Bool)) "PIntegralSeqBool: no instance for streams")
-	  n;
+          n;
 
 
 -- Field class
@@ -928,12 +927,12 @@ PRound a =
 
 PRoundRational : PRound Rational;
 PRoundRational =
-  { roundField	= PFieldRational
-  , roundCmp	= PCmpRational
-  , floor	= \(x : Rational) -> error Integer "Unimplemented: floor Rational"
-  , ceiling	= \(x : Rational) -> error Integer "Unimplemented: ceiling Rational"
-  , trunc	= \(x : Rational) -> error Integer "Unimplemented: trunc Rational"
-  , roundAway	= \(x : Rational) -> error Integer "Unimplemented: roundAway Rational"
+  { roundField  = PFieldRational
+  , roundCmp    = PCmpRational
+  , floor       = \(x : Rational) -> error Integer "Unimplemented: floor Rational"
+  , ceiling     = \(x : Rational) -> error Integer "Unimplemented: ceiling Rational"
+  , trunc       = \(x : Rational) -> error Integer "Unimplemented: trunc Rational"
+  , roundAway   = \(x : Rational) -> error Integer "Unimplemented: roundAway Rational"
   , roundToEven = \(x : Rational) -> error Integer "Unimplemented: roundToEven Rational"
   };
 
@@ -986,8 +985,8 @@ ecFromZ : (n : Num) -> IntModNum n -> Integer;
 ecFromZ n =
   Num#rec (\ (n : Num) -> IntModNum n -> Integer)
           fromIntMod
-	  (\ (x : Integer) -> x)
-	  n;
+          (\ (x : Integer) -> x)
+          n;
 
 -- Ring
 ecFromInteger : (a : sort 0) -> PRing a -> Integer -> a;
@@ -1131,15 +1130,15 @@ ecShiftL m =
     -- Case for (TCNum m)
     (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec m a) ->
         pix.posNegCases (Vec m a)
-	  (shiftL m a (ecZero a pz) xs)
-	  (shiftR m a (ecZero a pz) xs))
+          (shiftL m a (ecZero a pz) xs)
+          (shiftR m a (ecZero a pz) xs))
 
     -- Case for (infinity)
     (\ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) ->
        \ (xs:Stream a) ->
         pix.posNegCases (Stream a)
-	  (streamShiftL a xs)
-	  (streamShiftR a pz xs))
+          (streamShiftL a xs)
+          (streamShiftR a pz xs))
     m;
 
 ecShiftR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a ->
@@ -1151,14 +1150,14 @@ ecShiftR m =
     -- Case for (TCNum m)
     (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Vec m a) ->
         pix.posNegCases (Vec m a)
-	  (shiftR m a (ecZero a pz) xs)
-	  (shiftL m a (ecZero a pz) xs))
+          (shiftR m a (ecZero a pz) xs)
+          (shiftL m a (ecZero a pz) xs))
 
     -- Case for (infinity)
     (\ (ix:sort 0) -> \ (a:sort 0) -> \ (pix : PIntegral ix) -> \ (pz:PZero a) -> \ (xs:Stream a) ->
         pix.posNegCases (Stream a)
-	  (streamShiftR a pz xs)
-	  (streamShiftL a xs))
+          (streamShiftR a pz xs)
+          (streamShiftL a xs))
     m;
 
 ecSShiftR : (n : Num) -> (ix : sort 0) -> PIntegral ix -> seq n Bool -> ix -> seq n Bool;
@@ -1172,8 +1171,8 @@ ecSShiftR =
               (\ (xs : Vec 0 Bool) -> \ (_ : ix) -> xs)
               (\ (w : Nat) -> \ (xs : Vec (Succ w) Bool) ->
                    pix.posNegCases (Vec (Succ w) Bool)
-		     (bvSShr w xs)
-		     (bvShl (Succ w) xs))
+                     (bvSShr w xs)
+                     (bvShl (Succ w) xs))
               n));
 
 ecRotL : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a;
@@ -1183,7 +1182,7 @@ ecRotL =
     (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) ->
       pix.posNegCases (Vec m a)
         (rotateL m a xs)
-	(rotateR m a xs));
+        (rotateR m a xs));
 
 ecRotR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> seq m a -> ix -> seq m a;
 ecRotR =
@@ -1192,7 +1191,7 @@ ecRotR =
     (\ (m:Nat) -> \ (ix:sort 0) -> \ (a:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec m a) ->
       pix.posNegCases (Vec m a)
         (rotateR m a xs)
-	(rotateL m a xs));
+        (rotateL m a xs));
 
 ecCat : (m n : Num) -> (a : sort 0) -> seq m a -> seq n a -> seq (tcAdd m n) a;
 ecCat =
@@ -1224,9 +1223,9 @@ ecTake =
     (Num_rec
       (\ (n:Num) -> (a:sort 0) -> seq (tcAdd TCInf n) a -> Stream a)
         -- The case (TCInf, TCNum n)
-	(\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
-	-- The case (TCInf, TCInf)
-	(\ (a:sort 0) -> \ (xs:Stream a) -> xs));
+        (\ (n:Nat) -> \ (a:sort 0) -> \ (xs:Stream a) -> xs)
+        -- The case (TCInf, TCInf)
+        (\ (a:sort 0) -> \ (xs:Stream a) -> xs));
 
 ecDrop : (m n : Num) -> (a : sort 0) -> seq (tcAdd m n) a -> seq n a;
 ecDrop =
@@ -1336,30 +1335,30 @@ ecAt n =
     (\ (n:Num) -> (a ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a)
     (\ (n:Nat) -> \ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
           pix.posNegCases a
-	    (at n a xs)
-	    (\ (_:Nat) -> at n a xs 0))
-	    -- (error (Nat -> a) "ecAt : negative index"))
+            (at n a xs)
+            (\ (_:Nat) -> at n a xs 0))
+            -- (error (Nat -> a) "ecAt : negative index"))
     (\ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Stream a) ->
           pix.posNegCases a
-	    (streamGet a xs)
-	    (\ (_:Nat) -> streamGet a xs 0))
---	    (error (Nat -> a) "ecAt : negative index"))
+            (streamGet a xs)
+            (\ (_:Nat) -> streamGet a xs 0))
+--          (error (Nat -> a) "ecAt : negative index"))
     n;
 
 ecAtBack : (n : Num) -> (a ix : sort 0) -> PIntegral ix -> seq n a -> ix -> a;
 ecAtBack n a ix pix xs = ecAt n a ix pix (ecReverse n a xs);
 
-ecFromTo : (first last : Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
+ecFromTo : (first last : Num) -> (a : sort 0) -> PLiteral a ->
             seq (tcAdd (TCNum 1) (tcSub last first)) a;
 ecFromTo =
   finNumRec
-    (\ (first:Num) -> (last:Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
+    (\ (first:Num) -> (last:Num) -> (a : sort 0) -> PLiteral a ->
        seq (tcAdd (TCNum 1) (tcSub last first)) a)
     (\ (first:Nat) ->
        finNumRec
-         (\ (last:Num) -> (a : sort 0) -> PLiteral a -> PLiteral a ->
+         (\ (last:Num) -> (a : sort 0) -> PLiteral a ->
             seq (tcAdd (TCNum 1) (tcSub last (TCNum first))) a)
-         (\ (last:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) -> \ (_ : PLiteral a) ->
+         (\ (last:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
             gen (addNat 1 (subNat last first)) a
                 (\ (i : Nat) -> pa (addNat i first))));
 
@@ -1394,6 +1393,91 @@ ecFromThenTo first next _ a =
                                  (mulNat i (getFinNat next)))
                          (mulNat i (getFinNat first)))));
 
+ecFromToBy :
+  (first last stride : Num) -> (a : sort 0) -> PLiteral a ->
+  seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a;
+ecFromToBy =
+  finNumRec
+    (\ (first:Num) -> (last:Num) -> (stride : Num) -> (a : sort 0) -> PLiteral a ->
+       seq (tcAdd (TCNum 1) (tcDiv (tcSub last first) stride)) a)
+    (\ (first:Nat) ->
+       finNumRec
+         (\ (last:Num) -> (stride : Num) -> (a : sort 0) -> PLiteral a ->
+            seq (tcAdd (TCNum 1) (tcDiv (tcSub last (TCNum first)) stride)) a)
+         (\ (last:Nat) ->
+           finNumRec
+             (\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
+                seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat last first)) stride)) a)
+             (\ (stride:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
+               gen (addNat 1 (divNat (subNat last first) stride)) a
+                   (\ (i : Nat) -> pa (addNat first (mulNat i stride))))));
+
+ecFromToByLessThan :
+  (first bound stride : Num) -> (a : sort 0) -> PLiteralLessThan a ->
+  seq (tcCeilDiv (tcSub bound first) stride) a;
+ecFromToByLessThan =
+  finNumRec
+    (\ (first:Num) -> (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
+       seq (tcCeilDiv (tcSub bound first) stride) a)
+    (\ (first:Nat) ->
+      Num_rec
+        (\ (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
+           seq (tcCeilDiv (tcSub bound (TCNum first)) stride) a)
+
+        -- bound is finite case
+        (\ (bound:Nat) ->
+          finNumRec
+            (\ (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
+               seq (tcCeilDiv (TCNum (subNat bound first)) stride) a)
+            (\ (stride:Nat) -> \ (a:sort 0) -> \ (pa:PLiteralLessThan a) ->
+              gen (ceilDivNat (subNat bound first) stride) a
+                  (\ (i:Nat) -> pa (addNat first (mulNat i stride)))))
+
+        -- bound is infinite case
+        (finNumRec
+            (\ (stride:Num) -> (a : sort 0) -> PLiteralLessThan a ->
+               seq (tcCeilDiv TCInf stride) a)
+            (\ (stride:Nat) -> \ (a : sort 0) -> \ (pa:PLiteralLessThan a) ->
+               MkStream a (\ (i:Nat) -> pa (addNat first (mulNat i stride))))));
+
+ecFromToDownBy :
+  (first last stride : Num) -> (a : sort 0) -> PLiteral a ->
+  seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a;
+ecFromToDownBy =
+  finNumRec
+    (\ (first:Num) -> (last:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
+       seq (tcAdd (TCNum 1) (tcDiv (tcSub first last) stride)) a)
+    (\ (first:Nat) ->
+    finNumRec
+      (\ (last:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
+         seq (tcAdd (TCNum 1) (tcDiv (tcSub (TCNum first) last) stride)) a)
+      (\ (last:Nat) ->
+      finNumRec
+        (\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
+           seq (tcAdd (TCNum 1) (tcDiv (TCNum (subNat first last)) stride)) a)
+        (\ (stride:Nat) -> \ (a : sort 0) -> \ (pa : PLiteral a) ->
+           gen (addNat 1 (divNat (subNat first last) stride)) a
+               (\ (i:Nat) -> pa (subNat first (mulNat i stride))))));
+
+ecFromToDownByGreaterThan :
+  (first bound stride : Num) -> (a : sort 0) -> PLiteral a ->
+  seq (tcCeilDiv (tcSub first bound) stride) a;
+ecFromToDownByGreaterThan =
+  finNumRec
+    (\ (first:Num) -> (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
+       seq (tcCeilDiv (tcSub first bound) stride) a)
+    (\ (first:Nat) ->
+      finNumRec
+        (\ (bound:Num) -> (stride:Num) -> (a : sort 0) -> PLiteral a ->
+           seq (tcCeilDiv (tcSub (TCNum first) bound) stride) a)
+        (\ (bound:Nat) ->
+          finNumRec
+            (\ (stride:Num) -> (a : sort 0) -> PLiteral a ->
+               seq (tcCeilDiv (TCNum (subNat first bound)) stride) a)
+            (\ (stride:Nat) -> \ (a : sort 0) -> \ (pa:PLiteral a) ->
+               gen (ceilDivNat (subNat first bound) stride) a
+                   (\ (i:Nat) -> pa (subNat first (mulNat i stride))))));
+
 -- Infinite word sequences
 ecInfFrom : (a : sort 0) -> PIntegral a -> a -> seq TCInf a;
 ecInfFrom a pa x =
@@ -1582,13 +1666,13 @@ ecUpdate n =
        -- Case for (TCNum n, TCNum w)
        pix.posNegCases (a -> Vec n a)
          (upd n a xs)
-	 (\ (_:Nat) -> \ (_:a) -> xs))
-	 -- (error (Nat -> a -> Vec n a) "ecUpdate: negative index"))
+         (\ (_:Nat) -> \ (_:a) -> xs))
+         -- (error (Nat -> a -> Vec n a) "ecUpdate: negative index"))
     (\ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs : Stream a) ->
        pix.posNegCases (a -> Stream a)
          (streamUpd a xs)
-	 (\ (_:Nat) -> \ (_:a) -> xs))
-	 --(error (Nat -> a -> Stream a) "ecUpdate: negative index"))
+         (\ (_:Nat) -> \ (_:a) -> xs))
+         --(error (Nat -> a -> Stream a) "ecUpdate: negative index"))
     n;
 
 
@@ -1599,8 +1683,8 @@ ecUpdateEnd =
     (\ (n:Nat) -> \ (a:sort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
        pix.posNegCases (a -> Vec n a)
          (\ (i:Nat) -> upd n a xs (subNat (subNat n 1) i))
-	 (\ (_:Nat) -> \ (_:a) -> xs));
-	 -- (error (Nat -> a -> Vec n a) "ecUpdateEnd: negative index"));
+         (\ (_:Nat) -> \ (_:a) -> xs));
+         -- (error (Nat -> a -> Vec n a) "ecUpdateEnd: negative index"));
 
 
 -- Bitvector truncation
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index 1ec6b89645..ce937a24c2 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -759,21 +759,37 @@ prelPrims =
 
     -- -- Enumerations
   , ("fromTo",         flip scGlobalDef "Cryptol.ecFromTo")
-    --                            -- fromTo : {first, last, bits, a}
-    --                            --           ( fin last, fin bits, last >== first,
-    --                            --             Literal first a, Literal last a)
-    --                            --        => [1 + (last - first)]a
+                                  -- fromTo : {first, last, bits, a}
+                                  --           ( fin last, fin bits, last >== first,
+                                  --             Literal first a, Literal last a)
+                                  --        => [1 + (last - first)]a
   , ("fromToLessThan", flip scGlobalDef "Cryptol.ecFromToLessThan")
-    --                            -- fromToLessThan : {first, bound, a}
-    --                            --                   ( fin first, bound >= first,
-    --                            --                     LiteralLessThan bound a)
-    --                            --                => [bound - first]a
+                                  -- fromToLessThan : {first, bound, a}
+                                  --                   ( fin first, bound >= first,
+                                  --                     LiteralLessThan bound a)
+                                  --                => [bound - first]a
   , ("fromThenTo",     flip scGlobalDef "Cryptol.ecFromThenTo")
-    --                            -- fromThenTo : {first, next, last, a, len}
-    --                            --              ( fin first, fin next, fin last
-    --                            --              , Literal first a, Literal next a, Literal last a
-    --                            --              , first != next
-    --                            --              , lengthFromThenTo first next last == len) => [len]a
+                                  -- fromThenTo : {first, next, last, a, len}
+                                  --              ( fin first, fin next, fin last
+                                  --              , Literal first a, Literal next a, Literal last a
+                                  --              , first != next
+                                  --              , lengthFromThenTo first next last == len) => [len]a
+  , ("fromToBy",       flip scGlobalDef "Cryptol.ecFromToBy")
+                                  -- fromToBy : {first, last, stride, a}
+                                  --   (fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
+                                  --   [1 + (last - first)/stride]a
+  , ("fromToByLessThan", flip scGlobalDef "Cryptol.ecFromToByLessThan")
+                                  -- fromToByLessThan : {first, bound, stride, a}
+                                  --   (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
+                                  --   [(bound - first)/^stride]a
+  , ("fromToDownBy", flip scGlobalDef "Cryptol.ecFromToDownBy")
+                                  -- fromToDownBy : {first, last, stride, a}
+                                  --   (fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
+                                  --   [1 + (first - last)/stride]a
+  , ("fromToDownByGreaterThan", flip scGlobalDef "Cryptol.ecFromToDownByGreaterThan")
+                                  -- fromToDownByGreaterThan : {first, bound, stride, a}
+                                  --   (fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
+                                  --   [(first - bound)/^stride]a
 
     -- Evaluation primitives: deepseq, parmap
   , ("deepseq",      flip scGlobalDef "Cryptol.ecDeepseq")     -- {a, b} (Eq b) => a -> b -> b
diff --git a/deps/cryptol b/deps/cryptol
index 36475d1fd9..914f7fbe18 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 36475d1fd99eca94bb829b859cf2a9e7cfa3668f
+Subproject commit 914f7fbe18d79d77d59037725e5b8a7194d78697
diff --git a/deps/what4 b/deps/what4
index 200428c28e..ce5c0aa937 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit 200428c28ec776aa8739388a70964e9aff3b42a3
+Subproject commit ce5c0aa937286932f792fe33ad7692495cdd54a6