Documentation tweaks

CHANGES.md

@@ -13,7 +13,7 @@
   modulus methods (`(/)` and `(%)`), and the sequence indexing,
   sequence update and shifting operations are generalized over
   `Integral`.  The `toInteger` operation is also generalized over this
-  class.  `Integral` contains the bitvector types, `Integer` and `Z n`.
+  class.  `Integral` contains the bitvector types and `Integer`.
 
   The new `Field` class contains types representing mathematical
   fields (or types that are approximately fields). For now, it is
@@ -25,13 +25,15 @@
   There is also a new `Round` class for types that can sensibly be
   rounded to integers.  This class has the methods `floor`, `ceiling`,
   `trunc` and `round` for performing different kinds of
-  integer rounding.
+  integer rounding.  Currently `Rational` is the only meber of `Round`.
 
-  Finally the `(^^)`, `lg2`, `(/$)` and `(%$)` methods of Arith have
+  The type of `(^^)` is modified to be
-  had their types specialized.  `lg2` is now only an operation on
+  `{a, e} (Ring a, Integral e) => a -> e -> a`. This makes it clear
-  bitvectors, and the exponent of `(^^)` is specialized to be a
+  that the semantics are iterated multiplication, which makes sense
-  bitvector.  Likewise, `(/$)` and `(%$)` are now operations
+  in any ring.
-  only on bitvectors.
+
+  Finally, the `lg2`, `(/$)` and `(%$)` methods of Arith have
+  had their types specialized so operate only on bitvectors.
 
 * Added a base `Rational` type.  It is implemented as a pair of
   integers, quotiented in the usual way.  As such, it reduces to the

docs/CryptolPrims.md

@@ -20,6 +20,7 @@ Comparisons and Ordering
     instance (Cmp a, Cmp b) => Cmp (a, b)
     instance (Cmp a, Cmp b) => Cmp { x : a, y : b }
     instance                   Cmp Integer
+    instance (fin n, n>=1)  => Cmp (Z n)
     instance                   Cmp Rational
 
 Signed Comparisons
@@ -38,6 +39,13 @@ Signed Comparisons
     instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b)
     instance (SignedCmp a, SignedCmp b) => SignedCmp { x : a, y : b }
 
+Zero
+----
+
+    zero       : {a} (Zero a) => a
+
+Every base and structured type in Cryptol is a member of class `Zero`.
+
 
 Arithmetic
 ----------
@@ -58,7 +66,8 @@ Arithmetic
     trunc   : {a} (Round a) => a -> Integer
     round   : {a} (Round a) => a -> Integer
 
-    (^^)    : {a, n} (Ring a, fin n) => a -> [n] -> a
+    (^^)    : {a, e} (Ring a, Integral e) => a -> e -> a
+
     (/$)    : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
     (%$)    : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
     lg2     : {n} (fin n) => [n] -> [n]
@@ -80,7 +89,6 @@ the top two instances do not actually overlap.
 
     instance                  Integral Integer 
     instance (fin n)       => Integral ([n]Bit)
-    instance (fin n, n>=1) => Integral (Z n)
 
     instance Field Rational
 
@@ -92,7 +100,6 @@ Boolean
     False      : Bit
     True       : Bit
 
-    zero       : {a} (Zero a) => a
     (&&)       : {a} (Logic a) => a -> a -> a
     (||)       : {a} (Logic a) => a -> a -> a
     (^)        : {a} (Logic a) => a -> a -> a
@@ -108,6 +115,8 @@ Boolean
     instance (Logic a, Logic b) => Logic (a, b)
     instance (Logic a, Logic b) => Logic { x : a, y : b }
     // No instance for `Logic Integer`.
+    // No instance for `Logic (Z n)`.
+    // No instance for `Logic Rational`.
 
 Sequences
 ---------

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -283,7 +283,7 @@ value representing one half:
 
 Note, the division operation on \texttt{Rational} is
 written \texttt{/.}, and should not be confused with
-\texttt{/}, which is the division operation on for words
+\texttt{/}, which is the division operation for words
 and integers.
 
 
@@ -2984,11 +2984,11 @@ The sequence indexing, update and shifting operations
 take index arguments that can be of any \texttt{Integral} type.
 Infinite sequence enumerations \texttt{[x ...]}
 and \texttt{[x, y ...]} are also defined for class \texttt{Integral}.
-Bitvectors, integers, and moduluar integers are members of \texttt{Integral}.
+Bitvectors and integers members of \texttt{Integral}.
 
 \item
 The \texttt{Field} typeclass represents values that, in addition to
-being a \texttt{Ring} posess a multiplictive inverses.
+being a \texttt{Ring}, have multiplictive inverses.
 It includes the field division operation \texttt{/.} and the
 \texttt{recip} operation for computing the reciprocol of a value.
 Currently, only type \texttt{Rational} is a member of this class.

docs/ProgrammingCryptol/highAssurance/HighAssurance.tex

@@ -64,7 +64,8 @@ expressed (more concisely) using the \texttt{===} operator:
 
 \note{It is important to emphasize that the mathematical equality
   above and the Cryptol property are \emph{not} stating precisely the
-  same property.  Remember that all Cryptol arithmetic is
+  same property.  Remember that Cryptol arithmetic depends on the
+  types of the arguments and arithmetic on \texttt{[8]} is
   modular,\indModular while the mathematical equation is over
   arbitrary numbers, including negative, real, or even complex
   numbers.  The takeaway of this discussion is that we are only using

docs/ProgrammingCryptol/prims/Primitives.tex

@@ -26,7 +26,7 @@ primsPlaceHolder=1;
     +, -, *           : {a} (Ring a) => a -> a -> a
     negate            : {a} (Ring a) => a -> a
     fromInteger       : {a} (Ring a) => Integer -> a
-    ^^                : {a} (Ring a, fin n) => a -> [n] -> a
+    ^^                : {a, e} (Ring a, Integral e) => a -> e -> a
     abs               : {a} (Cmp a, Ring a) => a -> a
     /, %              : {a} (Integral a) => a -> a -> a
     toInteger         : {a} (Integral a) => a -> Integer

lib/Cryptol.cry

@@ -29,10 +29,31 @@ primitive type Bit : *
 /** The type of unbounded integers. */
 primitive type Integer : *
 
-/** 'Z n' is the type of integers, modulo 'n'. */
+/** 'Z n' is the type of integers, modulo 'n'.
+  *
+  * The values of `Z n` may be thought of as equivalance
+  * 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
+  * or indexing.
+  *
+  * 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
+  * the (unique) integer value `i`  where `0 <= i < n` and
+  * `i` is in the given equivalance class.
+  */
 primitive type {n : #} (fin n, n >= 1) => Z n : *
 
-/** `Rational` is the type of rational numbers. */
+/** `Rational` is the type of rational numbers.
+  * Rational numbers form a Field (and thus a Ring).
+  *
+  * The `ratio` operation may be used to directly create
+  * rational values from as a ratio of integers, or
+  * the `fromInteger` method and the field operations
+  * can be used.
+  */
 primitive type Rational : *
 
 type Bool = Bit
@@ -293,7 +314,10 @@ primitive toInteger : {a} (Integral a) => a -> Integer
 
 /**
  * Compute the exponentiation of a value in a ring.
- * The exponent is treated as an unsigned bitvector value.
+ *  * For type [n], the exponent is treated as unsigned.
+ *  * It is an error to raise a value to a negative integer exponent.
+ *  * Satisfies: `x ^^ 0 == fromInteger 1`
+ *  * Satisfies: `x ^^ e == x * x ^^ (e-1)` when `e > 0`.
  */
 primitive (^^) : {a, e} (Ring a, Integral e) => a -> e -> a
 

src/Cryptol/Eval/Reference.lhs

@@ -63,7 +63,7 @@ The value types of Cryptol, along with their Haskell representations,
 are as follows:
 
 | Cryptol type      | Description       | `TValue` representation     |
-|:----------------- |:-------------- ---|:--------------------------- |
+|:------------------|:------------------|:----------------------------|
 | `Bit`             | booleans          | `TVBit`                     |
 | `Integer`         | integers          | `TVInteger`                 |
 | `Z n`             | integers modulo n | `TVIntMod n`                |
@@ -856,7 +856,7 @@ For functions, `zero` returns the constant function that returns
 Literals
 --------
 
-Given a literal integer, construct a value of a type that can represent that literal
+Given a literal integer, construct a value of a type that can represent that literal.
 
 > literal :: Integer -> TValue -> Value
 > literal i = go

src/Cryptol/Prelude.hs

@@ -19,6 +19,7 @@ import Data.ByteString(ByteString)
 import qualified Data.ByteString.Char8 as B
 import Text.Heredoc (there)
 
+
 preludeContents :: ByteString
 preludeContents = B.pack [there|lib/Cryptol.cry|]