Merge pull request #1227 from GaloisInc/explicit-stride

Explicit stride

cry

@@ -23,6 +23,7 @@ Available commands:
   rpc-test                     Run RPC server tests
   rpc-docs                     Check that the RPC documentation is up-to-date
   exe-path                     Print the location of the local executable
+  check-docs                   Check the exercises embedded in the documentation
 EOM
 }
 
@@ -97,6 +98,10 @@ case $COMMAND in
     $DIR/cryptol-remote-api/check_docs.sh
     ;;
 
+  check-docs)
+    cabal v2-build exe:check-exercises
+    find ./docs/ProgrammingCryptol -name '*.tex' -print0 | xargs -0 -n1 cabal v2-exec check-exercises
+    ;;
 
   help) show_usage && exit 0 ;;
 

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -790,7 +790,7 @@ \subsection{Appending and indexing}
   []
   invalid sequence index: 12
    -- Backtrace --
-  (Cryptol::@) called at Cryptol:820:14--820:20
+  (Cryptol::@) called at Cryptol:870:14--870:20
   (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9
@@ -1795,7 +1795,7 @@ \section{Characters and strings}
   command to see the type Cryptol infers for this expression explicitly:
 \begin{replPrompt}
     Cryptol> :t [1:[_] .. 10]
-    [1 .. 10 : [_]] : {n} (n >= 4, n >= 1, fin n) => [10][n]
+    [1 .. 10 : [_]] : {n} (n >= 4, fin n) => [10][n]
 \end{replPrompt}
 Cryptol tells us that the sequence has precisely $10$ elements, and each
 element is at least $4$ bits wide.

lib/Cryptol.cry

@@ -32,7 +32,7 @@ primitive type Integer : *
 /**
  * 'Z n' is the type of integers, modulo 'n'.
  *
- * The values of 'Z n' may be thought of as equivalance
+ * The values of 'Z n' may be thought of as equivalence
  * classes of integers according to the equivalence
  * 'x ~ y' iff 'n' divides 'x - y'.  'Z n' naturally
  * forms a ring, but does not support integral division
@@ -41,9 +41,9 @@ primitive type Integer : *
  * However, you may use the 'fromZ' operation
  * to project values in 'Z n' into the integers if such operations
  * are required.  This will compute the reduced representative
- * of the equivalance class. In other words, 'fromZ' computes
+ * of the equivalence class. In other words, 'fromZ' computes
  * the (unique) integer value 'i'  where '0 <= i < n' and
- * 'i' is in the given equivalance class.
+ * 'i' is in the given equivalence class.
  *
  * If the modulus 'n' is prime, 'Z n' also
  * supports computing inverses and forms a field.
@@ -131,13 +131,13 @@ primitive type max : # -> # -> #
 /** Divide numeric types, rounding up. */
 primitive type
   { m : #, n : # }
-  (fin m, fin n, n >= 1) =>
+  (fin n, n >= 1) =>
   m /^ n : #
 
 /** How much we need to add to make a proper multiple of the second argument. */
 primitive type
   { m : #, n : # }
-  (fin m, fin n, n >= 1) =>
+  (fin n, n >= 1) =>
   m %^ n : #
 
 /** The length of an enumeration. */
@@ -195,20 +195,70 @@ length _ = `n
 /**
  * A finite sequence counting up from 'first' to 'last'.
  *
- * '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'.
+ * '[x .. y]' is syntactic sugar for 'fromTo`{first=x,last=y}'.
  */
-primitive fromTo : {first, last, a} (fin last, last >= first,
-                                    Literal first a, Literal last a) =>
-                                    [1 + (last - first)]a
+primitive fromTo : {first, last, a}
+  (fin last, last >= first, Literal last a) =>
+  [1 + (last - first)]a
 
 /**
  * A possibly infinite sequence counting up from 'first' up to (but not including) 'bound'.
  *
- * Note that if 'first' = 'bound' then the sequence will be empty.
+ * '[ x ..< y ]' is syntactic sugar for 'fromToLessThan`{first=x,bound=y}'.
+ *
+ * Note that if 'first' = 'bound' then the sequence will be empty.  If 'bound = inf'
+ * then the sequence will be infinite, and will eventually wrap around for bounded types.
  */
 primitive fromToLessThan :
-  {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) => [bound - first]a
+  {first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) =>
+  [bound - first]a
+
+/**
+ * A finite sequence counting up from 'first' to 'last' by 'stride'.
+ * Note that 'last' will only be an element of the enumeration if
+ * 'stride' divides 'last - first' evenly.
+ *
+ * '[x .. y by n]` is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'.
+ */
+primitive fromToBy : {first, last, stride, a}
+  (fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
+  [1 + (last - first)/stride]a
+
+/**
+ * A finite sequence counting from 'first' up to (but not including) 'bound'
+ * by 'stride'.  Note that if 'first = bound' then the sequence will
+ * be empty.  If 'bound = inf' then the sequence will be infinite, and will
+ * eventually wrap around for bounded types.
+ *
+ * '[x ..< y by n]' is syntactic sugar for 'fromToByLessThan`{first=a,bound=b,stride=n}'.
+ */
+primitive fromToByLessThan : {first, bound, stride, a}
+  (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
+  [(bound - first)/^stride]a
 
+/**
+ * A finite sequence counting from 'first' down to 'last' by 'stride'.
+ * Note that 'last' will only be an element of the enumeration if
+ * 'stride' divides 'first - last' evenly.
+ *
+ * '[x .. y down by n]` is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'.
+ */
+primitive fromToDownBy : {first, last, stride, a}
+  (fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
+  [1 + (first - last)/stride]a
+
+/**
+ * A finite sequence counting from 'first' down to (but not including)
+ * 'bound' by 'stride'.
+ *
+ * '[x ..> y down by n]` is syntactic sugar for
+ * 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'.
+ *
+ * Note that if 'first = bound' the sequence will be empty.
+ */
+primitive fromToDownByGreaterThan : {first, bound, stride, a}
+  (fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
+  [(first - bound)/^stride]a
 
 /**
  * A finite arithmetic sequence starting with 'first' and 'next',
@@ -387,7 +437,7 @@ primitive infFromThen : {a} (Integral a) => a -> a -> [inf]a
 
 /**
  * Value types that correspond to a field; that is,
- * a ring also posessing multiplicative inverses for
+ * a ring also possessing multiplicative inverses for
  * non-zero elements.
  *
  * Floating-point values are only approximately a field,
@@ -943,7 +993,7 @@ primitive pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
 
 /**
  * Parallel map.  The given function is applied to each element in the
- * given finite seqeuence, and the results are computed in parallel.
+ * given finite sequence, and the results are computed in parallel.
  * The values in the resulting sequence are reduced to normal form,
  * as is done with the deepseq operation.
  *

lib/CryptolTC.z3

@@ -293,15 +293,19 @@
 )
 
 (define-fun cryCeilDiv ((x InfNat) (y InfNat)) InfNat
-  (ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr
-  (ite (= (value y) 0) cryErr (cryNat (- (div (- (value x)) (value y)))))
-  )
+  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
+  (ite (= (value y) 0) cryErr
+  (ite (not (isFin x)) cryInf
+    (cryNat (- (div (- (value x)) (value y))))
+  )))
 )
 
 (define-fun cryCeilMod ((x InfNat) (y InfNat)) InfNat
-  (ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr
-  (ite (= (value y) 0) cryErr (cryNat (mod (- (value x)) (value y))))
-  )
+  (ite (or (isErr x) (isErr y) (not (isFin y))) cryErr
+  (ite (= (value y) 0) cryErr
+  (ite (not (isFin x)) (cryNat 0)
+    (cryNat (mod (- (value x)) (value y)))
+  )))
 )
 
 (define-fun cryLenFromThenTo ((x InfNat) (y InfNat) (z InfNat)) InfNat

src/Cryptol/Eval/Generic.hs

@@ -1437,7 +1437,6 @@ updatePrim sym updateWord updateSeq =
                              (do vs <- fromSeq "updatePrim" =<< xs; updateSeq len eltTy vs idx' val)
 
 {-# INLINE fromToV #-}
-
 -- @[ 0 .. 10 ]@
 fromToV :: Backend sym => sym -> Prim sym
 fromToV sym =
@@ -1452,23 +1451,7 @@ fromToV sym =
         in VSeq len $ indexSeqMap $ \i -> f (first' + i)
       _ -> evalPanic "fromToV" ["invalid arguments"]
 
-{-# INLINE fromToLessThanV #-}
-
--- @[ 0 .. <10 ]@
-fromToLessThanV :: Backend sym => sym -> Prim sym
-fromToLessThanV sym =
-  PFinPoly \first ->
-  PNumPoly \bound ->
-  PTyPoly  \ty ->
-  PVal
-    let !f = mkLit sym ty
-        ss = indexSeqMap $ \i -> f (first + i)
-    in case bound of
-         Inf        -> VStream ss
-         Nat bound' -> VSeq (bound' - first) ss
-
 {-# INLINE fromThenToV #-}
-
 -- @[ 0, 1 .. 10 ]@
 fromThenToV :: Backend sym => sym -> Prim sym
 fromThenToV sym =
@@ -1485,6 +1468,75 @@ fromThenToV sym =
         in VSeq len' $ indexSeqMap $ \i -> f (first' + i*diff)
       _ -> evalPanic "fromThenToV" ["invalid arguments"]
 
+{-# INLINE fromToLessThanV #-}
+-- @[ 0 .. <10 ]@
+fromToLessThanV :: Backend sym => sym -> Prim sym
+fromToLessThanV sym =
+  PFinPoly \first ->
+  PNumPoly \bound ->
+  PTyPoly  \ty ->
+  PVal
+    let !f = mkLit sym ty
+        ss = indexSeqMap $ \i -> f (first + i)
+    in case bound of
+         Inf        -> VStream ss
+         Nat bound' -> VSeq (bound' - first) ss
+
+{-# INLINE fromToByV #-}
+-- @[ 0 .. 10 by 2 ]@
+fromToByV :: Backend sym => sym -> Prim sym
+fromToByV sym =
+  PFinPoly \first ->
+  PFinPoly \lst ->
+  PFinPoly \stride ->
+  PTyPoly  \ty ->
+  PVal
+    let !f = mkLit sym ty
+        ss = indexSeqMap $ \i -> f (first + i*stride)
+     in VSeq (1 + ((lst - first) `div` stride)) ss
+
+{-# INLINE fromToByLessThanV #-}
+-- @[ 0 .. <10 by 2 ]@
+fromToByLessThanV :: Backend sym => sym -> Prim sym
+fromToByLessThanV sym =
+  PFinPoly \first ->
+  PNumPoly \bound ->
+  PFinPoly \stride ->
+  PTyPoly  \ty ->
+  PVal
+    let !f = mkLit sym ty
+        ss = indexSeqMap $ \i -> f (first + i*stride)
+     in case bound of
+          Inf -> VStream ss
+          Nat bound' -> VSeq ((bound' - first + stride - 1) `div` stride) ss
+
+
+{-# INLINE fromToDownByV #-}
+-- @[ 10 .. 0 down by 2 ]@
+fromToDownByV :: Backend sym => sym -> Prim sym
+fromToDownByV sym =
+  PFinPoly \first ->
+  PFinPoly \lst ->
+  PFinPoly \stride ->
+  PTyPoly  \ty ->
+  PVal
+    let !f = mkLit sym ty
+        ss = indexSeqMap $ \i -> f (first - i*stride)
+     in VSeq (1 + ((first - lst) `div` stride)) ss
+
+{-# INLINE fromToDownByGreaterThanV #-}
+-- @[ 10 .. >0 down by 2 ]@
+fromToDownByGreaterThanV :: Backend sym => sym -> Prim sym
+fromToDownByGreaterThanV sym =
+  PFinPoly \first ->
+  PFinPoly \bound ->
+  PFinPoly \stride ->
+  PTyPoly  \ty ->
+  PVal
+    let !f = mkLit sym ty
+        ss = indexSeqMap $ \i -> f (first - i*stride)
+     in VSeq ((first - bound + stride - 1) `div` stride) ss
+
 {-# INLINE infFromV #-}
 infFromV :: Backend sym => sym -> Prim sym
 infFromV sym =
@@ -2015,6 +2067,20 @@ genericPrimTable sym getEOpts =
                   , {-# SCC "Prelude::fromToLessThan" #-}
                     fromToLessThanV sym)
 
+  , ("fromToBy"   , {-# SCC "Prelude::fromToBy" #-}
+                    fromToByV sym)
+
+  , ("fromToByLessThan",
+                    {-# SCC "Prelude::fromToByLessThan" #-}
+                    fromToByLessThanV sym)
+
+  , ("fromToDownBy", {-# SCC "Prelude::fromToDownBy" #-}
+                     fromToDownByV sym)
+
+  , ("fromToDownByGreaterThan"
+                  , {-# SCC "Prelude::fromToDownByGreaterThan" #-}
+                    fromToDownByGreaterThanV sym)
+
     -- Sequence manipulations
   , ("#"          , {-# SCC "Prelude::(#)" #-}
                     PFinPoly \front ->

src/Cryptol/ModuleSystem/Renamer.hs

@@ -465,6 +465,13 @@ instance Rename PrimType where
        depsOf (NamedThing (thing x))
          do let (as,ps) = primTCts pt
             (_,cts) <- renameQual as ps $ \as' ps' -> pure (as',ps')
+
+            -- Record an additional use for each parameter since we checked
+            -- earlier that all the parameters are used exactly once in the
+            -- body of the signature.  This prevents incorret warnings
+            -- about unused names.
+            mapM_ (recordUse . tpName) (fst cts)
+
             pure pt { primTCts = cts, primTName = x }
 
 instance Rename ParameterType where
@@ -727,6 +734,18 @@ instance Rename Expr where
                                <*> traverse rename n
                                <*> rename e
                                <*> traverse rename t
+    EFromToBy isStrict s e b t ->
+                       EFromToBy isStrict
+                                 <$> rename s
+                                 <*> rename e
+                                 <*> rename b
+                                 <*> traverse rename t
+    EFromToDownBy isStrict s e b t ->
+                       EFromToDownBy isStrict
+                                 <$> rename s
+                                 <*> rename e
+                                 <*> rename b
+                                 <*> traverse rename t
     EFromToLessThan s e t ->
                        EFromToLessThan <$> rename s
                                        <*> rename e