Improve integer operation support in BOUNDER_RULE and BOUNDER_TAC

In general, BOUNDER_RULE now directly handles operations over Z and N,
assuming an outer real_of_int / real_of_num cast into R (this is also
automated in the tactic form BOUNDER_TAC). In particular, this change
can greatly improve bounds for terms involving integer or natural
number division and remainder (DIV, div, MOD and rem) as well as
cutoff subtraction over N. There is also now support for conditionals,
though the condition is not used as extra context, simply being the
basis for a case split.

This update rolls in various trivial typographic fixes in comments.

arm/curve25519/Makefile

@@ -3,7 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 #############################################################################
 
-# If actually on an ARM8 machine, just use the GNU assmbler (as). Otherwise
+# If actually on an ARM8 machine, just use the GNU assembler (as). Otherwise
 # use a cross-assembling version so that the code can still be assembled
 # and the proofs checked against the object files (though you won't be able
 # to run code without additional emulation infrastructure). The aarch64

arm/curve25519/bignum_inv_p25519.S

@@ -1106,7 +1106,7 @@ midloop:
 // since we know (for in-scope cases) that f is either +1 or -1.
 // We don't explicitly shift right by 59 either, but looking at
 // bit 63 (or any bit >= 60) of the unshifted result is enough
-// to distiguish -1 from +1; this is then made into a mask.
+// to distinguish -1 from +1; this is then made into a mask.
 
  ldr x0, [f]
  ldr x1, [g]

arm/curve25519/edwards25519_scalarmulbase.S

@@ -577,7 +577,7 @@ S2N_BN_SYMBOL(edwards25519_scalarmulbase):
 // (X,Y,Z,T), representing an affine point on the edwards25519 curve
 // (x,y) via x = X/Z, y = Y/Z and x * y = T/Z (so X * Y = T * Z).
 // In comments B means the standard basepoint (x,4/5) =
-// (0x216....f25d51a,0x0x6666..666658).
+// (0x216....f25d51a,0x6666..666658).
 //
 // Initialize accumulator "acc" to either 0 or 2^251 * B depending on
 // bit 251 of the (reduced) scalar. That leaves bits 0..250 to handle.

arm/curve25519/edwards25519_scalarmulbase_alt.S

@@ -419,7 +419,7 @@ S2N_BN_SYMBOL(edwards25519_scalarmulbase_alt):
 // (X,Y,Z,T), representing an affine point on the edwards25519 curve
 // (x,y) via x = X/Z, y = Y/Z and x * y = T/Z (so X * Y = T * Z).
 // In comments B means the standard basepoint (x,4/5) =
-// (0x216....f25d51a,0x0x6666..666658).
+// (0x216....f25d51a,0x6666..666658).
 //
 // Initialize accumulator "acc" to either 0 or 2^251 * B depending on
 // bit 251 of the (reduced) scalar. That leaves bits 0..250 to handle.

arm/curve25519/edwards25519_scalarmuldouble.S

@@ -1514,7 +1514,7 @@ edwards25519_scalarmuldouble_loop:
 // form amounts to swapping the first two fields and negating the third.
 // The negation does not always fully reduce even mod 2^256-38 in the zero
 // case, instead giving -0 = 2^256-38. But that is fine since the result is
-// always fed to a multipliction inside the "pepadd" function below that
+// always fed to a multiplication inside the "pepadd" function below that
 // handles any 256-bit input.
 
  cmp cf, xzr

arm/curve25519/edwards25519_scalarmuldouble_alt.S

@@ -1298,7 +1298,7 @@ edwards25519_scalarmuldouble_alt_loop:
 // form amounts to swapping the first two fields and negating the third.
 // The negation does not always fully reduce even mod 2^256-38 in the zero
 // case, instead giving -0 = 2^256-38. But that is fine since the result is
-// always fed to a multipliction inside the "pepadd" function below that
+// always fed to a multiplication inside the "pepadd" function below that
 // handles any 256-bit input.
 
  cmp cf, xzr

arm/fastmul/Makefile

@@ -3,7 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 #############################################################################
 
-# If actually on an ARM8 machine, just use the GNU assmbler (as). Otherwise
+# If actually on an ARM8 machine, just use the GNU assembler (as). Otherwise
 # use a cross-assembling version so that the code can still be assembled
 # and the proofs checked against the object files (though you won't be able
 # to run code without additional emulation infrastructure). The aarch64

arm/generic/Makefile

@@ -3,7 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 #############################################################################
 
-# If actually on an ARM8 machine, just use the GNU assmbler (as). Otherwise
+# If actually on an ARM8 machine, just use the GNU assembler (as). Otherwise
 # use a cross-assembling version so that the code can still be assembled
 # and the proofs checked against the object files (though you won't be able
 # to run code without additional emulation infrastructure). The aarch64

arm/generic/bignum_copy_row_from_table_8n_neon.S

@@ -3,7 +3,7 @@
 
 // ----------------------------------------------------------------------------
 // Given table: uint64_t[height*width], copy table[idx*width...(idx+1)*width-1]
-// into z[0..width-1]. width must be a mutiple of 8.
+// into z[0..width-1]. width must be a multiple of 8.
 // This function is constant-time with respect to the value of `idx`. This is
 // achieved by reading the whole table and using the bit-masking to get the
 // `idx`-th row.

arm/generic/word_divstep59.S

@@ -202,7 +202,7 @@ S2N_BN_SYMBOL(word_divstep59):
  tst grs, #1
 
 // Split the last divsteps into two blocks of 10 and 9 to insert the matrix
-// multiplication in betwen them. The first ten iterations:
+// multiplication in between them. The first ten iterations:
 
 .set i, 0
 .rep 10

arm/p256/Makefile

@@ -3,7 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 #############################################################################
 
-# If actually on an ARM8 machine, just use the GNU assmbler (as). Otherwise
+# If actually on an ARM8 machine, just use the GNU assembler (as). Otherwise
 # use a cross-assembling version so that the code can still be assembled
 # and the proofs checked against the object files (though you won't be able
 # to run code without additional emulation infrastructure). The aarch64

arm/p384/Makefile

@@ -3,7 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 #############################################################################
 
-# If actually on an ARM8 machine, just use the GNU assmbler (as). Otherwise
+# If actually on an ARM8 machine, just use the GNU assembler (as). Otherwise
 # use a cross-assembling version so that the code can still be assembled
 # and the proofs checked against the object files (though you won't be able
 # to run code without additional emulation infrastructure). The aarch64

arm/p521/Makefile

@@ -3,7 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 #############################################################################
 
-# If actually on an ARM8 machine, just use the GNU assmbler (as). Otherwise
+# If actually on an ARM8 machine, just use the GNU assembler (as). Otherwise
 # use a cross-assembling version so that the code can still be assembled
 # and the proofs checked against the object files (though you won't be able
 # to run code without additional emulation infrastructure). The aarch64

arm/proofs/base.ml

@@ -37,7 +37,7 @@ loadt "common/interval.ml";;
 loadt "common/elf.ml";;
 
 (* ------------------------------------------------------------------------- *)
-(* Support for additional SHA instrinsics (from Carl Kwan) *)
+(* Support for additional SHA intrinsics (from Carl Kwan)  *)
 (* ------------------------------------------------------------------------- *)
 
 loadt "arm/proofs/sha256.ml";;

arm/proofs/bignum_cmadd.ml

@@ -85,7 +85,7 @@ let BIGNUM_CMADD_CORRECT = prove
  X_GEN_TAC `pc:num` THEN REWRITE_TAC[NONOVERLAPPING_CLAUSES] THEN
  REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN DISCH_TAC THEN
 
- (*** Target the end label, removing redudancy in conclusion ***)
+ (*** Target the end label, removing redundancy in conclusion ***)
 
  BIGNUM_TERMRANGE_TAC `n:num` `a:num` THEN
  ENSURES_SEQUENCE_TAC `pc + 0x98`

arm/proofs/bignum_cmnegadd.ml

@@ -95,7 +95,7 @@ let BIGNUM_CMNEGADD_CORRECT = prove
  X_GEN_TAC `pc:num` THEN REWRITE_TAC[NONOVERLAPPING_CLAUSES] THEN
  REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN DISCH_TAC THEN
 
- (*** Target the end label, removing redudancy in conclusion ***)
+ (*** Target the end label, removing redundancy in conclusion ***)
 
  BIGNUM_TERMRANGE_TAC `n:num` `a:num` THEN
  ENSURES_SEQUENCE_TAC `pc + 0xb8`

arm/proofs/bignum_cmul.ml

@@ -77,7 +77,7 @@ let BIGNUM_CMUL_CORRECT = prove
  X_GEN_TAC `pc:num` THEN REWRITE_TAC[NONOVERLAPPING_CLAUSES] THEN
  REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN DISCH_TAC THEN
 
- (*** Target the end label, removing redudancy in conclusion ***)
+ (*** Target the end label, removing redundancy in conclusion ***)
 
  BIGNUM_TERMRANGE_TAC `n:num` `a:num` THEN
  ENSURES_SEQUENCE_TAC `pc + 0x80`

arm/proofs/bignum_emontredc_8n_neon.ml

@@ -2675,7 +2675,7 @@ let BIGNUM_EMONTREDC_8N_NEON_CORRECT = time prove
  CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV NUM_REDUCE_CONV)) THEN
  REWRITE_TAC[WORD_ADD_0;ARITH_RULE `x+0=x`;VAL_WORD_GALOIS;DIMINDEX_64; BIGDIGIT_BOUND] THEN STRIP_TAC] THEN
 
- (* From assupmtion
+ (* From assumption
  `bignum_from_memory (z',((k + 4) - 4 * i)) s0 = highdigits a (4 * i),
  make
  `bignum_from_memory (z'+32,k - 4*i) s0 = highdigits a (4 * (i + 1))

arm/proofs/bignum_ksqr_32_64.ml

@@ -843,7 +843,7 @@ let bignum_ksqr_32_64_mc =
 let BIGNUM_KSQR_32_64_EXEC = ARM_MK_EXEC_RULE bignum_ksqr_32_64_mc;;
 
 (* ------------------------------------------------------------------------- *)
-(* Proof for the inner-level 8->16 squring.  *)
+(* Proof for the inner-level 8->16 squaring. *)
 (* ------------------------------------------------------------------------- *)
 
 let lemma1 = prove

arm/proofs/bignum_ksqr_32_64_neon.ml

@@ -917,7 +917,7 @@ let bignum_ksqr_32_64_neon_mc =
 let BIGNUM_KSQR_32_64_NEON_EXEC = ARM_MK_EXEC_RULE bignum_ksqr_32_64_neon_mc;;
 
 (* ------------------------------------------------------------------------- *)
-(* Proof for the inner-level 8->16 squring.  *)
+(* Proof for the inner-level 8->16 squaring. *)
 (* ------------------------------------------------------------------------- *)
 
 let lemma1 = prove

arm/proofs/decode.ml

@@ -837,7 +837,7 @@ let PURE_DECODE_CONV =
  Precisely speaking, 'snd (eval_prod `:(A,B)prod`) (term, ls)' creates
  new variables that are to be mapped to the variables in term and returns
  the mapping list concatenated by ls. If the type variable is a tree of
- prod, it is recursively splitted and the mapping is correspondingly
+ prod, it is recursively split and the mapping is correspondingly
  created. *)
  let rec eval_prod = function
  | Tyapp("prod",[A;B]) ->

arm/secp256k1/Makefile

@@ -3,7 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 #############################################################################
 
-# If actually on an ARM8 machine, just use the GNU assmbler (as). Otherwise
+# If actually on an ARM8 machine, just use the GNU assembler (as). Otherwise
 # use a cross-assembling version so that the code can still be assembled
 # and the proofs checked against the object files (though you won't be able
 # to run code without additional emulation infrastructure). The aarch64

arm/sm2/Makefile

@@ -3,7 +3,7 @@
 # SPDX-License-Identifier: Apache-2.0 OR ISC
 #############################################################################
 
-# If actually on an ARM8 machine, just use the GNU assmbler (as). Otherwise
+# If actually on an ARM8 machine, just use the GNU assembler (as). Otherwise
 # use a cross-assembling version so that the code can still be assembled
 # and the proofs checked against the object files (though you won't be able
 # to run code without additional emulation infrastructure). The aarch64