diff --git a/arm/Makefile b/arm/Makefile index 515df2ee..aaec4a30 100644 --- a/arm/Makefile +++ b/arm/Makefile @@ -154,6 +154,10 @@ BIGNUM_OBJ = curve25519/bignum_add_p25519.o \ generic/bignum_cmul.o \ generic/bignum_coprime.o \ generic/bignum_copy.o \ + generic/bignum_copy_row_from_table.o \ + generic/bignum_copy_row_from_table_8n_neon.o \ + generic/bignum_copy_row_from_table_16_neon.o \ + generic/bignum_copy_row_from_table_32_neon.o \ generic/bignum_ctd.o \ generic/bignum_ctz.o \ generic/bignum_demont.o \ diff --git a/arm/generic/Makefile b/arm/generic/Makefile index 8a2da102..4f26b089 100644 --- a/arm/generic/Makefile +++ b/arm/generic/Makefile @@ -38,6 +38,10 @@ OBJ = bignum_add.o \ bignum_cmul.o \ bignum_coprime.o \ bignum_copy.o \ + bignum_copy_row_from_table.o \ + bignum_copy_row_from_table_8n_neon.o \ + bignum_copy_row_from_table_16_neon.o \ + bignum_copy_row_from_table_32_neon.o \ bignum_ctd.o \ bignum_ctz.o \ bignum_demont.o \ diff --git a/arm/generic/bignum_copy_row_from_table.S b/arm/generic/bignum_copy_row_from_table.S new file mode 100644 index 00000000..ba3e48d0 --- /dev/null +++ b/arm/generic/bignum_copy_row_from_table.S @@ -0,0 +1,81 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR ISC + +// ---------------------------------------------------------------------------- +// Given table: uint64_t[height*width], copy table[idx*width...(idx+1)*width-1] +// into z[0..width-1]. +// 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. +// +// extern void bignum_copy_from_table +// (uint64_t *z, uint64_t *table, uint64_t height, uint64_t width, +// uint64_t idx); +// +// Standard ARM ABI: X0 = z, X1 = table, X2 = height, X3 = width, X4 = idx +// ---------------------------------------------------------------------------- +#include "_internal_s2n_bignum.h" + + S2N_BN_SYM_VISIBILITY_DIRECTIVE(bignum_copy_row_from_table) + S2N_BN_SYM_PRIVACY_DIRECTIVE(bignum_copy_row_from_table) + .text + .balign 4 + +#define z x0 +#define table x1 +#define height x2 +#define width x3 +#define idx x4 + +#define i x5 +#define mask x6 +#define j x7 + +S2N_BN_SYMBOL(bignum_copy_row_from_table): + + cbz height, bignum_copy_row_from_table_end + cbz width, bignum_copy_row_from_table_end + mov i, width + mov x6, z + +bignum_copy_row_from_table_initzero: + str xzr, [x6] + add x6, x6, #8 + subs i, i, #1 + bne bignum_copy_row_from_table_initzero + + mov i, xzr + mov x8, table + +bignum_copy_row_from_table_outerloop: + + cmp i, idx + csetm mask, eq + + mov j, width + mov x9, z + +bignum_copy_row_from_table_innerloop: + + ldr x10, [x8] + ldr x11, [x9] + and x10, x10, mask + orr x11, x11, x10 + str x11, [x9] + + add x8, x8, #8 + add x9, x9, #8 + subs j, j, #1 + bne bignum_copy_row_from_table_innerloop + +bignum_copy_row_from_table_innerloop_done: + add i, i, #1 + cmp i, height + bne bignum_copy_row_from_table_outerloop + +bignum_copy_row_from_table_end: + ret + +#if defined(__linux__) && defined(__ELF__) +.section .note.GNU-stack,"",%progbits +#endif diff --git a/arm/generic/bignum_copy_row_from_table_16_neon.S b/arm/generic/bignum_copy_row_from_table_16_neon.S new file mode 100644 index 00000000..2b51db2c --- /dev/null +++ b/arm/generic/bignum_copy_row_from_table_16_neon.S @@ -0,0 +1,126 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR ISC + +// ---------------------------------------------------------------------------- +// Given table: uint64_t[height*16], copy table[idx*16...(idx+1)*16-1] +// into z[0..row-1]. +// 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. +// +// extern void bignum_copy_from_table_16_neon +// (uint64_t *z, uint64_t *table, uint64_t height, uint64_t idx); +// +// Initial version written by Hanno Becker +// Standard ARM ABI: X0 = z, X1 = table, X2 = height, X4 = idx +// ---------------------------------------------------------------------------- +#include "_internal_s2n_bignum.h" + + S2N_BN_SYM_VISIBILITY_DIRECTIVE(bignum_copy_row_from_table_16_neon) + S2N_BN_SYM_PRIVACY_DIRECTIVE(bignum_copy_row_from_table_16_neon) + .text + .balign 4 + + +// ***************************************************** +// Main code +// ***************************************************** + +#define z x0 +#define tbl x1 +#define height x2 +#define idx x3 + +#define mask x5 +#define cnt x6 + +#define ventry0 v20 +#define qentry0 q20 +#define ventry1 v21 +#define qentry1 q21 +#define ventry2 v22 +#define qentry2 q22 +#define ventry3 v23 +#define qentry3 q23 +#define ventry4 v24 +#define qentry4 q24 +#define ventry5 v25 +#define qentry5 q25 +#define ventry6 v26 +#define qentry6 q26 +#define ventry7 v27 +#define qentry7 q27 +#define ventry8 v28 + +#define vtmp v16 +#define qtmp q16 + +#define vmask v17 + +S2N_BN_SYMBOL(bignum_copy_row_from_table_16_neon): + + // Clear accumulator + // Zeroing can be done via xor, but xor isn't formalized yet. + dup ventry0.2d, xzr + mov ventry1.16b, ventry0.16b + mov ventry2.16b, ventry0.16b + mov ventry3.16b, ventry0.16b + mov ventry4.16b, ventry0.16b + mov ventry5.16b, ventry0.16b + mov ventry6.16b, ventry0.16b + mov ventry7.16b, ventry0.16b + + mov cnt, #0 +bignum_copy_row_from_table_16_neon_loop: + + // Compute mask: Check if current index matches target index + subs xzr, cnt, idx + cinv mask, xzr, eq + dup vmask.2d, mask + + ldr qtmp, [tbl, #16*0] + bit ventry0.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*1] + bit ventry1.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*2] + bit ventry2.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*3] + bit ventry3.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*4] + bit ventry4.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*5] + bit ventry5.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*6] + bit ventry6.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*7] + bit ventry7.16b, vtmp.16b, vmask.16b + + add tbl, tbl, #16*8 + + add cnt, cnt, #1 + subs xzr, height, cnt + b.ne bignum_copy_row_from_table_16_neon_loop + +bignum_copy_row_from_table_16_neon_end: + + str qentry0, [z, #16*0] + str qentry1, [z, #16*1] + str qentry2, [z, #16*2] + str qentry3, [z, #16*3] + str qentry4, [z, #16*4] + str qentry5, [z, #16*5] + str qentry6, [z, #16*6] + str qentry7, [z, #16*7] + + ret + +#if defined(__linux__) && defined(__ELF__) +.section .note.GNU-stack,"",%progbits +#endif diff --git a/arm/generic/bignum_copy_row_from_table_32_neon.S b/arm/generic/bignum_copy_row_from_table_32_neon.S new file mode 100644 index 00000000..dc36c000 --- /dev/null +++ b/arm/generic/bignum_copy_row_from_table_32_neon.S @@ -0,0 +1,181 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR ISC + +// ---------------------------------------------------------------------------- +// Given table: uint64_t[height*32], copy table[idx*32...(idx+1)*32-1] +// into z[0..row-1]. +// 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. +// +// extern void bignum_copy_from_table_32_neon +// (uint64_t *z, uint64_t *table, uint64_t height, uint64_t idx); +// +// Initial version written by Hanno Becker +// Standard ARM ABI: X0 = z, X1 = table, X2 = height, X4 = idx +// ---------------------------------------------------------------------------- +#include "_internal_s2n_bignum.h" + + S2N_BN_SYM_VISIBILITY_DIRECTIVE(bignum_copy_row_from_table_32_neon) + S2N_BN_SYM_PRIVACY_DIRECTIVE(bignum_copy_row_from_table_32_neon) + .text + .balign 4 + + +// ***************************************************** +// Main code +// ***************************************************** + +#define z x0 +#define tbl x1 +#define height x2 +#define idx x3 + +#define mask x5 +#define cnt x6 + +#define ventry0 v20 +#define qentry0 q20 +#define ventry1 v21 +#define qentry1 q21 +#define ventry2 v22 +#define qentry2 q22 +#define ventry3 v23 +#define qentry3 q23 +#define ventry4 v24 +#define qentry4 q24 +#define ventry5 v25 +#define qentry5 q25 +#define ventry6 v26 +#define qentry6 q26 +#define ventry7 v27 +#define qentry7 q27 +#define ventry8 v28 +#define qentry8 q28 +#define ventry9 v29 +#define qentry9 q29 +#define ventry10 v30 +#define qentry10 q30 +#define ventry11 v31 +#define qentry11 q31 +#define ventry12 v0 +#define qentry12 q0 +#define ventry13 v1 +#define qentry13 q1 +#define ventry14 v2 +#define qentry14 q2 +#define ventry15 v3 +#define qentry15 q3 + +#define vtmp v16 +#define qtmp q16 + +#define vmask v17 + +S2N_BN_SYMBOL(bignum_copy_row_from_table_32_neon): + + // Clear accumulator + // Zeroing can be done via xor, but xor isn't formalized yet. + dup ventry0.2d, xzr + mov ventry1.16b, ventry0.16b + mov ventry2.16b, ventry0.16b + mov ventry3.16b, ventry0.16b + mov ventry4.16b, ventry0.16b + mov ventry5.16b, ventry0.16b + mov ventry6.16b, ventry0.16b + mov ventry7.16b, ventry0.16b + mov ventry8.16b, ventry0.16b + mov ventry9.16b, ventry0.16b + mov ventry10.16b, ventry0.16b + mov ventry11.16b, ventry0.16b + mov ventry12.16b, ventry0.16b + mov ventry13.16b, ventry0.16b + mov ventry14.16b, ventry0.16b + mov ventry15.16b, ventry0.16b + + mov cnt, #0 +bignum_copy_row_from_table_32_neon_loop: + + // Compute mask: Check if current index matches target index + subs xzr, cnt, idx + cinv mask, xzr, eq + dup vmask.2d, mask + + ldr qtmp, [tbl, #16*0] + bit ventry0.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*1] + bit ventry1.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*2] + bit ventry2.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*3] + bit ventry3.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*4] + bit ventry4.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*5] + bit ventry5.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*6] + bit ventry6.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*7] + bit ventry7.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*8] + bit ventry8.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*9] + bit ventry9.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*10] + bit ventry10.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*11] + bit ventry11.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*12] + bit ventry12.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*13] + bit ventry13.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*14] + bit ventry14.16b, vtmp.16b, vmask.16b + + ldr qtmp, [tbl, #16*15] + bit ventry15.16b, vtmp.16b, vmask.16b + + add tbl, tbl, #32*8 + + add cnt, cnt, #1 + subs xzr, height, cnt + b.ne bignum_copy_row_from_table_32_neon_loop + +bignum_copy_row_from_table_32_neon_end: + + str qentry0, [z, #16*0] + str qentry1, [z, #16*1] + str qentry2, [z, #16*2] + str qentry3, [z, #16*3] + str qentry4, [z, #16*4] + str qentry5, [z, #16*5] + str qentry6, [z, #16*6] + str qentry7, [z, #16*7] + str qentry8, [z, #16*8] + str qentry9, [z, #16*9] + str qentry10, [z, #16*10] + str qentry11, [z, #16*11] + str qentry12, [z, #16*12] + str qentry13, [z, #16*13] + str qentry14, [z, #16*14] + str qentry15, [z, #16*15] + + ret + +#if defined(__linux__) && defined(__ELF__) +.section .note.GNU-stack,"",%progbits +#endif diff --git a/arm/generic/bignum_copy_row_from_table_8n_neon.S b/arm/generic/bignum_copy_row_from_table_8n_neon.S new file mode 100644 index 00000000..80db20d6 --- /dev/null +++ b/arm/generic/bignum_copy_row_from_table_8n_neon.S @@ -0,0 +1,102 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR ISC + +// ---------------------------------------------------------------------------- +// 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. +// 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. +// +// extern void bignum_copy_from_table_8_neon +// (uint64_t *z, uint64_t *table, uint64_t height, uint64_t width, uint64_t idx); +// +// Standard ARM ABI: X0 = z, X1 = table, X2 = height, X3 = width, X4 = idx +// ---------------------------------------------------------------------------- +#include "_internal_s2n_bignum.h" + + S2N_BN_SYM_VISIBILITY_DIRECTIVE(bignum_copy_row_from_table_8n_neon) + S2N_BN_SYM_PRIVACY_DIRECTIVE(bignum_copy_row_from_table_8n_neon) + .text + .balign 4 + + +#define z x0 +#define table x1 +#define height x2 +#define width x3 +#define idx x4 + +#define i x5 +#define mask x6 +#define j x7 + +#define vmask v16 + +S2N_BN_SYMBOL(bignum_copy_row_from_table_8n_neon): + + cbz height, bignum_copy_row_from_table_8n_neon_end + cbz width, bignum_copy_row_from_table_8n_neon_end + mov i, width + mov x6, z + dup v16.2d, xzr + +bignum_copy_row_from_table_8n_neon_initzero: + str q16, [x6] + str q16, [x6, #16] + str q16, [x6, #32] + str q16, [x6, #48] + add x6, x6, #64 + subs i, i, #8 + bne bignum_copy_row_from_table_8n_neon_initzero + + mov i, xzr + mov x8, table + +bignum_copy_row_from_table_8n_neon_outerloop: + + cmp i, idx + csetm mask, eq + dup vmask.2d, mask + + mov j, width + mov x9, z + +bignum_copy_row_from_table_8n_neon_innerloop: + + ldr q17, [x8] + ldr q18, [x9] + bit v18.16b, v17.16b, vmask.16b + str q18, [x9] + + ldr q17, [x8, #16] + ldr q18, [x9, #16] + bit v18.16b, v17.16b, vmask.16b + str q18, [x9, #16] + + ldr q17, [x8, #32] + ldr q18, [x9, #32] + bit v18.16b, v17.16b, vmask.16b + str q18, [x9, #32] + + ldr q17, [x8, #48] + ldr q18, [x9, #48] + bit v18.16b, v17.16b, vmask.16b + str q18, [x9, #48] + + add x8, x8, #64 + add x9, x9, #64 + subs j, j, #8 + bne bignum_copy_row_from_table_8n_neon_innerloop + +bignum_copy_row_from_table_8n_neon_innerloop_done: + add i, i, #1 + cmp i, height + bne bignum_copy_row_from_table_8n_neon_outerloop + +bignum_copy_row_from_table_8n_neon_end: + ret + +#if defined(__linux__) && defined(__ELF__) +.section .note.GNU-stack,"",%progbits +#endif diff --git a/arm/proofs/arm.ml b/arm/proofs/arm.ml index 3c07dc37..31eaec1d 100644 --- a/arm/proofs/arm.ml +++ b/arm/proofs/arm.ml @@ -310,8 +310,6 @@ let ARM_ENSURES_SUBSUBLEMMA_TAC = ENSURES_SUBSUBLEMMA_TAC o map (MATCH_MP aligned_bytes_loaded_update o CONJUNCT1);; -let WORD_SUB_ADD = WORD_RULE `word_sub (word (a + b)) (word b) = word a`;; - let ARM_CONV execth2 ths tm = let th = tryfind (MATCH_MP execth2) ths in let eth = tryfind (fun th2 -> GEN_REWRITE_CONV I [ARM_THM th th2] tm) ths in diff --git a/arm/proofs/bignum_copy_row_from_table.ml b/arm/proofs/bignum_copy_row_from_table.ml new file mode 100644 index 00000000..85055a39 --- /dev/null +++ b/arm/proofs/bignum_copy_row_from_table.ml @@ -0,0 +1,617 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC + *) + +(* ========================================================================= *) +(* Constant-time table lookup. *) +(* ========================================================================= *) + +let bignum_copy_row_from_table_mc = + define_assert_from_elf "bignum_copy_row_from_table_mc" + "arm/generic/bignum_copy_row_from_table.o" +[ + 0xb4000342; (* arm_CBZ X2 (word 104) *) + 0xb4000323; (* arm_CBZ X3 (word 100) *) + 0xaa0303e5; (* arm_MOV X5 X3 *) + 0xaa0003e6; (* arm_MOV X6 X0 *) + 0xf90000df; (* arm_STR XZR X6 (Immediate_Offset (word 0)) *) + 0x910020c6; (* arm_ADD X6 X6 (rvalue (word 8)) *) + 0xf10004a5; (* arm_SUBS X5 X5 (rvalue (word 1)) *) + 0x54ffffa1; (* arm_BNE (word 2097140) *) + 0xaa1f03e5; (* arm_MOV X5 XZR *) + 0xaa0103e8; (* arm_MOV X8 X1 *) + 0xeb0400bf; (* arm_CMP X5 X4 *) + 0xda9f13e6; (* arm_CSETM X6 Condition_EQ *) + 0xaa0303e7; (* arm_MOV X7 X3 *) + 0xaa0003e9; (* arm_MOV X9 X0 *) + 0xf940010a; (* arm_LDR X10 X8 (Immediate_Offset (word 0)) *) + 0xf940012b; (* arm_LDR X11 X9 (Immediate_Offset (word 0)) *) + 0x8a06014a; (* arm_AND X10 X10 X6 *) + 0xaa0a016b; (* arm_ORR X11 X11 X10 *) + 0xf900012b; (* arm_STR X11 X9 (Immediate_Offset (word 0)) *) + 0x91002108; (* arm_ADD X8 X8 (rvalue (word 8)) *) + 0x91002129; (* arm_ADD X9 X9 (rvalue (word 8)) *) + 0xf10004e7; (* arm_SUBS X7 X7 (rvalue (word 1)) *) + 0x54ffff01; (* arm_BNE (word 2097120) *) + 0x910004a5; (* arm_ADD X5 X5 (rvalue (word 1)) *) + 0xeb0200bf; (* arm_CMP X5 X2 *) + 0x54fffe21; (* arm_BNE (word 2097092) *) + 0xd65f03c0 (* arm_RET X30 *) +];; + +let BIGNUM_COPY_ROW_FROM_TABLE_EXEC = ARM_MK_EXEC_RULE bignum_copy_row_from_table_mc;; + +(* ARITH_RULE for proving `lp=rp` where lp and rp are pairs *) +let PAIR_EQ_ARITH_RULE (lp:term) (rp:term) = + let lpl,lpr = dest_pair lp in + let rpl,rpr = dest_pair rp in + let lth = ARITH_RULE (mk_eq (lpl,rpl)) in + let rth = ARITH_RULE (mk_eq (lpr,rpr)) in + let th = REFL lp in + let th = GEN_REWRITE_RULE (RAND_CONV o LAND_CONV) [lth] th in + GEN_REWRITE_RULE (RAND_CONV o RAND_CONV) [rth] th;; + +let REWRITE_ASSUMES_TAC (t:term) = + UNDISCH_THEN t (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm]) THEN ASSUME_TAC thm);; + +let READ_MEMORY_BYTES_0 = prove(`read (memory :> bytes (z,0)) s = 0`, + REWRITE_TAC[PAIR_EQ_ARITH_RULE `(x:int64,0)` `(x:int64, 8*0)`] THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_TRIVIAL]);; + +let LT_WORD_64 = prove(`!x (y:int64). x < val y ==> x < 2 EXP 64`, + REPEAT STRIP_TAC THEN + TRANS_TAC LT_TRANS `val (y:int64)` THEN + ONCE_REWRITE_TAC [GSYM DIMINDEX_64] THEN ASM_REWRITE_TAC[VAL_BOUND]);; + +let READ_MEMORY_BYTES_ELEM = prove(`!z w s m k. + w > k /\ read (memory :> bytes (z,8 * w)) s = m ==> + val (read (memory :> bytes64 (word_add z (word (8 * k)))) s) = lowdigits (highdigits m k) 1`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN EXPAND_TAC "m" THEN + REWRITE_TAC[HIGHDIGITS_BIGNUM_FROM_MEMORY; LOWDIGITS_BIGNUM_FROM_MEMORY] THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_SING] THEN + AP_THM_TAC THEN REPEAT AP_TERM_TAC THEN ASM_ARITH_TAC);; + +let READ_MEMORY_BYTES_FIRSTELEM = prove(`!z w s m. + w > 0 /\ read (memory :> bytes (z,8 * w)) s = m ==> + val (read (memory :> bytes64 z) s) = lowdigits m 1`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `z:int64 = word_add z (word (8 * 0))` (fun thm -> ONCE_REWRITE_TAC[thm]) THENL + [CONV_TAC WORD_RULE; ALL_TAC] THEN + IMP_REWRITE_TAC[READ_MEMORY_BYTES_ELEM] THEN REWRITE_TAC[HIGHDIGITS_0]);; + +let READ_MEMORY_BYTES_SLICE = prove(`!z w s m k w'. + w >= k + w' /\ read (memory :> bytes (z,8 * w)) s = m ==> + read (memory :> bytes (word_add z (word (8 * k)), 8 * w')) s = lowdigits (highdigits m k) w'`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN EXPAND_TAC "m" THEN + REWRITE_TAC[HIGHDIGITS_BIGNUM_FROM_MEMORY; LOWDIGITS_BIGNUM_FROM_MEMORY] THEN + AP_THM_TAC THEN REPEAT AP_TERM_TAC THEN ASM_ARITH_TAC);; + +let READ_MEMORY_BYTES_SLICE_HIGH = prove(`!z w s m k w'. + w = k + w' /\ read (memory :> bytes (z,8 * w)) s = m ==> + read (memory :> bytes (word_add z (word (8 * k)), 8 * w')) s = highdigits m k`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN EXPAND_TAC "m" THEN + REWRITE_TAC[HIGHDIGITS_BIGNUM_FROM_MEMORY] THEN + AP_THM_TAC THEN REPEAT AP_TERM_TAC THEN ASM_ARITH_TAC);; + +let READ_MEMORY_BYTES_MERGE = prove(`!z w w' w'' s m. + read (memory :> bytes (z,8 * w)) s = lowdigits m w /\ + read (memory :> bytes (word_add z (word (8 * w)),8 * w')) s = highdigits m w /\ + w + w' = w'' ==> + read (memory :> bytes (z, 8 * w'')) s = m`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN EXPAND_TAC "w''" THEN + ASM_REWRITE_TAC[BIGNUM_FROM_MEMORY_SPLIT] THEN + REWRITE_TAC[HIGH_LOW_DIGITS]);; + +let READ_MEMORY_BYTES_BYTES64 = prove(`!z s. + read (memory :> bytes (z,8)) s = val (read (memory :> bytes64 z) s)`, + REPEAT GEN_TAC THEN + REWRITE_TAC[PAIR_EQ_ARITH_RULE `(z:int64,8)` `(z:int64,8*1)`; + GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_SING]);; + + +let BIGNUM_COPY_ROW_FROM_TABLE_SUBROUTINE_CORRECT = prove(`!z table height width idx pc n m returnaddress. + nonoverlapping (word pc, 0x6c) (z, 8 * val width) /\ + nonoverlapping (word pc, 0x6c) (table, 8 * val height * val width) /\ + nonoverlapping (z, 8 * val width) (table, 8 * val height * val width) /\ + 8 * val width < 2 EXP 64 /\ + val idx < val height + ==> ensures arm + (\s. aligned_bytes_loaded s (word pc) bignum_copy_row_from_table_mc /\ + read PC s = word pc /\ + read X30 s = returnaddress /\ + C_ARGUMENTS [z; table; height; width; idx] s /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s = m) + (\s. read PC s = returnaddress /\ + bignum_from_memory (z, val width) s = m) + (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [memory :> bytes(z,8 * val width)])`, + + REPEAT GEN_TAC THEN REWRITE_TAC[C_ARGUMENTS; NONOVERLAPPING_CLAUSES; + MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN + REPEAT STRIP_TAC THEN + + ASM_CASES_TAC `val (height:(64)word) = 0` THENL [ + UNDISCH_TAC `val (idx:int64) < val (height:int64)` THEN + ASM_REWRITE_TAC[] THEN REWRITE_TAC[LT] THEN ENSURES_INIT_TAC "s0" THEN ITAUT_TAC; + ALL_TAC] THEN + ASM_CASES_TAC `width = (word 0):(64)word` THENL [ + ASM_REWRITE_TAC[] THEN + REWRITE_TAC[VAL_WORD_0; MULT_0; WORD_ADD_0] THEN + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [1;2;3] THEN + ASM_MESON_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_TRIVIAL]; + ALL_TAC] THEN + SUBGOAL_THEN `~(val (width:64 word) = 0)` ASSUME_TAC THENL [ + UNDISCH_TAC `~(width = word 0:64 word)` THEN + REWRITE_TAC[VAL_EQ_0]; + ALL_TAC] THEN + + ENSURES_SEQUENCE_TAC `pc + 0x10` + `\s. read X30 s = returnaddress /\ read X0 s = z /\ read X1 s = table /\ + read X2 s = height /\ read X3 s = width /\ read X4 s = idx /\ + read X5 s = width /\ read X6 s = z /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s + = m` THEN CONJ_TAC THENL [ + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC (1--4); + + ALL_TAC] THEN + + (* This is necessary to avoid stores from overwriting the table *) + SUBGOAL_THEN `val (idx:int64) * val (width:int64) + val width <= val (height:int64) * val width` ASSUME_TAC + THENL [IMP_REWRITE_TAC[LE_MULT_ADD]; ALL_TAC] THEN + + (* bignum_copy_row_from_table_initzero *) + ENSURES_WHILE_PDOWN_TAC `val (width:64 word):num` `pc + 0x10` `pc + 0x1c` + `\i s. (read X30 s = returnaddress /\ read X0 s = z /\ read X1 s = table /\ + read X2 s = height /\ read X3 s = width /\ read X4 s = idx /\ + read X5 s = word i /\ read X6 s = word (val z + 8 * (val width - i)) /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s + = m /\ + bignum_from_memory (z, val width - i) s = 0) /\ + (read ZF s <=> i = 0)` THEN REPEAT CONJ_TAC THENL [ + (* 1. width > 0 *) + ASM_MESON_TAC[]; + + (* 2. loop starts *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [] THEN + REWRITE_TAC[SUB_REFL; WORD_VAL; MULT_0; ADD_0; GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_TRIVIAL]; + + (* 3. loop body *) + REPEAT STRIP_TAC THEN REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN + MATCH_MP_TAC ENSURES_FRAME_SUBSUMED THEN + EXISTS_TAC `MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [memory :> bytes64 (word (val (z:int64) + 8 * (val (width:int64) - (i + 1))))]` THEN + REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN + CONJ_TAC THENL [ + REPEAT(MATCH_MP_TAC SUBSUMED_SEQ THEN REWRITE_TAC[SUBSUMED_REFL]) THEN + (* SIMPLE_ARITH_TAC isn't good at dealing with assumptions containing 'val'. Let's abbreviate + val width. *) + REWRITE_TAC[WORD_ADD; WORD_VAL] THEN + ABBREV_TAC `w' = val (width:int64)` THEN + SUBSUMED_MAYCHANGE_TAC; + + ALL_TAC] THEN + + ENSURES_INIT_TAC "s0" THEN + + SUBGOAL_THEN `val (width:64 word) - (i + 1) < val (width:64 word)` ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `8 * (val (width:int64) - (i + 1)) + 8 <= 18446744073709551616` ASSUME_TAC + THENL [ASM_ARITH_TAC; ALL_TAC] THEN + + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC (1--3) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REPEAT CONJ_TAC THENL [ + CONV_TAC WORD_RULE; + + REWRITE_TAC[GSYM WORD_ADD] THEN AP_TERM_TAC THEN UNDISCH_TAC `i < val (width:64 word)` + THEN ARITH_TAC; + + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + ASM_SIMP_TAC [ARITH_RULE `i < val (width:64 word) ==> val width - i = (val width - (i + 1)) + 1`] THEN + REWRITE_TAC[BIGNUM_FROM_MEMORY_STEP] THEN + ASM_REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES; WORD_RULE `word_add z (word c) = word (val z + c)`] THEN + CONV_TAC WORD_RULE; + + REWRITE_TAC[WORD_SUB_ADD; VAL_WORD] THEN + SUBGOAL_THEN `i < 2 EXP 64` ASSUME_TAC THENL [ + TRANS_TAC LT_TRANS `val (width:64 word)` THEN + ASM_REWRITE_TAC[] THEN + UNDISCH_TAC `8 * val (width:64 word) < 2 EXP 64` THEN + ARITH_TAC; + + ALL_TAC] THEN + ASM_SIMP_TAC[MOD_LT; DIMINDEX_64]]; + + (* 4. loop backedge *) + REPEAT STRIP_TAC THEN ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC (1--1); + + (* next *) + ALL_TAC] THEN + + (* bignum_copy_row_from_table_outerloop *) + ENSURES_WHILE_PUP_TAC `val (height:64 word):num` `pc + 0x28` `pc + 0x64` + `\i s. (read X30 s = returnaddress /\ read X0 s = z /\ read X1 s = table /\ + read X2 s = height /\ read X3 s = width /\ read X4 s = idx /\ + read X5 s = word i /\ read X8 s = word_add table (word (8 * i * val width)) /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s + = m /\ + ((i <= val idx /\ bignum_from_memory (z, val width) s = 0) \/ + (i > val idx /\ bignum_from_memory (z, val width) s = m))) /\ + (read ZF s <=> i = val height)` THEN REPEAT CONJ_TAC THENL [ + (* 1. height > 0 *) + ASM_MESON_TAC[]; + + (* 2. to loop start *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC (1--3) THEN + REWRITE_TAC[ARITH_RULE `x * 0 = 0`; ARITH_RULE `0 * x = 0`; WORD_ADD_0] THEN + RULE_ASSUM_TAC (REWRITE_RULE [ARITH_RULE `x - 0 = x`]) THEN + ASM_REWRITE_TAC[LE_0]; + + (* 3. loop body - pass *) + ALL_TAC; + + (* 4. loop backedge *) + REPEAT STRIP_TAC THEN + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC (1--1); + + (* next *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [1;2] THEN + CASES_FIRST_DISJ_ASSUM_TAC THEN SPLIT_FIRST_CONJ_ASSUM_TAC THENL [ + UNDISCH_TAC `val (idx:int64) < val (height:int64)` THEN + UNDISCH_TAC `val (height:int64) <= val (idx:int64)` THEN + ARITH_TAC; + + ASM_MESON_TAC[]]] THEN + + REPEAT STRIP_TAC THEN + + ENSURES_WHILE_PDOWN_TAC `val (width:64 word):num` `pc + 0x38` `pc + 0x58` + `\j s. (read X30 s = returnaddress /\ read X0 s = z /\ read X1 s = table /\ + read X2 s = height /\ read X3 s = width /\ read X4 s = idx /\ read X5 s = word i /\ + read X6 s = (if i = val idx then word 18446744073709551615 else word 0) /\ + read X7 s = word j /\ + // pointers + read X8 s = word_add table (word (8 * (i * val width + (val width - j)))) /\ + read X9 s = word_add z (word (8 * (val width - j)):64 word) /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s + = m /\ + ((i < val idx /\ + bignum_from_memory (z, val width - j) s = 0 /\ + bignum_from_memory (word_add z (word (8 * (val width - j))), j) s = 0) + \/ + (i = val idx /\ + bignum_from_memory (z, val width - j) s = lowdigits m (val width - j) /\ + bignum_from_memory (word_add z (word (8 * (val width - j))), j) s = 0) + \/ + (i > val idx /\ + bignum_from_memory (z, val width - j) s = lowdigits m (val width - j) /\ + bignum_from_memory (word_add z (word (8 * (val width - j))), j) s = highdigits m (val width - j)))) /\ + (read ZF s <=> j = 0)` THEN REPEAT CONJ_TAC THENL [ + ASM_MESON_TAC[]; + + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC (1--4) THEN + ASM_REWRITE_TAC[WORD_VAL; ADD_0; MULT_0; WORD_ADD_0] THEN + CONJ_TAC THENL [ + ASM_CASES_TAC `i = val (idx:int64)` THENL [ + ASM_REWRITE_TAC[VAL_WORD] THEN IMP_REWRITE_TAC[MOD_LT; VAL_BOUND]; + + ASM_REWRITE_TAC[VAL_WORD] THEN IMP_REWRITE_TAC[MOD_LT] THEN + TRANS_TAC LT_TRANS `val (height:int64)` THEN + ASM_REWRITE_TAC[VAL_BOUND]]; + + ASM_CASES_TAC `i > val (idx:int64)` THENL [ + SUBGOAL_THEN `~(i <= val (idx:int64))` ASSUME_TAC THENL + [ASM_REWRITE_TAC[NOT_LE; GSYM GT]; ALL_TAC] THEN + REWRITE_TAC[ASSUME `i > val (idx:int64)`] THEN + REWRITE_ASSUMES_TAC `i > val (idx:int64)` THEN + REWRITE_ASSUMES_TAC `~(i <= val (idx:int64))` THEN + ASM_REWRITE_TAC[READ_MEMORY_BYTES_0; LOWDIGITS_0; HIGHDIGITS_0]; + + SUBGOAL_THEN `i <= val (idx:int64)` ASSUME_TAC THENL + [UNDISCH_TAC `~(i > val (idx:int64))` THEN ARITH_TAC; ALL_TAC] THEN + REWRITE_ASSUMES_TAC `i <= val (idx:int64)` THEN + REWRITE_ASSUMES_TAC `~(i > val (idx:int64))` THEN + ASM_REWRITE_TAC[ASSUME `~(i > val (idx:int64))`; LOWDIGITS_0; READ_MEMORY_BYTES_0] THEN + UNDISCH_TAC `i <= val (idx:int64)` THEN + ARITH_TAC]]; + + (* loop body *) + ALL_TAC; + + (* backedge *) + REPEAT STRIP_TAC THEN ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [1]; + + (* finishes outer loop; pc 88 -> 100 *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [1;2;3] THEN + SUBGOAL_THEN `m < 2 EXP (64 * val (width:int64))` ASSUME_TAC THENL + [EXPAND_TAC "m" THEN SIMP_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_BOUND]; ALL_TAC] THEN + REWRITE_TAC[WORD_ADD; ARITH_RULE `a*b+b-0=(a+1)*b`] THEN + REWRITE_TAC[VAL_WORD_ADD;VAL_WORD;DIMINDEX_64;ARITH_RULE `1 MOD 2 EXP 64 = 1`; ADD_0] THEN + SUBGOAL_THEN `i < 2 EXP 64` ASSUME_TAC THENL [ + TRANS_TAC LT_TRANS `val (height:int64)` THEN + ASM_MESON_TAC[VAL_BOUND_64]; + ALL_TAC] THEN + SUBGOAL_THEN `i + 1 < 2 EXP 64` ASSUME_TAC THENL [ + TRANS_TAC LET_TRANS `val (height:int64)` THEN + CONJ_TAC THENL [ + UNDISCH_TAC `i < val (height:int64)` THEN ARITH_TAC; + REWRITE_TAC[VAL_BOUND_64]]; + + ALL_TAC] THEN + IMP_REWRITE_TAC[MOD_LT; VAL_BOUND_64] THEN + + ASM_CASES_TAC `i < val (idx:int64)` THENL [ + REWRITE_ASSUMES_TAC `i < val (idx:int64)` THEN + SUBGOAL_THEN `~(i = val (idx:int64))` (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm])) THENL [ + UNDISCH_TAC `i < val (idx:int64)` THEN ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `~(i > val (idx:int64))` (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm])) THENL [ + UNDISCH_TAC `i < val (idx:int64)` THEN ARITH_TAC; ALL_TAC] THEN + RULE_ASSUM_TAC (REWRITE_RULE [ARITH_RULE `x - 0 = x`]) THEN + ASM_REWRITE_TAC[] THEN DISJ1_TAC THEN + UNDISCH_TAC `i < val (idx:int64)` THEN ARITH_TAC; + + ASM_CASES_TAC `i = val (idx:int64)` THENL [ + REWRITE_ASSUMES_TAC `i = val (idx:int64)` THEN + RULE_ASSUM_TAC (REWRITE_RULE [LT_REFL; GT_REFL; SUB_0]) THEN + SPLIT_FIRST_CONJ_ASSUM_TAC THEN DISJ2_TAC THEN + ASM_REWRITE_TAC[ARITH_RULE `p + 1 > p`] THEN + IMP_REWRITE_TAC[LOWDIGITS_SELF] THEN + EXPAND_TAC "m" THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[SUB_0; BIGNUM_FROM_MEMORY_BOUND]; + + REWRITE_ASSUMES_TAC `~(i = val (idx:int64))` THEN + REWRITE_ASSUMES_TAC `~(i < val (idx:int64))` THEN + REPEAT SPLIT_FIRST_CONJ_ASSUM_TAC THEN (* get `i > val idx` *) + RULE_ASSUM_TAC (REWRITE_RULE [SUB_0]) THEN + DISJ2_TAC THEN + ASM_SIMP_TAC[ARITH_RULE `x > y ==> x + 1 > y`; ASSUME `i > val (idx:int64)`] THEN + ASM_REWRITE_TAC[LOWDIGITS_EQ_SELF] + ]] + + ] THEN + + REPEAT STRIP_TAC THEN REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN + + MATCH_MP_TAC ENSURES_FRAME_SUBSUMED THEN + EXISTS_TAC `MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [memory :> bytes64 (word (val (z:int64) + 8 * (val (width:int64) - (i' + 1))))]` THEN + REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN + CONJ_TAC THENL [ + REPEAT(MATCH_MP_TAC SUBSUMED_SEQ THEN REWRITE_TAC[SUBSUMED_REFL]) THEN + (* SIMPLE_ARITH_TAC isn't good at dealing with assumptions containing 'val'. Let's abbreviate + val width. *) + REWRITE_TAC[WORD_ADD; WORD_VAL] THEN + ABBREV_TAC `w' = val (width:int64)` THEN + SUBSUMED_MAYCHANGE_TAC; + + ALL_TAC] THEN + + ENSURES_INIT_TAC "s0" THEN + + ABBREV_TAC `p = read + (memory :> bytes64 (word_add table + (word (8 * (i * val (width:int64) + val (width:int64) - (i' + 1)))):int64)) + s0` THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [1] THEN + ABBREV_TAC `q = read + (memory :> bytes64 (word_add z + (word (8 * (val (width:int64) - (i' + 1))):int64))) s1` THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [2;3;4] THEN + SUBGOAL_THEN `val (width:int64) - (i'+1) < val width` ASSUME_TAC THENL [ + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `i * val (width:int64) + val (width:int64) - (i' + 1) < + val (height:int64) * val (width:int64)` ASSUME_TAC THENL [ + TRANS_TAC LTE_TRANS `i * val (width:int64) + val (width:int64)` THEN + IMP_REWRITE_TAC[LE_MULT_ADD] THEN + REWRITE_TAC[LT_ADD_LCANCEL] THEN ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `8 * (val (width:int64) - (i' + 1)) + 8 * (i' + 1) <= + 18446744073709551616` ASSUME_TAC THENL [ + REWRITE_TAC[GSYM LEFT_ADD_DISTRIB] THEN + IMP_REWRITE_TAC[SUB_ADD] THEN + ASM_ARITH_TAC; ALL_TAC] THEN + + ASM_CASES_TAC `i = val (idx:int64)` THENL [ + (* case 1 *) + REWRITE_TAC[ASSUME `i = val (idx:int64)`; LT_REFL; GT_REFL] THEN + REWRITE_ASSUMES_TAC `i = val (idx:int64)` THEN + RULE_ASSUM_TAC (REWRITE_RULE [LT_REFL; GT_REFL]) THEN + SPLIT_FIRST_CONJ_ASSUM_TAC THEN + SUBGOAL_THEN ` + q:int64 = word 0 /\ + read (memory :> + bytes (word_add z (word (8 * (val (width:int64) - i'))),8 * i')) s4 = 0` + (fun thm -> MAP_EVERY ASSUME_TAC (let x,y=CONJ_PAIR thm in [x;y])) THENL [ + CONJ_TAC THENL [ + EXPAND_TAC "q" THEN REWRITE_TAC[GSYM VAL_EQ] THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_SING; VAL_WORD_0] THEN + SUBGOAL_THEN `!z. (z:int64,1) = (z:int64, MIN (i'+1) 1)` (fun thm -> REWRITE_TAC[thm]) THENL [ + STRIP_TAC THEN REWRITE_TAC[MIN] THEN AP_TERM_TAC THEN ARITH_TAC; + ALL_TAC] THEN + ASM_REWRITE_TAC[GSYM LOWDIGITS_BIGNUM_FROM_MEMORY; BIGNUM_FROM_MEMORY_BYTES; LOWDIGITS_TRIVIAL]; + + UNDISCH_TAC `read + (memory :> + bytes (word_add z (word (8 * (val (width:int64) - (i' + 1)))):int64, + 8 * (i' + 1))) s4 = 0` THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[PAIR_EQ_ARITH_RULE `(temp:int64,i'+1)` `(temp:int64,1+i')`] THEN + REWRITE_TAC[BIGNUM_FROM_MEMORY_SPLIT] THEN + REWRITE_TAC[ADD_EQ_0; MULT_EQ_0; ARITH_RULE `~(2 EXP (64 * 1) = 0)`] THEN + SUBGOAL_THEN + `word_add (word_add (z:int64) (word (8 * (val (width:int64) - (i' + 1))):int64):int64) + (word (8 * 1)):int64 = + word_add z (word (8 * (val (width:int64) - i')):int64)` + (fun thm -> REWRITE_TAC[thm]) THENL [ + REWRITE_TAC[WORD_ADD_ASSOC_CONSTS] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC; + + ALL_TAC] THEN + MESON_TAC[] + ]; + + ALL_TAC + ] THEN + + SUBST_ALL_TAC (ASSUME `q=word 0:int64`) THEN + SUBGOAL_THEN `val (width:int64) - (i' + 1) < val (width:int64) - i'` ASSUME_TAC THENL + [ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `8 * (val (width:int64) - i') + 8 * i' <= 18446744073709551616` ASSUME_TAC THENL [ + ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `8 * (val (width:int64) - (i' + 1)) + 8 <= 18446744073709551616` ASSUME_TAC THENL [ + ASM_ARITH_TAC; ALL_TAC] THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [5] THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [6;7;8] THEN + ENSURES_FINAL_STATE_TAC THEN + ASM_REWRITE_TAC[WORD_SUB_ADD; WORD_ADD_ASSOC_CONSTS] THEN + REPEAT CONJ_TAC THENL [ + REPEAT AP_TERM_TAC THEN + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + + REPEAT AP_TERM_TAC THEN + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + SUBGOAL_THEN `val (width:int64) - i' = val width - (i'+1) + 1` (fun thm -> REWRITE_TAC[thm]) THENL [ + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; ALL_TAC] THEN + ASM_REWRITE_TAC[BIGNUM_FROM_MEMORY_EQ_LOWDIGITS; BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[WORD_BLAST `word_and p (word 18446744073709551615) = p:int64`] THEN + MAP_EVERY EXPAND_TAC ["p";"m"] THEN + ONCE_REWRITE_TAC[GSYM VAL_EQ] THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[BIGDIGIT_BIGNUM_FROM_MEMORY] THEN + SUBGOAL_THEN `val (width:int64) - (i' + 1) < val width` (fun thm->REWRITE_TAC[thm]) THENL [ + UNDISCH_TAC `i' val (idx:int64))` ASSUME_TAC THENL + [UNDISCH_TAC `i < val (idx:int64)` THEN ARITH_TAC; ALL_TAC] THEN + REWRITE_TAC [ASSUME `~(i > val (idx:int64))`] THEN + REWRITE_ASSUMES_TAC `~(i > val (idx:int64))` THEN + SUBGOAL_THEN `q = word 0:int64` SUBST_ALL_TAC THENL [ + EXPAND_TAC "q" THEN REWRITE_TAC[GSYM VAL_EQ] THEN + IMP_REWRITE_TAC[READ_MEMORY_BYTES_FIRSTELEM] THEN + MAP_EVERY EXISTS_TAC [`0:num`; `i'+1:num`] THEN + ASM_REWRITE_TAC[HIGHDIGITS_TRIVIAL; LOWDIGITS_TRIVIAL; VAL_WORD_0] THEN + ARITH_TAC; + + ALL_TAC] THEN + SPLIT_FIRST_CONJ_ASSUM_TAC THEN + ASSERT_USING_ASM_ARITH_TAC `8 * (val (width:int64) - (i' + 1)) + 8 <= 18446744073709551616` THEN + SUBGOAL_THEN `read (memory :> bytes + ((word_add (word_add (z:int64) (word (8 * (val (width:int64) - (i' + 1))))) (word (8 * 1))),8 * i')) + s4 = 0` (fun thm -> ASSUME_TAC (REWRITE_RULE [WORD_ADD_ASSOC_CONSTS] thm)) THENL + [IMP_REWRITE_TAC[READ_MEMORY_BYTES_SLICE; HIGHDIGITS_TRIVIAL; LOWDIGITS_TRIVIAL] THEN ARITH_TAC; + ALL_TAC] THEN + SUBGOAL_THEN `8 * (val (width:int64) - (i' + 1)) + 8 * 1 = 8 * (val (width:int64) - i')` + (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm])) THENL [ + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; ALL_TAC] THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `val (width:int64) - (i' + 1) < val (width:int64) - i'` `i' < val (width:int64)` THEN + ASSERT_USING_ASM_ARITH_TAC `8 * (val (width:int64) - i') + 8 * i' <= 18446744073709551616` THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [5] THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [6;7;8] THEN + ENSURES_FINAL_STATE_TAC THEN + ASM_REWRITE_TAC[WORD_SUB_ADD; WORD_ADD_ASSOC_CONSTS] THEN + REPEAT CONJ_TAC THENL [ + REPEAT AP_TERM_TAC THEN + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + + REPEAT AP_TERM_TAC THEN + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + + MATCH_MP_TAC (SPECL [`z:int64`; `(val (width:int64) - (i' + 1)):num`; `1:num`] READ_MEMORY_BYTES_MERGE) THEN + ASM_REWRITE_TAC[LOWDIGITS_TRIVIAL; HIGHDIGITS_TRIVIAL; ARITH_RULE `8*1=8`; READ_MEMORY_BYTES_BYTES64; + WORD_AND_0; VAL_WORD_0] THEN UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + + IMP_REWRITE_TAC[VAL_WORD; MOD_LT; DIMINDEX_64; LT_WORD_64] + ]; + + (* last case *) + ASSERT_USING_ASM_ARITH_TAC `i > val (idx:int64)` THEN + MAP_EVERY (fun t -> REWRITE_TAC [ASSUME t] THEN REWRITE_ASSUMES_TAC t) + [`i > val (idx:int64)`; `~(i = val (idx:int64))`; `~(i < val (idx:int64))`] THEN + SPLIT_FIRST_CONJ_ASSUM_TAC THEN + ASSERT_USING_ASM_ARITH_TAC `8 * (val (width:int64) - (i' + 1)) + 8 <= 18446744073709551616` THEN + SUBGOAL_THEN ` + q:int64 = word (lowdigits (highdigits m (val (width:int64) - (i' + 1))) 1) /\ + read (memory :> + bytes (word_add z (word (8 * (val width - i'))),8 * i')) s4 = highdigits m (val width - i')` + (fun thm -> MAP_EVERY ASSUME_TAC (let x,y=CONJ_PAIR thm in [x;y])) THENL [ + CONJ_TAC THENL [ + EXPAND_TAC "q" THEN + REWRITE_TAC[GSYM VAL_EQ] THEN + REWRITE_TAC[VAL_WORD; DIMINDEX_64] THEN + SUBGOAL_THEN `!x. (lowdigits x 1) MOD 2 EXP 64 = lowdigits x 1` (fun thm -> REWRITE_TAC [thm]) THENL [ + STRIP_TAC THEN IMP_REWRITE_TAC[MOD_LT] THEN ONCE_REWRITE_TAC[ARITH_RULE `64=64*1`] THEN MESON_TAC[LOWDIGITS_BOUND]; + ALL_TAC + ] THEN + MATCH_MP_TAC READ_MEMORY_BYTES_FIRSTELEM THEN + EXISTS_TAC `i'+1` THEN CONJ_TAC THENL [ARITH_TAC; ASM_REWRITE_TAC[]]; + + SUBGOAL_THEN + `word_add z (word (8 * (val (width:int64) - i'))):int64 = + word_add (word_add z (word (8 * (val width - (i'+1))))) (word (8 * 1))` (fun thm->ONCE_REWRITE_TAC[thm]) THENL + [REWRITE_TAC[WORD_ADD_ASSOC_CONSTS] THEN REPEAT AP_TERM_TAC THEN UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + ALL_TAC] THEN + IMP_REWRITE_TAC[READ_MEMORY_BYTES_SLICE_HIGH] THEN + REWRITE_TAC[HIGHDIGITS_HIGHDIGITS] THEN CONJ_TAC THENL [REPEAT AP_TERM_TAC THEN ASM_ARITH_TAC; ASM_ARITH_TAC] + ]; + + ALL_TAC + ] THEN + + ASSERT_USING_ASM_ARITH_TAC `val (width:int64) - (i' + 1) < val width - i'` THEN + ASSERT_USING_ASM_ARITH_TAC `8 * (val (width:int64) - i') + 8 * i' <= 18446744073709551616` THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [5] THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_EXEC [6;7;8] THEN + ENSURES_FINAL_STATE_TAC THEN + ASM_REWRITE_TAC[WORD_SUB_ADD; WORD_ADD_ASSOC_CONSTS] THEN + REPEAT CONJ_TAC THENL [ + REPEAT AP_TERM_TAC THEN + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + + REPEAT AP_TERM_TAC THEN + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + + MATCH_MP_TAC (SPECL [`z:int64`; `(val (width:int64) - (i' + 1)):num`; `1:num`] READ_MEMORY_BYTES_MERGE) THEN + ASM_REWRITE_TAC[ARITH_RULE `8*1=8`; READ_MEMORY_BYTES_BYTES64; LOWDIGITS_LOWDIGITS; + WORD_OR_0; WORD_AND_0; VAL_WORD] THEN + REPEAT CONJ_TAC THENL [ + AP_TERM_TAC THEN ARITH_TAC; + + SUBGOAL_THEN `!x. (lowdigits x 1) MOD 2 EXP 64 = lowdigits x 1` (fun thm -> REWRITE_TAC [DIMINDEX_64; thm]) THENL [ + STRIP_TAC THEN IMP_REWRITE_TAC[MOD_LT] THEN ONCE_REWRITE_TAC[ARITH_RULE `64=64*1`] THEN MESON_TAC[LOWDIGITS_BOUND]; + ALL_TAC + ] THEN + REWRITE_TAC[lowdigits; highdigits] THEN + REWRITE_TAC[DIV_MOD] THEN + AP_THM_TAC THEN REPEAT AP_TERM_TAC THEN + REWRITE_TAC[GSYM EXP_ADD] THEN + AP_TERM_TAC THEN + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + + UNDISCH_TAC `i' < val (width:int64)` THEN ARITH_TAC; + ]; + + REWRITE_TAC[VAL_WORD; DIMINDEX_64] THEN ASM_MESON_TAC[MOD_LT; LT_WORD_64] + ] + ] + ]);; + diff --git a/arm/proofs/bignum_copy_row_from_table_16_neon.ml b/arm/proofs/bignum_copy_row_from_table_16_neon.ml new file mode 100644 index 00000000..1ab24c47 --- /dev/null +++ b/arm/proofs/bignum_copy_row_from_table_16_neon.ml @@ -0,0 +1,338 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC + *) + +(* ========================================================================= *) +(* Constant-time table lookup. *) +(* ========================================================================= *) + +let bignum_copy_row_from_table_16_neon_mc = + define_assert_from_elf "bignum_copy_row_from_table_16_neon_mc" + "arm/generic/bignum_copy_row_from_table_16_neon.o" +[ + 0x4e080ff4; (* arm_DUP_GEN Q20 XZR *) + 0x4eb41e95; (* arm_MOV_VEC Q21 Q20 128 *) + 0x4eb41e96; (* arm_MOV_VEC Q22 Q20 128 *) + 0x4eb41e97; (* arm_MOV_VEC Q23 Q20 128 *) + 0x4eb41e98; (* arm_MOV_VEC Q24 Q20 128 *) + 0x4eb41e99; (* arm_MOV_VEC Q25 Q20 128 *) + 0x4eb41e9a; (* arm_MOV_VEC Q26 Q20 128 *) + 0x4eb41e9b; (* arm_MOV_VEC Q27 Q20 128 *) + 0xd2800006; (* arm_MOV X6 (rvalue (word 0)) *) + 0xeb0300df; (* arm_CMP X6 X3 *) + 0xda9f13e5; (* arm_CSETM X5 Condition_EQ *) + 0x4e080cb1; (* arm_DUP_GEN Q17 X5 *) + 0x3dc00030; (* arm_LDR Q16 X1 (Immediate_Offset (word 0)) *) + 0x6eb11e14; (* arm_BIT Q20 Q16 Q17 128 *) + 0x3dc00430; (* arm_LDR Q16 X1 (Immediate_Offset (word 16)) *) + 0x6eb11e15; (* arm_BIT Q21 Q16 Q17 128 *) + 0x3dc00830; (* arm_LDR Q16 X1 (Immediate_Offset (word 32)) *) + 0x6eb11e16; (* arm_BIT Q22 Q16 Q17 128 *) + 0x3dc00c30; (* arm_LDR Q16 X1 (Immediate_Offset (word 48)) *) + 0x6eb11e17; (* arm_BIT Q23 Q16 Q17 128 *) + 0x3dc01030; (* arm_LDR Q16 X1 (Immediate_Offset (word 64)) *) + 0x6eb11e18; (* arm_BIT Q24 Q16 Q17 128 *) + 0x3dc01430; (* arm_LDR Q16 X1 (Immediate_Offset (word 80)) *) + 0x6eb11e19; (* arm_BIT Q25 Q16 Q17 128 *) + 0x3dc01830; (* arm_LDR Q16 X1 (Immediate_Offset (word 96)) *) + 0x6eb11e1a; (* arm_BIT Q26 Q16 Q17 128 *) + 0x3dc01c30; (* arm_LDR Q16 X1 (Immediate_Offset (word 112)) *) + 0x6eb11e1b; (* arm_BIT Q27 Q16 Q17 128 *) + 0x91020021; (* arm_ADD X1 X1 (rvalue (word 128)) *) + 0x910004c6; (* arm_ADD X6 X6 (rvalue (word 1)) *) + 0xeb06005f; (* arm_CMP X2 X6 *) + 0x54fffd41; (* arm_BNE (word 2097064) *) + 0x3d800014; (* arm_STR Q20 X0 (Immediate_Offset (word 0)) *) + 0x3d800415; (* arm_STR Q21 X0 (Immediate_Offset (word 16)) *) + 0x3d800816; (* arm_STR Q22 X0 (Immediate_Offset (word 32)) *) + 0x3d800c17; (* arm_STR Q23 X0 (Immediate_Offset (word 48)) *) + 0x3d801018; (* arm_STR Q24 X0 (Immediate_Offset (word 64)) *) + 0x3d801419; (* arm_STR Q25 X0 (Immediate_Offset (word 80)) *) + 0x3d80181a; (* arm_STR Q26 X0 (Immediate_Offset (word 96)) *) + 0x3d801c1b; (* arm_STR Q27 X0 (Immediate_Offset (word 112)) *) + 0xd65f03c0 (* arm_RET X30 *) +];; + +let BIGNUM_COPY_ROW_FROM_TABLE_16_NEON_EXEC = + ARM_MK_EXEC_RULE bignum_copy_row_from_table_16_neon_mc;; + +(* ARITH_RULE for proving `lp=rp` where lp and rp are pairs *) +let PAIR_EQ_ARITH_RULE (lp,rp:term*term) = + let lpl,lpr = dest_pair lp in + let rpl,rpr = dest_pair rp in + let lth = ARITH_RULE (mk_eq (lpl,rpl)) in + let rth = ARITH_RULE (mk_eq (lpr,rpr)) in + let th = REFL lp in + let th = GEN_REWRITE_RULE (RAND_CONV o LAND_CONV) [lth] th in + GEN_REWRITE_RULE (RAND_CONV o RAND_CONV) [rth] th;; + +let REWRITE_ASSUMES_TAC (t:term) = + UNDISCH_THEN t (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm]) THEN ASSUME_TAC thm);; + +let LT_WORD_64 = prove(`!x (y:int64). x < val y ==> x < 2 EXP 64`, + REPEAT STRIP_TAC THEN + TRANS_TAC LT_TRANS `val (y:int64)` THEN + ONCE_REWRITE_TAC [GSYM DIMINDEX_64] THEN ASM_REWRITE_TAC[VAL_BOUND]);; + +let READ_MEMORY_BYTES_BYTES128 = prove(`!z s. + read (memory :> bytes (z,16)) s = val (read (memory :> bytes128 z) s)`, + REPEAT GEN_TAC THEN + REWRITE_TAC[fst (CONJ_PAIR READ_MEMORY_BYTESIZED_SPLIT)] THEN + REWRITE_TAC[VAL_WORD_JOIN;DIMINDEX_64;DIMINDEX_128] THEN + IMP_REWRITE_TAC[MOD_LT] THEN + REWRITE_TAC[ARITH_RULE`2 EXP 128 = 2 EXP 64 * 2 EXP 64`] THEN + IMP_REWRITE_TAC[LT_MULT_ADD_MULT] THEN + REWRITE_TAC[VAL_BOUND_64;ARITH_RULE`0<2 EXP 64`;LE_REFL] THEN + REWRITE_TAC[ARITH_RULE`16 = 8*(1+1)`;GSYM BIGNUM_FROM_MEMORY_BYTES;BIGNUM_FROM_MEMORY_STEP;BIGNUM_FROM_MEMORY_SING] THEN + REWRITE_TAC[ARITH_RULE`8*1=8`;ARITH_RULE`64*1=64`] THEN ARITH_TAC);; + +let ABBREV_TABLE_READ_128BITS_TAC name st ofs = + let v = mk_var (name, `:int128`) in + let templ = + if ofs = 0 then + `read (memory :> bytes128 (word_add table (word (8 * 16 * i)):int64)) s0` + else + let templ0 = `read (memory :> bytes128 (word_add table (word (8 * 16 * i + ofs)):int64)) s0` + in + let newofs = mk_numeral (Int ofs) in + subst [(newofs,`ofs:num`)] templ0 in + let rhs = subst [(mk_var(st,`:armstate`),`st0:armstate`)] templ in + ABBREV_TAC (mk_eq (v,rhs));; + +let VAL_WORD_JOIN_BIGDIGIT = prove( + `!m i j. val (word_join (word (bigdigit m i):int64) (word (bigdigit m j):int64):int128) = + 2 EXP 64 * (bigdigit m i) + bigdigit m j`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[VAL_WORD_JOIN; DIMINDEX_64; DIMINDEX_128; VAL_WORD] THEN + IMP_REWRITE_TAC[MOD_LT; BIGDIGIT_BOUND] THEN + REWRITE_TAC[ARITH_RULE `2 EXP 128 = 2 EXP 64 * 2 EXP 64`] THEN + IMP_REWRITE_TAC[LT_MULT_ADD_MULT; BIGDIGIT_BOUND; LE_REFL] THEN + ARITH_TAC);; + +let HELPER_RULE = prove(`!table i j k k1 m s. + read (memory :> bytes (word_add table (word i),8 * 16)) s = m /\ + j = i + 8 * k /\ k1 = k + 1 /\ k + 1 < 16 ==> + read (memory :> bytes128 (word_add table (word j))) s = + word_join (word (bigdigit m k1):int64) (word (bigdigit m k):int64)`, + REPEAT STRIP_TAC THEN + ASM_REWRITE_TAC[GSYM VAL_EQ; GSYM READ_MEMORY_BYTES_BYTES128;ARITH_RULE`16=8*2`] THEN + EXPAND_TAC "m" THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[VAL_WORD_JOIN_BIGDIGIT] THEN + REWRITE_TAC[ARITH_RULE `f (x, 2) = f (x, (1+1))`] THEN + REWRITE_TAC[BIGNUM_FROM_MEMORY_SPLIT] THEN + ASSERT_USING_ASM_ARITH_TAC `k < 16` THEN + ASM_REWRITE_TAC[BIGDIGIT_BIGNUM_FROM_MEMORY; BIGNUM_FROM_MEMORY_SING] THEN + REWRITE_TAC[WORD_ADD_ASSOC_CONSTS] THEN + REWRITE_TAC[ARITH_RULE`64*1=64`; ARITH_RULE`(i + 8 * k) + 8 * 1 = i + 8 * (k + 1)`]);; + +let HELPER_RULE2 = prove( + `!height idx. val idx < val height ==> + (val (word_sub height (word_add idx (word 1)):int64) = 0 <=> + val idx + 1 = val height)`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[VAL_WORD_SUB;VAL_WORD_ADD;DIMINDEX_64;VAL_WORD;ARITH_RULE`1 MOD 2 EXP 64 = 1`] THEN + SUBGOAL_THEN `val (height:int64) < 2 EXP 64` ASSUME_TAC THENL [REWRITE_TAC[VAL_BOUND_64]; ALL_TAC] THEN + SUBGOAL_THEN `(val (idx:int64) + 1) MOD 2 EXP 64 = val (idx:int64) + 1` + (fun thm -> REWRITE_TAC[thm]) THENL [MATCH_MP_TAC MOD_LT THEN ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `val (height:int64) + 2 EXP 64 - (val (idx:int64) + 1) = + 2 EXP 64 + val height - (val idx + 1)` (fun thm -> REWRITE_TAC[thm]) THENL [ + MATCH_MP_TAC ADD_SUB_SWAP THEN ASM_ARITH_TAC; ALL_TAC] THEN + + ONCE_REWRITE_TAC[GSYM ADD_MOD_MOD_REFL] THEN + REWRITE_TAC[MOD_REFL; ADD] THEN + IMP_REWRITE_TAC[MOD_LT] THEN + SUBGOAL_THEN `val (height:int64) - (val (idx:int64) + 1) < 2 EXP 64` ASSUME_TAC THENL [ + ASM_ARITH_TAC; ALL_TAC] THEN + ASM_SIMP_TAC[MOD_LT;SUB_EQ_0] THEN ASM_ARITH_TAC);; + +let HELPER_RULE3 = prove( + `!i (idx:int64). i < 2 EXP 64 /\ val idx < 2 EXP 64 /\ i < val idx ==> + ~(val (word_sub (word i) idx) = 0)`, + REWRITE_TAC[VAL_WORD_SUB;DIMINDEX_64] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN + SUBGOAL_THEN`val (word i:int64) = i` ASSUME_TAC THENL [ASM_SIMP_TAC[VAL_WORD;DIMINDEX_64;MOD_LT]; ALL_TAC] THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `(i + 2 EXP 64 - val (idx:int64)) < 2 EXP 64` (fun thm -> SIMP_TAC[MOD_LT; thm]) THEN + ASM_ARITH_TAC);; + +let HELPER_RULE4 = prove( + `!i (idx:int64). i < 2 EXP 64 /\ val idx < 2 EXP 64 /\ i > val idx ==> + ~(val (word_sub (word i) idx) = 0)`, + REWRITE_TAC[VAL_WORD_SUB;DIMINDEX_64] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN + SUBGOAL_THEN`val (word i:int64) = i` ASSUME_TAC THENL [ASM_SIMP_TAC[VAL_WORD;DIMINDEX_64;MOD_LT]; ALL_TAC] THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `i + 2 EXP 64 - val (idx:int64) = 2 EXP 64 + i - val (idx:int64)` + (fun thm -> REWRITE_TAC[thm]) THENL [ASM_ARITH_TAC;ALL_TAC] THEN + ONCE_REWRITE_TAC[GSYM ADD_MOD_MOD_REFL] THEN REWRITE_TAC[MOD_REFL;ADD] THEN IMP_REWRITE_TAC[MOD_LT] THEN ASM_ARITH_TAC);; + + + +let BIGNUM_COPY_ROW_FROM_TABLE_16_NEON_SUBROUTINE_CORRECT = prove( + `!z table height idx pc n m returnaddress. + nonoverlapping (word pc, 0xbc) (z, 8 * 16) /\ + nonoverlapping (word pc, 0xbc) (table, 8 * val height * 16) /\ + nonoverlapping (z, 8 * 16) (table, 8 * val height * 16) /\ + val idx < val height + ==> ensures arm + (\s. aligned_bytes_loaded s (word pc) bignum_copy_row_from_table_16_neon_mc /\ + read PC s = word pc /\ + read X30 s = returnaddress /\ + C_ARGUMENTS [z; table; height; idx] s /\ + bignum_from_memory (table, val height * 16) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * 16)), 16) s = m) + (\s. read PC s = returnaddress /\ + bignum_from_memory (z, 16) s = m) + (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [memory :> bytes(z,8 * 16)])`, + + REPEAT GEN_TAC THEN REWRITE_TAC[C_ARGUMENTS; NONOVERLAPPING_CLAUSES; + MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN + REPEAT STRIP_TAC THEN + + (* bignum_copy_row_from_table_16_neon_loop *) + ENSURES_WHILE_PUP_TAC `val (height:64 word):num` `pc + 0x24` `pc + 0x7c` + `\i s. (read X30 s = returnaddress /\ read X0 s = z /\ read X2 s = height /\ read X3 s = idx /\ + read X6 s = word i /\ + read X1 s = word_add table (word (8 * 16 * i)) /\ + bignum_from_memory (table, val height * 16) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * 16)), 16) s = m /\ + ((i <= val idx /\ + read Q20 s = word 0 /\ read Q21 s = word 0 /\ read Q22 s = word 0 /\ read Q23 s = word 0 /\ + read Q24 s = word 0 /\ read Q25 s = word 0 /\ read Q26 s = word 0 /\ read Q27 s = word 0) \/ + (i > val idx /\ + read Q20 s = word_join (word (bigdigit m 1):64 word) (word (bigdigit m 0):64 word) /\ + read Q21 s = word_join (word (bigdigit m 3):64 word) (word (bigdigit m 2):64 word) /\ + read Q22 s = word_join (word (bigdigit m 5):64 word) (word (bigdigit m 4):64 word) /\ + read Q23 s = word_join (word (bigdigit m 7):64 word) (word (bigdigit m 6):64 word) /\ + read Q24 s = word_join (word (bigdigit m 9):64 word) (word (bigdigit m 8):64 word) /\ + read Q25 s = word_join (word (bigdigit m 11):64 word) (word (bigdigit m 10):64 word) /\ + read Q26 s = word_join (word (bigdigit m 13):64 word) (word (bigdigit m 12):64 word) /\ + read Q27 s = word_join (word (bigdigit m 15):64 word) (word (bigdigit m 14):64 word)))) /\ + (read ZF s <=> i = val height)` THEN REPEAT CONJ_TAC THENL [ + (* 1. height > 0 *) + ASM_ARITH_TAC; + + (* 2. to loop start *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_16_NEON_EXEC (1--9) THEN + REWRITE_TAC[ARITH_RULE `x * 0 = 0`; ARITH_RULE `0 * x = 0`; WORD_ADD_0] THEN + ASM_REWRITE_TAC[LE_0]; + + (* 3. loop body - pass *) + ALL_TAC; + + (* 4. loop backedge *) + REPEAT STRIP_TAC THEN + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_16_NEON_EXEC (1--1); + + (* to return *) + SUBGOAL_THEN `val (height:int64) > val (idx:int64)` (fun thm -> REWRITE_TAC[thm]) THENL [ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `~(val (height:int64) <= val (idx:int64))` (fun thm -> REWRITE_TAC[thm]) THENL [ASM_ARITH_TAC; ALL_TAC] THEN + ENSURES_INIT_TAC "s0" THEN + SUBGOAL_THEN `m < 2 EXP (64 * 16)` ASSUME_TAC THENL [EXPAND_TAC "m" THEN REWRITE_TAC[BIGNUM_FROM_MEMORY_BOUND]; ALL_TAC] THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_16_NEON_EXEC (1--10) THEN + ENSURES_FINAL_STATE_TAC THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[ARITH_RULE`16 = 2+2+2+2+2+2+2+2`] THEN + REWRITE_TAC[BIGNUM_FROM_MEMORY_SPLIT;WORD_ADD_ASSOC_CONSTS] THEN + REWRITE_TAC(map ARITH_RULE [`8*2=16`;`16+16=32`;`16+32=48`;`16+48=64`;`16+64=80`;`16+80=96`;`16+96=112`]) THEN + ASM_REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES;ARITH_RULE`8*2=16`;READ_MEMORY_BYTES_BYTES128] THEN + REWRITE_TAC[VAL_WORD_JOIN;DIMINDEX_64;DIMINDEX_128] THEN + IMP_REWRITE_TAC[VAL_WORD;DIMINDEX_64;MOD_LT;VAL_BOUND_64;BIGDIGIT_BOUND] THEN + IMP_REWRITE_TAC[ARITH_RULE`2 EXP 128 = 2 EXP 64 * 2 EXP 64`;LT_MULT_ADD_MULT;ARITH_RULE`0 < 2 EXP 64`;BIGDIGIT_BOUND;LE_REFL] THEN + GEN_REWRITE_TAC RAND_CONV [GSYM HIGHDIGITS_0] THEN + REPEAT_N 16 (ONCE_REWRITE_TAC[HIGHDIGITS_STEP]) THEN + CONV_TAC (DEPTH_CONV NUM_ADD_CONV) THEN + SUBGOAL_THEN `highdigits m 16 = 0` (fun thm -> REWRITE_TAC[thm]) THENL [ASM_REWRITE_TAC[HIGHDIGITS_EQ_0]; ALL_TAC] + THEN ARITH_TAC + ] THEN + + REPEAT STRIP_TAC THEN + REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN + + ENSURES_INIT_TAC "s0" THEN + REPEAT_I_N 0 8 (fun i-> ABBREV_TABLE_READ_128BITS_TAC ("tmp" ^ string_of_int i) "s0" (16*i)) THEN + + ASM_CASES_TAC `i <= val (idx:int64)` THENL [ + REWRITE_ASSUMES_TAC `i <= val (idx:int64)` THEN + ASSERT_USING_ASM_ARITH_TAC `~(i > val (idx:int64))` THEN + REWRITE_ASSUMES_TAC `~(i > val (idx:int64))` THEN + REPEAT SPLIT_FIRST_CONJ_ASSUM_TAC THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_16_NEON_EXEC (1--22) THEN + ASM_CASES_TAC `i = val (idx:int64)` THENL [ + ASSERT_USING_UNDISCH_AND_ARITH_TAC `i + 1 > val (idx:int64)` `i = val (idx:int64)` THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `~(i + 1 <= val (idx:int64))` `i = val (idx:int64)` THEN + REWRITE_TAC(map ASSUME [`i + 1 > val (idx:int64)`; `~(i + 1 <= val (idx:int64))`]) THEN + ENSURES_FINAL_STATE_TAC THEN + ASM_REWRITE_TAC[] THEN + REWRITE_TAC[WORD_AND_0; WORD_VAL; WORD_SUB_REFL; VAL_WORD_0; WORD_OR_0; + WORD_BLAST `word_and (x:int128) (word_join (word 18446744073709551615:int64) + (word 18446744073709551615:int64):int128) = x`] THEN + DISCARD_MATCHING_ASSUMPTIONS [`read Q16 s22 = tmp7`] THEN + REPEAT CONJ_TAC THEN TRY (CONV_TAC WORD_RULE) THENL + (* solve equalities involving tmp0 ~ tmp7 *) + (let t = MATCH_MP_TAC HELPER_RULE THEN EXISTS_TAC `8 * i * 16` THEN + ASM_REWRITE_TAC[] THEN ARITH_TAC in + (map (fun i -> EXPAND_TAC ("tmp" ^ string_of_int i) THEN t) (0--7)) @ [ALL_TAC]) THEN + IMP_REWRITE_TAC[HELPER_RULE2]; + + SUBGOAL_THEN `i+1 <= val (idx:int64)` (fun thm -> REWRITE_TAC[thm]) THENL + [MAP_EVERY UNDISCH_TAC [`~(i = val (idx:int64))`; `i <= val (idx:int64)`] THEN ARITH_TAC;ALL_TAC] THEN + SUBGOAL_THEN `~((i+1) > val (idx:int64))` (fun thm -> REWRITE_TAC[thm]) THENL + [MAP_EVERY UNDISCH_TAC [`~(i = val (idx:int64))`; `i <= val (idx:int64)`] THEN ARITH_TAC;ALL_TAC] THEN + ENSURES_FINAL_STATE_TAC THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `~(val (word_sub (word i) idx:int64) = 0)` (fun thm -> REWRITE_TAC[thm]) THENL [ + MATCH_MP_TAC HELPER_RULE3 THEN REPEAT CONJ_TAC THENL [ + IMP_REWRITE_TAC[LT_WORD_64]; + IMP_REWRITE_TAC[LT_WORD_64]; + MAP_EVERY UNDISCH_TAC [`i <= val (idx:int64)`; `~(i = val (idx:int64))`] THEN ARITH_TAC + ]; + ALL_TAC] THEN + + REPEAT CONJ_TAC THEN TRY (CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC WORD_RULE) THEN + IMP_REWRITE_TAC[HELPER_RULE2] THEN + SUBGOAL_THEN `val (word i:int64)=i` (fun thm->REWRITE_TAC[thm]) THENL [ + SUBGOAL_THEN `i < 2 EXP 64` ASSUME_TAC THENL [ + IMP_REWRITE_TAC[LT_WORD_64]; + + ALL_TAC] THEN + IMP_REWRITE_TAC[VAL_WORD;MOD_LT;DIMINDEX_64]; + + ALL_TAC] THEN + ASM_REWRITE_TAC[] + ]; + + REWRITE_ASSUMES_TAC `~(i <= val (idx:int64))` THEN + REPEAT SPLIT_FIRST_CONJ_ASSUM_TAC THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `i + 1 > val (idx:int64)` `i > val (idx:int64)` THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `~(i + 1 <= val (idx:int64))` `i > val (idx:int64)` THEN + REWRITE_TAC(map ASSUME [`i + 1 > val (idx:int64)`; `~(i + 1 <= val (idx:int64))`]) THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_16_NEON_EXEC (1--22) THEN + ENSURES_FINAL_STATE_TAC THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `~(val (word_sub (word i) idx:int64) = 0)` (fun thm -> REWRITE_TAC[thm]) THENL [ + MATCH_MP_TAC HELPER_RULE4 THEN REPEAT CONJ_TAC THENL [ + MATCH_MP_TAC LT_WORD_64 THEN EXISTS_TAC `(height:int64)` THEN ASM_REWRITE_TAC[]; + REWRITE_TAC[VAL_BOUND_64]; + ASM_REWRITE_TAC[] + ]; + + ALL_TAC + ] THEN + REWRITE_TAC[ + WORD_BLAST `word_join (word 0:int64) (word 0:int64):int128 = word 0`; WORD_AND_0;WORD_OR_0; + WORD_BLAST `word_and (x:int128) (word_not (word 0)) = x`] THEN + REPEAT CONJ_TAC THEN TRY (CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC WORD_RULE) THEN + IMP_REWRITE_TAC[HELPER_RULE2] THEN + SUBGOAL_THEN `val (word i:int64)=i` (fun thm->REWRITE_TAC[thm]) THENL [ + SUBGOAL_THEN `i < 2 EXP 64` ASSUME_TAC THENL [ + IMP_REWRITE_TAC[LT_WORD_64]; + ALL_TAC + ] THEN + IMP_REWRITE_TAC[VAL_WORD;MOD_LT;DIMINDEX_64]; + + ALL_TAC + ] THEN + ASM_REWRITE_TAC[] + ]);; diff --git a/arm/proofs/bignum_copy_row_from_table_32_neon.ml b/arm/proofs/bignum_copy_row_from_table_32_neon.ml new file mode 100644 index 00000000..9b4f7987 --- /dev/null +++ b/arm/proofs/bignum_copy_row_from_table_32_neon.ml @@ -0,0 +1,365 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC + *) + +(* ========================================================================= *) +(* Constant-time table lookup. *) +(* ========================================================================= *) + +let bignum_copy_row_from_table_32_neon_mc = + define_assert_from_elf "bignum_copy_row_from_table_32_neon_mc" + "arm/generic/bignum_copy_row_from_table_32_neon.o" +[ + 0x4e080ff4; (* arm_DUP_GEN Q20 XZR *) + 0x4eb41e95; (* arm_MOV_VEC Q21 Q20 128 *) + 0x4eb41e96; (* arm_MOV_VEC Q22 Q20 128 *) + 0x4eb41e97; (* arm_MOV_VEC Q23 Q20 128 *) + 0x4eb41e98; (* arm_MOV_VEC Q24 Q20 128 *) + 0x4eb41e99; (* arm_MOV_VEC Q25 Q20 128 *) + 0x4eb41e9a; (* arm_MOV_VEC Q26 Q20 128 *) + 0x4eb41e9b; (* arm_MOV_VEC Q27 Q20 128 *) + 0x4eb41e9c; (* arm_MOV_VEC Q28 Q20 128 *) + 0x4eb41e9d; (* arm_MOV_VEC Q29 Q20 128 *) + 0x4eb41e9e; (* arm_MOV_VEC Q30 Q20 128 *) + 0x4eb41e9f; (* arm_MOV_VEC Q31 Q20 128 *) + 0x4eb41e80; (* arm_MOV_VEC Q0 Q20 128 *) + 0x4eb41e81; (* arm_MOV_VEC Q1 Q20 128 *) + 0x4eb41e82; (* arm_MOV_VEC Q2 Q20 128 *) + 0x4eb41e83; (* arm_MOV_VEC Q3 Q20 128 *) + 0xd2800006; (* arm_MOV X6 (rvalue (word 0)) *) + 0xeb0300df; (* arm_CMP X6 X3 *) + 0xda9f13e5; (* arm_CSETM X5 Condition_EQ *) + 0x4e080cb1; (* arm_DUP_GEN Q17 X5 *) + 0x3dc00030; (* arm_LDR Q16 X1 (Immediate_Offset (word 0)) *) + 0x6eb11e14; (* arm_BIT Q20 Q16 Q17 128 *) + 0x3dc00430; (* arm_LDR Q16 X1 (Immediate_Offset (word 16)) *) + 0x6eb11e15; (* arm_BIT Q21 Q16 Q17 128 *) + 0x3dc00830; (* arm_LDR Q16 X1 (Immediate_Offset (word 32)) *) + 0x6eb11e16; (* arm_BIT Q22 Q16 Q17 128 *) + 0x3dc00c30; (* arm_LDR Q16 X1 (Immediate_Offset (word 48)) *) + 0x6eb11e17; (* arm_BIT Q23 Q16 Q17 128 *) + 0x3dc01030; (* arm_LDR Q16 X1 (Immediate_Offset (word 64)) *) + 0x6eb11e18; (* arm_BIT Q24 Q16 Q17 128 *) + 0x3dc01430; (* arm_LDR Q16 X1 (Immediate_Offset (word 80)) *) + 0x6eb11e19; (* arm_BIT Q25 Q16 Q17 128 *) + 0x3dc01830; (* arm_LDR Q16 X1 (Immediate_Offset (word 96)) *) + 0x6eb11e1a; (* arm_BIT Q26 Q16 Q17 128 *) + 0x3dc01c30; (* arm_LDR Q16 X1 (Immediate_Offset (word 112)) *) + 0x6eb11e1b; (* arm_BIT Q27 Q16 Q17 128 *) + 0x3dc02030; (* arm_LDR Q16 X1 (Immediate_Offset (word 128)) *) + 0x6eb11e1c; (* arm_BIT Q28 Q16 Q17 128 *) + 0x3dc02430; (* arm_LDR Q16 X1 (Immediate_Offset (word 144)) *) + 0x6eb11e1d; (* arm_BIT Q29 Q16 Q17 128 *) + 0x3dc02830; (* arm_LDR Q16 X1 (Immediate_Offset (word 160)) *) + 0x6eb11e1e; (* arm_BIT Q30 Q16 Q17 128 *) + 0x3dc02c30; (* arm_LDR Q16 X1 (Immediate_Offset (word 176)) *) + 0x6eb11e1f; (* arm_BIT Q31 Q16 Q17 128 *) + 0x3dc03030; (* arm_LDR Q16 X1 (Immediate_Offset (word 192)) *) + 0x6eb11e00; (* arm_BIT Q0 Q16 Q17 128 *) + 0x3dc03430; (* arm_LDR Q16 X1 (Immediate_Offset (word 208)) *) + 0x6eb11e01; (* arm_BIT Q1 Q16 Q17 128 *) + 0x3dc03830; (* arm_LDR Q16 X1 (Immediate_Offset (word 224)) *) + 0x6eb11e02; (* arm_BIT Q2 Q16 Q17 128 *) + 0x3dc03c30; (* arm_LDR Q16 X1 (Immediate_Offset (word 240)) *) + 0x6eb11e03; (* arm_BIT Q3 Q16 Q17 128 *) + 0x91040021; (* arm_ADD X1 X1 (rvalue (word 256)) *) + 0x910004c6; (* arm_ADD X6 X6 (rvalue (word 1)) *) + 0xeb06005f; (* arm_CMP X2 X6 *) + 0x54fffb41; (* arm_BNE (word 2097000) *) + 0x3d800014; (* arm_STR Q20 X0 (Immediate_Offset (word 0)) *) + 0x3d800415; (* arm_STR Q21 X0 (Immediate_Offset (word 16)) *) + 0x3d800816; (* arm_STR Q22 X0 (Immediate_Offset (word 32)) *) + 0x3d800c17; (* arm_STR Q23 X0 (Immediate_Offset (word 48)) *) + 0x3d801018; (* arm_STR Q24 X0 (Immediate_Offset (word 64)) *) + 0x3d801419; (* arm_STR Q25 X0 (Immediate_Offset (word 80)) *) + 0x3d80181a; (* arm_STR Q26 X0 (Immediate_Offset (word 96)) *) + 0x3d801c1b; (* arm_STR Q27 X0 (Immediate_Offset (word 112)) *) + 0x3d80201c; (* arm_STR Q28 X0 (Immediate_Offset (word 128)) *) + 0x3d80241d; (* arm_STR Q29 X0 (Immediate_Offset (word 144)) *) + 0x3d80281e; (* arm_STR Q30 X0 (Immediate_Offset (word 160)) *) + 0x3d802c1f; (* arm_STR Q31 X0 (Immediate_Offset (word 176)) *) + 0x3d803000; (* arm_STR Q0 X0 (Immediate_Offset (word 192)) *) + 0x3d803401; (* arm_STR Q1 X0 (Immediate_Offset (word 208)) *) + 0x3d803802; (* arm_STR Q2 X0 (Immediate_Offset (word 224)) *) + 0x3d803c03; (* arm_STR Q3 X0 (Immediate_Offset (word 240)) *) + 0xd65f03c0 (* arm_RET X30 *) +];; + +let BIGNUM_COPY_ROW_FROM_TABLE_32_NEON_EXEC = + ARM_MK_EXEC_RULE bignum_copy_row_from_table_32_neon_mc;; + + +let REWRITE_ASSUMES_TAC (t:term) = + UNDISCH_THEN t (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm]) THEN ASSUME_TAC thm);; + +let LT_WORD_64 = prove(`!x (y:int64). x < val y ==> x < 2 EXP 64`, + REPEAT STRIP_TAC THEN + TRANS_TAC LT_TRANS `val (y:int64)` THEN + ONCE_REWRITE_TAC [GSYM DIMINDEX_64] THEN ASM_REWRITE_TAC[VAL_BOUND]);; + +let READ_MEMORY_BYTES_BYTES128 = prove(`!z s. + read (memory :> bytes (z,16)) s = val (read (memory :> bytes128 z) s)`, + REPEAT GEN_TAC THEN + REWRITE_TAC[fst (CONJ_PAIR READ_MEMORY_BYTESIZED_SPLIT)] THEN + REWRITE_TAC[VAL_WORD_JOIN;DIMINDEX_64;DIMINDEX_128] THEN + IMP_REWRITE_TAC[MOD_LT] THEN + REWRITE_TAC[ARITH_RULE`2 EXP 128 = 2 EXP 64 * 2 EXP 64`] THEN + IMP_REWRITE_TAC[LT_MULT_ADD_MULT] THEN + REWRITE_TAC[VAL_BOUND_64;ARITH_RULE`0<2 EXP 64`;LE_REFL] THEN + REWRITE_TAC[ARITH_RULE`16 = 8*(1+1)`;GSYM BIGNUM_FROM_MEMORY_BYTES;BIGNUM_FROM_MEMORY_STEP;BIGNUM_FROM_MEMORY_SING] THEN + REWRITE_TAC[ARITH_RULE`8*1=8`;ARITH_RULE`64*1=64`] THEN ARITH_TAC);; + + +let ABBREV_TABLE_READ_128BITS_TAC name st ofs = + let v = mk_var (name, `:int128`) in + let templ = + if ofs = 0 then + `read (memory :> bytes128 (word_add table (word (8 * 32 * i)):int64)) s0` + else + let templ0 = `read (memory :> bytes128 (word_add table (word (8 * 32 * i + ofs)):int64)) s0` + in + let newofs = mk_numeral (Int ofs) in + subst [(newofs,`ofs:num`)] templ0 in + let rhs = subst [(mk_var(st,`:armstate`),`st0:armstate`)] templ in + ABBREV_TAC (mk_eq (v,rhs));; + +let VAL_WORD_JOIN_BIGDIGIT = prove( + `!m i j. val (word_join (word (bigdigit m i):int64) (word (bigdigit m j):int64):int128) = + 2 EXP 64 * (bigdigit m i) + bigdigit m j`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[VAL_WORD_JOIN; DIMINDEX_64; DIMINDEX_128; VAL_WORD] THEN + IMP_REWRITE_TAC[MOD_LT; BIGDIGIT_BOUND] THEN + REWRITE_TAC[ARITH_RULE `2 EXP 128 = 2 EXP 64 * 2 EXP 64`] THEN + IMP_REWRITE_TAC[LT_MULT_ADD_MULT; BIGDIGIT_BOUND; LE_REFL] THEN + ARITH_TAC);; + +let HELPER_RULE = prove(`!table i j k k1 m s. + read (memory :> bytes (word_add table (word i),8 * 32)) s = m /\ + j = i + 8 * k /\ k1 = k + 1 /\ k + 1 < 32 ==> + read (memory :> bytes128 (word_add table (word j))) s = + word_join (word (bigdigit m k1):int64) (word (bigdigit m k):int64)`, + REPEAT STRIP_TAC THEN + ASM_REWRITE_TAC[GSYM VAL_EQ; GSYM READ_MEMORY_BYTES_BYTES128;ARITH_RULE`16=8*2`] THEN + EXPAND_TAC "m" THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[VAL_WORD_JOIN_BIGDIGIT] THEN + REWRITE_TAC[ARITH_RULE `f (x, 2) = f (x, (1+1))`] THEN + REWRITE_TAC[BIGNUM_FROM_MEMORY_SPLIT] THEN + ASSERT_USING_ASM_ARITH_TAC `k < 32` THEN + ASM_REWRITE_TAC[BIGDIGIT_BIGNUM_FROM_MEMORY; BIGNUM_FROM_MEMORY_SING] THEN + REWRITE_TAC[WORD_ADD_ASSOC_CONSTS] THEN + REWRITE_TAC[ARITH_RULE`64*1=64`; ARITH_RULE`(i + 8 * k) + 8 * 1 = i + 8 * (k + 1)`]);; + +let HELPER_RULE2 = prove( + `!height idx. val idx < val height ==> + (val (word_sub height (word_add idx (word 1)):int64) = 0 <=> + val idx + 1 = val height)`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[VAL_WORD_SUB;VAL_WORD_ADD;DIMINDEX_64;VAL_WORD;ARITH_RULE`1 MOD 2 EXP 64 = 1`] THEN + SUBGOAL_THEN `val (height:int64) < 2 EXP 64` ASSUME_TAC THENL [REWRITE_TAC[VAL_BOUND_64]; ALL_TAC] THEN + SUBGOAL_THEN `(val (idx:int64) + 1) MOD 2 EXP 64 = val (idx:int64) + 1` + (fun thm -> REWRITE_TAC[thm]) THENL [MATCH_MP_TAC MOD_LT THEN ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `val (height:int64) + 2 EXP 64 - (val (idx:int64) + 1) = + 2 EXP 64 + val height - (val idx + 1)` (fun thm -> REWRITE_TAC[thm]) THENL [ + MATCH_MP_TAC ADD_SUB_SWAP THEN ASM_ARITH_TAC; ALL_TAC] THEN + + ONCE_REWRITE_TAC[GSYM ADD_MOD_MOD_REFL] THEN + REWRITE_TAC[MOD_REFL; ADD] THEN + IMP_REWRITE_TAC[MOD_LT] THEN + SUBGOAL_THEN `val (height:int64) - (val (idx:int64) + 1) < 2 EXP 64` ASSUME_TAC THENL [ + ASM_ARITH_TAC; ALL_TAC] THEN + ASM_SIMP_TAC[MOD_LT;SUB_EQ_0] THEN ASM_ARITH_TAC);; + +let HELPER_RULE3 = prove( + `!i (idx:int64). i < 2 EXP 64 /\ val idx < 2 EXP 64 /\ i < val idx ==> + ~(val (word_sub (word i) idx) = 0)`, + REWRITE_TAC[VAL_WORD_SUB;DIMINDEX_64] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN + SUBGOAL_THEN`val (word i:int64) = i` ASSUME_TAC THENL [ASM_SIMP_TAC[VAL_WORD;DIMINDEX_64;MOD_LT]; ALL_TAC] THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `(i + 2 EXP 64 - val (idx:int64)) < 2 EXP 64` (fun thm -> SIMP_TAC[MOD_LT; thm]) THEN + ASM_ARITH_TAC);; + +let HELPER_RULE4 = prove( + `!i (idx:int64). i < 2 EXP 64 /\ val idx < 2 EXP 64 /\ i > val idx ==> + ~(val (word_sub (word i) idx) = 0)`, + REWRITE_TAC[VAL_WORD_SUB;DIMINDEX_64] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN + SUBGOAL_THEN`val (word i:int64) = i` ASSUME_TAC THENL [ASM_SIMP_TAC[VAL_WORD;DIMINDEX_64;MOD_LT]; ALL_TAC] THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `i + 2 EXP 64 - val (idx:int64) = 2 EXP 64 + i - val (idx:int64)` + (fun thm -> REWRITE_TAC[thm]) THENL [ASM_ARITH_TAC;ALL_TAC] THEN + ONCE_REWRITE_TAC[GSYM ADD_MOD_MOD_REFL] THEN REWRITE_TAC[MOD_REFL;ADD] THEN IMP_REWRITE_TAC[MOD_LT] THEN ASM_ARITH_TAC);; + + +let BIGNUM_COPY_ROW_FROM_TABLE_32_NEON_SUBROUTINE_CORRECT = prove( + `!z table height idx pc n m returnaddress. + nonoverlapping (word pc, 0x124) (z, 8 * 32) /\ + nonoverlapping (word pc, 0x124) (table, 8 * val height * 32) /\ + nonoverlapping (z, 8 * 16) (table, 8 * val height * 32) /\ + val idx < val height + ==> ensures arm + (\s. aligned_bytes_loaded s (word pc) bignum_copy_row_from_table_32_neon_mc /\ + read PC s = word pc /\ + read X30 s = returnaddress /\ + C_ARGUMENTS [z; table; height; idx] s /\ + bignum_from_memory (table, val height * 32) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * 32)), 32) s = m) + (\s. read PC s = returnaddress /\ + bignum_from_memory (z, 32) s = m) + (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [memory :> bytes(z,8 * 32)])`, + REPEAT GEN_TAC THEN REWRITE_TAC[C_ARGUMENTS; NONOVERLAPPING_CLAUSES; + MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN + REPEAT STRIP_TAC THEN + (* bignum_copy_row_from_table_32_neon_loop *) + ENSURES_WHILE_PUP_TAC `val (height:64 word):num` `pc + 0x44` `pc + 0xdc` + `\i s. (read X30 s = returnaddress /\ read X0 s = z /\ read X2 s = height /\ read X3 s = idx /\ + read X6 s = word i /\ + read X1 s = word_add table (word (8 * 32 * i)) /\ + bignum_from_memory (table, val height * 32) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * 32)), 32) s = m /\ + ((i <= val idx /\ + read Q20 s = word 0 /\ read Q21 s = word 0 /\ read Q22 s = word 0 /\ read Q23 s = word 0 /\ + read Q24 s = word 0 /\ read Q25 s = word 0 /\ read Q26 s = word 0 /\ read Q27 s = word 0 /\ + read Q28 s = word 0 /\ read Q29 s = word 0 /\ read Q30 s = word 0 /\ read Q31 s = word 0 /\ + read Q0 s = word 0 /\ read Q1 s = word 0 /\ read Q2 s = word 0 /\ read Q3 s = word 0) \/ + (i > val idx /\ + read Q20 s = word_join (word (bigdigit m 1):64 word) (word (bigdigit m 0):64 word) /\ + read Q21 s = word_join (word (bigdigit m 3):64 word) (word (bigdigit m 2):64 word) /\ + read Q22 s = word_join (word (bigdigit m 5):64 word) (word (bigdigit m 4):64 word) /\ + read Q23 s = word_join (word (bigdigit m 7):64 word) (word (bigdigit m 6):64 word) /\ + read Q24 s = word_join (word (bigdigit m 9):64 word) (word (bigdigit m 8):64 word) /\ + read Q25 s = word_join (word (bigdigit m 11):64 word) (word (bigdigit m 10):64 word) /\ + read Q26 s = word_join (word (bigdigit m 13):64 word) (word (bigdigit m 12):64 word) /\ + read Q27 s = word_join (word (bigdigit m 15):64 word) (word (bigdigit m 14):64 word) /\ + read Q28 s = word_join (word (bigdigit m 17):64 word) (word (bigdigit m 16):64 word) /\ + read Q29 s = word_join (word (bigdigit m 19):64 word) (word (bigdigit m 18):64 word) /\ + read Q30 s = word_join (word (bigdigit m 21):64 word) (word (bigdigit m 20):64 word) /\ + read Q31 s = word_join (word (bigdigit m 23):64 word) (word (bigdigit m 22):64 word) /\ + read Q0 s = word_join (word (bigdigit m 25):64 word) (word (bigdigit m 24):64 word) /\ + read Q1 s = word_join (word (bigdigit m 27):64 word) (word (bigdigit m 26):64 word) /\ + read Q2 s = word_join (word (bigdigit m 29):64 word) (word (bigdigit m 28):64 word) /\ + read Q3 s = word_join (word (bigdigit m 31):64 word) (word (bigdigit m 30):64 word)))) /\ + (read ZF s <=> i = val height)` THEN REPEAT CONJ_TAC THENL [ + (* 1. height > 0 *) + ASM_ARITH_TAC; + + (* 2. to loop start *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_32_NEON_EXEC (1--17) THEN + REWRITE_TAC[ARITH_RULE `x * 0 = 0`; ARITH_RULE `0 * x = 0`; WORD_ADD_0] THEN + ASM_REWRITE_TAC[LE_0]; + + (* 3. loop body - pass *) + ALL_TAC; + + (* 4. loop backedge *) + REPEAT STRIP_TAC THEN + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_32_NEON_EXEC (1--1); + + (* to return *) + SUBGOAL_THEN `val (height:int64) > val (idx:int64)` (fun thm -> REWRITE_TAC[thm]) THENL [ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `~(val (height:int64) <= val (idx:int64))` (fun thm -> REWRITE_TAC[thm]) THENL [ASM_ARITH_TAC; ALL_TAC] THEN + ENSURES_INIT_TAC "s0" THEN + SUBGOAL_THEN `m < 2 EXP (64 * 32)` ASSUME_TAC THENL [EXPAND_TAC "m" THEN REWRITE_TAC[BIGNUM_FROM_MEMORY_BOUND]; ALL_TAC] THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_32_NEON_EXEC (1--18) THEN + ENSURES_FINAL_STATE_TAC THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[ARITH_RULE`32 = 2+2+2+2+2+2+2+2+2+2+2+2+2+2+2+2`] THEN + REWRITE_TAC[BIGNUM_FROM_MEMORY_SPLIT;WORD_ADD_ASSOC_CONSTS] THEN + REWRITE_TAC(map ARITH_RULE [ + `8*2=16`;`16+16=32`;`16+32=48`;`16+48=64`;`16+64=80`;`16+80=96`;`16+96=112`; + `16+112=128`;`16+128=144`;`16+144=160`;`16+160=176`;`16+176=192`;`16+192=208`; + `16+208=224`;`16+224=240`;`16+240=256`]) THEN + ASM_REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES;ARITH_RULE`8*2=16`;READ_MEMORY_BYTES_BYTES128] THEN + REWRITE_TAC[VAL_WORD_JOIN;DIMINDEX_64;DIMINDEX_128] THEN + IMP_REWRITE_TAC[VAL_WORD;DIMINDEX_64;MOD_LT;VAL_BOUND_64;BIGDIGIT_BOUND] THEN + IMP_REWRITE_TAC[ARITH_RULE`2 EXP 128 = 2 EXP 64 * 2 EXP 64`;LT_MULT_ADD_MULT;ARITH_RULE`0 < 2 EXP 64`;BIGDIGIT_BOUND;LE_REFL] THEN + GEN_REWRITE_TAC RAND_CONV [GSYM HIGHDIGITS_0] THEN + REPEAT_N 32 (ONCE_REWRITE_TAC[HIGHDIGITS_STEP]) THEN + CONV_TAC (DEPTH_CONV NUM_ADD_CONV) THEN + SUBGOAL_THEN `highdigits m 32 = 0` (fun thm -> REWRITE_TAC[thm]) THENL [ASM_REWRITE_TAC[HIGHDIGITS_EQ_0]; ALL_TAC] + THEN ARITH_TAC + ] THEN + + REPEAT STRIP_TAC THEN + REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN + ENSURES_INIT_TAC "s0" THEN + REPEAT_I_N 0 16 (fun i-> ABBREV_TABLE_READ_128BITS_TAC ("tmp" ^ string_of_int i) "s0" (16*i)) THEN + ASM_CASES_TAC `i <= val (idx:int64)` THENL [ + REWRITE_ASSUMES_TAC `i <= val (idx:int64)` THEN + ASSERT_USING_ASM_ARITH_TAC `~(i > val (idx:int64))` THEN + REWRITE_ASSUMES_TAC `~(i > val (idx:int64))` THEN + REPEAT SPLIT_FIRST_CONJ_ASSUM_TAC THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_32_NEON_EXEC (1--38) THEN + ASM_CASES_TAC `i = val (idx:int64)` THENL [ + ASSERT_USING_UNDISCH_AND_ARITH_TAC `i + 1 > val (idx:int64)` `i = val (idx:int64)` THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `~(i + 1 <= val (idx:int64))` `i = val (idx:int64)` THEN + REWRITE_TAC(map ASSUME [`i + 1 > val (idx:int64)`; `~(i + 1 <= val (idx:int64))`]) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REWRITE_TAC[WORD_AND_0; WORD_VAL; WORD_SUB_REFL; VAL_WORD_0; WORD_OR_0; + WORD_BLAST `word_and (x:int128) (word_join (word 18446744073709551615:int64) + (word 18446744073709551615:int64):int128) = x`] THEN + DISCARD_MATCHING_ASSUMPTIONS [`read Q16 s38 = tmp15`] THEN + REPEAT CONJ_TAC THEN TRY (CONV_TAC WORD_RULE) THENL + (* solve equalities involving tmp0 ~ tmp15 *) + (let t = MATCH_MP_TAC HELPER_RULE THEN EXISTS_TAC `8 * i * 32` THEN + ASM_REWRITE_TAC[] THEN ARITH_TAC in + (map (fun i -> EXPAND_TAC ("tmp" ^ string_of_int i) THEN t) (0--15)) @ [ALL_TAC]) THEN + IMP_REWRITE_TAC[HELPER_RULE2]; + + SUBGOAL_THEN `i+1 <= val (idx:int64)` (fun thm -> REWRITE_TAC[thm]) THENL + [MAP_EVERY UNDISCH_TAC [`~(i = val (idx:int64))`; `i <= val (idx:int64)`] THEN ARITH_TAC;ALL_TAC] THEN + SUBGOAL_THEN `~((i+1) > val (idx:int64))` (fun thm -> REWRITE_TAC[thm]) THENL + [MAP_EVERY UNDISCH_TAC [`~(i = val (idx:int64))`; `i <= val (idx:int64)`] THEN ARITH_TAC;ALL_TAC] THEN + ENSURES_FINAL_STATE_TAC THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `~(val (word_sub (word i) idx:int64) = 0)` (fun thm -> REWRITE_TAC[thm]) THENL [ + MATCH_MP_TAC HELPER_RULE3 THEN REPEAT CONJ_TAC THENL [ + IMP_REWRITE_TAC[LT_WORD_64]; + IMP_REWRITE_TAC[LT_WORD_64]; + MAP_EVERY UNDISCH_TAC [`i <= val (idx:int64)`; `~(i = val (idx:int64))`] THEN ARITH_TAC + ]; + ALL_TAC] THEN + REPEAT CONJ_TAC THEN TRY (CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC WORD_RULE) THEN + IMP_REWRITE_TAC[HELPER_RULE2] THEN + SUBGOAL_THEN `val (word i:int64)=i` (fun thm->REWRITE_TAC[thm]) THENL [ + SUBGOAL_THEN `i < 2 EXP 64` ASSUME_TAC THENL [ + IMP_REWRITE_TAC[LT_WORD_64]; + + ALL_TAC] THEN + IMP_REWRITE_TAC[VAL_WORD;MOD_LT;DIMINDEX_64]; + + ALL_TAC] THEN + ASM_REWRITE_TAC[] + ]; + + REWRITE_ASSUMES_TAC `~(i <= val (idx:int64))` THEN + REPEAT SPLIT_FIRST_CONJ_ASSUM_TAC THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `i + 1 > val (idx:int64)` `i > val (idx:int64)` THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `~(i + 1 <= val (idx:int64))` `i > val (idx:int64)` THEN + REWRITE_TAC(map ASSUME [`i + 1 > val (idx:int64)`; `~(i + 1 <= val (idx:int64))`]) THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_32_NEON_EXEC (1--38) THEN + ENSURES_FINAL_STATE_TAC THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `~(val (word_sub (word i) idx:int64) = 0)` (fun thm -> REWRITE_TAC[thm]) THENL [ + MATCH_MP_TAC HELPER_RULE4 THEN REPEAT CONJ_TAC THENL [ + MATCH_MP_TAC LT_WORD_64 THEN EXISTS_TAC `(height:int64)` THEN ASM_REWRITE_TAC[]; + REWRITE_TAC[VAL_BOUND_64]; + ASM_REWRITE_TAC[]]; + + ALL_TAC + ] THEN + REWRITE_TAC[ + WORD_BLAST `word_join (word 0:int64) (word 0:int64):int128 = word 0`; WORD_AND_0;WORD_OR_0; + WORD_BLAST `word_and (x:int128) (word_not (word 0)) = x`] THEN + REPEAT CONJ_TAC THEN TRY (CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC WORD_RULE) THEN + IMP_REWRITE_TAC[HELPER_RULE2] THEN + SUBGOAL_THEN `val (word i:int64)=i` (fun thm->REWRITE_TAC[thm]) THENL [ + SUBGOAL_THEN `i < 2 EXP 64` ASSUME_TAC THENL [ + IMP_REWRITE_TAC[LT_WORD_64]; ALL_TAC] THEN + IMP_REWRITE_TAC[VAL_WORD;MOD_LT;DIMINDEX_64]; + + ALL_TAC + ] THEN + ASM_REWRITE_TAC[] + ]);; diff --git a/arm/proofs/bignum_copy_row_from_table_8n_neon.ml b/arm/proofs/bignum_copy_row_from_table_8n_neon.ml new file mode 100644 index 00000000..bba4d021 --- /dev/null +++ b/arm/proofs/bignum_copy_row_from_table_8n_neon.ml @@ -0,0 +1,873 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC + *) + +(* ========================================================================= *) +(* Constant-time table lookup. *) +(* ========================================================================= *) + +let bignum_copy_row_from_table_8n_neon_mc = + define_assert_from_elf "bignum_copy_row_from_table_8n_neon_mc" + "arm/generic/bignum_copy_row_from_table_8n_neon.o" +[ + 0xb4000542; (* arm_CBZ X2 (word 168) *) + 0xb4000523; (* arm_CBZ X3 (word 164) *) + 0xaa0303e5; (* arm_MOV X5 X3 *) + 0xaa0003e6; (* arm_MOV X6 X0 *) + 0x4e080ff0; (* arm_DUP_GEN Q16 XZR *) + 0x3d8000d0; (* arm_STR Q16 X6 (Immediate_Offset (word 0)) *) + 0x3d8004d0; (* arm_STR Q16 X6 (Immediate_Offset (word 16)) *) + 0x3d8008d0; (* arm_STR Q16 X6 (Immediate_Offset (word 32)) *) + 0x3d800cd0; (* arm_STR Q16 X6 (Immediate_Offset (word 48)) *) + 0x910100c6; (* arm_ADD X6 X6 (rvalue (word 64)) *) + 0xf10020a5; (* arm_SUBS X5 X5 (rvalue (word 8)) *) + 0x54ffff41; (* arm_BNE (word 2097128) *) + 0xaa1f03e5; (* arm_MOV X5 XZR *) + 0xaa0103e8; (* arm_MOV X8 X1 *) + 0xeb0400bf; (* arm_CMP X5 X4 *) + 0xda9f13e6; (* arm_CSETM X6 Condition_EQ *) + 0x4e080cd0; (* arm_DUP_GEN Q16 X6 *) + 0xaa0303e7; (* arm_MOV X7 X3 *) + 0xaa0003e9; (* arm_MOV X9 X0 *) + 0x3dc00111; (* arm_LDR Q17 X8 (Immediate_Offset (word 0)) *) + 0x3dc00132; (* arm_LDR Q18 X9 (Immediate_Offset (word 0)) *) + 0x6eb01e32; (* arm_BIT Q18 Q17 Q16 128 *) + 0x3d800132; (* arm_STR Q18 X9 (Immediate_Offset (word 0)) *) + 0x3dc00511; (* arm_LDR Q17 X8 (Immediate_Offset (word 16)) *) + 0x3dc00532; (* arm_LDR Q18 X9 (Immediate_Offset (word 16)) *) + 0x6eb01e32; (* arm_BIT Q18 Q17 Q16 128 *) + 0x3d800532; (* arm_STR Q18 X9 (Immediate_Offset (word 16)) *) + 0x3dc00911; (* arm_LDR Q17 X8 (Immediate_Offset (word 32)) *) + 0x3dc00932; (* arm_LDR Q18 X9 (Immediate_Offset (word 32)) *) + 0x6eb01e32; (* arm_BIT Q18 Q17 Q16 128 *) + 0x3d800932; (* arm_STR Q18 X9 (Immediate_Offset (word 32)) *) + 0x3dc00d11; (* arm_LDR Q17 X8 (Immediate_Offset (word 48)) *) + 0x3dc00d32; (* arm_LDR Q18 X9 (Immediate_Offset (word 48)) *) + 0x6eb01e32; (* arm_BIT Q18 Q17 Q16 128 *) + 0x3d800d32; (* arm_STR Q18 X9 (Immediate_Offset (word 48)) *) + 0x91010108; (* arm_ADD X8 X8 (rvalue (word 64)) *) + 0x91010129; (* arm_ADD X9 X9 (rvalue (word 64)) *) + 0xf10020e7; (* arm_SUBS X7 X7 (rvalue (word 8)) *) + 0x54fffda1; (* arm_BNE (word 2097076) *) + 0x910004a5; (* arm_ADD X5 X5 (rvalue (word 1)) *) + 0xeb0200bf; (* arm_CMP X5 X2 *) + 0x54fffca1; (* arm_BNE (word 2097044) *) + 0xd65f03c0 (* arm_RET X30 *) +];; + + +let BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC = ARM_MK_EXEC_RULE bignum_copy_row_from_table_8n_neon_mc;; + +(* ARITH_RULE for proving `lp=rp` where lp and rp are pairs *) +let PAIR_EQ_ARITH_RULE (lp,rp:term*term) = + let lpl,lpr = dest_pair lp in + let rpl,rpr = dest_pair rp in + let lth = ARITH_RULE (mk_eq (lpl,rpl)) in + let rth = ARITH_RULE (mk_eq (lpr,rpr)) in + let th = REFL lp in + let th = GEN_REWRITE_RULE (RAND_CONV o LAND_CONV) [lth] th in + GEN_REWRITE_RULE (RAND_CONV o RAND_CONV) [rth] th;; + +let REWRITE_ASSUMES_TAC (t:term) = + UNDISCH_THEN t (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm]) THEN ASSUME_TAC thm);; + +let READ_MEMORY_BYTES_0 = prove(`read (memory :> bytes (z,0)) s = 0`, + REWRITE_TAC[PAIR_EQ_ARITH_RULE (`(x:int64,0)`,`(x:int64, 8*0)`)] THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_TRIVIAL]);; + +let LT_WORD_64 = prove(`!x (y:int64). x < val y ==> x < 2 EXP 64`, + REPEAT STRIP_TAC THEN + TRANS_TAC LT_TRANS `val (y:int64)` THEN + ONCE_REWRITE_TAC [GSYM DIMINDEX_64] THEN ASM_REWRITE_TAC[VAL_BOUND]);; + +let LT_WORD_64_DIV_N = prove(`!x (y:int64) n. x < val y DIV n ==> x < 2 EXP 64`, + REPEAT STRIP_TAC THEN + MATCH_MP_TAC LT_WORD_64 THEN EXISTS_TAC `y:int64` THEN + TRANS_TAC LTE_TRANS `val (y:int64) DIV n` THEN ASM_REWRITE_TAC[DIV_LE]);; + +let READ_MEMORY_BYTES_ELEM = prove(`!z w s m k. + w > k /\ read (memory :> bytes (z,8 * w)) s = m ==> + val (read (memory :> bytes64 (word_add z (word (8 * k)))) s) = lowdigits (highdigits m k) 1`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN EXPAND_TAC "m" THEN + REWRITE_TAC[HIGHDIGITS_BIGNUM_FROM_MEMORY; LOWDIGITS_BIGNUM_FROM_MEMORY] THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_SING] THEN + AP_THM_TAC THEN REPEAT AP_TERM_TAC THEN ASM_ARITH_TAC);; + +let READ_MEMORY_BYTES_FIRSTELEM = prove(`!z w s m. + w > 0 /\ read (memory :> bytes (z,8 * w)) s = m ==> + val (read (memory :> bytes64 z) s) = lowdigits m 1`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `z:int64 = word_add z (word (8 * 0))` (fun thm -> ONCE_REWRITE_TAC[thm]) THENL + [CONV_TAC WORD_RULE; ALL_TAC] THEN + IMP_REWRITE_TAC[READ_MEMORY_BYTES_ELEM] THEN REWRITE_TAC[HIGHDIGITS_0]);; + +let READ_MEMORY_BYTES_SLICE = prove(`!z w s m k w'. + w >= k + w' /\ read (memory :> bytes (z,8 * w)) s = m ==> + read (memory :> bytes (word_add z (word (8 * k)), 8 * w')) s = lowdigits (highdigits m k) w'`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN EXPAND_TAC "m" THEN + REWRITE_TAC[HIGHDIGITS_BIGNUM_FROM_MEMORY; LOWDIGITS_BIGNUM_FROM_MEMORY] THEN + AP_THM_TAC THEN REPEAT AP_TERM_TAC THEN ASM_ARITH_TAC);; + +let READ_MEMORY_BYTES_SLICE_HIGH = prove(`!z w s m k w'. + w = k + w' /\ read (memory :> bytes (z,8 * w)) s = m ==> + read (memory :> bytes (word_add z (word (8 * k)), 8 * w')) s = highdigits m k`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN EXPAND_TAC "m" THEN + REWRITE_TAC[HIGHDIGITS_BIGNUM_FROM_MEMORY] THEN + AP_THM_TAC THEN REPEAT AP_TERM_TAC THEN ASM_ARITH_TAC);; + +let READ_MEMORY_BYTES_MERGE = prove(`!z w w' w'' s m. + read (memory :> bytes (z,8 * w)) s = lowdigits m w /\ + read (memory :> bytes (word_add z (word (8 * w)),8 * w')) s = highdigits m w /\ + w + w' = w'' ==> + read (memory :> bytes (z, 8 * w'')) s = m`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN EXPAND_TAC "w''" THEN + ASM_REWRITE_TAC[BIGNUM_FROM_MEMORY_SPLIT] THEN + REWRITE_TAC[HIGH_LOW_DIGITS]);; + +let READ_MEMORY_BYTES_BYTES64 = prove(`!z s. + read (memory :> bytes (z,8)) s = val (read (memory :> bytes64 z) s)`, + REPEAT GEN_TAC THEN + REWRITE_TAC[PAIR_EQ_ARITH_RULE (`(z:int64,8)`, `(z:int64,8*1)`); + GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_SING]);; + +let READ_MEMORY_BYTES_BYTES128 = prove(`!z s. + read (memory :> bytes (z,16)) s = val (read (memory :> bytes128 z) s)`, + REPEAT GEN_TAC THEN + REWRITE_TAC[fst (CONJ_PAIR READ_MEMORY_BYTESIZED_SPLIT)] THEN + REWRITE_TAC[VAL_WORD_JOIN;DIMINDEX_64;DIMINDEX_128] THEN + IMP_REWRITE_TAC[MOD_LT] THEN + REWRITE_TAC[ARITH_RULE`2 EXP 128 = 2 EXP 64 * 2 EXP 64`] THEN + IMP_REWRITE_TAC[LT_MULT_ADD_MULT] THEN + REWRITE_TAC[VAL_BOUND_64;ARITH_RULE`0<2 EXP 64`;LE_REFL] THEN + REWRITE_TAC[ARITH_RULE`16 = 8*(1+1)`;GSYM BIGNUM_FROM_MEMORY_BYTES;BIGNUM_FROM_MEMORY_STEP;BIGNUM_FROM_MEMORY_SING] THEN + REWRITE_TAC[ARITH_RULE`8*1=8`;ARITH_RULE`64*1=64`] THEN ARITH_TAC);; + +let READ_MEMORY_BYTES_MERGE_FOUR128 = prove( + `!z0 z1 z2 z3 m0 m1 m2 m3 m s. + val (read (memory :> bytes128 z0) s) = m0 /\ + val (read (memory :> bytes128 z1) s) = m1 /\ + val (read (memory :> bytes128 z2) s) = m2 /\ + val (read (memory :> bytes128 z3) s) = m3 /\ + z1 = word_add z0 (word 16) /\ + z2 = word_add z0 (word 32) /\ + z3 = word_add z0 (word 48) /\ + (2 EXP 384) * m3 + (2 EXP 256) * m2 + (2 EXP 128) * m1 + m0 = m ==> + read (memory :> bytes (z0, 64)) s = m`, + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128] THEN + REWRITE_TAC(map ARITH_RULE [`16=8*2`;`32=8*4`;`48=8*6`]) THEN + REPEAT STRIP_TAC THEN + MAP_EVERY (fun t -> UNDISCH_THEN t SUBST_ALL_TAC) [ + `z1 = word_add z0 (word (8*2)):int64`; + `z2 = word_add z0 (word (8*4)):int64`; + `z3 = word_add z0 (word (8*6)):int64` + ] THEN + RULE_ASSUM_TAC (REWRITE_RULE[ADD_ASSOC]) THEN + RULE_ASSUM_TAC (REWRITE_RULE[ARITH_RULE`2 EXP 384=2 EXP (128 + 128 + 128)`;ARITH_RULE`2 EXP 256=2 EXP (128 + 128)`]) THEN + RULE_ASSUM_TAC (REWRITE_RULE [EXP_ADD;GSYM MULT_ASSOC;GSYM LEFT_ADD_DISTRIB]) THEN + let mytac s = EXPAND_TAC s THEN REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + SIMP_TAC[BIGNUM_FROM_MEMORY_BOUND;ARITH_RULE`128=64*2`] in + SUBGOAL_THEN `m0 < 2 EXP 128` ASSUME_TAC THENL [ mytac "m0"; ALL_TAC ] THEN + SUBGOAL_THEN `m1 < 2 EXP 128` ASSUME_TAC THENL [ mytac "m1"; ALL_TAC ] THEN + SUBGOAL_THEN `m2 < 2 EXP 128` ASSUME_TAC THENL [ mytac "m2"; ALL_TAC ] THEN + SUBGOAL_THEN `m3 < 2 EXP 128` ASSUME_TAC THENL [ mytac "m3"; ALL_TAC ] THEN + + SUBGOAL_THEN `m0 = lowdigits m 2` SUBST_ALL_TAC THENL + [ EXPAND_TAC "m" THEN REWRITE_TAC[lowdigits;ARITH_RULE`64*2=128`] THEN REWRITE_TAC[MOD_MULT_ADD] THEN + IMP_REWRITE_TAC[MOD_LT]; ALL_TAC ] THEN + SUBGOAL_THEN `m1 = lowdigits (highdigits m 2) 2` SUBST_ALL_TAC THENL + [ EXPAND_TAC "m" THEN REWRITE_TAC[lowdigits;highdigits;ARITH_RULE`64*2=128`] THEN + IMP_REWRITE_TAC[DIV_MULT_ADD; MOD_DIV_EQ_0;ADD_0;MOD_MULT_ADD] THEN + IMP_REWRITE_TAC[MOD_LT] THEN ARITH_TAC; ALL_TAC ] THEN + SUBGOAL_THEN `m2 = lowdigits (highdigits m 4) 2` SUBST_ALL_TAC THENL + [ EXPAND_TAC "m" THEN REWRITE_TAC[lowdigits;highdigits; + ARITH_RULE`64*4=128+128`;ARITH_RULE`64*2=128`;EXP_ADD;GSYM DIV_DIV] THEN + IMP_REWRITE_TAC[DIV_MULT_ADD; MOD_DIV_EQ_0;ADD_0;MOD_MULT_ADD] THEN + IMP_REWRITE_TAC[MOD_LT] THEN ARITH_TAC; ALL_TAC ] THEN + SUBGOAL_THEN `m3 = highdigits m 6` SUBST_ALL_TAC THENL + [ EXPAND_TAC "m" THEN REWRITE_TAC[lowdigits;highdigits; + ARITH_RULE`64*6=128+128+128`;ARITH_RULE`64*2=128`;EXP_ADD;GSYM DIV_DIV] THEN + IMP_REWRITE_TAC[DIV_MULT_ADD; MOD_DIV_EQ_0;ADD_0;MOD_MULT_ADD] THEN + ARITH_TAC; ALL_TAC ] THEN + + REWRITE_TAC[ARITH_RULE`64=8*8`] THEN + + MATCH_MP_TAC READ_MEMORY_BYTES_MERGE THEN + MAP_EVERY EXISTS_TAC [`2`;`6`] THEN + ASM_REWRITE_TAC[ARITH_RULE`2+6=8`] THEN + + MATCH_MP_TAC READ_MEMORY_BYTES_MERGE THEN + MAP_EVERY EXISTS_TAC [`2`;`4`] THEN + ASM_REWRITE_TAC[ARITH_RULE`2+4=6`] THEN + + REWRITE_TAC[WORD_ADD_ASSOC_CONSTS;ARITH_RULE`8*2+8*2=8*4`] THEN + MATCH_MP_TAC READ_MEMORY_BYTES_MERGE THEN + MAP_EVERY EXISTS_TAC [`2`;`2`] THEN + ASM_REWRITE_TAC[ARITH_RULE`2+2=4`;ARITH_RULE`2+4=6`; + HIGHDIGITS_HIGHDIGITS;WORD_ADD_ASSOC_CONSTS;ARITH_RULE`8*4+8*2=8*6`]);; + +let ABBREV_Z_READ_128BITS_TAC name stname ofs = + let v = mk_var (name, `:int128`) in + let templ = + if ofs = 0 then + `read (memory :> bytes128 (word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)))):int64)) s0` + else + let templ0 = `read (memory :> bytes128 (word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + ofs)):int64)) s0` in + let newofs = mk_numeral (Int ofs) in + subst [(newofs,`ofs:num`)] templ0 in + let rhs = subst [(mk_var(stname, `:armstate`),`st0:armstate`)] templ in + ABBREV_TAC (mk_eq (v,rhs));; + +let ABBREV_TABLE_READ_128BITS_TAC name stname ofs = + let v = mk_var (name, `:int128`) in + let templ = + if ofs = 0 then + `read (memory :> bytes128 (word_add table + (word (8 * (i * val (width:int64) + val (width:int64) - 8 * (i' + 1)))):int64)) s0` + else + let templ0 = `read (memory :> bytes128 (word_add table + (word (8 * (i * val (width:int64) + val (width:int64) - 8 * (i' + 1)) + ofs)):int64)) s0` in + let newofs = mk_numeral (Int ofs) in + subst [(newofs,`ofs:num`)] templ0 in + let rhs = subst [(mk_var(stname, `:armstate`),`st0:armstate`)] templ in + ABBREV_TAC (mk_eq (v,rhs));; + +let READ_MEMORY_BYTES_FIRSTELEM128 = prove(`!z w s m. + w >= 2 /\ read (memory :> bytes (z,8 * w)) s = m ==> + val (read (memory :> bytes128 z) s) = lowdigits m 2`, + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128; ARITH_RULE`16=8*2`] THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REPEAT STRIP_TAC THEN + EXPAND_TAC"m" THEN REWRITE_TAC[LOWDIGITS_BIGNUM_FROM_MEMORY] THEN + AP_THM_TAC THEN REPEAT AP_TERM_TAC THEN ASM_ARITH_TAC);; + +let WORD_AND_128_FULLBITS = prove( + `!(x:int128). word_and (word 340282366920938463463374607431768211455) x = x /\ + word_and x (word 340282366920938463463374607431768211455) = x`, + STRIP_TAC THEN CONV_TAC WORD_BLAST);; + +let VAL_WORD_8_EQ_0 = prove( + `!i' x. i' < val (x:int64) DIV 8 ==> (val (word (8 * i'):int64) = 0 <=> i' = 0)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[VAL_WORD;DIMINDEX_64] THEN + SUBGOAL_THEN `val (x:int64) < 2 EXP 64` ASSUME_TAC THENL [REWRITE_TAC[VAL_BOUND_64]; ALL_TAC] THEN + SUBGOAL_THEN `8*i'<2 EXP 64` (fun thm -> REWRITE_TAC[MATCH_MP MOD_LT thm]) THENL [ASM_ARITH_TAC; ALL_TAC] THEN + ARITH_TAC);; + + +let BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_SUBROUTINE_CORRECT = prove( + `!z table height width idx pc n m returnaddress. + nonoverlapping (word pc, 0xac) (z, 8 * val width) /\ + nonoverlapping (word pc, 0xac) (table, 8 * val height * val width) /\ + nonoverlapping (z, 8 * val width) (table, 8 * val height * val width) /\ + 8 * val width < 2 EXP 64 /\ val width MOD 8 = 0 /\ val idx < val height + ==> ensures arm + (\s. aligned_bytes_loaded s (word pc) bignum_copy_row_from_table_8n_neon_mc /\ + read PC s = word pc /\ + read X30 s = returnaddress /\ + C_ARGUMENTS [z; table; height; width; idx] s /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s = m) + (\s. read PC s = returnaddress /\ + bignum_from_memory (z, val width) s = m) + (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [memory :> bytes(z,8 * val width)])`, + + REPEAT GEN_TAC THEN REWRITE_TAC[C_ARGUMENTS; NONOVERLAPPING_CLAUSES; + MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN + REPEAT STRIP_TAC THEN + + ASM_CASES_TAC `val (height:(64)word) = 0` THENL [ + UNDISCH_TAC `val (idx:int64) < val (height:int64)` THEN + ASM_REWRITE_TAC[] THEN REWRITE_TAC[LT] THEN ENSURES_INIT_TAC "s0" THEN ITAUT_TAC; + ALL_TAC] THEN + ASM_CASES_TAC `width = (word 0):(64)word` THENL [ + ASM_REWRITE_TAC[] THEN + REWRITE_TAC[VAL_WORD_0; MULT_0; WORD_ADD_0] THEN + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC [1;2;3] THEN + ASM_MESON_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_TRIVIAL]; + ALL_TAC] THEN + SUBGOAL_THEN `~(val (width:64 word) = 0)` ASSUME_TAC THENL [ + UNDISCH_TAC `~(width = word 0:64 word)` THEN + REWRITE_TAC[VAL_EQ_0]; + ALL_TAC] THEN + + ENSURES_SEQUENCE_TAC `pc + 0x14` + `\s. read X30 s = returnaddress /\ read X0 s = z /\ read X1 s = table /\ + read X2 s = height /\ read X3 s = width /\ read X4 s = idx /\ + read X5 s = width /\ read X6 s = z /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s = m /\ + read Q16 s = word 0` THEN CONJ_TAC THENL [ + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--5); + + ALL_TAC] THEN + +(* This is necessary to avoid stores from overwriting the table *) + SUBGOAL_THEN `val (idx:int64) * val (width:int64) + val width <= val (height:int64) * val width` ASSUME_TAC + THENL [IMP_REWRITE_TAC[LE_MULT_ADD]; ALL_TAC] THEN + + SUBGOAL_THEN `word (8 * val width DIV 8) = width:int64` ASSUME_TAC THENL [ + REWRITE_TAC [GSYM VAL_EQ; VAL_WORD; DIMINDEX_64] THEN IMP_REWRITE_TAC[MOD_LT] THEN CONJ_TAC THEN ASM_ARITH_TAC; + ALL_TAC] THEN + +(* bignum_copy_row_from_table_initzero *) + ENSURES_WHILE_PDOWN_TAC `val (width:64 word) DIV 8:num` `pc + 0x14` `pc + 0x2c` + `\i s. (read X30 s = returnaddress /\ read X0 s = z /\ read X1 s = table /\ + read X2 s = height /\ read X3 s = width /\ read X4 s = idx /\ + read X5 s = word (8 * i) /\ + read X6 s = word (val z + 64 * (val width DIV 8 - i)) /\ + read Q16 s = word 0 /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s + = m /\ + bignum_from_memory (z, 8 * (val width DIV 8 - i)) s = 0) /\ + (read ZF s <=> i = 0)` THEN REPEAT CONJ_TAC THENL [ + (* 1. width > 0 *) + ASM_ARITH_TAC; + + (* 2. loop starts *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC [] THEN + REWRITE_TAC[SUB_REFL; WORD_VAL; MULT_0; ADD_0; GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_TRIVIAL]; + + (* 3. loop body *) + REPEAT STRIP_TAC THEN REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN + MATCH_MP_TAC ENSURES_FRAME_SUBSUMED THEN + EXISTS_TAC `MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [ + memory :> bytes128 (word (val (z:int64) + 64 * (val (width:int64) DIV 8 - (i + 1)))); + memory :> bytes128 (word_add (word (val (z:int64) + 64 * (val (width:int64) DIV 8 - (i + 1)))) + (word 16)); + memory :> bytes128 (word_add (word (val (z:int64) + 64 * (val (width:int64) DIV 8 - (i + 1)))) + (word 32)); + memory :> bytes128 (word_add (word (val (z:int64) + 64 * (val (width:int64) DIV 8 - (i + 1)))) + (word 48))]` THEN + REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN + CONJ_TAC THENL [ + REPEAT(MATCH_MP_TAC SUBSUMED_SEQ THEN REWRITE_TAC[SUBSUMED_REFL]) THEN + (* SIMPLE_ARITH_TAC isn't good at dealing with assumptions containing 'val'. Let's abbreviate + val width. *) + REWRITE_TAC[WORD_ADD; WORD_VAL] THEN + REWRITE_TAC[WORD_ADD_ASSOC_CONSTS] THEN + ABBREV_TAC `w' = val (width:int64)` THEN + SUBSUMED_MAYCHANGE_TAC; + + ALL_TAC] THEN + + ENSURES_INIT_TAC "s0" THEN + MAP_EVERY ASSERT_USING_ASM_ARITH_TAC [ + `8 * (val (width:int64) DIV 8 - (i + 1)) + 2 <= val (width:int64)`; + `(8 * (val (width:int64) DIV 8 - (i + 1)) + 2) + 2 <= val (width:int64)`; + `(8 * (val (width:int64) DIV 8 - (i + 1)) + 4) + 2 <= val (width:int64)`; + `(8 * (val (width:int64) DIV 8 - (i + 1)) + 6) + 2 <= val (width:int64)`; + `64 * (val (width:int64) DIV 8 - (i + 1)) + 16 <= 18446744073709551616`; + `(64 * (val (width:int64) DIV 8 - (i + 1)) + 16) + 16 <= 18446744073709551616`; + `(64 * (val (width:int64) DIV 8 - (i + 1)) + 32) + 16 <= 18446744073709551616`; + `(64 * (val (width:int64) DIV 8 - (i + 1)) + 48) + 16 <= 18446744073709551616`] THEN + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--6) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REPEAT CONJ_TAC THENL [ + CONV_TAC WORD_RULE; + + REWRITE_TAC[GSYM WORD_ADD] THEN AP_TERM_TAC THEN + UNDISCH_TAC `i < val (width:int64) DIV 8` THEN ARITH_TAC; + + MATCH_MP_TAC READ_MEMORY_BYTES_MERGE THEN + MAP_EVERY EXISTS_TAC [`8 * (val (width:int64) DIV 8 - (i + 1))`; `8`] THEN + ASM_REWRITE_TAC[LOWDIGITS_TRIVIAL; HIGHDIGITS_TRIVIAL] THEN + CONJ_TAC THENL [ALL_TAC; UNDISCH_TAC `i < val (width:int64) DIV 8` THEN ARITH_TAC] THEN + REWRITE_TAC[ARITH_RULE`8*8=64`] THEN MATCH_MP_TAC READ_MEMORY_BYTES_MERGE_FOUR128 THEN + MAP_EVERY EXISTS_TAC [ + `word_add (word (val (z:int64) + 64 * (val (width:int64) DIV 8 - (i + 1)))) (word 16):int64`; + `word_add (word (val (z:int64) + 64 * (val (width:int64) DIV 8 - (i + 1)))) (word 32):int64`; + `word_add (word (val (z:int64) + 64 * (val (width:int64) DIV 8 - (i + 1)))) (word 48):int64` + ] THEN + ASM_REWRITE_TAC [WORD_RULE `word_add x (word y) = word (val x + y)`; ARITH_RULE`8*8*x=64*x`] THEN + MAP_EVERY EXISTS_TAC [`0`;`0`;`0`;`0`] THEN + REWRITE_TAC[VAL_WORD_0] THEN ARITH_TAC; + + REWRITE_TAC[VAL_WORD_SUB; DIMINDEX_64; VAL_WORD] THEN + SUBGOAL_THEN `(8 * (i + 1)) < 2 EXP 64` + (fun thm -> REWRITE_TAC[MATCH_MP MOD_LT thm] THEN ASSUME_TAC thm) THENL [ + TRANS_TAC LET_TRANS `val (width:int64)` THEN + CONJ_TAC THENL [ + IMP_REWRITE_TAC [GSYM LDIV_LT_EQ] THEN ARITH_TAC; + UNDISCH_TAC `8 * val (width:int64) < 2 EXP 64` THEN ARITH_TAC + ]; + + ALL_TAC + ] THEN + REWRITE_TAC[ARITH_RULE `8 MOD 2 EXP 64 = 8`] THEN + ONCE_REWRITE_TAC[MATCH_MP ADD_SUB_SWAP (ARITH_RULE`2 EXP 64>=8 /\ 8*(i+1)>=8`)] THEN + ONCE_REWRITE_TAC[GSYM MOD_ADD_MOD] THEN + REWRITE_TAC[MOD_REFL;MOD_MOD_REFL;ADD;ARITH_RULE`8*(i+1)-8=8*i`] THEN + SUBGOAL_THEN `8*i < 2 EXP 64` (fun thm -> REWRITE_TAC[MATCH_MP MOD_LT thm]) THENL [ + UNDISCH_TAC `8*(i+1)<2 EXP 64` THEN ARITH_TAC; ALL_TAC + ] THEN ARITH_TAC + ]; + + (* 4. loop backedge *) + REPEAT STRIP_TAC THEN ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--1); + + ALL_TAC + ] THEN + +(* bignum_copy_row_from_table_outerloop *) + ENSURES_WHILE_PUP_TAC `val (height:64 word):num` `pc + 0x38` `pc + 0xa4` + `\i s. (read X30 s = returnaddress /\ read X0 s = z /\ read X1 s = table /\ + read X2 s = height /\ read X3 s = width /\ read X4 s = idx /\ + read X5 s = word i /\ read X8 s = word_add table (word (8 * i * val width)) /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s + = m /\ + ((i <= val idx /\ bignum_from_memory (z, val width) s = 0) \/ + (i > val idx /\ bignum_from_memory (z, val width) s = m))) /\ + (read ZF s <=> i = val height)` THEN REPEAT CONJ_TAC THENL [ + (* 1. height > 0 *) + ASM_MESON_TAC[]; + + (* 2. to loop start *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--3) THEN + REWRITE_TAC[ARITH_RULE `x * 0 = 0`; ARITH_RULE `0 * x = 0`; WORD_ADD_0] THEN + SUBGOAL_THEN `8 * (val (width:int64) DIV 8 - 0) = val width` (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm])) THENL + [ASM_ARITH_TAC; ALL_TAC] THEN + ASM_REWRITE_TAC[LE_0]; + + (* 3. loop body - pass *) + ALL_TAC; + + (* 4. loop backedge *) + REPEAT STRIP_TAC THEN + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--1); + + (* next *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC [1;2] THEN + CASES_FIRST_DISJ_ASSUM_TAC THEN SPLIT_FIRST_CONJ_ASSUM_TAC THENL [ + UNDISCH_TAC `val (idx:int64) < val (height:int64)` THEN + UNDISCH_TAC `val (height:int64) <= val (idx:int64)` THEN + ARITH_TAC; + + ASM_MESON_TAC[]] +] THEN + + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `i < 2 EXP 64` ASSUME_TAC THENL [ASM_MESON_TAC[LT_WORD_64]; ALL_TAC] THEN + SUBGOAL_THEN `i + 1 < 2 EXP 64` ASSUME_TAC THENL [ + TRANS_TAC LET_TRANS `val (height:int64)` THEN + CONJ_TAC THENL [ + UNDISCH_TAC `i < val (height:int64)` THEN ARITH_TAC; + REWRITE_TAC[VAL_BOUND_64]]; + + ALL_TAC] THEN + + ENSURES_WHILE_PDOWN_TAC `(val (width:64 word) DIV 8):num` `pc + 0x4c` `pc + 0x98` + `\j s. (read X30 s = returnaddress /\ read X0 s = z /\ read X1 s = table /\ + read X2 s = height /\ read X3 s = width /\ read X4 s = idx /\ read X5 s = word i /\ + read Q16 s = (if i = val idx then word 340282366920938463463374607431768211455 else word 0) /\ + read X7 s = word (8 * j) /\ + // pointers + read X8 s = word_add table (word (8 * (i * val width + (val width - 8 * j)))) /\ + read X9 s = word_add z (word (8 * (val width - 8 * j)):64 word) /\ + bignum_from_memory (table, val height * val width) s = n /\ + bignum_from_memory (word_add table (word (8 * val idx * val width)), val width) s + = m /\ + ((i < val idx /\ + bignum_from_memory (z, val width - 8 * j) s = 0 /\ + bignum_from_memory (word_add z (word (8 * (val width - 8 * j))), 8 * j) s = 0) + \/ + (i = val idx /\ + bignum_from_memory (z, val width - 8 * j) s = lowdigits m (val width - 8 * j) /\ + bignum_from_memory (word_add z (word (8 * (val width - 8 * j))), 8 * j) s = 0) + \/ + (i > val idx /\ + bignum_from_memory (z, val width - 8 * j) s = lowdigits m (val width - 8 * j) /\ + bignum_from_memory (word_add z (word (8 * (val width - 8 * j))), 8 * j) s = highdigits m (val width - 8 * j)))) /\ + (read ZF s <=> j = 0)` THEN REPEAT CONJ_TAC THENL [ + ASM_ARITH_TAC; + + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--5) THEN + SUBGOAL_THEN `8 * val (width:int64) DIV 8 = val width` (fun thm -> REWRITE_TAC[thm]) THENL [ + UNDISCH_TAC `val (width:int64) MOD 8 = 0` THEN ARITH_TAC; ALL_TAC] THEN + ASM_REWRITE_TAC[SUB_REFL; WORD_VAL; ADD_0; MULT_0; WORD_ADD_0] THEN + REWRITE_TAC[READ_MEMORY_BYTES_0; LOWDIGITS_0; HIGHDIGITS_0] THEN + CONJ_TAC THENL [ + ASM_CASES_TAC `i = val (idx:int64)` THENL [ + ASM_REWRITE_TAC[VAL_WORD] THEN IMP_REWRITE_TAC[MOD_LT; VAL_BOUND] THEN + CONV_TAC WORD_REDUCE_CONV; + + ASM_REWRITE_TAC[VAL_WORD] THEN IMP_REWRITE_TAC[DIMINDEX_64; MOD_LT] THEN + CONV_TAC WORD_REDUCE_CONV]; + + ASM_CASES_TAC `i > val (idx:int64)` THENL [ + SUBGOAL_THEN `~(i <= val (idx:int64))` ASSUME_TAC THENL + [ASM_REWRITE_TAC[NOT_LE; GSYM GT]; ALL_TAC] THEN + REWRITE_TAC[ASSUME `i > val (idx:int64)`] THEN + REWRITE_ASSUMES_TAC `i > val (idx:int64)` THEN + REWRITE_ASSUMES_TAC `~(i <= val (idx:int64))` THEN + ASM_REWRITE_TAC[]; + + SUBGOAL_THEN `i <= val (idx:int64)` ASSUME_TAC THENL + [UNDISCH_TAC `~(i > val (idx:int64))` THEN ARITH_TAC; ALL_TAC] THEN + REWRITE_ASSUMES_TAC `i <= val (idx:int64)` THEN + REWRITE_ASSUMES_TAC `~(i > val (idx:int64))` THEN + ASM_REWRITE_TAC[] THEN + UNDISCH_TAC `i <= val (idx:int64)` THEN + ARITH_TAC]]; + + (* loop body *) + ALL_TAC; + + (* backedge *) + REPEAT STRIP_TAC THEN ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC [1]; + + (* finishes outer loop; pc ac -> b4 *) + ARM_SIM_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC [1;2;3] THEN + REWRITE_TAC[WORD_ADD; ARITH_RULE `a*b+b-8*0=(a+1)*b`] THEN + REWRITE_TAC[VAL_WORD_ADD;VAL_WORD;DIMINDEX_64;ARITH_RULE `1 MOD 2 EXP 64 = 1`; ADD_0] THEN + REWRITE_TAC[MATCH_MP MOD_LT (ASSUME `i < 2 EXP 64`); MATCH_MP MOD_LT (ASSUME `i + 1 < 2 EXP 64`)] THEN + RULE_ASSUM_TAC (REWRITE_RULE [ARITH_RULE `8*0=0`; SUB_0; READ_MEMORY_BYTES_0]) THEN + SUBGOAL_THEN `m < 2 EXP (64 * val (width:int64))` ASSUME_TAC THENL + [EXPAND_TAC "m" THEN SIMP_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES; BIGNUM_FROM_MEMORY_BOUND]; ALL_TAC] THEN + RULE_ASSUM_TAC (REWRITE_RULE [MATCH_MP LOWDIGITS_SELF (ASSUME `m < 2 EXP (64 * val (width:int64))`)]) THEN + RULE_ASSUM_TAC (REWRITE_RULE [MATCH_MP HIGHDIGITS_ZERO (ASSUME `m < 2 EXP (64 * val (width:int64))`)]) THEN + + ASM_CASES_TAC `i < val (idx:int64)` THENL [ + REWRITE_ASSUMES_TAC `i < val (idx:int64)` THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `~(i = val (idx:int64))` `i < val (idx:int64)` THEN + ASSERT_USING_UNDISCH_AND_ARITH_TAC `~(i > val (idx:int64))` `i < val (idx:int64)` THEN + MAP_EVERY REWRITE_ASSUMES_TAC [`~(i = val (idx:int64))`; `~(i > val (idx:int64))`] THEN + ASM_REWRITE_TAC[] THEN DISJ1_TAC THEN + UNDISCH_TAC `i < val (idx:int64)` THEN ARITH_TAC; + + ASM_CASES_TAC `i = val (idx:int64)` THENL [ + REWRITE_ASSUMES_TAC `i = val (idx:int64)` THEN + RULE_ASSUM_TAC (REWRITE_RULE [LT_REFL; GT_REFL; SUB_0]) THEN + DISJ2_TAC THEN + ASM_REWRITE_TAC[ARITH_RULE `p + 1 > p`]; + + REWRITE_ASSUMES_TAC `~(i = val (idx:int64))` THEN + REWRITE_ASSUMES_TAC `~(i < val (idx:int64))` THEN + SPLIT_FIRST_CONJ_ASSUM_TAC THEN (* get `i > val idx` *) + DISJ2_TAC THEN + ASM_SIMP_TAC[ARITH_RULE `x > y ==> x + 1 > y`; ASSUME `i > val (idx:int64)`] + ]] + + ] THEN + + + REPEAT STRIP_TAC THEN REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN + + MATCH_MP_TAC ENSURES_FRAME_SUBSUMED THEN + EXISTS_TAC `MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [ + memory :> bytes128 (word_add (z:int64) (word (8 * (val (width:int64) - 8 * (i' + 1))))); + memory :> bytes128 (word_add (z:int64) (word (8 * (val (width:int64) - 8 * (i' + 1)) + 16))); + memory :> bytes128 (word_add (z:int64) (word (8 * (val (width:int64) - 8 * (i' + 1)) + 32))); + memory :> bytes128 (word_add (z:int64) (word (8 * (val (width:int64) - 8 * (i' + 1)) + 48)))]` THEN + REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI] THEN + CONJ_TAC THENL [ + REPEAT(MATCH_MP_TAC SUBSUMED_SEQ THEN REWRITE_TAC[SUBSUMED_REFL]) THEN + (* SIMPLE_ARITH_TAC isn't good at dealing with assumptions containing 'val'. Let's abbreviate + val width. *) + REWRITE_TAC[WORD_ADD; WORD_VAL] THEN + REWRITE_TAC[WORD_ADD_ASSOC_CONSTS] THEN + ABBREV_TAC `w' = val (width:int64)` THEN + SUBSUMED_MAYCHANGE_TAC; + + ALL_TAC] THEN + + ENSURES_INIT_TAC "s0" THEN + MAP_EVERY ASSERT_USING_ASM_ARITH_TAC [ + `val (width:int64) - 8 * (i' + 1) + 2 <= val width`; + `(val (width:int64) - 8 * (i' + 1) + 2) + 2 <= val width`; + `(val (width:int64) - 8 * (i' + 1) + 4) + 2 <= val width`; + `(val (width:int64) - 8 * (i' + 1) + 6) + 2 <= val width`] THEN + MAP_EVERY (fun t -> ASSERT_USING_UNDISCH_AND_ARITH_TAC t `8 * val (width:int64) < 2 EXP 64`) [ + `(8 * (val (width:int64) - 8 * (i' + 1)) + 48) + 16 <= 18446744073709551616`; + `(8 * (val (width:int64) - 8 * (i' + 1)) + 32) + 16 <= 18446744073709551616`; + `(8 * (val (width:int64) - 8 * (i' + 1)) + 16) + 16 <= 18446744073709551616`; + `8 * (val (width:int64) - 8 * (i' + 1)) + 16 <= 18446744073709551616`] THEN + MAP_EVERY (fun t -> SUBGOAL_THEN t ASSUME_TAC THENL [ + TRANS_TAC LE_TRANS `i * val (width:int64) + val width` THEN CONJ_TAC THENL + [UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; + IMP_REWRITE_TAC [LE_MULT_ADD]]; + ALL_TAC + ]) [ + `((i * val (width:int64) + val width - 8 * (i' + 1)) + 6) + 2 <= val (height:int64) * val width`; + `((i * val (width:int64) + val width - 8 * (i' + 1)) + 4) + 2 <= val (height:int64) * val width`; + `((i * val (width:int64) + val width - 8 * (i' + 1)) + 2) + 2 <= val (height:int64) * val width`; + `(i * val (width:int64) + val width - 8 * (i' + 1)) + 2 <= val (height:int64) * val width`] THEN + MAP_EVERY (fun i -> + let si = string_of_int i in + ABBREV_TABLE_READ_128BITS_TAC ("p" ^ si) "s0" (i*16) THEN + ABBREV_Z_READ_128BITS_TAC ("q" ^ si) "s0" (i*16)) (0--3) THEN + + ASM_CASES_TAC `i = val (idx:int64)` THENL [ + (* case 1 *) + REWRITE_TAC[ASSUME `i = val (idx:int64)`; LT_REFL; GT_REFL] THEN + REWRITE_ASSUMES_TAC `i = val (idx:int64)` THEN + RULE_ASSUM_TAC (REWRITE_RULE [LT_REFL; GT_REFL]) THEN + SPLIT_FIRST_CONJ_ASSUM_TAC THEN + SUBGOAL_THEN + `val (q0:int128) = lowdigits 0 2 /\ val (q1:int128) = lowdigits (highdigits 0 2) 2 /\ + val (q2:int128) = lowdigits (highdigits 0 4) 2 /\ val (q3:int128) = lowdigits (highdigits 0 6) 2` + (fun thm -> + let thm2 = REWRITE_RULE + [LOWDIGITS_TRIVIAL; HIGHDIGITS_TRIVIAL; WORD_ARITH `val (x:int128) = 0 <=> x = word 0`] + thm in + RULE_ASSUM_TAC (REWRITE_RULE [thm2])) THENL [ + MAP_EVERY EXPAND_TAC ["q0";"q1";"q2";"q3"] THEN + REWRITE_TAC[GSYM WORD_ADD_ASSOC_CONSTS] THEN REWRITE_TAC(map ARITH_RULE [`16=8*2`;`32=8*4`;`48=8*6`]) THEN + CONJ_TAC THENL [ + MATCH_MP_TAC READ_MEMORY_BYTES_FIRSTELEM128 THEN EXISTS_TAC `8 * (i' + 1)` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; + + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128] THEN + REWRITE_TAC[ARITH_RULE `16=8*2`] THEN + REPEAT CONJ_TAC THEN MATCH_MP_TAC READ_MEMORY_BYTES_SLICE THEN EXISTS_TAC `8 * (i' + 1)` THEN + ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC]; + + ALL_TAC] THEN + SUBGOAL_THEN `read (memory :> + bytes (word_add (word_add (z:int64) (word (8 * (val (width:int64) - 8 * (i' + 1))))) (word (8 * 8)), + 8 * 8 * i')) s0 = + highdigits 0 8` (fun thm -> + ASSUME_TAC (REWRITE_RULE [HIGHDIGITS_TRIVIAL; WORD_ADD_ASSOC_CONSTS;ARITH_RULE`8*8=64`] thm)) THENL [ + MATCH_MP_TAC READ_MEMORY_BYTES_SLICE_HIGH THEN + EXISTS_TAC `8 * (i' + 1)` THEN ASM_REWRITE_TAC[ARITH_RULE `8*(x+1)=8+8*x`]; + + ALL_TAC] THEN + ABBREV_TAC `i'' = val (width:int64) - 8 * (i'+1)` THEN + ASSERT_USING_ASM_ARITH_TAC `(8 * i'' + 64) + 8 * 8 * i' <= 18446744073709551616` THEN + + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--19) THEN + ENSURES_FINAL_STATE_TAC THEN + SUBST_ALL_TAC (GSYM (ASSUME `val (width:int64) - 8 * (i' + 1) = i''`)) THEN + SUBGOAL_THEN `8 * (val (width:int64) - 8 * (i' + 1)) + 64 = 8 * (val width - 8 * i')` SUBST_ALL_TAC THENL [ + UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; ALL_TAC] THEN + ASM_REWRITE_TAC[WORD_SUB_ADD; WORD_ADD_ASSOC_CONSTS; + WORD_RULE `word_sub (word (8 * (i' + 1))) (word 8):int64 = word (8 * i')`] THEN + REPEAT CONJ_TAC THENL [ + REPEAT AP_TERM_TAC THEN UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; + + REPEAT AP_TERM_TAC THEN UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; + + MATCH_MP_TAC READ_MEMORY_BYTES_MERGE THEN + MAP_EVERY EXISTS_TAC [`val (width:int64) - 8 * (i'+1)`; `8`] THEN ASM_REWRITE_TAC[] THEN + REPEAT CONJ_TAC THENL [ + REWRITE_TAC[LOWDIGITS_LOWDIGITS] THEN AP_TERM_TAC THEN ARITH_TAC; + + REWRITE_TAC[ARITH_RULE`8*8=64`] THEN MATCH_MP_TAC READ_MEMORY_BYTES_MERGE_FOUR128 THEN + MAP_EVERY EXISTS_TAC [ + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 16)):int64`; + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 32)):int64`; + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 48)):int64`; + ] THEN + MAP_EVERY EXISTS_TAC [`val (p0:int128)`;`val (p1:int128)`;`val (p2:int128)`;`val (p3:int128)`] THEN + ASM_REWRITE_TAC[WORD_AND_128_FULLBITS] THEN + REPEAT CONJ_TAC THEN TRY (REWRITE_TAC [WORD_ADD_ASSOC_CONSTS] THEN CONV_TAC WORD_ARITH) THEN + DISCARD_MATCHING_ASSUMPTIONS [`read Q17 s19 = p3`] THEN + MAP_EVERY EXPAND_TAC ["p0";"p1";"p2";"p3";"m"] THEN + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128;ARITH_RULE`16=8*2`] THEN + REWRITE_TAC[GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[LOWDIGITS_BIGNUM_FROM_MEMORY;ARITH_RULE`MIN x (x-y) = x-y`] THEN + REWRITE_TAC[HIGHDIGITS_BIGNUM_FROM_MEMORY] THEN + SUBGOAL_THEN `val (width:int64) - 8 * i' - (val width - 8 * (i' + 1)) = 8` (fun thm -> REWRITE_TAC[thm]) THENL [ + UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; ALL_TAC + ] THEN + REWRITE_TAC[WORD_ADD_ASSOC_CONSTS] THEN + REWRITE_TAC((map PAIR_EQ_ARITH_RULE [ + (`(x:int64,8)`, `(x:int64,2+6)`); + (`(x:int64,6)`, `(x:int64,2+4)`); + (`(x:int64,4)`, `(x:int64,2+2)`)]) @ [BIGNUM_FROM_MEMORY_SPLIT]) THEN + REWRITE_TAC [WORD_ADD_ASSOC_CONSTS; LEFT_ADD_DISTRIB;MULT_ASSOC;GSYM EXP_ADD;GSYM ADD_ASSOC] THEN + ARITH_TAC; + + UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC + ]; + + IMP_REWRITE_TAC[VAL_WORD_8_EQ_0] + ]; ALL_TAC] THEN + + (* case 2 *) + REWRITE_ASSUMES_TAC `~(i = val (idx:int64))` THEN + REWRITE_TAC[ASSUME `~(i = val (idx:int64))`] THEN + ASM_CASES_TAC `i < val (idx:int64)` THENL [ + ASSERT_USING_UNDISCH_AND_ARITH_TAC `~(i > val (idx:int64))` `i < val (idx:int64)` THEN + MAP_EVERY REWRITE_ASSUMES_TAC [`~(i > val (idx:int64))`; `i < val (idx:int64)`] THEN + MAP_EVERY (fun t -> REWRITE_TAC[ASSUME t]) [`~(i > val (idx:int64))`; `i < val (idx:int64)`] THEN + SPLIT_FIRST_CONJ_ASSUM_TAC THEN + SUBGOAL_THEN + `val (q0:int128) = lowdigits 0 2 /\ val (q1:int128) = lowdigits (highdigits 0 2) 2 /\ + val (q2:int128) = lowdigits (highdigits 0 4) 2 /\ val (q3:int128) = lowdigits (highdigits 0 6) 2` + (fun thm -> + let thm2 = REWRITE_RULE + [LOWDIGITS_TRIVIAL; HIGHDIGITS_TRIVIAL; WORD_ARITH `val (x:int128) = 0 <=> x = word 0`] + thm in + RULE_ASSUM_TAC (REWRITE_RULE [thm2])) THENL [ + MAP_EVERY EXPAND_TAC ["q0";"q1";"q2";"q3"] THEN + REWRITE_TAC[GSYM WORD_ADD_ASSOC_CONSTS] THEN REWRITE_TAC(map ARITH_RULE [`16=8*2`;`32=8*4`;`48=8*6`]) THEN + CONJ_TAC THENL [ + MATCH_MP_TAC READ_MEMORY_BYTES_FIRSTELEM128 THEN EXISTS_TAC `8 * (i' + 1)` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; + + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128] THEN + REWRITE_TAC[ARITH_RULE `16=8*2`] THEN + REPEAT CONJ_TAC THEN MATCH_MP_TAC READ_MEMORY_BYTES_SLICE THEN EXISTS_TAC `8 * (i' + 1)` THEN + ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC]; + + ALL_TAC] THEN + SUBGOAL_THEN `read (memory :> + bytes (word_add (word_add (z:int64) (word (8 * (val (width:int64) - 8 * (i' + 1))))) (word (8 * 8)), + 8 * 8 * i')) s0 = + highdigits 0 8` (fun thm -> + ASSUME_TAC (REWRITE_RULE [HIGHDIGITS_TRIVIAL; WORD_ADD_ASSOC_CONSTS;ARITH_RULE`8*8=64`] thm)) THENL [ + MATCH_MP_TAC READ_MEMORY_BYTES_SLICE_HIGH THEN + EXISTS_TAC `8 * (i' + 1)` THEN ASM_REWRITE_TAC[ARITH_RULE `8*(x+1)=8+8*x`]; + + ALL_TAC] THEN + ABBREV_TAC `i'' = val (width:int64) - 8 * (i'+1)` THEN + ASSERT_USING_ASM_ARITH_TAC `(8 * i'' + 64) + 8 * 8 * i' <= 18446744073709551616` THEN + + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--19) THEN + ENSURES_FINAL_STATE_TAC THEN + SUBST_ALL_TAC (GSYM (ASSUME `val (width:int64) - 8 * (i' + 1) = i''`)) THEN + SUBGOAL_THEN `8 * (val (width:int64) - 8 * (i' + 1)) + 64 = 8 * (val width - 8 * i')` SUBST_ALL_TAC THENL [ + UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; ALL_TAC] THEN + ASM_REWRITE_TAC[WORD_SUB_ADD; WORD_ADD_ASSOC_CONSTS; + WORD_RULE `word_sub (word (8 * (i' + 1))) (word 8):int64 = word (8 * i')`] THEN + REPEAT CONJ_TAC THENL [ + REPEAT AP_TERM_TAC THEN UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; + + REPEAT AP_TERM_TAC THEN UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; + + MATCH_MP_TAC READ_MEMORY_BYTES_MERGE THEN + MAP_EVERY EXISTS_TAC [`val (width:int64) - 8 * (i'+1)`; `8`] THEN + ASM_REWRITE_TAC[LOWDIGITS_TRIVIAL] THEN + CONJ_TAC THENL [ + REWRITE_TAC[ARITH_RULE`8*8=64`] THEN MATCH_MP_TAC READ_MEMORY_BYTES_MERGE_FOUR128 THEN + MAP_EVERY EXISTS_TAC [ + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 16)):int64`; + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 32)):int64`; + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 48)):int64`; + ] THEN + MAP_EVERY EXISTS_TAC [`val (word 0:int128)`;`val (word 0:int128)`;`val (word 0:int128)`;`val (word 0:int128)`] THEN + ASM_REWRITE_TAC[VAL_WORD_0; WORD_AND_0; HIGHDIGITS_TRIVIAL; MULT_0; ADD_0] THEN + REWRITE_TAC [WORD_ADD_ASSOC_CONSTS] THEN CONV_TAC WORD_ARITH; + + UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC + ]; + + IMP_REWRITE_TAC[VAL_WORD_8_EQ_0] + ]; ALL_TAC] THEN + + ASSERT_USING_ASM_ARITH_TAC `i > val (idx:int64)` THEN + MAP_EVERY REWRITE_ASSUMES_TAC [`~(i < val (idx:int64))`; `i > val (idx:int64)`] THEN + MAP_EVERY (fun t -> REWRITE_TAC[ASSUME t]) [`~(i < val (idx:int64))`; `i > val (idx:int64)`] THEN + SPLIT_FIRST_CONJ_ASSUM_TAC THEN + + ABBREV_TAC `i'' = val (width:int64) - 8 * (i'+1)` THEN + SUBGOAL_THEN `read (memory :> bytes (z, 8 * val (width:int64))) s0 = m` ASSUME_TAC THENL [ + MATCH_MP_TAC READ_MEMORY_BYTES_MERGE THEN + MAP_EVERY EXISTS_TAC [`i'':num`; `8*((i':num)+1)`] THEN + ASM_REWRITE_TAC[] THEN EXPAND_TAC "i''" THEN ASM_ARITH_TAC; + ALL_TAC + ] THEN + SUBGOAL_THEN + `(q0:int128) = word (lowdigits (highdigits m i'') 2) /\ + (q1:int128) = word (lowdigits (highdigits m (i''+2)) 2) /\ + (q2:int128) = word (lowdigits (highdigits m (i''+4)) 2) /\ + (q3:int128) = word (lowdigits (highdigits m (i''+6)) 2)` + (fun thm -> RULE_ASSUM_TAC (REWRITE_RULE [thm])) THENL [ + MAP_EVERY EXPAND_TAC ["q0";"q1";"q2";"q3"] THEN + REWRITE_TAC[GSYM WORD_ADD_ASSOC_CONSTS] THEN REWRITE_TAC(map ARITH_RULE [`16=8*2`;`32=8*4`;`48=8*6`]) THEN + REPEAT CONJ_TAC THEN ONCE_REWRITE_TAC[GSYM VAL_EQ] THEN + SIMP_TAC[VAL_WORD_EQ;DIMINDEX_128;ARITH_RULE`128=64*2`;LOWDIGITS_BOUND] THENL [ + MATCH_MP_TAC READ_MEMORY_BYTES_FIRSTELEM128 THEN EXISTS_TAC `8 * (i' + 1)` THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; + + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128] THEN + REWRITE_TAC[ARITH_RULE `16=8*2`; WORD_ADD_ASSOC_CONSTS; GSYM LEFT_ADD_DISTRIB] THEN + MATCH_MP_TAC READ_MEMORY_BYTES_SLICE THEN EXISTS_TAC `val (width:int64)` THEN + ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; + + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128] THEN + REWRITE_TAC[ARITH_RULE `16=8*2`; WORD_ADD_ASSOC_CONSTS; GSYM LEFT_ADD_DISTRIB] THEN + MATCH_MP_TAC READ_MEMORY_BYTES_SLICE THEN EXISTS_TAC `val (width:int64)` THEN + ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; + + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128] THEN + REWRITE_TAC[ARITH_RULE `16=8*2`; WORD_ADD_ASSOC_CONSTS; GSYM LEFT_ADD_DISTRIB] THEN + MATCH_MP_TAC READ_MEMORY_BYTES_SLICE THEN EXISTS_TAC `val (width:int64)` THEN + ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC; + ]; + + ALL_TAC + ] THEN + SUBGOAL_THEN `read (memory :> + bytes (word_add (word_add (z:int64) (word (8 * i''))) (word (8 * 8)), 8 * 8 * i')) s0 = + highdigits (highdigits m i'') 8` (fun thm -> + ASSUME_TAC (REWRITE_RULE [HIGHDIGITS_HIGHDIGITS; WORD_ADD_ASSOC_CONSTS;ARITH_RULE`8*8=64`] thm)) THENL [ + MATCH_MP_TAC READ_MEMORY_BYTES_SLICE_HIGH THEN + EXISTS_TAC `8 * (i' + 1)` THEN ASM_REWRITE_TAC[ARITH_RULE `8*(x+1)=8+8*x`]; + + ALL_TAC] THEN + ASSERT_USING_ASM_ARITH_TAC `(8 * i'' + 64) + 8 * 8 * i' <= 18446744073709551616` THEN + + ARM_STEPS_TAC BIGNUM_COPY_ROW_FROM_TABLE_8N_NEON_EXEC (1--19) THEN + ENSURES_FINAL_STATE_TAC THEN + SUBST_ALL_TAC (GSYM (ASSUME `val (width:int64) - 8 * (i' + 1) = i''`)) THEN + SUBGOAL_THEN `8 * (val (width:int64) - 8 * (i' + 1)) + 64 = 8 * (val width - 8 * i')` SUBST_ALL_TAC THENL [ + UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; ALL_TAC] THEN + ASM_REWRITE_TAC[WORD_SUB_ADD; WORD_ADD_ASSOC_CONSTS; + WORD_RULE `word_sub (word (8 * (i' + 1))) (word 8):int64 = word (8 * i')`] THEN + REPEAT CONJ_TAC THENL [ + REPEAT AP_TERM_TAC THEN UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; + + REPEAT AP_TERM_TAC THEN UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; + + MATCH_MP_TAC READ_MEMORY_BYTES_MERGE THEN + MAP_EVERY EXISTS_TAC [`val (width:int64) - 8 * (i'+1)`; `8`] THEN ASM_REWRITE_TAC[] THEN + REPEAT CONJ_TAC THENL [ + REWRITE_TAC[LOWDIGITS_LOWDIGITS] THEN AP_TERM_TAC THEN ARITH_TAC; + + REWRITE_TAC[ARITH_RULE`8*8=64`] THEN MATCH_MP_TAC READ_MEMORY_BYTES_MERGE_FOUR128 THEN + MAP_EVERY EXISTS_TAC [ + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 16)):int64`; + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 32)):int64`; + `word_add z (word (8 * (val (width:int64) - 8 * (i' + 1)) + 48)):int64`; + ] THEN + MAP_EVERY EXISTS_TAC [ + `lowdigits (highdigits m (val (width:int64) - 8 * (i' + 1))) 2`; + `lowdigits (highdigits m (val (width:int64) - 8 * (i' + 1) + 2)) 2`; + `lowdigits (highdigits m (val (width:int64) - 8 * (i' + 1) + 4)) 2`; + `lowdigits (highdigits m (val (width:int64) - 8 * (i' + 1) + 6)) 2`] THEN + ASM_SIMP_TAC [WORD_AND_0;WORD_OR_0;VAL_WORD_EQ;DIMINDEX_128;ARITH_RULE`128=64*2`;LOWDIGITS_BOUND;WORD_AND_128_FULLBITS] THEN + REPEAT CONJ_TAC THEN TRY (REWRITE_TAC [WORD_ADD_ASSOC_CONSTS] THEN CONV_TAC WORD_ARITH) THEN + EXPAND_TAC "m" THEN + REWRITE_TAC[GSYM READ_MEMORY_BYTES_BYTES128;ARITH_RULE`16=8*2`;GSYM BIGNUM_FROM_MEMORY_BYTES] THEN + REWRITE_TAC[LOWDIGITS_BIGNUM_FROM_MEMORY;ARITH_RULE`MIN x (x-y) = x-y`;HIGHDIGITS_BIGNUM_FROM_MEMORY] THEN + IMP_REWRITE_TAC (map ARITH_RULE [ + `!x y. y < x DIV 8 ==> MIN (x-(x-8*(y+1)+6)) 2 = 2`; + `!x y. y < x DIV 8 ==> MIN (x-(x-8*(y+1)+4)) 2 = 2`; + `!x y. y < x DIV 8 ==> MIN (x-(x-8*(y+1)+2)) 2 = 2`; + `!x y. y < x DIV 8 ==> MIN (x-(x-8*(y+1))) 2 = 2` + ]) THEN + SUBGOAL_THEN `val (width:int64) - 8 * i' - (val width - 8 * (i' + 1)) = 8` (fun thm -> REWRITE_TAC[thm]) THENL [ + UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; ALL_TAC + ] THEN + REWRITE_TAC[WORD_ADD_ASSOC_CONSTS] THEN + REWRITE_TAC((map PAIR_EQ_ARITH_RULE [ + (`(x:int64,8)`, `(x:int64,2+6)`); + (`(x:int64,6)`, `(x:int64,2+4)`); + (`(x:int64,4)`, `(x:int64,2+2)`)]) @ [BIGNUM_FROM_MEMORY_SPLIT]) THEN + REWRITE_TAC [WORD_ADD_ASSOC_CONSTS; LEFT_ADD_DISTRIB;MULT_ASSOC;GSYM EXP_ADD;GSYM ADD_ASSOC] THEN + ARITH_TAC; + + UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC + ]; + + AP_TERM_TAC THEN UNDISCH_TAC `i' < val (width:int64) DIV 8` THEN ARITH_TAC; + + IMP_REWRITE_TAC[VAL_WORD_8_EQ_0] + ]);; \ No newline at end of file diff --git a/benchmarks/benchmark.c b/benchmarks/benchmark.c index 0e7ab5b9..986b476a 100644 --- a/benchmarks/benchmark.c +++ b/benchmarks/benchmark.c @@ -740,22 +740,48 @@ void call_sm2_montjdouble(void) repeat(sm2_montjdouble(b1,b2)) void call_sm2_montjmixadd(void) repeat(sm2_montjmixadd(b1,b2,b3)) #ifdef __ARM_NEON -void call_bignum_mul_8_16_neon(void) repeat(bignum_mul_8_16_neon(b0,b1,b2)) -void call_bignum_sqr_8_16_neon(void) repeat(bignum_sqr_8_16_neon(b0,b1)) +// TODO: Once the x86 version of bignum_copy_row_from_table is added, move +// these two functions outside. +void call_bignum_copy_row_from_table__32_16(void) \ + repeat(bignum_copy_row_from_table(b0,b1,32,16,0)) +void call_bignum_copy_row_from_table__32_32(void) \ + repeat(bignum_copy_row_from_table(b0,b1,32,32,0)) + +void call_bignum_copy_row_from_table_8n_neon__32_16(void) \ + repeat(bignum_copy_row_from_table_8n_neon(b0,b1,32,16,0)) +void call_bignum_copy_row_from_table_8n_neon__32_32(void) \ + repeat(bignum_copy_row_from_table_8n_neon(b0,b1,32,32,0)) +void call_bignum_copy_row_from_table_16_neon__32(void) \ + repeat(bignum_copy_row_from_table_16_neon(b0,b1,32,0)) +void call_bignum_copy_row_from_table_32_neon__32(void) \ + repeat(bignum_copy_row_from_table_32_neon(b0,b1,32,0)) + +void call_bignum_emontredc_8n_neon__32(void) repeat(bignum_emontredc_8n_neon(32,b0,b1,b2[0])) void call_bignum_kmul_16_32_neon(void) repeat(bignum_kmul_16_32_neon(b0,b1,b2,b3)) void call_bignum_ksqr_16_32_neon(void) repeat(bignum_ksqr_16_32_neon(b0,b1,b2)) void call_bignum_kmul_32_64_neon(void) repeat(bignum_kmul_32_64_neon(b0,b1,b2,b3)) void call_bignum_ksqr_32_64_neon(void) repeat(bignum_ksqr_32_64_neon(b0,b1,b2)) -void call_bignum_emontredc_8n_neon__32(void) repeat(bignum_emontredc_8n_neon(32,b0,b1,b2[0])) +void call_bignum_mul_8_16_neon(void) repeat(bignum_mul_8_16_neon(b0,b1,b2)) +void call_bignum_sqr_8_16_neon(void) repeat(bignum_sqr_8_16_neon(b0,b1)) #else -void call_bignum_mul_8_16_neon(void) {} -void call_bignum_sqr_8_16_neon(void) {} +// TODO: Once the x86 version of bignum_copy_row_from_table is added, remove these +// two functions. +void call_bignum_copy_row_from_table__32_16(void) {} +void call_bignum_copy_row_from_table__32_32(void) {} + +void call_bignum_copy_row_from_table_8n_neon__32_16(void) {} +void call_bignum_copy_row_from_table_8n_neon__32_32(void) {} +void call_bignum_copy_row_from_table_16_neon__32(void) {} +void call_bignum_copy_row_from_table_32_neon__32(void) {} + +void call_bignum_emontredc_8n_neon__32(void) {} void call_bignum_kmul_16_32_neon(void) {} void call_bignum_ksqr_16_32_neon(void) {} void call_bignum_kmul_32_64_neon(void) {} void call_bignum_ksqr_32_64_neon(void) {} -void call_bignum_emontredc_8n_neon__32(void) {} +void call_bignum_mul_8_16_neon(void) {} +void call_bignum_sqr_8_16_neon(void) {} #endif @@ -866,6 +892,14 @@ int main(int argc, char *argv[]) timingtest(all,"bignum_coprime (6x6)",call_bignum_coprime__6_6); timingtest(all,"bignum_coprime (16x16)",call_bignum_coprime__16_16); timingtest(all,"bignum_copy (32 -> 32)" ,call_bignum_copy__32_32); + // TODO: Once the x86 version of bignum_copy_row_from_table is verified, + // change the conditions of these two timingtest from 'neon' to 'all'. + timingtest(neon,"bignum_copy_row_from_table (h=32,w=16)",call_bignum_copy_row_from_table__32_16); + timingtest(neon,"bignum_copy_row_from_table (h=32,w=32)",call_bignum_copy_row_from_table__32_32); + timingtest(neon,"bignum_copy_row_from_table_8n_neon (h=32,w=16)",call_bignum_copy_row_from_table_8n_neon__32_16); + timingtest(neon,"bignum_copy_row_from_table_8n_neon (h=32,w=32)",call_bignum_copy_row_from_table_8n_neon__32_32); + timingtest(neon,"bignum_copy_row_from_table_16_neon (h=32)",call_bignum_copy_row_from_table_16_neon__32); + timingtest(neon,"bignum_copy_row_from_table_32_neon (h=32)",call_bignum_copy_row_from_table_32_neon__32); timingtest(all,"bignum_ctd (32)" ,call_bignum_ctd__32); timingtest(all,"bignum_ctz (32)" ,call_bignum_ctz__32); timingtest(bmi,"bignum_deamont_p256",call_bignum_deamont_p256); diff --git a/common/misc.ml b/common/misc.ml index cf9a0f14..6f238251 100644 --- a/common/misc.ml +++ b/common/misc.ml @@ -1196,6 +1196,44 @@ let cache f = fun x -> try assoc x (!memo) with Failure _ -> (let y = f x in (memo := (x,y) :: (!memo); y));; +(* ------------------------------------------------------------------------- *) +(* Extensions of REPEAT tactic *) +(* ------------------------------------------------------------------------- *) + +let rec REPEAT_N (n:int) (t:tactic):tactic = + if n = 0 then ALL_TAC + else t THEN (REPEAT_N (n-1) t);; + +let rec REPEAT_I_N (i:int) (n:int) (t:int->tactic):tactic = + if i = n then ALL_TAC + else (t i) THEN (REPEAT_I_N (i+1) n t);; + +(* ------------------------------------------------------------------------- *) +(* Tactics that break a conjunction/disjunction in assumptions *) +(* ------------------------------------------------------------------------- *) + +let SPLIT_FIRST_CONJ_ASSUM_TAC = + FIRST_X_ASSUM (fun thm -> + let t1,t2 = CONJ_PAIR thm in MAP_EVERY ASSUME_TAC [t1;t2]);; + +let CASES_FIRST_DISJ_ASSUM_TAC = + FIRST_X_ASSUM (fun thm -> + if is_disj (concl thm) then DISJ_CASES_TAC thm else failwith "");; + +(* ------------------------------------------------------------------------- *) +(* Tactics that prove a subgoal using {ASM_}ARITH_TAC. *) +(* ------------------------------------------------------------------------- *) + +(* ASSERT_USING_UNDISCH_AND_ARITH_TAC t1 t0 proves t1 using t0 and + assumes t1 *) +let ASSERT_USING_UNDISCH_AND_ARITH_TAC t t' = + SUBGOAL_THEN t ASSUME_TAC THENL [UNDISCH_TAC t' THEN ARITH_TAC; ALL_TAC];; + +(* ASSERT_USING_ASM_ARITH_TAC t proves t using ASM_ARITH_TAC and + assumes t *) +let ASSERT_USING_ASM_ARITH_TAC t = + SUBGOAL_THEN t ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC];; + (* ------------------------------------------------------------------------- *) (* A few more lemmas about words. *) (* ------------------------------------------------------------------------- *) @@ -1273,10 +1311,14 @@ let WORD_MUL_EQ = prove( REWRITE_TAC[GSYM VAL_EQ; VAL_WORD_MUL; VAL_WORD; DIMINDEX_64; MOD_MOD_REFL; MOD_MOD_EXP_MIN] THEN CONV_TAC(DEPTH_CONV NUM_MIN_CONV) THEN MESON_TAC[]);; +let WORD_SUB_ADD = WORD_RULE `word_sub (word (a + b)) (word b) = word a`;; + (* ------------------------------------------------------------------------- *) (* A few more lemmas about natural numbers. *) (* ------------------------------------------------------------------------- *) +let GT_REFL = prove(`!(x:num). ~(x > x)`, ARITH_TAC);; + let ADD_MOD_MOD_REFL = prove(`!a b m. (a + b MOD m) MOD m = (a + b) MOD m /\ (a MOD m + b) MOD m = (a + b) MOD m`, @@ -1338,6 +1380,14 @@ let ADD_DIV_MOD_SIMP2_LEMMA = prove(`!(x:num) (y:num) (m:num). ASM_SIMP_TAC[MOD_MULT_ADD;DIV_MULT_ADD;MOD_LT;DIV_LT;ADD_SYM] THEN ARITH_TAC);; +let LE_MULT_ADD = prove(`!(x:num) (x2:num) (y:num). x < x2 ==> x * y + y <= x2 * y`, + REPEAT STRIP_TAC THEN REWRITE_TAC[ARITH_RULE `x * y + y= (x + 1)*y`] THEN + REWRITE_TAC[LE_MULT_RCANCEL] THEN + ASM_ARITH_TAC);; + +let ADD_SUB_SWAP = prove(`!(x:num) (y:num) (z:num). y >= z /\ x >= z ==> x + (y - z) = y + (x - z)`, + ARITH_TAC);; + (* ------------------------------------------------------------------------- *) (* A simple tactic that is helpful for debugging. *) (* ------------------------------------------------------------------------- *) diff --git a/include/s2n-bignum-c89.h b/include/s2n-bignum-c89.h index 8d3e8c64..80074a57 100644 --- a/include/s2n-bignum-c89.h +++ b/include/s2n-bignum-c89.h @@ -156,6 +156,40 @@ extern uint64_t bignum_coprime (uint64_t m, uint64_t *x, uint64_t n, uint64_t *y /* Input x[n]; output z[k] */ extern void bignum_copy (uint64_t k, uint64_t *z, uint64_t n, uint64_t *x); +/* Given table: uint64_t[height*width], copy table[idx*width...(idx+1)*width-1] */ +/* into z[0..width-1]. */ +/* 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. */ +/* Input table[height*width]; output z[width] */ +extern void bignum_copy_row_from_table (uint64_t *z, uint64_t *table, uint64_t height, + uint64_t width, uint64_t idx); + +/* Given table: uint64_t[height*width], copy table[idx*width...(idx+1)*width-1] */ +/* 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. */ +/* Input table[height*width]; output z[width] */ +extern void bignum_copy_row_from_table_8n_neon (uint64_t *z, uint64_t *table, + uint64_t height, uint64_t width, uint64_t idx); + +/* Given table: uint64_t[height*16], copy table[idx*16...(idx+1)*16-1] into z[0..row-1]. */ +/* 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. */ +/* Input table[height*16]; output z[16] */ +extern void bignum_copy_row_from_table_16_neon (uint64_t *z, uint64_t *table, + uint64_t height, uint64_t idx); + +/* Given table: uint64_t[height*32], copy table[idx*32...(idx+1)*32-1] into z[0..row-1]. */ +/* 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. */ +/* Input table[height*32]; output z[32] */ +extern void bignum_copy_row_from_table_32_neon (uint64_t *z, uint64_t *table, + uint64_t height, uint64_t idx); + /* Count trailing zero digits (64-bit words) */ /* Input x[k]; output function return */ extern uint64_t bignum_ctd (uint64_t k, uint64_t *x); diff --git a/include/s2n-bignum.h b/include/s2n-bignum.h index 3916ce05..bf669c35 100644 --- a/include/s2n-bignum.h +++ b/include/s2n-bignum.h @@ -154,6 +154,40 @@ extern uint64_t bignum_coprime (uint64_t m, uint64_t *x, uint64_t n, uint64_t *y // Input x[n]; output z[k] extern void bignum_copy (uint64_t k, uint64_t *z, uint64_t n, uint64_t *x); +// Given table: uint64_t[height*width], copy table[idx*width...(idx+1)*width-1] +// into z[0..width-1]. +// 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. +// Input table[height*width]; output z[width] +extern void bignum_copy_row_from_table (uint64_t *z, uint64_t *table, uint64_t height, + uint64_t width, uint64_t idx); + +// Given table: uint64_t[height*width], copy table[idx*width...(idx+1)*width-1] +// 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. +// Input table[height*width]; output z[width] +extern void bignum_copy_row_from_table_8n_neon (uint64_t *z, uint64_t *table, + uint64_t height, uint64_t width, uint64_t idx); + +// Given table: uint64_t[height*16], copy table[idx*16...(idx+1)*16-1] into z[0..row-1]. +// 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. +// Input table[height*16]; output z[16] +extern void bignum_copy_row_from_table_16_neon (uint64_t *z, uint64_t *table, + uint64_t height, uint64_t idx); + +// Given table: uint64_t[height*32], copy table[idx*32...(idx+1)*32-1] into z[0..row-1]. +// 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. +// Input table[height*32]; output z[32] +extern void bignum_copy_row_from_table_32_neon (uint64_t *z, uint64_t *table, + uint64_t height, uint64_t idx); + // Count trailing zero digits (64-bit words) // Input x[k]; output function return extern uint64_t bignum_ctd (uint64_t k, uint64_t *x); diff --git a/tests/test.c b/tests/test.c index b96a56d8..a954f675 100644 --- a/tests/test.c +++ b/tests/test.c @@ -9,9 +9,11 @@ // against disparities between the formal model and the real world. // *************************************************************************** +#include #include #include #include +#include #include #include #include @@ -2554,6 +2556,112 @@ int test_bignum_copy(void) return 0; } +int test_bignum_copy_row_from_table_specific(const char *name, uint64_t fixed_width, + int width_multiple_of_8, + void (*f)(uint64_t*, uint64_t*, uint64_t, uint64_t, uint64_t)) +{ uint64_t i, t; + // The height, width, height*width of table + uint64_t h, w, n; + printf("Testing %s with %d cases\n", name, tests); + int c; + + for (t = 0; t < tests; ++t) + { // Use BUFFERSIZE instead of MAXSIZE because MAXSIZE is too small + if (fixed_width) w = fixed_width; + else { + w = (uint64_t) rand() % (uint64_t)sqrt((double)BUFFERSIZE); + if (width_multiple_of_8) w = w & ~7ull; + } + + h = (uint64_t) rand() % (uint64_t)sqrt((double)BUFFERSIZE); + if (h == 0) ++h; + n = h * w; + uint64_t *table = malloc(n * sizeof(uint64_t)); + for (i = 0; i < h; ++i) + random_bignum(w,&table[w * i]); + + i = rand() % h; + reference_copy(w,b1,w,&table[w * i]); + f(b2, table, h, w, i); + + c = reference_compare(w,b2,w,b1); + free(table); + + if (c != 0) + { printf("### Disparity: [height %5"PRIu64", width %5"PRIu64"] " + "table [%5"PRIu64"*%5"PRIu64"] = ....0x%016"PRIx64" not ...0x%016"PRIx64"\n", + h, w, i, w, b2[0], b1[0]); + return 1; + } + else if (VERBOSE) + { printf("OK: [height %5"PRIu64", width %5"PRIu64"]", h, w); + if (n == 0) printf("\n"); + else printf(" element [%5"PRIu64"*%5"PRIu64"] = .0x%016"PRIx64"\n", + i, w, b2[0]); + } + } + printf("All OK\n"); + return 0; +} + +int test_bignum_copy_row_from_table(void) +{ +// TODO: Once the x86 version of bignum_copy_row_from_table is verified, +// remove this __ARM_NEON guard. +#ifdef __ARM_NEON + return test_bignum_copy_row_from_table_specific("bignum_copy_row_from_table", + 0, 0, bignum_copy_row_from_table); +#else + return 1; +#endif +} + +int test_bignum_copy_row_from_table_8n_neon(void) +{ +#ifdef __ARM_NEON + return test_bignum_copy_row_from_table_specific("bignum_copy_row_from_table_8n_neon", + 0, 1, bignum_copy_row_from_table_8n_neon); +#else + return 1; +#endif +} + +#ifdef __ARM_NEON +void _bignum_copy_row_from_table_16_neon_wrapper(uint64_t *z, uint64_t *table, + uint64_t height, uint64_t width, uint64_t index) +{ assert(width == 16); + bignum_copy_row_from_table_16_neon(z, table, height, index); +} + +int test_bignum_copy_row_from_table_16_neon(void) +{ return test_bignum_copy_row_from_table_specific( + "bignum_copy_row_from_table_16_neon", 16, 0, + _bignum_copy_row_from_table_16_neon_wrapper); +} +#else +int test_bignum_copy_row_from_table_16_neon(void) +{ return 1; +} +#endif + +#ifdef __ARM_NEON +void _bignum_copy_row_from_table_32_neon_wrapper(uint64_t *z, uint64_t *table, + uint64_t height, uint64_t width, uint64_t index) +{ assert(width == 32); + bignum_copy_row_from_table_32_neon(z, table, height, index); +} + +int test_bignum_copy_row_from_table_32_neon(void) +{ return test_bignum_copy_row_from_table_specific( + "bignum_copy_row_from_table_32_neon", 32, 0, + _bignum_copy_row_from_table_32_neon_wrapper); +} +#else +int test_bignum_copy_row_from_table_32_neon(void) +{ return 1; +} +#endif + int test_bignum_ctd(void) { uint64_t t, k; printf("Testing bignum_ctd with %d cases\n",tests); @@ -10940,6 +11048,13 @@ int main(int argc, char *argv[]) if (get_arch_name() == ARCH_AARCH64) { int neon = supports_neon(); + // TODO: Once the x86 version of bignum_copy_row_from_table is verified, hoist + // this functionaltest out of this if branch and turn the condition into 'all'. + functionaltest(neon,"bignum_copy_row_from_table",test_bignum_copy_row_from_table); + + functionaltest(neon,"bignum_copy_row_from_table_8n_neon",test_bignum_copy_row_from_table_8n_neon); + functionaltest(neon,"bignum_copy_row_from_table_16_neon",test_bignum_copy_row_from_table_16_neon); + functionaltest(neon,"bignum_copy_row_from_table_32_neon",test_bignum_copy_row_from_table_32_neon); functionaltest(neon,"bignum_emontredc_8n_neon",test_bignum_emontredc_8n_neon); functionaltest(neon,"bignum_kmul_16_32_neon", test_bignum_kmul_16_32_neon); functionaltest(neon,"bignum_kmul_32_64_neon", test_bignum_kmul_32_64_neon);