Minor fixes to the Z_n version of the ECDSA spec to be forward-compat…

…ible

with Cryptol changes.

At the same time, fix a bug in the `ec_decompress`, and add
a property for testing it.

Common/utils.cry

@@ -36,21 +36,29 @@ mul8 x = mul2(mul4 x)
 type constraint isOdd a = (a / 2) * 2 == a - 1
 
 half : {p} (fin p, p >= 3, isOdd p) => Z p -> Z p
-half x = if isEven (fromZ x) then x/2 else (fromInteger ((fromZ x + `p) / 2))
+half x = fromInteger (if isEven xint then xint/2 else ((xint + `p) / 2))
+  where
+  xint = fromZ x
+
+half_correct : {p} (fin p, p >= 3, isOdd p) => Z p -> Bit
+property half_correct x = half x + half x == x
 
-mp_mod_inv : {a} (fin a, a >= 1) => Z a -> Z a
+mp_mod_inv : {n} (fin n, n >= 1) => Z n -> Z n
 mp_mod_inv c = if c == 0 then error "Zero does not have a multiplicative inverse"
                else fromInteger (if u'' == 1 then x1'' else x2'')
   where
     innercond (a, x) = isEven a
-    innerbody (a, x) = (a / 2, if isEven x then x / 2 else (x + `a) / 2)
+    innerbody (a, x) = (a / 2, if isEven x then x / 2 else (x + `n) / 2)
 
     outtercond (u, v, x1, x2) = (u != 1) /\ (v != 1)
-    outterbody (u, v, x1, x2) = if(u' >= v') then (u' - v', v', x1' - x2' % `a, x2')
-                                             else (u', v' - u', x1', x2' - x1' % `a)
+    outterbody (u, v, x1, x2) = if(u' >= v') then (u' - v', v', x1' - x2' % `n, x2')
+                                             else (u', v' - u', x1', x2' - x1' % `n)
       where
         (u', x1') = while innercond innerbody (u, x1)
         (v', x2') = while innercond innerbody (v, x2)
 
-    (u'', _, x1'', x2'') = while outtercond outterbody (fromZ c, `a, 1, 0)
+    (u'', _, x1'', x2'') = while outtercond outterbody (fromZ c, `n, 1, 0)
 
+// Note, this property will only hold when the modulus is prime
+mp_mod_inv_correct : {a} (fin a, a >=2) => Z a -> Bit
+property mp_mod_inv_correct x = x != 0 ==> x * mp_mod_inv x == 1

Primitive/Asymmetric/Signature/ECDSA/ECDSA.cry

@@ -44,6 +44,16 @@ joint_scalar_multiply_example R S T d e =
 
 mp_mod_sqrt_correct x = (mp_mod_sqrt (x ^^ 2)) ^^ 2 == (x ^^ 2)
 
+// This only holds for proper affine points
+affine_decompress_correct : AffinePoint p -> Bit
+affine_decompress_correct R = ~err /\ R == R'
+  where
+  (R',err) = ec_decompress (ec_compress`{width p+2} R)
+
+// Use the generator G to produce random affine points and test
+// the compression/decompression algorithm
+decompress_correct : Z p -> Bit
+property decompress_correct k = affine_decompress_correct (ec_affinify (ec_mult k G))
 
 parameter
 
@@ -80,14 +90,14 @@ private
     where Sx = ZtoBV S.x : [width p]
           Sy = ZtoBV S.y : [r - width p]
 
-  ec_decompress : {a, b} (fin a, a >= width p + 2, fin b, p >= 1 + b) => [a] -> (AffinePoint p, Bit)
+  ec_decompress : {a} (fin a, a >= width p + 2) => [a] -> (AffinePoint p, Bit)
   ec_decompress S = ({x = Rx, y = Ry}, err)
-    where c = BVtoZ  (take S : [2])
+    where c  = toInteger (take S : [2])
           Rx = BVtoZ (drop S : [a-2])
-          t0 = Rx ^^ 3 - (mul3 Rx) + `b
+          t0 = Rx ^^ 3 - (mul3 Rx) + b
           t1 = mp_mod_sqrt t0
           err = t1 ^^ 2 != t0
-          Ry = if t1 == c%2 then t1 else -t1
+          Ry = if (fromZ t1)%2 == c%2 then t1 else -t1
 
   ec_is_point_affine : AffinePoint p -> Bit
   ec_is_point_affine S = S.y ^^ 2 == t

Primitive/Asymmetric/Signature/ECDSA/ECDSA_tests.cry

@@ -19,6 +19,9 @@ p192_S = {x = BVtoZ 0xd458e7d127ae671b0c330266d246769353a012073e97acf8,
 p192_T = {x = BVtoZ 0xf22c4395213e9ebe67ddecdd87fdbd01be16fb059b9753a4,
           y = BVtoZ 0x264424096af2b3597796db48f8dfb41fa9cecc97691a9c79}
 
+property p192_decompress_S = p192::affine_decompress_correct p192_S
+property p192_decompress_T = p192::affine_decompress_correct p192_T
+
 property p192_full_add_example =
   p192::full_add_example R p192_S p192_T
   where R = {x = BVtoZ 0x48e1e4096b9b8e5ca9d0f1f077b8abf58e843894de4d0290,