diff --git a/arm/curve25519/bignum_mul_p25519.S b/arm/curve25519/bignum_mul_p25519.S index 291573a3..fcdd0790 100644 --- a/arm/curve25519/bignum_mul_p25519.S +++ b/arm/curve25519/bignum_mul_p25519.S @@ -29,149 +29,208 @@ .text .balign 4 -// --------------------------------------------------------------------------- -// Macro computing [c,b,a] := [b,a] + (x - y) * (w - z), adding with carry -// to the [b,a] components but leaving CF aligned with the c term, which is -// a sign bitmask for (x - y) * (w - z). Continued add-with-carry operations -// with [c,...,c] will continue the carry chain correctly starting from -// the c position if desired to add to a longer term of the form [...,b,a]. -// -// c,h,l,t should all be different and t,h should not overlap w,z. -// --------------------------------------------------------------------------- - -#define muldiffnadd(b,a,x,y,w,z) \ - subs t, x, y; \ - cneg t, t, cc; \ - csetm c, cc; \ - subs h, w, z; \ - cneg h, h, cc; \ - mul l, t, h; \ - umulh h, t, h; \ - cinv c, c, cc; \ - adds xzr, c, #1; \ - eor l, l, c; \ - adcs a, a, l; \ - eor h, h, c; \ - adcs b, b, h +#define z x0 +#define x x1 +#define y x2 #define a0 x3 #define a1 x4 -#define a2 x5 -#define a3 x6 -#define b0 x7 -#define b1 x8 -#define b2 x9 -#define b3 x10 - -#define s0 x11 -#define s1 x12 -#define s2 x13 -#define s3 x14 -#define s4 x15 - -#define m x15 -#define q x15 - -#define t0 x11 -#define t1 x16 -#define t2 x12 -#define t3 x13 -#define t4 x14 -#define t5 x15 - -#define u0 x11 -#define u1 x16 -#define u2 x1 -#define u3 x2 -#define u4 x12 -#define u5 x13 -#define u6 x14 -#define u7 x15 - -#define c x17 -#define h x19 -#define l x20 -#define t x21 -#define d x21 +#define b0 x5 +#define b1 x6 + +#define u0 x7 +#define u1 x8 +#define u2 x9 +#define u3 x10 +#define u4 x11 +#define u5 x12 +#define u6 x13 +#define u7 x14 + +#define t x15 + +#define sgn x16 +#define ysgn x17 + +// These are aliases to registers used elsewhere including input pointers. +// By the time they are used this does not conflict with other uses. + +#define m0 y +#define m1 ysgn +#define m2 t +#define m3 x +#define u u2 + +// For the reduction stages, again aliasing other things but not the u's + +#define c x3 +#define h x4 +#define l x5 +#define d x6 +#define q x17 S2N_BN_SYMBOL(bignum_mul_p25519): -// Save additional registers to use - - stp x19, x20, [sp, #-16]! - stp x21, x22, [sp, #-16]! - -// Load operands - - ldp a0, a1, [x1] - ldp b0, b1, [x2] - ldp a2, a3, [x1, #16] - ldp b2, b3, [x2, #16] - -// First accumulate all the "simple" products as [s4,s3,s2,s1,s0] - - mul s0, a0, b0 - mul s1, a1, b1 - mul s2, a2, b2 - mul s3, a3, b3 - - umulh m, a0, b0 - adds s1, s1, m - umulh m, a1, b1 - adcs s2, s2, m - umulh m, a2, b2 - adcs s3, s3, m - umulh m, a3, b3 - adc s4, m, xzr - -// Multiply by B + 1 to get [t5;t4;t3;t2;t1;t0] where t0 == s0 - - adds t1, s1, s0 - adcs t2, s2, s1 - adcs t3, s3, s2 - adcs t4, s4, s3 - adc t5, xzr, s4 - -// Multiply by B^2 + 1 to get [u6;u5;u4;u3;u2;u1;-]. Note that -// u0 == t0 == s0 and u1 == t1 - - adds u2, t2, t0 - adcs u3, t3, t1 - adcs u4, t4, t2 - adcs u5, t5, t3 - adcs u6, xzr, t4 - adc u7, xzr, t5 - -// Now add in all the "complicated" terms. - - muldiffnadd(u6,u5, a2,a3, b3,b2) - adc u7, u7, c - - muldiffnadd(u2,u1, a0,a1, b1,b0) - adcs u3, u3, c - adcs u4, u4, c - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd(u5,u4, a1,a3, b3,b1) - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd(u3,u2, a0,a2, b2,b0) - adcs u4, u4, c - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd(u4,u3, a0,a3, b3,b0) - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - muldiffnadd(u4,u3, a1,a2, b2,b1) - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c +// Multiply the low halves using Karatsuba 2x2->4 to get [u3,u2,u1,u0] + + ldp a0, a1, [x] + ldp b0, b1, [y] + + mul u0, a0, b0 + umulh u1, a0, b0 + mul u2, a1, b1 + umulh u3, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm sgn, cc + + adds u2, u2, u1 + adc u3, u3, xzr + + subs a0, b0, b1 + cneg a0, a0, cc + cinv sgn, sgn, cc + + mul t, a1, a0 + umulh a0, a1, a0 + + adds u1, u0, u2 + adcs u2, u2, u3 + adc u3, u3, xzr + + adds xzr, sgn, #1 + eor t, t, sgn + adcs u1, t, u1 + eor a0, a0, sgn + adcs u2, a0, u2 + adc u3, u3, sgn + +// Multiply the high halves using Karatsuba 2x2->4 to get [u7,u6,u5,u4] + + ldp a0, a1, [x, #16] + ldp b0, b1, [y, #16] + + mul u4, a0, b0 + umulh u5, a0, b0 + mul u6, a1, b1 + umulh u7, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm sgn, cc + + adds u6, u6, u5 + adc u7, u7, xzr + + subs a0, b0, b1 + cneg a0, a0, cc + cinv sgn, sgn, cc + + mul t, a1, a0 + umulh a0, a1, a0 + + adds u5, u4, u6 + adcs u6, u6, u7 + adc u7, u7, xzr + + adds xzr, sgn, #1 + eor t, t, sgn + adcs u5, t, u5 + eor a0, a0, sgn + adcs u6, a0, u6 + adc u7, u7, sgn + +// Compute sgn,[a1,a0] = x_hi - x_lo +// and ysgn,[b1,b0] = y_lo - y_hi +// sign-magnitude differences + + ldp a0, a1, [x, #16] + ldp t, sgn, [x] + subs a0, a0, t + sbcs a1, a1, sgn + csetm sgn, cc + + ldp t, ysgn, [y] + subs b0, t, b0 + sbcs b1, ysgn, b1 + csetm ysgn, cc + + eor a0, a0, sgn + subs a0, a0, sgn + eor a1, a1, sgn + sbc a1, a1, sgn + + eor b0, b0, ysgn + subs b0, b0, ysgn + eor b1, b1, ysgn + sbc b1, b1, ysgn + +// Save the correct sign for the sub-product + + eor sgn, ysgn, sgn + +// Add H' = H + L_top, still in [u7,u6,u5,u4] + + adds u4, u4, u2 + adcs u5, u5, u3 + adcs u6, u6, xzr + adc u7, u7, xzr + +// Now compute the mid-product as [m3,m2,m1,m0] + + mul m0, a0, b0 + umulh m1, a0, b0 + mul m2, a1, b1 + umulh m3, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm u, cc + + adds m2, m2, m1 + adc m3, m3, xzr + + subs b1, b0, b1 + cneg b1, b1, cc + cinv u, u, cc + + mul b0, a1, b1 + umulh b1, a1, b1 + + adds m1, m0, m2 + adcs m2, m2, m3 + adc m3, m3, xzr + + adds xzr, u, #1 + eor b0, b0, u + adcs m1, b0, m1 + eor b1, b1, u + adcs m2, b1, m2 + adc m3, m3, u + +// Accumulate the positive mid-terms as [u7,u6,u5,u4,u3,u2] + + adds u2, u4, u0 + adcs u3, u5, u1 + adcs u4, u6, u4 + adcs u5, u7, u5 + adcs u6, u6, xzr + adc u7, u7, xzr + +// Add in the sign-adjusted complex term + + adds xzr, sgn, #1 + eor m0, m0, sgn + adcs u2, m0, u2 + eor m1, m1, sgn + adcs u3, m1, u3 + eor m2, m2, sgn + adcs u4, m2, u4 + eor m3, m3, sgn + adcs u5, m3, u5 + adcs u6, u6, sgn + adc u7, u7, sgn // Now we have the full 8-digit product 2^256 * h + l where // h = [u7,u6,u5,u4] and l = [u3,u2,u1,u0] @@ -249,12 +308,6 @@ S2N_BN_SYMBOL(bignum_mul_p25519): stp u0, u1, [x0] stp u2, u3, [x0, #16] - -// Restore regs and return - - ldp x21, x22, [sp], #16 - ldp x19, x20, [sp], #16 - ret #if defined(__linux__) && defined(__ELF__) diff --git a/arm/fastmul/bignum_mul_4_8.S b/arm/fastmul/bignum_mul_4_8.S index 1492154a..f2fe02e4 100644 --- a/arm/fastmul/bignum_mul_4_8.S +++ b/arm/fastmul/bignum_mul_4_8.S @@ -29,159 +29,207 @@ .text .balign 4 -// --------------------------------------------------------------------------- -// Macro computing [c,b,a] := [b,a] + (x - y) * (w - z), adding with carry -// to the [b,a] components but leaving CF aligned with the c term, which is -// a sign bitmask for (x - y) * (w - z). Continued add-with-carry operations -// with [c,...,c] will continue the carry chain correctly starting from -// the c position if desired to add to a longer term of the form [...,b,a]. -// -// c,h,l,t should all be different and t,h should not overlap w,z. -// --------------------------------------------------------------------------- - -.macro muldiffnadd b,a, c,h,l,t, x,y, w,z - subs \t, \x, \y - cneg \t, \t, cc - csetm \c, cc - subs \h, \w, \z - cneg \h, \h, cc - mul \l, \t, \h - umulh \h, \t, \h - cinv \c, \c, cc - adds xzr, \c, #1 - eor \l, \l, \c - adcs \a, \a, \l - eor \h, \h, \c - adcs \b, \b, \h -.endm - -// --------------------------------------------------------------------------- -// ADK version of 4x4->8 -// --------------------------------------------------------------------------- +#define z x0 +#define x x1 +#define y x2 #define a0 x3 #define a1 x4 -#define a2 x5 -#define a3 x6 -#define b0 x7 -#define b1 x8 -#define b2 x9 -#define b3 x10 - -#define s0 x11 -#define s1 x12 -#define s2 x13 -#define s3 x14 -#define s4 x15 - -#define m x15 - -#define t0 x11 -#define t1 x16 -#define t2 x12 -#define t3 x13 -#define t4 x14 -#define t5 x15 - -#define u0 x11 -#define u1 x16 -#define u2 x1 -#define u3 x2 -#define u4 x12 -#define u5 x13 -#define u6 x14 -#define u7 x15 - -#define c x11 -#define h x17 -#define l x19 -#define t x20 +#define b0 x5 +#define b1 x6 + +#define u0 x7 +#define u1 x8 +#define u2 x9 +#define u3 x10 +#define u4 x11 +#define u5 x12 +#define u6 x13 +#define u7 x14 + +#define t x15 + +#define sgn x16 +#define ysgn x17 + +// These are aliases to registers used elsewhere including input pointers. +// By the time they are used this does not conflict with other uses. + +#define m0 y +#define m1 ysgn +#define m2 t +#define m3 x +#define u u2 S2N_BN_SYMBOL(bignum_mul_4_8): -stp x19, x20, [sp, #-16]! - -// Load operands - - ldp a0, a1, [x1] - ldp b0, b1, [x2] - ldp a2, a3, [x1, #16] - ldp b2, b3, [x2, #16] - -// First accumulate all the "simple" products as [s4,s3,s2,s1,s0] - - mul s0, a0, b0 - mul s1, a1, b1 - mul s2, a2, b2 - mul s3, a3, b3 - - umulh m, a0, b0 - adds s1, s1, m - umulh m, a1, b1 - adcs s2, s2, m - umulh m, a2, b2 - adcs s3, s3, m - umulh m, a3, b3 - adc s4, m, xzr - -// Multiply by B + 1 to get [t5;t4;t3;t2;t1;t0] where t0 == s0 - - adds t1, s1, s0 - adcs t2, s2, s1 - adcs t3, s3, s2 - adcs t4, s4, s3 - adc t5, xzr, s4 - -// Multiply by B^2 + 1 to get [u6;u5;u4;u3;u2;u1;-], writing back LSD -// u0 == t0 == s0 and u1 == t1 - - str u0, [x0] - adds u2, t2, t0 - adcs u3, t3, t1 - adcs u4, t4, t2 - adcs u5, t5, t3 - adcs u6, xzr, t4 - adc u7, xzr, t5 - -// Now add in all the "complicated" terms. - - muldiffnadd u6,u5, c,h,l,t, a2,a3, b3,b2 - adc u7, u7, c - - muldiffnadd u2,u1, c,h,l,t, a0,a1, b1,b0 - str u1, [x0, #8] - adcs u3, u3, c - adcs u4, u4, c - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd u5,u4, c,h,l,t, a1,a3, b3,b1 - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd u3,u2, c,h,l,t, a0,a2, b2,b0 - adcs u4, u4, c - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd u4,u3, c,h,l,t, a0,a3, b3,b0 - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - muldiffnadd u4,u3, c,h,l,t, a1,a2, b2,b1 - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - - stp u2, u3, [x0, #16] - stp u4, u5, [x0, #32] - stp u6, u7, [x0, #48] - -// Restore regs and return - - ldp x19, x20, [sp], #16 +// Multiply the low halves using Karatsuba 2x2->4 to get [u3,u2,u1,u0] + + ldp a0, a1, [x] + ldp b0, b1, [y] + + mul u0, a0, b0 + umulh u1, a0, b0 + mul u2, a1, b1 + umulh u3, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm sgn, cc + + adds u2, u2, u1 + adc u3, u3, xzr + + subs a0, b0, b1 + cneg a0, a0, cc + cinv sgn, sgn, cc + + mul t, a1, a0 + umulh a0, a1, a0 + + adds u1, u0, u2 + adcs u2, u2, u3 + adc u3, u3, xzr + + adds xzr, sgn, #1 + eor t, t, sgn + adcs u1, t, u1 + eor a0, a0, sgn + adcs u2, a0, u2 + adc u3, u3, sgn + +// Multiply the high halves using Karatsuba 2x2->4 to get [u7,u6,u5,u4] + + ldp a0, a1, [x, #16] + ldp b0, b1, [y, #16] + + mul u4, a0, b0 + umulh u5, a0, b0 + mul u6, a1, b1 + umulh u7, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm sgn, cc + + adds u6, u6, u5 + adc u7, u7, xzr + + subs a0, b0, b1 + cneg a0, a0, cc + cinv sgn, sgn, cc + + mul t, a1, a0 + umulh a0, a1, a0 + + adds u5, u4, u6 + adcs u6, u6, u7 + adc u7, u7, xzr + + adds xzr, sgn, #1 + eor t, t, sgn + adcs u5, t, u5 + eor a0, a0, sgn + adcs u6, a0, u6 + adc u7, u7, sgn + +// Compute sgn,[a1,a0] = x_hi - x_lo +// and ysgn,[b1,b0] = y_lo - y_hi +// sign-magnitude differences + + ldp a0, a1, [x, #16] + ldp t, sgn, [x] + subs a0, a0, t + sbcs a1, a1, sgn + csetm sgn, cc + + ldp t, ysgn, [y] + subs b0, t, b0 + sbcs b1, ysgn, b1 + csetm ysgn, cc + + eor a0, a0, sgn + subs a0, a0, sgn + eor a1, a1, sgn + sbc a1, a1, sgn + + eor b0, b0, ysgn + subs b0, b0, ysgn + eor b1, b1, ysgn + sbc b1, b1, ysgn + +// Save the correct sign for the sub-product + + eor sgn, ysgn, sgn + +// Add H' = H + L_top, still in [u7,u6,u5,u4] + + adds u4, u4, u2 + adcs u5, u5, u3 + adcs u6, u6, xzr + adc u7, u7, xzr + +// Now compute the mid-product as [m3,m2,m1,m0] + + mul m0, a0, b0 + umulh m1, a0, b0 + mul m2, a1, b1 + umulh m3, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm u, cc + + adds m2, m2, m1 + adc m3, m3, xzr + + subs b1, b0, b1 + cneg b1, b1, cc + cinv u, u, cc + + mul b0, a1, b1 + umulh b1, a1, b1 + + adds m1, m0, m2 + adcs m2, m2, m3 + adc m3, m3, xzr + + adds xzr, u, #1 + eor b0, b0, u + adcs m1, b0, m1 + eor b1, b1, u + adcs m2, b1, m2 + adc m3, m3, u + +// Accumulate the positive mid-terms as [u7,u6,u5,u4,u3,u2] + + adds u2, u4, u0 + adcs u3, u5, u1 + adcs u4, u6, u4 + adcs u5, u7, u5 + adcs u6, u6, xzr + adc u7, u7, xzr + +// Add in the sign-adjusted complex term + + adds xzr, sgn, #1 + eor m0, m0, sgn + adcs u2, m0, u2 + eor m1, m1, sgn + adcs u3, m1, u3 + eor m2, m2, sgn + adcs u4, m2, u4 + eor m3, m3, sgn + adcs u5, m3, u5 + adcs u6, u6, sgn + adc u7, u7, sgn + +// Store back the result + + stp u0, u1, [z] + stp u2, u3, [z, #16] + stp u4, u5, [z, #32] + stp u6, u7, [z, #48] ret diff --git a/arm/proofs/arm.ml b/arm/proofs/arm.ml index 0d0ae5c7..3afe3f23 100644 --- a/arm/proofs/arm.ml +++ b/arm/proofs/arm.ml @@ -517,6 +517,16 @@ let (ARM_BIGSTEP_TAC:thm->string->tactic) = (* Simulate a subroutine, instantiating it from the state. *) (* ------------------------------------------------------------------------- *) +let TWEAK_PC_OFFSET = + let conv = + GEN_REWRITE_CONV (RAND_CONV o RAND_CONV) [ARITH_RULE `pc = pc + 0`] + and tweakneeded tm = + match tm with + Comb(Comb(Const("aligned_bytes_loaded",_),Var(_,_)), + Comb(Const("word",_),Var("pc",_))) -> true + | _ -> false in + CONV_RULE(ONCE_DEPTH_CONV(conv o check tweakneeded));; + let ARM_SUBROUTINE_SIM_TAC (machinecode,execth,offset,submachinecode,subth) = let subimpth = let th = MATCH_MP aligned_bytes_loaded_of_append3 @@ -533,7 +543,7 @@ let ARM_SUBROUTINE_SIM_TAC (machinecode,execth,offset,submachinecode,subth) = let svar = mk_var(sname,`:armstate`) and svar0 = mk_var("s",`:armstate`) in let ilist = map (vsubst[svar,svar0]) ilist0 in - MP_TAC(SPECL ilist subth) THEN + MP_TAC(TWEAK_PC_OFFSET(SPECL ilist subth)) THEN ASM_REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN REWRITE_TAC[ALLPAIRS; ALL; PAIRWISE; NONOVERLAPPING_CLAUSES] THEN ANTS_TAC THENL @@ -558,6 +568,71 @@ let ARM_SUBROUTINE_SIM_ABBREV_TAC tupper ilist0 = (tac n THEN ABBREV_TAC(mk_eq(mk_var(abn,type_of comp1),comp1))) (asl,w);; +(* ------------------------------------------------------------------------- *) +(* Simulate a macro, generating subgoal from a template *) +(* ------------------------------------------------------------------------- *) + +let ARM_MACRO_SIM_ABBREV_TAC = + let dest_pc tm = + match tm with + Comb(Const("word",_),Var("pc",_)) -> 0 + | Comb(Const("word",_),Comb(Comb(Const("+",_),Var("pc",_)),n)) -> + dest_small_numeral n + | _ -> failwith "dest_pc" + and mk_pc = + let pat0 = `word pc:int64` + and patn = `word(pc + n):int64` + and pan = `n:num` in + fun n -> if n = 0 then pat0 + else vsubst[mk_small_numeral n,pan] patn + and grab_dest = + let pat = `read (memory :> bytes(p,8 * n))` in + fun th -> + let cortm = rand(body(lhand(repeat (snd o dest_imp) (concl th)))) in + hd(find_terms (can (term_match [] pat)) cortm) in + let get_statenpc = + let fils = can (term_match [] `read PC s = word n`) o concl o snd in + fun asl -> + let rips = concl(snd(find fils asl)) in + rand(lhand rips),dest_pc(rand rips) in + let simprule = + CONV_RULE (ONCE_DEPTH_CONV NORMALIZE_ADD_SUBTRACT_WORD_CONV) o + GEN_REWRITE_RULE ONCE_DEPTH_CONV + [WORD_RULE `word_add z (word 0):int64 = z`] in + fun mc -> + let execth = ARM_MK_EXEC_RULE mc in + fun codelen localvars template core_tac prep ilist -> + let main_tac (asl,w) = + let svp,pc = get_statenpc asl in + let gv = genvar(type_of svp) in + let n = int_of_string(implode(tl(explode(fst(dest_var svp))))) + 1 in + let svn = mk_var("s"^string_of_int n,`:armstate`) in + let pc' = pc + 4 * codelen in + let svs = svp::(mk_pc pc)::(mk_pc pc'):: + end_itlist (@) (map (C assoc localvars) ilist) in + let rawsg = simprule(SPECL svs (ASSUME template)) in + let insig = PURE_REWRITE_RULE + (filter (is_eq o concl) (map snd asl)) rawsg in + let subg = mk_forall(gv,vsubst[gv,svp] (concl(simprule insig))) in + let avoids = itlist (union o thm_frees o snd) asl (frees w) in + let abv = mk_primed_var avoids (mk_var(hd ilist,`:num`)) in + (SUBGOAL_THEN subg MP_TAC THENL + [X_GEN_TAC gv THEN POP_ASSUM_LIST(K ALL_TAC) THEN + REPEAT(GEN_TAC THEN DISCH_THEN(K ALL_TAC o SYM)) THEN + core_tac THEN NO_TAC; + ALL_TAC] THEN + DISCH_THEN(MP_TAC o SPEC svp) THEN + GEN_REWRITE_TAC (REPEATC o LAND_CONV) [FORALL_UNWIND_THM1] THEN + DISCH_THEN(fun subth -> + let dest = grab_dest subth in + ARM_SUBROUTINE_SIM_TAC(mc,execth,0,mc,subth) [] n THEN + ABBREV_TAC (mk_eq(abv,mk_comb(dest,svn))))) + (asl,w) in + fun (asl,w) -> + let sv,_ = get_statenpc asl in + let n = int_of_string(implode(tl(explode(fst(dest_var sv))))) in + (ARM_STEPS_TAC execth ((n+1)--(n+prep)) THEN main_tac) (asl,w);; + (* ------------------------------------------------------------------------- *) (* Fix up call/return boilerplate given core correctness. *) (* ------------------------------------------------------------------------- *) diff --git a/arm/proofs/bignum_add_p25519.ml b/arm/proofs/bignum_add_p25519.ml index 9faa731a..862b91a0 100644 --- a/arm/proofs/bignum_add_p25519.ml +++ b/arm/proofs/bignum_add_p25519.ml @@ -50,7 +50,7 @@ let BIGNUM_ADD_P25519_EXEC = ARM_MK_EXEC_RULE bignum_add_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let BIGNUM_ADD_P25519_CORRECT = time prove (`!z x y m n pc. diff --git a/arm/proofs/bignum_cmul_p25519.ml b/arm/proofs/bignum_cmul_p25519.ml index bb26ae63..f8845e02 100644 --- a/arm/proofs/bignum_cmul_p25519.ml +++ b/arm/proofs/bignum_cmul_p25519.ml @@ -64,7 +64,7 @@ let BIGNUM_CMUL_P25519_EXEC = ARM_MK_EXEC_RULE bignum_cmul_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/arm/proofs/bignum_mul_4_8.ml b/arm/proofs/bignum_mul_4_8.ml index 57649bc7..e57016ac 100644 --- a/arm/proofs/bignum_mul_4_8.ml +++ b/arm/proofs/bignum_mul_4_8.ml @@ -14,153 +14,151 @@ *) (* ========================================================================= *) -(* 4x4 -> 8 multiply (arbitrary degree Karatsuba even at this small size). *) +(* 4x4 -> 8 multiply (2-level Karatsuba even at this small size). *) (* ========================================================================= *) (**** print_literal_from_elf "arm/fastmul/bignum_mul_4_8.o";; ****) -let bignum_mul_4_8_mc = define_assert_from_elf "bignum_mul_4_8_mc" "arm/fastmul/bignum_mul_4_8.o" +let bignum_mul_4_8_mc = + define_assert_from_elf "bignum_mul_4_8_mc" "arm/fastmul/bignum_mul_4_8.o" [ - 0xa9bf53f3; (* arm_STP X19 X20 SP (Preimmediate_Offset (iword (-- &16))) *) 0xa9401023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&0))) *) - 0xa9402047; (* arm_LDP X7 X8 X2 (Immediate_Offset (iword (&0))) *) - 0xa9411825; (* arm_LDP X5 X6 X1 (Immediate_Offset (iword (&16))) *) - 0xa9412849; (* arm_LDP X9 X10 X2 (Immediate_Offset (iword (&16))) *) - 0x9b077c6b; (* arm_MUL X11 X3 X7 *) - 0x9b087c8c; (* arm_MUL X12 X4 X8 *) - 0x9b097cad; (* arm_MUL X13 X5 X9 *) - 0x9b0a7cce; (* arm_MUL X14 X6 X10 *) - 0x9bc77c6f; (* arm_UMULH X15 X3 X7 *) - 0xab0f018c; (* arm_ADDS X12 X12 X15 *) - 0x9bc87c8f; (* arm_UMULH X15 X4 X8 *) - 0xba0f01ad; (* arm_ADCS X13 X13 X15 *) - 0x9bc97caf; (* arm_UMULH X15 X5 X9 *) - 0xba0f01ce; (* arm_ADCS X14 X14 X15 *) - 0x9bca7ccf; (* arm_UMULH X15 X6 X10 *) - 0x9a1f01ef; (* arm_ADC X15 X15 XZR *) - 0xab0b0190; (* arm_ADDS X16 X12 X11 *) - 0xba0c01ac; (* arm_ADCS X12 X13 X12 *) - 0xba0d01cd; (* arm_ADCS X13 X14 X13 *) - 0xba0e01ee; (* arm_ADCS X14 X15 X14 *) - 0x9a0f03ef; (* arm_ADC X15 XZR X15 *) - 0xf900000b; (* arm_STR X11 X0 (Immediate_Offset (word 0)) *) - 0xab0b0181; (* arm_ADDS X1 X12 X11 *) - 0xba1001a2; (* arm_ADCS X2 X13 X16 *) + 0xa9401845; (* arm_LDP X5 X6 X2 (Immediate_Offset (iword (&0))) *) + 0x9b057c67; (* arm_MUL X7 X3 X5 *) + 0x9bc57c68; (* arm_UMULH X8 X3 X5 *) + 0x9b067c89; (* arm_MUL X9 X4 X6 *) + 0x9bc67c8a; (* arm_UMULH X10 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xab080129; (* arm_ADDS X9 X9 X8 *) + 0x9a1f014a; (* arm_ADC X10 X10 XZR *) + 0xeb0600a3; (* arm_SUBS X3 X5 X6 *) + 0xda832463; (* arm_CNEG X3 X3 Condition_CC *) + 0xda902210; (* arm_CINV X16 X16 Condition_CC *) + 0x9b037c8f; (* arm_MUL X15 X4 X3 *) + 0x9bc37c83; (* arm_UMULH X3 X4 X3 *) + 0xab0900e8; (* arm_ADDS X8 X7 X9 *) + 0xba0a0129; (* arm_ADCS X9 X9 X10 *) + 0x9a1f014a; (* arm_ADC X10 X10 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0801e8; (* arm_ADCS X8 X15 X8 *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xba090069; (* arm_ADCS X9 X3 X9 *) + 0x9a10014a; (* arm_ADC X10 X10 X16 *) + 0xa9411023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&16))) *) + 0xa9411845; (* arm_LDP X5 X6 X2 (Immediate_Offset (iword (&16))) *) + 0x9b057c6b; (* arm_MUL X11 X3 X5 *) + 0x9bc57c6c; (* arm_UMULH X12 X3 X5 *) + 0x9b067c8d; (* arm_MUL X13 X4 X6 *) + 0x9bc67c8e; (* arm_UMULH X14 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xab0c01ad; (* arm_ADDS X13 X13 X12 *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xeb0600a3; (* arm_SUBS X3 X5 X6 *) + 0xda832463; (* arm_CNEG X3 X3 Condition_CC *) + 0xda902210; (* arm_CINV X16 X16 Condition_CC *) + 0x9b037c8f; (* arm_MUL X15 X4 X3 *) + 0x9bc37c83; (* arm_UMULH X3 X4 X3 *) + 0xab0d016c; (* arm_ADDS X12 X11 X13 *) + 0xba0e01ad; (* arm_ADCS X13 X13 X14 *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0c01ec; (* arm_ADCS X12 X15 X12 *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xba0d006d; (* arm_ADCS X13 X3 X13 *) + 0x9a1001ce; (* arm_ADC X14 X14 X16 *) + 0xa9411023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&16))) *) + 0xa940402f; (* arm_LDP X15 X16 X1 (Immediate_Offset (iword (&0))) *) + 0xeb0f0063; (* arm_SUBS X3 X3 X15 *) + 0xfa100084; (* arm_SBCS X4 X4 X16 *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xa940444f; (* arm_LDP X15 X17 X2 (Immediate_Offset (iword (&0))) *) + 0xeb0501e5; (* arm_SUBS X5 X15 X5 *) + 0xfa060226; (* arm_SBCS X6 X17 X6 *) + 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xeb100063; (* arm_SUBS X3 X3 X16 *) + 0xca100084; (* arm_EOR X4 X4 X16 *) + 0xda100084; (* arm_SBC X4 X4 X16 *) + 0xca1100a5; (* arm_EOR X5 X5 X17 *) + 0xeb1100a5; (* arm_SUBS X5 X5 X17 *) + 0xca1100c6; (* arm_EOR X6 X6 X17 *) + 0xda1100c6; (* arm_SBC X6 X6 X17 *) + 0xca100230; (* arm_EOR X16 X17 X16 *) + 0xab09016b; (* arm_ADDS X11 X11 X9 *) + 0xba0a018c; (* arm_ADCS X12 X12 X10 *) + 0xba1f01ad; (* arm_ADCS X13 X13 XZR *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0x9b057c62; (* arm_MUL X2 X3 X5 *) + 0x9bc57c71; (* arm_UMULH X17 X3 X5 *) + 0x9b067c8f; (* arm_MUL X15 X4 X6 *) + 0x9bc67c81; (* arm_UMULH X1 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23e9; (* arm_CSETM X9 Condition_CC *) + 0xab1101ef; (* arm_ADDS X15 X15 X17 *) + 0x9a1f0021; (* arm_ADC X1 X1 XZR *) + 0xeb0600a6; (* arm_SUBS X6 X5 X6 *) + 0xda8624c6; (* arm_CNEG X6 X6 Condition_CC *) + 0xda892129; (* arm_CINV X9 X9 Condition_CC *) + 0x9b067c85; (* arm_MUL X5 X4 X6 *) + 0x9bc67c86; (* arm_UMULH X6 X4 X6 *) + 0xab0f0051; (* arm_ADDS X17 X2 X15 *) + 0xba0101ef; (* arm_ADCS X15 X15 X1 *) + 0x9a1f0021; (* arm_ADC X1 X1 XZR *) + 0xb100053f; (* arm_CMN X9 (rvalue (word 1)) *) + 0xca0900a5; (* arm_EOR X5 X5 X9 *) + 0xba1100b1; (* arm_ADCS X17 X5 X17 *) + 0xca0900c6; (* arm_EOR X6 X6 X9 *) + 0xba0f00cf; (* arm_ADCS X15 X6 X15 *) + 0x9a090021; (* arm_ADC X1 X1 X9 *) + 0xab070169; (* arm_ADDS X9 X11 X7 *) + 0xba08018a; (* arm_ADCS X10 X12 X8 *) + 0xba0b01ab; (* arm_ADCS X11 X13 X11 *) 0xba0c01cc; (* arm_ADCS X12 X14 X12 *) - 0xba0d01ed; (* arm_ADCS X13 X15 X13 *) - 0xba0e03ee; (* arm_ADCS X14 XZR X14 *) - 0x9a0f03ef; (* arm_ADC X15 XZR X15 *) - 0xeb0600b4; (* arm_SUBS X20 X5 X6 *) - 0xda942694; (* arm_CNEG X20 X20 Condition_CC *) - 0xda9f23eb; (* arm_CSETM X11 Condition_CC *) - 0xeb090151; (* arm_SUBS X17 X10 X9 *) - 0xda912631; (* arm_CNEG X17 X17 Condition_CC *) - 0x9b117e93; (* arm_MUL X19 X20 X17 *) - 0x9bd17e91; (* arm_UMULH X17 X20 X17 *) - 0xda8b216b; (* arm_CINV X11 X11 Condition_CC *) - 0xb100057f; (* arm_CMN X11 (rvalue (word 1)) *) - 0xca0b0273; (* arm_EOR X19 X19 X11 *) - 0xba1301ad; (* arm_ADCS X13 X13 X19 *) - 0xca0b0231; (* arm_EOR X17 X17 X11 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a0b01ef; (* arm_ADC X15 X15 X11 *) - 0xeb040074; (* arm_SUBS X20 X3 X4 *) - 0xda942694; (* arm_CNEG X20 X20 Condition_CC *) - 0xda9f23eb; (* arm_CSETM X11 Condition_CC *) - 0xeb070111; (* arm_SUBS X17 X8 X7 *) - 0xda912631; (* arm_CNEG X17 X17 Condition_CC *) - 0x9b117e93; (* arm_MUL X19 X20 X17 *) - 0x9bd17e91; (* arm_UMULH X17 X20 X17 *) - 0xda8b216b; (* arm_CINV X11 X11 Condition_CC *) - 0xb100057f; (* arm_CMN X11 (rvalue (word 1)) *) - 0xca0b0273; (* arm_EOR X19 X19 X11 *) - 0xba130210; (* arm_ADCS X16 X16 X19 *) - 0xca0b0231; (* arm_EOR X17 X17 X11 *) - 0xba110021; (* arm_ADCS X1 X1 X17 *) - 0xf9000410; (* arm_STR X16 X0 (Immediate_Offset (word 8)) *) - 0xba0b0042; (* arm_ADCS X2 X2 X11 *) - 0xba0b018c; (* arm_ADCS X12 X12 X11 *) - 0xba0b01ad; (* arm_ADCS X13 X13 X11 *) - 0xba0b01ce; (* arm_ADCS X14 X14 X11 *) - 0x9a0b01ef; (* arm_ADC X15 X15 X11 *) - 0xeb060094; (* arm_SUBS X20 X4 X6 *) - 0xda942694; (* arm_CNEG X20 X20 Condition_CC *) - 0xda9f23eb; (* arm_CSETM X11 Condition_CC *) - 0xeb080151; (* arm_SUBS X17 X10 X8 *) - 0xda912631; (* arm_CNEG X17 X17 Condition_CC *) - 0x9b117e93; (* arm_MUL X19 X20 X17 *) - 0x9bd17e91; (* arm_UMULH X17 X20 X17 *) - 0xda8b216b; (* arm_CINV X11 X11 Condition_CC *) - 0xb100057f; (* arm_CMN X11 (rvalue (word 1)) *) - 0xca0b0273; (* arm_EOR X19 X19 X11 *) - 0xba13018c; (* arm_ADCS X12 X12 X19 *) - 0xca0b0231; (* arm_EOR X17 X17 X11 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba0b01ce; (* arm_ADCS X14 X14 X11 *) - 0x9a0b01ef; (* arm_ADC X15 X15 X11 *) - 0xeb050074; (* arm_SUBS X20 X3 X5 *) - 0xda942694; (* arm_CNEG X20 X20 Condition_CC *) - 0xda9f23eb; (* arm_CSETM X11 Condition_CC *) - 0xeb070131; (* arm_SUBS X17 X9 X7 *) - 0xda912631; (* arm_CNEG X17 X17 Condition_CC *) - 0x9b117e93; (* arm_MUL X19 X20 X17 *) - 0x9bd17e91; (* arm_UMULH X17 X20 X17 *) - 0xda8b216b; (* arm_CINV X11 X11 Condition_CC *) - 0xb100057f; (* arm_CMN X11 (rvalue (word 1)) *) - 0xca0b0273; (* arm_EOR X19 X19 X11 *) - 0xba130021; (* arm_ADCS X1 X1 X19 *) - 0xca0b0231; (* arm_EOR X17 X17 X11 *) - 0xba110042; (* arm_ADCS X2 X2 X17 *) - 0xba0b018c; (* arm_ADCS X12 X12 X11 *) - 0xba0b01ad; (* arm_ADCS X13 X13 X11 *) - 0xba0b01ce; (* arm_ADCS X14 X14 X11 *) - 0x9a0b01ef; (* arm_ADC X15 X15 X11 *) - 0xeb060074; (* arm_SUBS X20 X3 X6 *) - 0xda942694; (* arm_CNEG X20 X20 Condition_CC *) - 0xda9f23eb; (* arm_CSETM X11 Condition_CC *) - 0xeb070151; (* arm_SUBS X17 X10 X7 *) - 0xda912631; (* arm_CNEG X17 X17 Condition_CC *) - 0x9b117e93; (* arm_MUL X19 X20 X17 *) - 0x9bd17e91; (* arm_UMULH X17 X20 X17 *) - 0xda8b216b; (* arm_CINV X11 X11 Condition_CC *) - 0xb100057f; (* arm_CMN X11 (rvalue (word 1)) *) - 0xca0b0273; (* arm_EOR X19 X19 X11 *) - 0xba130042; (* arm_ADCS X2 X2 X19 *) - 0xca0b0231; (* arm_EOR X17 X17 X11 *) - 0xba11018c; (* arm_ADCS X12 X12 X17 *) - 0xba0b01ad; (* arm_ADCS X13 X13 X11 *) - 0xba0b01ce; (* arm_ADCS X14 X14 X11 *) - 0x9a0b01ef; (* arm_ADC X15 X15 X11 *) - 0xeb050094; (* arm_SUBS X20 X4 X5 *) - 0xda942694; (* arm_CNEG X20 X20 Condition_CC *) - 0xda9f23eb; (* arm_CSETM X11 Condition_CC *) - 0xeb080131; (* arm_SUBS X17 X9 X8 *) - 0xda912631; (* arm_CNEG X17 X17 Condition_CC *) - 0x9b117e93; (* arm_MUL X19 X20 X17 *) - 0x9bd17e91; (* arm_UMULH X17 X20 X17 *) - 0xda8b216b; (* arm_CINV X11 X11 Condition_CC *) - 0xb100057f; (* arm_CMN X11 (rvalue (word 1)) *) - 0xca0b0273; (* arm_EOR X19 X19 X11 *) - 0xba130042; (* arm_ADCS X2 X2 X19 *) - 0xca0b0231; (* arm_EOR X17 X17 X11 *) - 0xba11018c; (* arm_ADCS X12 X12 X17 *) - 0xba0b01ad; (* arm_ADCS X13 X13 X11 *) - 0xba0b01ce; (* arm_ADCS X14 X14 X11 *) - 0x9a0b01ef; (* arm_ADC X15 X15 X11 *) - 0xa9010801; (* arm_STP X1 X2 X0 (Immediate_Offset (iword (&16))) *) - 0xa902340c; (* arm_STP X12 X13 X0 (Immediate_Offset (iword (&32))) *) - 0xa9033c0e; (* arm_STP X14 X15 X0 (Immediate_Offset (iword (&48))) *) - 0xa8c153f3; (* arm_LDP X19 X20 SP (Postimmediate_Offset (iword (&16))) *) + 0xba1f01ad; (* arm_ADCS X13 X13 XZR *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca100042; (* arm_EOR X2 X2 X16 *) + 0xba090049; (* arm_ADCS X9 X2 X9 *) + 0xca100231; (* arm_EOR X17 X17 X16 *) + 0xba0a022a; (* arm_ADCS X10 X17 X10 *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0b01eb; (* arm_ADCS X11 X15 X11 *) + 0xca100021; (* arm_EOR X1 X1 X16 *) + 0xba0c002c; (* arm_ADCS X12 X1 X12 *) + 0xba1001ad; (* arm_ADCS X13 X13 X16 *) + 0x9a1001ce; (* arm_ADC X14 X14 X16 *) + 0xa9002007; (* arm_STP X7 X8 X0 (Immediate_Offset (iword (&0))) *) + 0xa9012809; (* arm_STP X9 X10 X0 (Immediate_Offset (iword (&16))) *) + 0xa902300b; (* arm_STP X11 X12 X0 (Immediate_Offset (iword (&32))) *) + 0xa903380d; (* arm_STP X13 X14 X0 (Immediate_Offset (iword (&48))) *) 0xd65f03c0 (* arm_RET X30 *) ];; let BIGNUM_MUL_4_8_EXEC = ARM_MK_EXEC_RULE bignum_mul_4_8_mc;; (* ------------------------------------------------------------------------- *) -(* Lemmas to halve the number of case splits, useful for efficiency. *) +(* Simplifying lemmas. *) (* ------------------------------------------------------------------------- *) +let lemma0 = prove + (`!x0 x1:int64. + &(val(if val x0 <= val x1 then word_sub x1 x0 + else word_neg(word_sub x1 x0))):real = abs(&(val x1) - &(val x0))`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN + REWRITE_TAC[WORD_NEG_SUB; REAL_ARITH + `abs(x - y):real = if y <= x then x - y else y - x`] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN + RULE_ASSUM_TAC(REWRITE_RULE[REAL_OF_NUM_CLAUSES; NOT_LE]) THEN + ASM_SIMP_TAC[VAL_WORD_SUB_CASES; LT_IMP_LE; REAL_OF_NUM_SUB]);; + let lemma1 = prove (`!(x0:num) x1 (y0:num) y1. (if y0 <= y1 @@ -173,84 +171,259 @@ let lemma1 = prove CONV_TAC WORD_REDUCE_CONV);; let lemma2 = prove - (`!(x0:int64) (x1:int64) (y0:int64) (y1:int64). - &(val(if val x1 <= val x0 then word_sub x0 x1 - else word_neg (word_sub x0 x1))) * - &(val(if val y0 <= val y1 then word_sub y1 y0 - else word_neg (word_sub y1 y0))):real = - --(&1) pow bitval(val y0 <= val y1 <=> val x0 < val x1) * - (&(val x0) - &(val x1)) * (&(val y1) - &(val y0))`, - REPEAT GEN_TAC THEN REWRITE_TAC[GSYM NOT_LE; WORD_NEG_SUB] THEN - REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES]) THEN - REPEAT(FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE - `~(m:num <= n) ==> n <= m /\ ~(m <= n)`))) THEN - ASM_SIMP_TAC[VAL_WORD_SUB_CASES; GSYM REAL_OF_NUM_SUB] THEN - REAL_ARITH_TAC);; + (`!p x0 x1 y0 y1:real. + (x0 + p * x1) * (y0 + p * y1) = + x0 * y0 + p pow 2 * x1 * y1 + + p * (x0 * y0 + x1 * y1 + + --(&1) pow bitval(y1 <= y0 <=> x1 < x0) * + abs(x1 - x0) * abs(y0 - y1))`, + REPEAT GEN_TAC THEN + MAP_EVERY ASM_CASES_TAC [`y1:real <= y0`; `x1:real < x0`] THEN + ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN ASM_REAL_ARITH_TAC);; (* ------------------------------------------------------------------------- *) (* Proof. *) (* ------------------------------------------------------------------------- *) +let KARATSUBA12_TAC = + REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID] THEN + MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN + MAP_EVERY EXISTS_TAC [`256`; `&0:real`] THEN + ASM_REWRITE_TAC[INTEGER_CLOSED] THEN + REPLICATE_TAC 2 (CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC]) THEN + REWRITE_TAC[lemma2; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN + ACCUMULATOR_POP_ASSUM_LIST(fun thl -> + MP_TAC(end_itlist CONJ(rev thl)) THEN + REWRITE_TAC[WORD_XOR_MASK] THEN + REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE; GSYM NOT_LE] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN + CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV) THEN + REWRITE_TAC[REAL_VAL_WORD_NOT; DIMINDEX_64] THEN + DISCH_THEN(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN + CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN + REWRITE_TAC(filter(is_ratconst o rand o concl) (DECARRY_RULE thl)) THEN + REAL_INTEGER_TAC);; + let BIGNUM_MUL_4_8_CORRECT = prove (`!z x y a b pc. - nonoverlapping (word pc,0x20c) (z,8 * 8) + nonoverlapping (word pc,0x1d4) (z,8 * 8) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) bignum_mul_4_8_mc /\ - read PC s = word(pc + 0x04) /\ + read PC s = word pc /\ C_ARGUMENTS [z; x; y] s /\ bignum_from_memory (x,4) s = a /\ bignum_from_memory (y,4) s = b) - (\s. read PC s = word (pc + 0x204) /\ + (\s. read PC s = word (pc + 0x1d0) /\ bignum_from_memory (z,8) s = a * b) (MAYCHANGE [PC; X1; X2; X3; X4; X5; X6; X7; X8; X9; X10; X11; - X12; X13; X14; X15; X16; X17; X19; X20] ,, + X12; X13; X14; X15; X16; X17] ,, MAYCHANGE [memory :> bytes(z,8 * 8)] ,, MAYCHANGE SOME_FLAGS)`, MAP_EVERY X_GEN_TAC [`z:int64`; `x:int64`; `y:int64`; `a:num`; `b:num`; `pc:num`] THEN - REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN + REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN + REWRITE_TAC[ALL; NONOVERLAPPING_CLAUSES] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN ENSURES_INIT_TAC "s0" THEN - BIGNUM_DIGITIZE_TAC "x_" `bignum_from_memory (x,4) s0` THEN - BIGNUM_DIGITIZE_TAC "y_" `bignum_from_memory (y,4) s0` THEN + BIGNUM_LDIGITIZE_TAC "x_" `bignum_from_memory (x,4) s0` THEN + BIGNUM_LDIGITIZE_TAC "y_" `bignum_from_memory (y,4) s0` THEN + + (*** First nested block multiplying the lower halves ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_4_8_EXEC + [3;5;10;11;15;17;18;19;22;24;25] (1--25) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN + + MAP_EVERY ABBREV_TAC + [`q0 = bignum_of_wordlist[mullo_s3;sum_s22]`; + `q1 = bignum_of_wordlist[sum_s24;sum_s25]`] THEN + SUBGOAL_THEN + `2 EXP 128 * q1 + q0 = + bignum_of_wordlist [x_0;x_1] * bignum_of_wordlist[y_0;y_1]` + ASSUME_TAC THENL + [MAP_EVERY EXPAND_TAC ["q0"; "q1"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** Second nested block multiplying the upper halves ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_4_8_EXEC + [28;30;35;36;40;42;43;44;47;49;50] (26--50) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN + + ABBREV_TAC + `q23 = bignum_of_wordlist[mullo_s28;sum_s47; sum_s49;sum_s50]` THEN + SUBGOAL_THEN + `q23 = bignum_of_wordlist [x_2;x_3] * bignum_of_wordlist[y_2;y_3]` + ASSUME_TAC THENL + [EXPAND_TAC "q23" THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** The sign-magnitude difference computation ***) + ARM_ACCSTEPS_TAC BIGNUM_MUL_4_8_EXEC - [5;6;7;8;10;12;14;16;17;18;19;20;21;23;24;25;26;27;28;34;39; - 41;42;48;53;55;57;58;59;60;61;67;72;74;75;76;82;87;89;90;91; - 92;93;99;104;106;107;108;109;115;120;122;123;124;125] - (1--128) THEN + [53;54; 57;58; 61;63; 65;67] (51--68) THEN + RULE_ASSUM_TAC(REWRITE_RULE[WORD_UNMASK_64]) THEN + + MAP_EVERY ABBREV_TAC + [`sgn <=> ~(carry_s58 <=> carry_s54)`; + `xd = bignum_of_wordlist[sum_s61;sum_s63]`; + `yd = bignum_of_wordlist[sum_s65;sum_s67]`] THEN + SUBGOAL_THEN + `(&(bignum_of_wordlist[x_2;x_3]) - + &(bignum_of_wordlist[x_0;x_1])) * + (&(bignum_of_wordlist[y_0;y_1]) - + &(bignum_of_wordlist[y_2;y_3])):real = + --(&1) pow bitval sgn * &xd * &yd` + ASSUME_TAC THENL + [TRANS_TAC EQ_TRANS + `(--(&1) pow bitval carry_s54 * &xd) * + (--(&1) pow bitval carry_s58 * &yd):real` THEN + CONJ_TAC THENL + [ALL_TAC; + EXPAND_TAC "sgn" THEN REWRITE_TAC[BITVAL_NOT; BITVAL_IFF] THEN + POP_ASSUM_LIST(K ALL_TAC) THEN REWRITE_TAC[bitval] THEN + REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + CONV_TAC NUM_REDUCE_CONV THEN REAL_ARITH_TAC] THEN + SUBGOAL_THEN + `(carry_s54 <=> + bignum_of_wordlist[x_2;x_3] < bignum_of_wordlist[x_0;x_1]) /\ + (carry_s58 <=> + bignum_of_wordlist[y_0;y_1] < bignum_of_wordlist[y_2;y_3])` + (CONJUNCTS_THEN SUBST_ALL_TAC) + THENL + [CONJ_TAC THEN MATCH_MP_TAC FLAG_FROM_CARRY_LT THEN EXISTS_TAC `128` THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN + REWRITE_TAC[REAL_BITVAL_NOT; REAL_VAL_WORD_MASK; DIMINDEX_64] THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN BOUNDER_TAC[]; + ALL_TAC] THEN + BINOP_TAC THEN REWRITE_TAC[bitval] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_LID] THEN + REWRITE_TAC[REAL_ARITH `x - y:real = --(&1) pow 1 * z <=> y - x = z`] THEN + MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN + MAP_EVERY EXISTS_TAC [`128`; `&0:real`] THEN + (CONJ_TAC THENL + [MATCH_MP_TAC(REAL_ARITH + `y:real <= x /\ (&0 <= x /\ x < e) /\ (&0 <= y /\ y < e) + ==> &0 <= x - y /\ x - y < e`) THEN + ASM_SIMP_TAC[REAL_OF_NUM_CLAUSES; LT_IMP_LE; + ARITH_RULE `~(a:num < b) ==> b <= a`] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + CONJ_TAC THEN BOUNDER_TAC[]; + ALL_TAC] THEN + MAP_EVERY EXPAND_TAC ["xd"; "yd"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + CONJ_TAC THENL [BOUNDER_TAC[]; REWRITE_TAC[INTEGER_CLOSED]]) THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN + ASM_REWRITE_TAC[WORD_XOR_MASK] THEN + REWRITE_TAC[REAL_VAL_WORD_NOT; BITVAL_CLAUSES; DIMINDEX_64] THEN + DISCH_THEN(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN + + (*** Clean up the overall sign ***) + + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [WORD_XOR_MASKS]) THEN + ASM_REWRITE_TAC[] THEN DISCH_TAC THEN + + (*** The augmented H' = H + L_top ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_4_8_EXEC (69--72) (69--72) THEN + MAP_EVERY ABBREV_TAC + [`q2 = bignum_of_wordlist[sum_s69;sum_s70]`; + `q3 = bignum_of_wordlist[sum_s71;sum_s72]`] THEN + SUBGOAL_THEN + `2 EXP 128 * q3 + q2 = + bignum_of_wordlist [x_2;x_3] * bignum_of_wordlist[y_2;y_3] + q1` + ASSUME_TAC THENL + [MAP_EVERY EXPAND_TAC ["q1"; "q2"; "q3"] THEN + MATCH_MP_TAC CONG_IMP_EQ THEN EXISTS_TAC `2 EXP 256` THEN + REPEAT(CONJ_TAC THENL + [CONV_TAC NUM_REDUCE_CONV THEN BOUNDER_TAC[]; ALL_TAC]) THEN + FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC + (LAND_CONV o LAND_CONV) [SYM th]) THEN + MAP_EVERY EXPAND_TAC ["q23"] THEN + REWRITE_TAC[REAL_CONGRUENCE] THEN CONV_TAC NUM_REDUCE_CONV THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; + ALL_TAC] THEN + + (*** Third nested block multiplying the absolute differences ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_4_8_EXEC + [73;75;80;81;85;87;88;89;92;94;95] (73--95) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN + SUBGOAL_THEN + `&xd * &yd:real = + &(bignum_of_wordlist[mullo_s73; sum_s92; sum_s94; sum_s95])` + SUBST_ALL_TAC THENL + [MAP_EVERY EXPAND_TAC ["xd"; "yd"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** The rest of the computation ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_4_8_EXEC + [96;97;98;99;100;101;104;106;108;110;111;112] (96--116) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN - MAP_EVERY EXPAND_TAC ["a"; "b"] THEN + DISCARD_STATE_TAC "s116" THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN MAP_EVERY EXISTS_TAC [`512`; `&0:real`] THEN - REPLICATE_TAC 2 (CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC]) THEN - CONJ_TAC THENL [REAL_INTEGER_TAC; ALL_TAC] THEN + CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC] THEN CONJ_TAC THENL + [MAP_EVERY EXPAND_TAC ["a"; "b"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN BOUNDER_TAC[]; + REWRITE_TAC[INTEGER_CLOSED]] THEN + + (*** The core rearrangement we are using ***) + + SUBGOAL_THEN + `&a * &b:real = + (&1 + &2 pow 128) * (&q0 + &2 pow 128 * &q2 + &2 pow 256 * &q3) + + &2 pow 128 * + (&(bignum_of_wordlist [x_2; x_3]) - + &(bignum_of_wordlist [x_0; x_1])) * + (&(bignum_of_wordlist [y_0; y_1]) - + &(bignum_of_wordlist [y_2; y_3]))` + SUBST1_TAC THENL + [MAP_EVERY UNDISCH_TAC + [`2 EXP 128 * q1 + q0 = + bignum_of_wordlist[x_0; x_1] * bignum_of_wordlist[y_0; y_1]`; + `2 EXP 128 * q3 + q2 = + bignum_of_wordlist[x_2; x_3] * bignum_of_wordlist[y_2; y_3] + + q1`] THEN + MAP_EVERY EXPAND_TAC ["a"; "b"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN + CONV_TAC REAL_RING; + ASM_REWRITE_TAC[]] THEN + MAP_EVERY EXPAND_TAC ["q0"; "q2"; "q3"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN POP_ASSUM_LIST(K ALL_TAC) THEN - REWRITE_TAC[lemma1; lemma2] THEN REWRITE_TAC[WORD_XOR_MASK] THEN - REPEAT(COND_CASES_TAC THEN - ASM_REWRITE_TAC[BITVAL_CLAUSES; REAL_VAL_WORD_NOT]) THEN + REWRITE_TAC[WORD_XOR_MASK] THEN COND_CASES_TAC THEN + ASM_REWRITE_TAC[REAL_VAL_WORD_NOT; BITVAL_CLAUSES; DIMINDEX_64] THEN CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC NUM_REDUCE_CONV THEN - REWRITE_TAC[BITVAL_CLAUSES; DIMINDEX_64] THEN - POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC THEN + REWRITE_TAC[BITVAL_CLAUSES] THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN - DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN - CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN - FIRST_ASSUM(MP_TAC o end_itlist CONJ o filter (is_ratconst o rand o concl) o - DECARRY_RULE o CONJUNCTS) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC);; let BIGNUM_MUL_4_8_SUBROUTINE_CORRECT = prove - (`!z x y a b pc stackpointer returnaddress. - aligned 16 stackpointer /\ - nonoverlapping (word pc,0x20c) (z,8 * 8) /\ - ALL (nonoverlapping (word_sub stackpointer (word 16),16)) - [(word pc,0x20c); (x,8 * 4); (y,8 * 4); (z,8 * 8)] + (`!z x y a b pc returnaddress. + nonoverlapping (word pc,0x1d4) (z,8 * 8) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) bignum_mul_4_8_mc /\ read PC s = word pc /\ - read SP s = stackpointer /\ read X30 s = returnaddress /\ C_ARGUMENTS [z; x; y] s /\ bignum_from_memory (x,4) s = a /\ @@ -259,9 +432,7 @@ let BIGNUM_MUL_4_8_SUBROUTINE_CORRECT = prove bignum_from_memory (z,8) s = a * b) (MAYCHANGE [PC; X1; X2; X3; X4; X5; X6; X7; X8; X9; X10; X11; X12; X13; X14; X15; X16; X17] ,, - MAYCHANGE [memory :> bytes(z,8 * 8); - memory :> bytes(word_sub stackpointer (word 16),16)] ,, + MAYCHANGE [memory :> bytes(z,8 * 8)] ,, MAYCHANGE SOME_FLAGS)`, - ARM_ADD_RETURN_STACK_TAC - BIGNUM_MUL_4_8_EXEC BIGNUM_MUL_4_8_CORRECT - `[X19;X20]` 16);; + ARM_ADD_RETURN_NOSTACK_TAC + BIGNUM_MUL_4_8_EXEC BIGNUM_MUL_4_8_CORRECT);; diff --git a/arm/proofs/bignum_mul_p25519.ml b/arm/proofs/bignum_mul_p25519.ml index fd4edba9..79d8f5cd 100644 --- a/arm/proofs/bignum_mul_p25519.ml +++ b/arm/proofs/bignum_mul_p25519.ml @@ -22,182 +22,167 @@ let bignum_mul_p25519_mc = define_assert_from_elf "bignum_mul_p25519_mc" "arm/curve25519/bignum_mul_p25519.o" [ - 0xa9bf53f3; (* arm_STP X19 X20 SP (Preimmediate_Offset (iword (-- &16))) *) - 0xa9bf5bf5; (* arm_STP X21 X22 SP (Preimmediate_Offset (iword (-- &16))) *) 0xa9401023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&0))) *) - 0xa9402047; (* arm_LDP X7 X8 X2 (Immediate_Offset (iword (&0))) *) - 0xa9411825; (* arm_LDP X5 X6 X1 (Immediate_Offset (iword (&16))) *) - 0xa9412849; (* arm_LDP X9 X10 X2 (Immediate_Offset (iword (&16))) *) - 0x9b077c6b; (* arm_MUL X11 X3 X7 *) - 0x9b087c8c; (* arm_MUL X12 X4 X8 *) - 0x9b097cad; (* arm_MUL X13 X5 X9 *) - 0x9b0a7cce; (* arm_MUL X14 X6 X10 *) - 0x9bc77c6f; (* arm_UMULH X15 X3 X7 *) - 0xab0f018c; (* arm_ADDS X12 X12 X15 *) - 0x9bc87c8f; (* arm_UMULH X15 X4 X8 *) - 0xba0f01ad; (* arm_ADCS X13 X13 X15 *) - 0x9bc97caf; (* arm_UMULH X15 X5 X9 *) - 0xba0f01ce; (* arm_ADCS X14 X14 X15 *) - 0x9bca7ccf; (* arm_UMULH X15 X6 X10 *) - 0x9a1f01ef; (* arm_ADC X15 X15 XZR *) - 0xab0b0190; (* arm_ADDS X16 X12 X11 *) - 0xba0c01ac; (* arm_ADCS X12 X13 X12 *) - 0xba0d01cd; (* arm_ADCS X13 X14 X13 *) - 0xba0e01ee; (* arm_ADCS X14 X15 X14 *) - 0x9a0f03ef; (* arm_ADC X15 XZR X15 *) - 0xab0b0181; (* arm_ADDS X1 X12 X11 *) - 0xba1001a2; (* arm_ADCS X2 X13 X16 *) - 0xba0c01cc; (* arm_ADCS X12 X14 X12 *) - 0xba0d01ed; (* arm_ADCS X13 X15 X13 *) - 0xba0e03ee; (* arm_ADCS X14 XZR X14 *) - 0x9a0f03ef; (* arm_ADC X15 XZR X15 *) - 0xeb0600b5; (* arm_SUBS X21 X5 X6 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb090153; (* arm_SUBS X19 X10 X9 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba1401ad; (* arm_ADCS X13 X13 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba1301ce; (* arm_ADCS X14 X14 X19 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb040075; (* arm_SUBS X21 X3 X4 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb070113; (* arm_SUBS X19 X8 X7 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba140210; (* arm_ADCS X16 X16 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba130021; (* arm_ADCS X1 X1 X19 *) - 0xba110042; (* arm_ADCS X2 X2 X17 *) - 0xba11018c; (* arm_ADCS X12 X12 X17 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb060095; (* arm_SUBS X21 X4 X6 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb080153; (* arm_SUBS X19 X10 X8 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba14018c; (* arm_ADCS X12 X12 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba1301ad; (* arm_ADCS X13 X13 X19 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb050075; (* arm_SUBS X21 X3 X5 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) + 0xa9401845; (* arm_LDP X5 X6 X2 (Immediate_Offset (iword (&0))) *) + 0x9b057c67; (* arm_MUL X7 X3 X5 *) + 0x9bc57c68; (* arm_UMULH X8 X3 X5 *) + 0x9b067c89; (* arm_MUL X9 X4 X6 *) + 0x9bc67c8a; (* arm_UMULH X10 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xab080129; (* arm_ADDS X9 X9 X8 *) + 0x9a1f014a; (* arm_ADC X10 X10 XZR *) + 0xeb0600a3; (* arm_SUBS X3 X5 X6 *) + 0xda832463; (* arm_CNEG X3 X3 Condition_CC *) + 0xda902210; (* arm_CINV X16 X16 Condition_CC *) + 0x9b037c8f; (* arm_MUL X15 X4 X3 *) + 0x9bc37c83; (* arm_UMULH X3 X4 X3 *) + 0xab0900e8; (* arm_ADDS X8 X7 X9 *) + 0xba0a0129; (* arm_ADCS X9 X9 X10 *) + 0x9a1f014a; (* arm_ADC X10 X10 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0801e8; (* arm_ADCS X8 X15 X8 *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xba090069; (* arm_ADCS X9 X3 X9 *) + 0x9a10014a; (* arm_ADC X10 X10 X16 *) + 0xa9411023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&16))) *) + 0xa9411845; (* arm_LDP X5 X6 X2 (Immediate_Offset (iword (&16))) *) + 0x9b057c6b; (* arm_MUL X11 X3 X5 *) + 0x9bc57c6c; (* arm_UMULH X12 X3 X5 *) + 0x9b067c8d; (* arm_MUL X13 X4 X6 *) + 0x9bc67c8e; (* arm_UMULH X14 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xab0c01ad; (* arm_ADDS X13 X13 X12 *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xeb0600a3; (* arm_SUBS X3 X5 X6 *) + 0xda832463; (* arm_CNEG X3 X3 Condition_CC *) + 0xda902210; (* arm_CINV X16 X16 Condition_CC *) + 0x9b037c8f; (* arm_MUL X15 X4 X3 *) + 0x9bc37c83; (* arm_UMULH X3 X4 X3 *) + 0xab0d016c; (* arm_ADDS X12 X11 X13 *) + 0xba0e01ad; (* arm_ADCS X13 X13 X14 *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0c01ec; (* arm_ADCS X12 X15 X12 *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xba0d006d; (* arm_ADCS X13 X3 X13 *) + 0x9a1001ce; (* arm_ADC X14 X14 X16 *) + 0xa9411023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&16))) *) + 0xa940402f; (* arm_LDP X15 X16 X1 (Immediate_Offset (iword (&0))) *) + 0xeb0f0063; (* arm_SUBS X3 X3 X15 *) + 0xfa100084; (* arm_SBCS X4 X4 X16 *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xa940444f; (* arm_LDP X15 X17 X2 (Immediate_Offset (iword (&0))) *) + 0xeb0501e5; (* arm_SUBS X5 X15 X5 *) + 0xfa060226; (* arm_SBCS X6 X17 X6 *) 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb070133; (* arm_SUBS X19 X9 X7 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba140021; (* arm_ADCS X1 X1 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba130042; (* arm_ADCS X2 X2 X19 *) - 0xba11018c; (* arm_ADCS X12 X12 X17 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb060075; (* arm_SUBS X21 X3 X6 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb070153; (* arm_SUBS X19 X10 X7 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba140042; (* arm_ADCS X2 X2 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba13018c; (* arm_ADCS X12 X12 X19 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb050095; (* arm_SUBS X21 X4 X5 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb080133; (* arm_SUBS X19 X9 X8 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba140042; (* arm_ADCS X2 X2 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba13018c; (* arm_ADCS X12 X12 X19 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xd28004d1; (* arm_MOV X17 (rvalue (word 38)) *) - 0x92407d94; (* arm_AND X20 X12 (rvalue (word 4294967295)) *) - 0xd360fd93; (* arm_LSR X19 X12 32 *) - 0x9b147e34; (* arm_MUL X20 X17 X20 *) - 0x9b137e33; (* arm_MUL X19 X17 X19 *) - 0xab14016b; (* arm_ADDS X11 X11 X20 *) - 0x92407db4; (* arm_AND X20 X13 (rvalue (word 4294967295)) *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xeb100063; (* arm_SUBS X3 X3 X16 *) + 0xca100084; (* arm_EOR X4 X4 X16 *) + 0xda100084; (* arm_SBC X4 X4 X16 *) + 0xca1100a5; (* arm_EOR X5 X5 X17 *) + 0xeb1100a5; (* arm_SUBS X5 X5 X17 *) + 0xca1100c6; (* arm_EOR X6 X6 X17 *) + 0xda1100c6; (* arm_SBC X6 X6 X17 *) + 0xca100230; (* arm_EOR X16 X17 X16 *) + 0xab09016b; (* arm_ADDS X11 X11 X9 *) + 0xba0a018c; (* arm_ADCS X12 X12 X10 *) + 0xba1f01ad; (* arm_ADCS X13 X13 XZR *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0x9b057c62; (* arm_MUL X2 X3 X5 *) + 0x9bc57c71; (* arm_UMULH X17 X3 X5 *) + 0x9b067c8f; (* arm_MUL X15 X4 X6 *) + 0x9bc67c81; (* arm_UMULH X1 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23e9; (* arm_CSETM X9 Condition_CC *) + 0xab1101ef; (* arm_ADDS X15 X15 X17 *) + 0x9a1f0021; (* arm_ADC X1 X1 XZR *) + 0xeb0600a6; (* arm_SUBS X6 X5 X6 *) + 0xda8624c6; (* arm_CNEG X6 X6 Condition_CC *) + 0xda892129; (* arm_CINV X9 X9 Condition_CC *) + 0x9b067c85; (* arm_MUL X5 X4 X6 *) + 0x9bc67c86; (* arm_UMULH X6 X4 X6 *) + 0xab0f0051; (* arm_ADDS X17 X2 X15 *) + 0xba0101ef; (* arm_ADCS X15 X15 X1 *) + 0x9a1f0021; (* arm_ADC X1 X1 XZR *) + 0xb100053f; (* arm_CMN X9 (rvalue (word 1)) *) + 0xca0900a5; (* arm_EOR X5 X5 X9 *) + 0xba1100b1; (* arm_ADCS X17 X5 X17 *) + 0xca0900c6; (* arm_EOR X6 X6 X9 *) + 0xba0f00cf; (* arm_ADCS X15 X6 X15 *) + 0x9a090021; (* arm_ADC X1 X1 X9 *) + 0xab070169; (* arm_ADDS X9 X11 X7 *) + 0xba08018a; (* arm_ADCS X10 X12 X8 *) + 0xba0b01ab; (* arm_ADCS X11 X13 X11 *) + 0xba0c01cc; (* arm_ADCS X12 X14 X12 *) + 0xba1f01ad; (* arm_ADCS X13 X13 XZR *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca100042; (* arm_EOR X2 X2 X16 *) + 0xba090049; (* arm_ADCS X9 X2 X9 *) + 0xca100231; (* arm_EOR X17 X17 X16 *) + 0xba0a022a; (* arm_ADCS X10 X17 X10 *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0b01eb; (* arm_ADCS X11 X15 X11 *) + 0xca100021; (* arm_EOR X1 X1 X16 *) + 0xba0c002c; (* arm_ADCS X12 X1 X12 *) + 0xba1001ad; (* arm_ADCS X13 X13 X16 *) + 0x9a1001ce; (* arm_ADC X14 X14 X16 *) + 0xd28004c3; (* arm_MOV X3 (rvalue (word 38)) *) + 0x92407d65; (* arm_AND X5 X11 (rvalue (word 4294967295)) *) + 0xd360fd64; (* arm_LSR X4 X11 32 *) + 0x9b057c65; (* arm_MUL X5 X3 X5 *) + 0x9b047c64; (* arm_MUL X4 X3 X4 *) + 0xab0500e7; (* arm_ADDS X7 X7 X5 *) + 0x92407d85; (* arm_AND X5 X12 (rvalue (word 4294967295)) *) + 0xd360fd8c; (* arm_LSR X12 X12 32 *) + 0x9b057c65; (* arm_MUL X5 X3 X5 *) + 0x9b0c7c6c; (* arm_MUL X12 X3 X12 *) + 0xba050108; (* arm_ADCS X8 X8 X5 *) + 0x92407da5; (* arm_AND X5 X13 (rvalue (word 4294967295)) *) 0xd360fdad; (* arm_LSR X13 X13 32 *) - 0x9b147e34; (* arm_MUL X20 X17 X20 *) - 0x9b0d7e2d; (* arm_MUL X13 X17 X13 *) - 0xba140210; (* arm_ADCS X16 X16 X20 *) - 0x92407dd4; (* arm_AND X20 X14 (rvalue (word 4294967295)) *) + 0x9b057c65; (* arm_MUL X5 X3 X5 *) + 0x9b0d7c6d; (* arm_MUL X13 X3 X13 *) + 0xba050129; (* arm_ADCS X9 X9 X5 *) + 0x92407dc5; (* arm_AND X5 X14 (rvalue (word 4294967295)) *) 0xd360fdce; (* arm_LSR X14 X14 32 *) - 0x9b147e34; (* arm_MUL X20 X17 X20 *) - 0x9b0e7e2e; (* arm_MUL X14 X17 X14 *) - 0xba140021; (* arm_ADCS X1 X1 X20 *) - 0x92407df4; (* arm_AND X20 X15 (rvalue (word 4294967295)) *) - 0xd360fdef; (* arm_LSR X15 X15 32 *) - 0x9b147e34; (* arm_MUL X20 X17 X20 *) - 0x9b0f7e2f; (* arm_MUL X15 X17 X15 *) - 0xba140042; (* arm_ADCS X2 X2 X20 *) - 0x9a9f37ec; (* arm_CSET X12 Condition_CS *) - 0xd3607e74; (* arm_LSL X20 X19 32 *) - 0xab14016b; (* arm_ADDS X11 X11 X20 *) - 0x93d381b4; (* arm_EXTR X20 X13 X19 32 *) - 0xba140210; (* arm_ADCS X16 X16 X20 *) - 0x93cd81d4; (* arm_EXTR X20 X14 X13 32 *) - 0xba140021; (* arm_ADCS X1 X1 X20 *) - 0x93ce81f4; (* arm_EXTR X20 X15 X14 32 *) - 0xba140042; (* arm_ADCS X2 X2 X20 *) - 0xd360fdf4; (* arm_LSR X20 X15 32 *) - 0x9a14018c; (* arm_ADC X12 X12 X20 *) - 0xab02005f; (* arm_CMN X2 X2 *) - 0xb2410042; (* arm_ORR X2 X2 (rvalue (word 9223372036854775808)) *) - 0x9a0c018f; (* arm_ADC X15 X12 X12 *) - 0xd2800271; (* arm_MOV X17 (rvalue (word 19)) *) - 0x9b0f4634; (* arm_MADD X20 X17 X15 X17 *) - 0xab14016b; (* arm_ADDS X11 X11 X20 *) - 0xba1f0210; (* arm_ADCS X16 X16 XZR *) - 0xba1f0021; (* arm_ADCS X1 X1 XZR *) - 0xba1f0042; (* arm_ADCS X2 X2 XZR *) - 0x9a9f3231; (* arm_CSEL X17 X17 XZR Condition_CC *) - 0xeb11016b; (* arm_SUBS X11 X11 X17 *) - 0xfa1f0210; (* arm_SBCS X16 X16 XZR *) - 0xfa1f0021; (* arm_SBCS X1 X1 XZR *) - 0xda1f0042; (* arm_SBC X2 X2 XZR *) - 0x9240f842; (* arm_AND X2 X2 (rvalue (word 9223372036854775807)) *) - 0xa900400b; (* arm_STP X11 X16 X0 (Immediate_Offset (iword (&0))) *) - 0xa9010801; (* arm_STP X1 X2 X0 (Immediate_Offset (iword (&16))) *) - 0xa8c15bf5; (* arm_LDP X21 X22 SP (Postimmediate_Offset (iword (&16))) *) - 0xa8c153f3; (* arm_LDP X19 X20 SP (Postimmediate_Offset (iword (&16))) *) + 0x9b057c65; (* arm_MUL X5 X3 X5 *) + 0x9b0e7c6e; (* arm_MUL X14 X3 X14 *) + 0xba05014a; (* arm_ADCS X10 X10 X5 *) + 0x9a9f37eb; (* arm_CSET X11 Condition_CS *) + 0xd3607c85; (* arm_LSL X5 X4 32 *) + 0xab0500e7; (* arm_ADDS X7 X7 X5 *) + 0x93c48185; (* arm_EXTR X5 X12 X4 32 *) + 0xba050108; (* arm_ADCS X8 X8 X5 *) + 0x93cc81a5; (* arm_EXTR X5 X13 X12 32 *) + 0xba050129; (* arm_ADCS X9 X9 X5 *) + 0x93cd81c5; (* arm_EXTR X5 X14 X13 32 *) + 0xba05014a; (* arm_ADCS X10 X10 X5 *) + 0xd360fdc5; (* arm_LSR X5 X14 32 *) + 0x9a05016b; (* arm_ADC X11 X11 X5 *) + 0xab0a015f; (* arm_CMN X10 X10 *) + 0xb241014a; (* arm_ORR X10 X10 (rvalue (word 9223372036854775808)) *) + 0x9a0b0171; (* arm_ADC X17 X11 X11 *) + 0xd2800263; (* arm_MOV X3 (rvalue (word 19)) *) + 0x9b110c65; (* arm_MADD X5 X3 X17 X3 *) + 0xab0500e7; (* arm_ADDS X7 X7 X5 *) + 0xba1f0108; (* arm_ADCS X8 X8 XZR *) + 0xba1f0129; (* arm_ADCS X9 X9 XZR *) + 0xba1f014a; (* arm_ADCS X10 X10 XZR *) + 0x9a9f3063; (* arm_CSEL X3 X3 XZR Condition_CC *) + 0xeb0300e7; (* arm_SUBS X7 X7 X3 *) + 0xfa1f0108; (* arm_SBCS X8 X8 XZR *) + 0xfa1f0129; (* arm_SBCS X9 X9 XZR *) + 0xda1f014a; (* arm_SBC X10 X10 XZR *) + 0x9240f94a; (* arm_AND X10 X10 (rvalue (word 9223372036854775807)) *) + 0xa9002007; (* arm_STP X7 X8 X0 (Immediate_Offset (iword (&0))) *) + 0xa9012809; (* arm_STP X9 X10 X0 (Immediate_Offset (iword (&16))) *) 0xd65f03c0 (* arm_RET X30 *) ];; @@ -207,7 +192,18 @@ let BIGNUM_MUL_P25519_EXEC = ARM_MK_EXEC_RULE bignum_mul_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; + +let lemma0 = prove + (`!x0 x1:int64. + &(val(if val x0 <= val x1 then word_sub x1 x0 + else word_neg(word_sub x1 x0))):real = abs(&(val x1) - &(val x0))`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN + REWRITE_TAC[WORD_NEG_SUB; REAL_ARITH + `abs(x - y):real = if y <= x then x - y else y - x`] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN + RULE_ASSUM_TAC(REWRITE_RULE[REAL_OF_NUM_CLAUSES; NOT_LE]) THEN + ASM_SIMP_TAC[VAL_WORD_SUB_CASES; LT_IMP_LE; REAL_OF_NUM_SUB]);; let lemma1 = prove (`!(x0:num) x1 (y0:num) y1. @@ -221,19 +217,15 @@ let lemma1 = prove CONV_TAC WORD_REDUCE_CONV);; let lemma2 = prove - (`!(x0:int64) (x1:int64) (y0:int64) (y1:int64). - &(val(if val x1 <= val x0 then word_sub x0 x1 - else word_neg (word_sub x0 x1))) * - &(val(if val y0 <= val y1 then word_sub y1 y0 - else word_neg (word_sub y1 y0))):real = - --(&1) pow bitval(val y0 <= val y1 <=> val x0 < val x1) * - (&(val x0) - &(val x1)) * (&(val y1) - &(val y0))`, - REPEAT GEN_TAC THEN REWRITE_TAC[GSYM NOT_LE; WORD_NEG_SUB] THEN - REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES]) THEN - REPEAT(FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE - `~(m:num <= n) ==> n <= m /\ ~(m <= n)`))) THEN - ASM_SIMP_TAC[VAL_WORD_SUB_CASES; GSYM REAL_OF_NUM_SUB] THEN - REAL_ARITH_TAC);; + (`!p x0 x1 y0 y1:real. + (x0 + p * x1) * (y0 + p * y1) = + x0 * y0 + p pow 2 * x1 * y1 + + p * (x0 * y0 + x1 * y1 + + --(&1) pow bitval(y1 <= y0 <=> x1 < x0) * + abs(x1 - x0) * abs(y0 - y1))`, + REPEAT GEN_TAC THEN + MAP_EVERY ASM_CASES_TAC [`y1:real <= y0`; `x1:real < x0`] THEN + ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN ASM_REAL_ARITH_TAC);; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) @@ -257,19 +249,39 @@ let shiftandlemma = prove CONV_TAC NUM_REDUCE_CONV THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN ARITH_TAC);; +let KARATSUBA12_TAC = + REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID] THEN + MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN + MAP_EVERY EXISTS_TAC [`256`; `&0:real`] THEN + ASM_REWRITE_TAC[INTEGER_CLOSED] THEN + REPLICATE_TAC 2 (CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC]) THEN + REWRITE_TAC[lemma2; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN + ACCUMULATOR_POP_ASSUM_LIST(fun thl -> + MP_TAC(end_itlist CONJ(rev thl)) THEN + REWRITE_TAC[WORD_XOR_MASK] THEN + REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE; GSYM NOT_LE] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN + CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV) THEN + REWRITE_TAC[REAL_VAL_WORD_NOT; DIMINDEX_64] THEN + DISCH_THEN(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN + CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN + REWRITE_TAC(filter(is_ratconst o rand o concl) (DECARRY_RULE thl)) THEN + REAL_INTEGER_TAC);; + let BIGNUM_MUL_P25519_CORRECT = time prove (`!z x y m n pc. - nonoverlapping (word pc,0x2c4) (z,8 * 4) + nonoverlapping (word pc,0x288) (z,8 * 4) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) bignum_mul_p25519_mc /\ - read PC s = word(pc + 0x8) /\ + read PC s = word pc /\ C_ARGUMENTS [z; x; y] s /\ bignum_from_memory (x,4) s = m /\ bignum_from_memory (y,4) s = n) - (\s. read PC s = word (pc + 0x2b8) /\ + (\s. read PC s = word (pc + 0x284) /\ bignum_from_memory (z,4) s = (m * n) MOD p_25519) (MAYCHANGE [PC; X1; X2; X3; X4; X5; X6; X7; X8; X9; X10; X11; X12; - X13; X14; X15; X16; X17; X19; X20; X21] ,, + X13; X14; X15; X16; X17] ,, MAYCHANGE [memory :> bytes(z,8 * 4)] ,, MAYCHANGE SOME_FLAGS)`, MAP_EVERY X_GEN_TAC @@ -277,41 +289,195 @@ let BIGNUM_MUL_P25519_CORRECT = time prove REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN ENSURES_INIT_TAC "s0" THEN - BIGNUM_LDIGITIZE_TAC "m_" `read (memory :> bytes (x,8 * 4)) s0` THEN - BIGNUM_LDIGITIZE_TAC "n_" `read (memory :> bytes (y,8 * 4)) s0` THEN + BIGNUM_LDIGITIZE_TAC "x_" `read (memory :> bytes (x,8 * 4)) s0` THEN + BIGNUM_LDIGITIZE_TAC "y_" `read (memory :> bytes (y,8 * 4)) s0` THEN + + (*** First nested block multiplying the lower halves ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC + [3;5;10;11;15;17;18;19;22;24;25] (1--25) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN + + MAP_EVERY ABBREV_TAC + [`q0 = bignum_of_wordlist[mullo_s3;sum_s22]`; + `q1 = bignum_of_wordlist[sum_s24;sum_s25]`] THEN + SUBGOAL_THEN + `2 EXP 128 * q1 + q0 = + bignum_of_wordlist [x_0;x_1] * bignum_of_wordlist[y_0;y_1]` + ASSUME_TAC THENL + [MAP_EVERY EXPAND_TAC ["q0"; "q1"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** Second nested block multiplying the upper halves ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC + [28;30;35;36;40;42;43;44;47;49;50] (26--50) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN + + ABBREV_TAC + `q23 = bignum_of_wordlist[mullo_s28;sum_s47; sum_s49;sum_s50]` THEN + SUBGOAL_THEN + `q23 = bignum_of_wordlist [x_2;x_3] * bignum_of_wordlist[y_2;y_3]` + ASSUME_TAC THENL + [EXPAND_TAC "q23" THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** The sign-magnitude difference computation ***) - (*** The initial multiply block, very similar to bignum_mul_4_8 ***) + ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC + [53;54; 57;58; 61;63; 65;67] (51--68) THEN + RULE_ASSUM_TAC(REWRITE_RULE[WORD_UNMASK_64]) THEN + + MAP_EVERY ABBREV_TAC + [`sgn <=> ~(carry_s58 <=> carry_s54)`; + `xd = bignum_of_wordlist[sum_s61;sum_s63]`; + `yd = bignum_of_wordlist[sum_s65;sum_s67]`] THEN + SUBGOAL_THEN + `(&(bignum_of_wordlist[x_2;x_3]) - + &(bignum_of_wordlist[x_0;x_1])) * + (&(bignum_of_wordlist[y_0;y_1]) - + &(bignum_of_wordlist[y_2;y_3])):real = + --(&1) pow bitval sgn * &xd * &yd` + ASSUME_TAC THENL + [TRANS_TAC EQ_TRANS + `(--(&1) pow bitval carry_s54 * &xd) * + (--(&1) pow bitval carry_s58 * &yd):real` THEN + CONJ_TAC THENL + [ALL_TAC; + EXPAND_TAC "sgn" THEN REWRITE_TAC[BITVAL_NOT; BITVAL_IFF] THEN + POP_ASSUM_LIST(K ALL_TAC) THEN REWRITE_TAC[bitval] THEN + REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + CONV_TAC NUM_REDUCE_CONV THEN REAL_ARITH_TAC] THEN + SUBGOAL_THEN + `(carry_s54 <=> + bignum_of_wordlist[x_2;x_3] < bignum_of_wordlist[x_0;x_1]) /\ + (carry_s58 <=> + bignum_of_wordlist[y_0;y_1] < bignum_of_wordlist[y_2;y_3])` + (CONJUNCTS_THEN SUBST_ALL_TAC) + THENL + [CONJ_TAC THEN MATCH_MP_TAC FLAG_FROM_CARRY_LT THEN EXISTS_TAC `128` THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN + REWRITE_TAC[REAL_BITVAL_NOT; REAL_VAL_WORD_MASK; DIMINDEX_64] THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN BOUNDER_TAC[]; + ALL_TAC] THEN + BINOP_TAC THEN REWRITE_TAC[bitval] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_LID] THEN + REWRITE_TAC[REAL_ARITH `x - y:real = --(&1) pow 1 * z <=> y - x = z`] THEN + MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN + MAP_EVERY EXISTS_TAC [`128`; `&0:real`] THEN + (CONJ_TAC THENL + [MATCH_MP_TAC(REAL_ARITH + `y:real <= x /\ (&0 <= x /\ x < e) /\ (&0 <= y /\ y < e) + ==> &0 <= x - y /\ x - y < e`) THEN + ASM_SIMP_TAC[REAL_OF_NUM_CLAUSES; LT_IMP_LE; + ARITH_RULE `~(a:num < b) ==> b <= a`] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + CONJ_TAC THEN BOUNDER_TAC[]; + ALL_TAC] THEN + MAP_EVERY EXPAND_TAC ["xd"; "yd"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + CONJ_TAC THENL [BOUNDER_TAC[]; REWRITE_TAC[INTEGER_CLOSED]]) THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN + ASM_REWRITE_TAC[WORD_XOR_MASK] THEN + REWRITE_TAC[REAL_VAL_WORD_NOT; BITVAL_CLAUSES; DIMINDEX_64] THEN + DISCH_THEN(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN + + (*** Clean up the overall sign ***) + + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [WORD_XOR_MASKS]) THEN + ASM_REWRITE_TAC[] THEN DISCH_TAC THEN + + (*** The augmented H' = H + L_top ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC (69--72) (69--72) THEN + MAP_EVERY ABBREV_TAC + [`q2 = bignum_of_wordlist[sum_s69;sum_s70]`; + `q3 = bignum_of_wordlist[sum_s71;sum_s72]`] THEN + SUBGOAL_THEN + `2 EXP 128 * q3 + q2 = + bignum_of_wordlist [x_2;x_3] * bignum_of_wordlist[y_2;y_3] + q1` + ASSUME_TAC THENL + [MAP_EVERY EXPAND_TAC ["q1"; "q2"; "q3"] THEN + MATCH_MP_TAC CONG_IMP_EQ THEN EXISTS_TAC `2 EXP 256` THEN + REPEAT(CONJ_TAC THENL + [CONV_TAC NUM_REDUCE_CONV THEN BOUNDER_TAC[]; ALL_TAC]) THEN + FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC + (LAND_CONV o LAND_CONV) [SYM th]) THEN + MAP_EVERY EXPAND_TAC ["q23"] THEN + REWRITE_TAC[REAL_CONGRUENCE] THEN CONV_TAC NUM_REDUCE_CONV THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; + ALL_TAC] THEN + + (*** Third nested block multiplying the absolute differences ***) ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC - [5; 6; 7; 8; 10; 12; 14; 16; 17; 18; 19; 20; 21; 22; 23; 24; - 25; 26; 27; 33; 38; 40; 41; 47; 52; 54; 55; 56; 57; 58; 59; - 65; 70; 72; 73; 74; 80; 85; 87; 88; 89; 90; 91; 97; 102; - 104; 105; 106; 107; 113; 118; 120; 121; 122; 123] - (1--123) THEN + [73;75;80;81;85;87;88;89;92;94;95] (73--95) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN + SUBGOAL_THEN + `&xd * &yd:real = + &(bignum_of_wordlist[mullo_s73; sum_s92; sum_s94; sum_s95])` + SUBST_ALL_TAC THENL + [MAP_EVERY EXPAND_TAC ["xd"; "yd"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** The rest of the basic 4x4->8 multiply computation and its proof ***) + ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC + [96;97;98;99;100;101;104;106;108;110;111;112] (96--112) THEN MAP_EVERY ABBREV_TAC - [`l = bignum_of_wordlist[mullo_s5; sum_s52; sum_s85; sum_s118]`; - `h = bignum_of_wordlist[sum_s120; sum_s121; sum_s122; sum_s123]`] THEN + [`l = bignum_of_wordlist[mullo_s3; sum_s22; sum_s104; sum_s106]`; + `h = bignum_of_wordlist[sum_s108; sum_s110; sum_s111; sum_s112]`] THEN SUBGOAL_THEN `2 EXP 256 * h + l = m * n` (SUBST1_TAC o SYM) THENL - [MAP_EVERY EXPAND_TAC ["h"; "l"; "m"; "n"] THEN - REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN + [DISCARD_STATE_TAC "s112" THEN MAP_EVERY EXPAND_TAC ["h"; "l"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN MAP_EVERY EXISTS_TAC [`512`; `&0:real`] THEN - REPLICATE_TAC 2 (CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC]) THEN - CONJ_TAC THENL [REAL_INTEGER_TAC; ALL_TAC] THEN + CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC] THEN CONJ_TAC THENL + [MAP_EVERY EXPAND_TAC ["m"; "n"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN BOUNDER_TAC[]; + REWRITE_TAC[INTEGER_CLOSED]] THEN + SUBGOAL_THEN + `&m * &n:real = + (&1 + &2 pow 128) * (&q0 + &2 pow 128 * &q2 + &2 pow 256 * &q3) + + &2 pow 128 * + (&(bignum_of_wordlist [x_2; x_3]) - + &(bignum_of_wordlist [x_0; x_1])) * + (&(bignum_of_wordlist [y_0; y_1]) - + &(bignum_of_wordlist [y_2; y_3]))` + SUBST1_TAC THENL + [MAP_EVERY UNDISCH_TAC + [`2 EXP 128 * q1 + q0 = + bignum_of_wordlist[x_0; x_1] * bignum_of_wordlist[y_0; y_1]`; + `2 EXP 128 * q3 + q2 = + bignum_of_wordlist[x_2; x_3] * bignum_of_wordlist[y_2; y_3] + + q1`] THEN + MAP_EVERY EXPAND_TAC ["m"; "n"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN + CONV_TAC REAL_RING; + ASM_REWRITE_TAC[]] THEN + MAP_EVERY EXPAND_TAC ["h"; "l"; "q0"; "q2"; "q3"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN POP_ASSUM_LIST(K ALL_TAC) THEN - REWRITE_TAC[lemma1; lemma2] THEN REWRITE_TAC[WORD_XOR_MASK] THEN - REPEAT(COND_CASES_TAC THEN - ASM_REWRITE_TAC[BITVAL_CLAUSES; REAL_VAL_WORD_NOT]) THEN + REWRITE_TAC[WORD_XOR_MASK] THEN COND_CASES_TAC THEN + ASM_REWRITE_TAC[REAL_VAL_WORD_NOT; BITVAL_CLAUSES; DIMINDEX_64] THEN CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC NUM_REDUCE_CONV THEN - REWRITE_TAC[BITVAL_CLAUSES; DIMINDEX_64] THEN - POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC THEN + REWRITE_TAC[BITVAL_CLAUSES] THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN - DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN - CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN - FIRST_ASSUM(MP_TAC o end_itlist CONJ o filter(is_ratconst o rand o concl) o - DECARRY_RULE o CONJUNCTS) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN @@ -335,13 +501,13 @@ let BIGNUM_MUL_P25519_CORRECT = time prove (*** Reduction from 8 digits to 5 digits ***) ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC - [127;128;129;132;133;134;137;138;139;142;143;144;147;149;151;153;155] - (124--155) THEN + [116;117;118;121;122;123;126;127;128;131;132;133;136;138;140;142;144] + (113--144) THEN RULE_ASSUM_TAC(REWRITE_RULE[COND_SWAP; GSYM WORD_BITVAL]) THEN ABBREV_TAC `ca = bignum_of_wordlist - [sum_s147; sum_s149; sum_s151; sum_s153; sum_s155]` THEN + [sum_s136; sum_s138; sum_s140; sum_s142; sum_s144]` THEN SUBGOAL_THEN `(38 * h + l) DIV 2 EXP 255 + 1 <= 78` ASSUME_TAC THENL [REWRITE_TAC[ARITH_RULE `a + 1 <= b <=> a < b`] THEN @@ -352,10 +518,10 @@ let BIGNUM_MUL_P25519_CORRECT = time prove [MAP_EVERY EXPAND_TAC ["h"; "l"; "ca"] THEN TRANS_TAC EQ_TRANS - `bignum_of_wordlist[sum_s129; sum_s134; sum_s139; sum_s144; - word(bitval carry_s144)] + + `bignum_of_wordlist[sum_s118; sum_s123; sum_s128; sum_s133; + word(bitval carry_s133)] + 2 EXP 32 * - bignum_of_wordlist[mullo_s128; mullo_s133; mullo_s138; mullo_s143]` THEN + bignum_of_wordlist[mullo_s117; mullo_s122; mullo_s127; mullo_s132]` THEN CONJ_TAC THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN REWRITE_TAC[VAL_WORD_BITVAL] THENL @@ -378,10 +544,10 @@ let BIGNUM_MUL_P25519_CORRECT = time prove (*** Quotient estimate computation ***) - ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC (156--158) (156--158) THEN + ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC (145--147) (145--147) THEN ABBREV_TAC `t = bignum_of_wordlist - [sum_s147; sum_s149; sum_s151; - word_or sum_s153 (word 9223372036854775808)]` THEN + [sum_s136; sum_s138; sum_s140; + word_or sum_s142 (word 9223372036854775808)]` THEN SUBGOAL_THEN `&ca = &t + &2 pow 255 * (&(ca DIV 2 EXP 255) - &1)` ASSUME_TAC THENL [REWRITE_TAC[REAL_ARITH @@ -396,7 +562,7 @@ let BIGNUM_MUL_P25519_CORRECT = time prove `2 EXP 255 = 2 EXP 192 * 2 EXP 63`] THEN REWRITE_TAC[BIGNUM_OF_WORDLIST_SPLIT_RULE(3,1)] THEN SIMP_TAC[MOD_MULT_ADD; DIV_MULT_ADD; EXP_EQ_0; ARITH_EQ] THEN - SUBGOAL_THEN `bignum_of_wordlist [sum_s147; sum_s149; sum_s151] < 2 EXP 192` + SUBGOAL_THEN `bignum_of_wordlist [sum_s136; sum_s138; sum_s140] < 2 EXP 192` (fun th -> SIMP_TAC[th; MOD_LT; DIV_LT]) THENL [BOUNDER_TAC[]; ALL_TAC] THEN REWRITE_TAC[ADD_CLAUSES; ARITH_RULE @@ -409,7 +575,7 @@ let BIGNUM_MUL_P25519_CORRECT = time prove `word_and (word_and x (word_not m)) m = word 0`] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV); ALL_TAC] THEN - SUBGOAL_THEN `ca DIV 2 EXP 255 = val(sum_s158:int64)` SUBST_ALL_TAC THENL + SUBGOAL_THEN `ca DIV 2 EXP 255 = val(sum_s147:int64)` SUBST_ALL_TAC THENL [UNDISCH_TAC `ca DIV 2 EXP 255 + 1 <= 78` THEN REWRITE_TAC[ARITH_RULE `n DIV 2 EXP 255 = n DIV 2 EXP 192 DIV 2 EXP 63`] THEN EXPAND_TAC "ca" THEN @@ -419,7 +585,7 @@ let BIGNUM_MUL_P25519_CORRECT = time prove CONJ_TAC THENL [MP_TAC th THEN ARITH_TAC; REWRITE_TAC[VAL_BOUND_64]]) THEN REWRITE_TAC[ARITH_RULE `n DIV 2 EXP 63 = (2 * n) DIV 2 EXP 64`] THEN SUBST1_TAC(SYM(BIGNUM_OF_WORDLIST_DIV_CONV - `bignum_of_wordlist [sum_s156; sum_s158] DIV 2 EXP 64`)) THEN + `bignum_of_wordlist [sum_s145; sum_s147] DIV 2 EXP 64`)) THEN MATCH_MP_TAC CONG_DIV2 THEN REWRITE_TAC[REAL_CONGRUENCE] THEN CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN @@ -427,30 +593,30 @@ let BIGNUM_MUL_P25519_CORRECT = time prove DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN ARM_STEPS_TAC BIGNUM_MUL_P25519_EXEC (159--160) THEN - ABBREV_TAC `qm:int64 = word(19 + 19 * val(sum_s158:int64))` THEN - SUBGOAL_THEN `&(val(qm:int64)):real = &19 * (&(val(sum_s158:int64)) + &1)` + ABBREV_TAC `qm:int64 = word(19 + 19 * val(sum_s147:int64))` THEN + SUBGOAL_THEN `&(val(qm:int64)):real = &19 * (&(val(sum_s147:int64)) + &1)` ASSUME_TAC THENL [EXPAND_TAC "qm" THEN REWRITE_TAC[VAL_WORD; DIMINDEX_64; REAL_OF_NUM_CLAUSES] THEN REWRITE_TAC[ARITH_RULE `c + c * q = c * (q + 1)`] THEN MATCH_MP_TAC MOD_LT THEN - UNDISCH_TAC `val(sum_s158:int64) + 1 <= 78` THEN ARITH_TAC; + UNDISCH_TAC `val(sum_s147:int64) + 1 <= 78` THEN ARITH_TAC; ALL_TAC] THEN (*** The rest of the computation ***) - ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC (161--172) (161--172) THEN + ARM_ACCSTEPS_TAC BIGNUM_MUL_P25519_EXEC (150--161) (150--161) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_UNIQ_BALANCED_REAL THEN - MAP_EVERY EXISTS_TAC [`val(sum_s158:int64) + 1`; `255`] THEN + MAP_EVERY EXISTS_TAC [`val(sum_s147:int64) + 1`; `255`] THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [REWRITE_TAC[p_25519] THEN ARITH_TAC; ALL_TAC] THEN CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC] THEN (*** Comparison computation and then the rest is easy ***) - SUBGOAL_THEN `ca < (val(sum_s158:int64) + 1) * p_25519 <=> ~carry_s164` + SUBGOAL_THEN `ca < (val(sum_s147:int64) + 1) * p_25519 <=> ~carry_s153` SUBST1_TAC THENL [CONV_TAC SYM_CONV THEN MATCH_MP_TAC FLAG_FROM_CARRY_LT THEN EXISTS_TAC `256` THEN ASM_REWRITE_TAC[] THEN EXPAND_TAC "t" THEN @@ -468,20 +634,16 @@ let BIGNUM_MUL_P25519_CORRECT = time prove REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; REAL_OF_NUM_MOD] THEN ACCUMULATOR_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN - ASM_CASES_TAC `carry_s164:bool` THEN + ASM_CASES_TAC `carry_s153:bool` THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN CONV_TAC WORD_REDUCE_CONV THEN REAL_INTEGER_TAC]);; let BIGNUM_MUL_P25519_SUBROUTINE_CORRECT = time prove - (`!z x y m n pc stackpointer returnaddress. - aligned 16 stackpointer /\ - nonoverlapping (word pc,0x2c4) (z,8 * 4) /\ - ALL (nonoverlapping (word_sub stackpointer (word 32),32)) - [(x,8 * 4); (y,8 * 4); (z,8 * 4); (word pc,0x2c4)] + (`!z x y m n pc returnaddress. + nonoverlapping (word pc,0x288) (z,8 * 4) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) bignum_mul_p25519_mc /\ read PC s = word pc /\ - read SP s = stackpointer /\ read X30 s = returnaddress /\ C_ARGUMENTS [z; x; y] s /\ bignum_from_memory(x,4) s = m /\ @@ -490,9 +652,7 @@ let BIGNUM_MUL_P25519_SUBROUTINE_CORRECT = time prove bignum_from_memory(z,4) s = (m * n) MOD p_25519) (MAYCHANGE [PC; X1; X2; X3; X4; X5; X6; X7; X8; X9; X10; X11; X12; X13; X14; X15; X16; X17] ,, - MAYCHANGE [memory :> bytes(z,8 * 4); - memory :> bytes(word_sub stackpointer (word 32),32)] ,, + MAYCHANGE [memory :> bytes(z,8 * 4)] ,, MAYCHANGE SOME_FLAGS)`, - ARM_ADD_RETURN_STACK_TAC - BIGNUM_MUL_P25519_EXEC BIGNUM_MUL_P25519_CORRECT - `[X19;X20;X21;X22]` 32);; + ARM_ADD_RETURN_NOSTACK_TAC + BIGNUM_MUL_P25519_EXEC BIGNUM_MUL_P25519_CORRECT);; diff --git a/arm/proofs/bignum_mul_p25519_alt.ml b/arm/proofs/bignum_mul_p25519_alt.ml index 25e2a77b..6552731b 100644 --- a/arm/proofs/bignum_mul_p25519_alt.ml +++ b/arm/proofs/bignum_mul_p25519_alt.ml @@ -133,7 +133,7 @@ let BIGNUM_MUL_P25519_ALT_EXEC = ARM_MK_EXEC_RULE bignum_mul_p25519_alt_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/arm/proofs/bignum_mul_p256k1.ml b/arm/proofs/bignum_mul_p256k1.ml index 81ee2f84..9c501efb 100644 --- a/arm/proofs/bignum_mul_p256k1.ml +++ b/arm/proofs/bignum_mul_p256k1.ml @@ -25,173 +25,162 @@ let bignum_mul_p256k1_mc = define_assert_from_elf "bignum_mul_p256k1_mc" "arm/se 0xa9bf53f3; (* arm_STP X19 X20 SP (Preimmediate_Offset (iword (-- &16))) *) 0xa9bf5bf5; (* arm_STP X21 X22 SP (Preimmediate_Offset (iword (-- &16))) *) 0xa9401023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&0))) *) - 0xa9402047; (* arm_LDP X7 X8 X2 (Immediate_Offset (iword (&0))) *) - 0xa9411825; (* arm_LDP X5 X6 X1 (Immediate_Offset (iword (&16))) *) - 0xa9412849; (* arm_LDP X9 X10 X2 (Immediate_Offset (iword (&16))) *) - 0x9b077c6b; (* arm_MUL X11 X3 X7 *) - 0x9b087c8c; (* arm_MUL X12 X4 X8 *) - 0x9b097cad; (* arm_MUL X13 X5 X9 *) - 0x9b0a7cce; (* arm_MUL X14 X6 X10 *) - 0x9bc77c6f; (* arm_UMULH X15 X3 X7 *) - 0xab0f018c; (* arm_ADDS X12 X12 X15 *) - 0x9bc87c8f; (* arm_UMULH X15 X4 X8 *) - 0xba0f01ad; (* arm_ADCS X13 X13 X15 *) - 0x9bc97caf; (* arm_UMULH X15 X5 X9 *) - 0xba0f01ce; (* arm_ADCS X14 X14 X15 *) - 0x9bca7ccf; (* arm_UMULH X15 X6 X10 *) - 0x9a1f01ef; (* arm_ADC X15 X15 XZR *) - 0xab0b0190; (* arm_ADDS X16 X12 X11 *) - 0xba0c01ac; (* arm_ADCS X12 X13 X12 *) - 0xba0d01cd; (* arm_ADCS X13 X14 X13 *) - 0xba0e01ee; (* arm_ADCS X14 X15 X14 *) - 0x9a0f03ef; (* arm_ADC X15 XZR X15 *) - 0xab0b0181; (* arm_ADDS X1 X12 X11 *) - 0xba1001a2; (* arm_ADCS X2 X13 X16 *) - 0xba0c01cc; (* arm_ADCS X12 X14 X12 *) - 0xba0d01ed; (* arm_ADCS X13 X15 X13 *) - 0xba0e03ee; (* arm_ADCS X14 XZR X14 *) - 0x9a0f03ef; (* arm_ADC X15 XZR X15 *) - 0xeb0600b5; (* arm_SUBS X21 X5 X6 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb090153; (* arm_SUBS X19 X10 X9 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba1401ad; (* arm_ADCS X13 X13 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba1301ce; (* arm_ADCS X14 X14 X19 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb040075; (* arm_SUBS X21 X3 X4 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb070113; (* arm_SUBS X19 X8 X7 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba140210; (* arm_ADCS X16 X16 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba130021; (* arm_ADCS X1 X1 X19 *) - 0xba110042; (* arm_ADCS X2 X2 X17 *) - 0xba11018c; (* arm_ADCS X12 X12 X17 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb060095; (* arm_SUBS X21 X4 X6 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb080153; (* arm_SUBS X19 X10 X8 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba14018c; (* arm_ADCS X12 X12 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba1301ad; (* arm_ADCS X13 X13 X19 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb050075; (* arm_SUBS X21 X3 X5 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) + 0xa9401845; (* arm_LDP X5 X6 X2 (Immediate_Offset (iword (&0))) *) + 0x9b057c67; (* arm_MUL X7 X3 X5 *) + 0x9bc57c68; (* arm_UMULH X8 X3 X5 *) + 0x9b067c89; (* arm_MUL X9 X4 X6 *) + 0x9bc67c8a; (* arm_UMULH X10 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xab080129; (* arm_ADDS X9 X9 X8 *) + 0x9a1f014a; (* arm_ADC X10 X10 XZR *) + 0xeb0600a3; (* arm_SUBS X3 X5 X6 *) + 0xda832463; (* arm_CNEG X3 X3 Condition_CC *) + 0xda902210; (* arm_CINV X16 X16 Condition_CC *) + 0x9b037c8f; (* arm_MUL X15 X4 X3 *) + 0x9bc37c83; (* arm_UMULH X3 X4 X3 *) + 0xab0900e8; (* arm_ADDS X8 X7 X9 *) + 0xba0a0129; (* arm_ADCS X9 X9 X10 *) + 0x9a1f014a; (* arm_ADC X10 X10 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0801e8; (* arm_ADCS X8 X15 X8 *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xba090069; (* arm_ADCS X9 X3 X9 *) + 0x9a10014a; (* arm_ADC X10 X10 X16 *) + 0xa9411023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&16))) *) + 0xa9411845; (* arm_LDP X5 X6 X2 (Immediate_Offset (iword (&16))) *) + 0x9b057c6b; (* arm_MUL X11 X3 X5 *) + 0x9bc57c6c; (* arm_UMULH X12 X3 X5 *) + 0x9b067c8d; (* arm_MUL X13 X4 X6 *) + 0x9bc67c8e; (* arm_UMULH X14 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xab0c01ad; (* arm_ADDS X13 X13 X12 *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xeb0600a3; (* arm_SUBS X3 X5 X6 *) + 0xda832463; (* arm_CNEG X3 X3 Condition_CC *) + 0xda902210; (* arm_CINV X16 X16 Condition_CC *) + 0x9b037c8f; (* arm_MUL X15 X4 X3 *) + 0x9bc37c83; (* arm_UMULH X3 X4 X3 *) + 0xab0d016c; (* arm_ADDS X12 X11 X13 *) + 0xba0e01ad; (* arm_ADCS X13 X13 X14 *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0c01ec; (* arm_ADCS X12 X15 X12 *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xba0d006d; (* arm_ADCS X13 X3 X13 *) + 0x9a1001ce; (* arm_ADC X14 X14 X16 *) + 0xa9411023; (* arm_LDP X3 X4 X1 (Immediate_Offset (iword (&16))) *) + 0xa940402f; (* arm_LDP X15 X16 X1 (Immediate_Offset (iword (&0))) *) + 0xeb0f0063; (* arm_SUBS X3 X3 X15 *) + 0xfa100084; (* arm_SBCS X4 X4 X16 *) + 0xda9f23f0; (* arm_CSETM X16 Condition_CC *) + 0xa940444f; (* arm_LDP X15 X17 X2 (Immediate_Offset (iword (&0))) *) + 0xeb0501e5; (* arm_SUBS X5 X15 X5 *) + 0xfa060226; (* arm_SBCS X6 X17 X6 *) 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb070133; (* arm_SUBS X19 X9 X7 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba140021; (* arm_ADCS X1 X1 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba130042; (* arm_ADCS X2 X2 X19 *) - 0xba11018c; (* arm_ADCS X12 X12 X17 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb060075; (* arm_SUBS X21 X3 X6 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb070153; (* arm_SUBS X19 X10 X7 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba140042; (* arm_ADCS X2 X2 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba13018c; (* arm_ADCS X12 X12 X19 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xeb050095; (* arm_SUBS X21 X4 X5 *) - 0xda9526b5; (* arm_CNEG X21 X21 Condition_CC *) - 0xda9f23f1; (* arm_CSETM X17 Condition_CC *) - 0xeb080133; (* arm_SUBS X19 X9 X8 *) - 0xda932673; (* arm_CNEG X19 X19 Condition_CC *) - 0x9b137eb4; (* arm_MUL X20 X21 X19 *) - 0x9bd37eb3; (* arm_UMULH X19 X21 X19 *) - 0xda912231; (* arm_CINV X17 X17 Condition_CC *) - 0xb100063f; (* arm_CMN X17 (rvalue (word 1)) *) - 0xca110294; (* arm_EOR X20 X20 X17 *) - 0xba140042; (* arm_ADCS X2 X2 X20 *) - 0xca110273; (* arm_EOR X19 X19 X17 *) - 0xba13018c; (* arm_ADCS X12 X12 X19 *) - 0xba1101ad; (* arm_ADCS X13 X13 X17 *) - 0xba1101ce; (* arm_ADCS X14 X14 X17 *) - 0x9a1101ef; (* arm_ADC X15 X15 X17 *) - 0xd2807a35; (* arm_MOV X21 (rvalue (word 977)) *) - 0xb26002b1; (* arm_ORR X17 X21 (rvalue (word 4294967296)) *) - 0x9b0c7e23; (* arm_MUL X3 X17 X12 *) - 0x9bcc7e27; (* arm_UMULH X7 X17 X12 *) - 0x92407db4; (* arm_AND X20 X13 (rvalue (word 4294967295)) *) - 0xd360fdb3; (* arm_LSR X19 X13 32 *) - 0x9b147ea4; (* arm_MUL X4 X21 X20 *) - 0x9b1352b4; (* arm_MADD X20 X21 X19 X20 *) - 0xab148084; (* arm_ADDS X4 X4 (Shiftedreg X20 LSL 32) *) - 0xd360fe94; (* arm_LSR X20 X20 32 *) - 0x9a140268; (* arm_ADC X8 X19 X20 *) - 0x9b0e7e25; (* arm_MUL X5 X17 X14 *) - 0x9bce7e29; (* arm_UMULH X9 X17 X14 *) - 0x92407df4; (* arm_AND X20 X15 (rvalue (word 4294967295)) *) - 0xd360fdf3; (* arm_LSR X19 X15 32 *) - 0x9b147ea6; (* arm_MUL X6 X21 X20 *) - 0x9b1352b4; (* arm_MADD X20 X21 X19 X20 *) - 0xab1480c6; (* arm_ADDS X6 X6 (Shiftedreg X20 LSL 32) *) - 0xd360fe94; (* arm_LSR X20 X20 32 *) - 0x9a14026a; (* arm_ADC X10 X19 X20 *) - 0xab03016b; (* arm_ADDS X11 X11 X3 *) - 0xba040210; (* arm_ADCS X16 X16 X4 *) - 0xba050021; (* arm_ADCS X1 X1 X5 *) - 0xba060042; (* arm_ADCS X2 X2 X6 *) - 0x9a9f37ec; (* arm_CSET X12 Condition_CS *) - 0xab070210; (* arm_ADDS X16 X16 X7 *) - 0xba080021; (* arm_ADCS X1 X1 X8 *) - 0xba090042; (* arm_ADCS X2 X2 X9 *) - 0x9a0a018c; (* arm_ADC X12 X12 X10 *) - 0x9100058f; (* arm_ADD X15 X12 (rvalue (word 1)) *) - 0x9b0f7ea3; (* arm_MUL X3 X21 X15 *) - 0xd360fde4; (* arm_LSR X4 X15 32 *) - 0xab0f8063; (* arm_ADDS X3 X3 (Shiftedreg X15 LSL 32) *) + 0xca100063; (* arm_EOR X3 X3 X16 *) + 0xeb100063; (* arm_SUBS X3 X3 X16 *) + 0xca100084; (* arm_EOR X4 X4 X16 *) + 0xda100084; (* arm_SBC X4 X4 X16 *) + 0xca1100a5; (* arm_EOR X5 X5 X17 *) + 0xeb1100a5; (* arm_SUBS X5 X5 X17 *) + 0xca1100c6; (* arm_EOR X6 X6 X17 *) + 0xda1100c6; (* arm_SBC X6 X6 X17 *) + 0xca100230; (* arm_EOR X16 X17 X16 *) + 0xab09016b; (* arm_ADDS X11 X11 X9 *) + 0xba0a018c; (* arm_ADCS X12 X12 X10 *) + 0xba1f01ad; (* arm_ADCS X13 X13 XZR *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0x9b057c62; (* arm_MUL X2 X3 X5 *) + 0x9bc57c71; (* arm_UMULH X17 X3 X5 *) + 0x9b067c8f; (* arm_MUL X15 X4 X6 *) + 0x9bc67c81; (* arm_UMULH X1 X4 X6 *) + 0xeb030084; (* arm_SUBS X4 X4 X3 *) + 0xda842484; (* arm_CNEG X4 X4 Condition_CC *) + 0xda9f23e9; (* arm_CSETM X9 Condition_CC *) + 0xab1101ef; (* arm_ADDS X15 X15 X17 *) + 0x9a1f0021; (* arm_ADC X1 X1 XZR *) + 0xeb0600a6; (* arm_SUBS X6 X5 X6 *) + 0xda8624c6; (* arm_CNEG X6 X6 Condition_CC *) + 0xda892129; (* arm_CINV X9 X9 Condition_CC *) + 0x9b067c85; (* arm_MUL X5 X4 X6 *) + 0x9bc67c86; (* arm_UMULH X6 X4 X6 *) + 0xab0f0051; (* arm_ADDS X17 X2 X15 *) + 0xba0101ef; (* arm_ADCS X15 X15 X1 *) + 0x9a1f0021; (* arm_ADC X1 X1 XZR *) + 0xb100053f; (* arm_CMN X9 (rvalue (word 1)) *) + 0xca0900a5; (* arm_EOR X5 X5 X9 *) + 0xba1100b1; (* arm_ADCS X17 X5 X17 *) + 0xca0900c6; (* arm_EOR X6 X6 X9 *) + 0xba0f00cf; (* arm_ADCS X15 X6 X15 *) + 0x9a090021; (* arm_ADC X1 X1 X9 *) + 0xab070169; (* arm_ADDS X9 X11 X7 *) + 0xba08018a; (* arm_ADCS X10 X12 X8 *) + 0xba0b01ab; (* arm_ADCS X11 X13 X11 *) + 0xba0c01cc; (* arm_ADCS X12 X14 X12 *) + 0xba1f01ad; (* arm_ADCS X13 X13 XZR *) + 0x9a1f01ce; (* arm_ADC X14 X14 XZR *) + 0xb100061f; (* arm_CMN X16 (rvalue (word 1)) *) + 0xca100042; (* arm_EOR X2 X2 X16 *) + 0xba090049; (* arm_ADCS X9 X2 X9 *) + 0xca100231; (* arm_EOR X17 X17 X16 *) + 0xba0a022a; (* arm_ADCS X10 X17 X10 *) + 0xca1001ef; (* arm_EOR X15 X15 X16 *) + 0xba0b01eb; (* arm_ADCS X11 X15 X11 *) + 0xca100021; (* arm_EOR X1 X1 X16 *) + 0xba0c002c; (* arm_ADCS X12 X1 X12 *) + 0xba1001ad; (* arm_ADCS X13 X13 X16 *) + 0x9a1001ce; (* arm_ADC X14 X14 X16 *) + 0xd2807a30; (* arm_MOV X16 (rvalue (word 977)) *) + 0xb2600201; (* arm_ORR X1 X16 (rvalue (word 4294967296)) *) + 0x9b0b7c23; (* arm_MUL X3 X1 X11 *) + 0x9bcb7c25; (* arm_UMULH X5 X1 X11 *) + 0x92407d8f; (* arm_AND X15 X12 (rvalue (word 4294967295)) *) + 0xd360fd82; (* arm_LSR X2 X12 32 *) + 0x9b0f7e04; (* arm_MUL X4 X16 X15 *) + 0x9b023e0f; (* arm_MADD X15 X16 X2 X15 *) + 0xab0f8084; (* arm_ADDS X4 X4 (Shiftedreg X15 LSL 32) *) + 0xd360fdef; (* arm_LSR X15 X15 32 *) + 0x9a0f0046; (* arm_ADC X6 X2 X15 *) + 0x9b0d7c33; (* arm_MUL X19 X1 X13 *) + 0x9bcd7c35; (* arm_UMULH X21 X1 X13 *) + 0x92407dcf; (* arm_AND X15 X14 (rvalue (word 4294967295)) *) + 0xd360fdc2; (* arm_LSR X2 X14 32 *) + 0x9b0f7e14; (* arm_MUL X20 X16 X15 *) + 0x9b023e0f; (* arm_MADD X15 X16 X2 X15 *) + 0xab0f8294; (* arm_ADDS X20 X20 (Shiftedreg X15 LSL 32) *) + 0xd360fdef; (* arm_LSR X15 X15 32 *) + 0x9a0f0056; (* arm_ADC X22 X2 X15 *) + 0xab0300e7; (* arm_ADDS X7 X7 X3 *) + 0xba040108; (* arm_ADCS X8 X8 X4 *) + 0xba130129; (* arm_ADCS X9 X9 X19 *) + 0xba14014a; (* arm_ADCS X10 X10 X20 *) + 0x9a9f37eb; (* arm_CSET X11 Condition_CS *) + 0xab050108; (* arm_ADDS X8 X8 X5 *) + 0xba060129; (* arm_ADCS X9 X9 X6 *) + 0xba15014a; (* arm_ADCS X10 X10 X21 *) + 0x9a16016b; (* arm_ADC X11 X11 X22 *) + 0x91000571; (* arm_ADD X17 X11 (rvalue (word 1)) *) + 0x9b117e03; (* arm_MUL X3 X16 X17 *) + 0xd360fe24; (* arm_LSR X4 X17 32 *) + 0xab118063; (* arm_ADDS X3 X3 (Shiftedreg X17 LSL 32) *) 0x9a0403e4; (* arm_ADC X4 XZR X4 *) - 0xab03016b; (* arm_ADDS X11 X11 X3 *) - 0xba040210; (* arm_ADCS X16 X16 X4 *) - 0xba1f0021; (* arm_ADCS X1 X1 XZR *) - 0xba1f0042; (* arm_ADCS X2 X2 XZR *) - 0x9a9f3231; (* arm_CSEL X17 X17 XZR Condition_CC *) - 0xeb11016b; (* arm_SUBS X11 X11 X17 *) - 0xfa1f0210; (* arm_SBCS X16 X16 XZR *) - 0xfa1f0021; (* arm_SBCS X1 X1 XZR *) - 0xda1f0042; (* arm_SBC X2 X2 XZR *) - 0xa900400b; (* arm_STP X11 X16 X0 (Immediate_Offset (iword (&0))) *) - 0xa9010801; (* arm_STP X1 X2 X0 (Immediate_Offset (iword (&16))) *) + 0xab0300e7; (* arm_ADDS X7 X7 X3 *) + 0xba040108; (* arm_ADCS X8 X8 X4 *) + 0xba1f0129; (* arm_ADCS X9 X9 XZR *) + 0xba1f014a; (* arm_ADCS X10 X10 XZR *) + 0x9a9f3021; (* arm_CSEL X1 X1 XZR Condition_CC *) + 0xeb0100e7; (* arm_SUBS X7 X7 X1 *) + 0xfa1f0108; (* arm_SBCS X8 X8 XZR *) + 0xfa1f0129; (* arm_SBCS X9 X9 XZR *) + 0xda1f014a; (* arm_SBC X10 X10 XZR *) + 0xa9002007; (* arm_STP X7 X8 X0 (Immediate_Offset (iword (&0))) *) + 0xa9012809; (* arm_STP X9 X10 X0 (Immediate_Offset (iword (&16))) *) 0xa8c15bf5; (* arm_LDP X21 X22 SP (Postimmediate_Offset (iword (&16))) *) 0xa8c153f3; (* arm_LDP X19 X20 SP (Postimmediate_Offset (iword (&16))) *) 0xd65f03c0 (* arm_RET X30 *) @@ -205,6 +194,17 @@ let BIGNUM_MUL_P256K1_EXEC = ARM_MK_EXEC_RULE bignum_mul_p256k1_mc;; let p_256k1 = new_definition `p_256k1 = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F`;; +let lemma0 = prove + (`!x0 x1:int64. + &(val(if val x0 <= val x1 then word_sub x1 x0 + else word_neg(word_sub x1 x0))):real = abs(&(val x1) - &(val x0))`, + REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN + REWRITE_TAC[WORD_NEG_SUB; REAL_ARITH + `abs(x - y):real = if y <= x then x - y else y - x`] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN + RULE_ASSUM_TAC(REWRITE_RULE[REAL_OF_NUM_CLAUSES; NOT_LE]) THEN + ASM_SIMP_TAC[VAL_WORD_SUB_CASES; LT_IMP_LE; REAL_OF_NUM_SUB]);; + let lemma1 = prove (`!(x0:num) x1 (y0:num) y1. (if y0 <= y1 @@ -217,19 +217,15 @@ let lemma1 = prove CONV_TAC WORD_REDUCE_CONV);; let lemma2 = prove - (`!(x0:int64) (x1:int64) (y0:int64) (y1:int64). - &(val(if val x1 <= val x0 then word_sub x0 x1 - else word_neg (word_sub x0 x1))) * - &(val(if val y0 <= val y1 then word_sub y1 y0 - else word_neg (word_sub y1 y0))):real = - --(&1) pow bitval(val y0 <= val y1 <=> val x0 < val x1) * - (&(val x0) - &(val x1)) * (&(val y1) - &(val y0))`, - REPEAT GEN_TAC THEN REWRITE_TAC[GSYM NOT_LE; WORD_NEG_SUB] THEN - REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES]) THEN - REPEAT(FIRST_X_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE - `~(m:num <= n) ==> n <= m /\ ~(m <= n)`))) THEN - ASM_SIMP_TAC[VAL_WORD_SUB_CASES; GSYM REAL_OF_NUM_SUB] THEN - REAL_ARITH_TAC);; + (`!p x0 x1 y0 y1:real. + (x0 + p * x1) * (y0 + p * y1) = + x0 * y0 + p pow 2 * x1 * y1 + + p * (x0 * y0 + x1 * y1 + + --(&1) pow bitval(y1 <= y0 <=> x1 < x0) * + abs(x1 - x0) * abs(y0 - y1))`, + REPEAT GEN_TAC THEN + MAP_EVERY ASM_CASES_TAC [`y1:real <= y0`; `x1:real < x0`] THEN + ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN ASM_REAL_ARITH_TAC);; let p256k1redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_256k1 - 1) @@ -239,19 +235,39 @@ let p256k1redlemma = prove n < q * p_256k1 + p_256k1`, CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REWRITE_TAC[p_256k1] THEN ARITH_TAC);; +let KARATSUBA12_TAC = + REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID] THEN + MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN + MAP_EVERY EXISTS_TAC [`256`; `&0:real`] THEN + ASM_REWRITE_TAC[INTEGER_CLOSED] THEN + REPLICATE_TAC 2 (CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC]) THEN + REWRITE_TAC[lemma2; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN + ACCUMULATOR_POP_ASSUM_LIST(fun thl -> + MP_TAC(end_itlist CONJ(rev thl)) THEN + REWRITE_TAC[WORD_XOR_MASK] THEN + REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE; GSYM NOT_LE] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN + CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV) THEN + REWRITE_TAC[REAL_VAL_WORD_NOT; DIMINDEX_64] THEN + DISCH_THEN(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN + CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN + REWRITE_TAC(filter(is_ratconst o rand o concl) (DECARRY_RULE thl)) THEN + REAL_INTEGER_TAC);; + let BIGNUM_MUL_P256K1_CORRECT = time prove (`!z x y m n pc. - nonoverlapping (word pc,0x2b4) (z,8 * 4) + nonoverlapping (word pc,0x288) (z,8 * 4) ==> ensures arm (\s. aligned_bytes_loaded s (word pc) bignum_mul_p256k1_mc /\ read PC s = word(pc + 0x8) /\ C_ARGUMENTS [z; x; y] s /\ bignum_from_memory (x,4) s = m /\ bignum_from_memory (y,4) s = n) - (\s. read PC s = word (pc + 0x2a8) /\ + (\s. read PC s = word (pc + 0x27c) /\ bignum_from_memory (z,4) s = (m * n) MOD p_256k1) (MAYCHANGE [PC; X1; X2; X3; X4; X5; X6; X7; X8; X9; X10; X11; X12; - X13; X14; X15; X16; X17; X19; X20; X21] ,, + X13; X14; X15; X16; X17; X19; X20; X21; X22] ,, MAYCHANGE [memory :> bytes(z,8 * 4)] ,, MAYCHANGE SOME_FLAGS)`, MAP_EVERY X_GEN_TAC @@ -259,41 +275,196 @@ let BIGNUM_MUL_P256K1_CORRECT = time prove REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS; NONOVERLAPPING_CLAUSES] THEN DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN REWRITE_TAC[BIGNUM_FROM_MEMORY_BYTES] THEN ENSURES_INIT_TAC "s0" THEN - BIGNUM_LDIGITIZE_TAC "m_" `read (memory :> bytes (x,8 * 4)) s0` THEN - BIGNUM_LDIGITIZE_TAC "n_" `read (memory :> bytes (y,8 * 4)) s0` THEN + BIGNUM_LDIGITIZE_TAC "x_" `read (memory :> bytes (x,8 * 4)) s0` THEN + BIGNUM_LDIGITIZE_TAC "y_" `read (memory :> bytes (y,8 * 4)) s0` THEN - (*** The initial multiply block, very similar to bignum_mul_4_8 ***) + (*** First nested block multiplying the lower halves ***) ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC - [5; 6; 7; 8; 10; 12; 14; 16; 17; 18; 19; 20; 21; 22; 23; 24; - 25; 26; 27; 33; 38; 40; 41; 47; 52; 54; 55; 56; 57; 58; 59; - 65; 70; 72; 73; 74; 80; 85; 87; 88; 89; 90; 91; 97; 102; - 104; 105; 106; 107; 113; 118; 120; 121; 122; 123] - (1--123) THEN + [3;5;10;11;15;17;18;19;22;24;25] (1--25) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN MAP_EVERY ABBREV_TAC - [`l = bignum_of_wordlist[mullo_s5; sum_s52; sum_s85; sum_s118]`; - `h = bignum_of_wordlist[sum_s120; sum_s121; sum_s122; sum_s123]`] THEN + [`q0 = bignum_of_wordlist[mullo_s3;sum_s22]`; + `q1 = bignum_of_wordlist[sum_s24;sum_s25]`] THEN + SUBGOAL_THEN + `2 EXP 128 * q1 + q0 = + bignum_of_wordlist [x_0;x_1] * bignum_of_wordlist[y_0;y_1]` + ASSUME_TAC THENL + [MAP_EVERY EXPAND_TAC ["q0"; "q1"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** Second nested block multiplying the upper halves ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC + [28;30;35;36;40;42;43;44;47;49;50] (26--50) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN + + ABBREV_TAC + `q23 = bignum_of_wordlist[mullo_s28;sum_s47; sum_s49;sum_s50]` THEN + SUBGOAL_THEN + `q23 = bignum_of_wordlist [x_2;x_3] * bignum_of_wordlist[y_2;y_3]` + ASSUME_TAC THENL + [EXPAND_TAC "q23" THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** The sign-magnitude difference computation ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC + [53;54; 57;58; 61;63; 65;67] (51--68) THEN + RULE_ASSUM_TAC(REWRITE_RULE[WORD_UNMASK_64]) THEN + + MAP_EVERY ABBREV_TAC + [`sgn <=> ~(carry_s58 <=> carry_s54)`; + `xd = bignum_of_wordlist[sum_s61;sum_s63]`; + `yd = bignum_of_wordlist[sum_s65;sum_s67]`] THEN + SUBGOAL_THEN + `(&(bignum_of_wordlist[x_2;x_3]) - + &(bignum_of_wordlist[x_0;x_1])) * + (&(bignum_of_wordlist[y_0;y_1]) - + &(bignum_of_wordlist[y_2;y_3])):real = + --(&1) pow bitval sgn * &xd * &yd` + ASSUME_TAC THENL + [TRANS_TAC EQ_TRANS + `(--(&1) pow bitval carry_s54 * &xd) * + (--(&1) pow bitval carry_s58 * &yd):real` THEN + CONJ_TAC THENL + [ALL_TAC; + EXPAND_TAC "sgn" THEN REWRITE_TAC[BITVAL_NOT; BITVAL_IFF] THEN + POP_ASSUM_LIST(K ALL_TAC) THEN REWRITE_TAC[bitval] THEN + REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN + CONV_TAC NUM_REDUCE_CONV THEN REAL_ARITH_TAC] THEN + SUBGOAL_THEN + `(carry_s54 <=> + bignum_of_wordlist[x_2;x_3] < bignum_of_wordlist[x_0;x_1]) /\ + (carry_s58 <=> + bignum_of_wordlist[y_0;y_1] < bignum_of_wordlist[y_2;y_3])` + (CONJUNCTS_THEN SUBST_ALL_TAC) + THENL + [CONJ_TAC THEN MATCH_MP_TAC FLAG_FROM_CARRY_LT THEN EXISTS_TAC `128` THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN + REWRITE_TAC[REAL_BITVAL_NOT; REAL_VAL_WORD_MASK; DIMINDEX_64] THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN BOUNDER_TAC[]; + ALL_TAC] THEN + BINOP_TAC THEN REWRITE_TAC[bitval] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_LID] THEN + REWRITE_TAC[REAL_ARITH `x - y:real = --(&1) pow 1 * z <=> y - x = z`] THEN + MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN + MAP_EVERY EXISTS_TAC [`128`; `&0:real`] THEN + (CONJ_TAC THENL + [MATCH_MP_TAC(REAL_ARITH + `y:real <= x /\ (&0 <= x /\ x < e) /\ (&0 <= y /\ y < e) + ==> &0 <= x - y /\ x - y < e`) THEN + ASM_SIMP_TAC[REAL_OF_NUM_CLAUSES; LT_IMP_LE; + ARITH_RULE `~(a:num < b) ==> b <= a`] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + CONJ_TAC THEN BOUNDER_TAC[]; + ALL_TAC] THEN + MAP_EVERY EXPAND_TAC ["xd"; "yd"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + CONJ_TAC THENL [BOUNDER_TAC[]; REWRITE_TAC[INTEGER_CLOSED]]) THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN + ASM_REWRITE_TAC[WORD_XOR_MASK] THEN + REWRITE_TAC[REAL_VAL_WORD_NOT; BITVAL_CLAUSES; DIMINDEX_64] THEN + DISCH_THEN(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN + + (*** Clean up the overall sign ***) + + FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [WORD_XOR_MASKS]) THEN + ASM_REWRITE_TAC[] THEN DISCH_TAC THEN + + (*** The augmented H' = H + L_top ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC (69--72) (69--72) THEN + MAP_EVERY ABBREV_TAC + [`q2 = bignum_of_wordlist[sum_s69;sum_s70]`; + `q3 = bignum_of_wordlist[sum_s71;sum_s72]`] THEN + SUBGOAL_THEN + `2 EXP 128 * q3 + q2 = + bignum_of_wordlist [x_2;x_3] * bignum_of_wordlist[y_2;y_3] + q1` + ASSUME_TAC THENL + [MAP_EVERY EXPAND_TAC ["q1"; "q2"; "q3"] THEN + MATCH_MP_TAC CONG_IMP_EQ THEN EXISTS_TAC `2 EXP 256` THEN + REPEAT(CONJ_TAC THENL + [CONV_TAC NUM_REDUCE_CONV THEN BOUNDER_TAC[]; ALL_TAC]) THEN + FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC + (LAND_CONV o LAND_CONV) [SYM th]) THEN + MAP_EVERY EXPAND_TAC ["q23"] THEN + REWRITE_TAC[REAL_CONGRUENCE] THEN CONV_TAC NUM_REDUCE_CONV THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN + DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; + ALL_TAC] THEN + + (*** Third nested block multiplying the absolute differences ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC + [73;75;80;81;85;87;88;89;92;94;95] (73--95) THEN + RULE_ASSUM_TAC(REWRITE_RULE[lemma0; lemma1]) THEN + SUBGOAL_THEN + `&xd * &yd:real = + &(bignum_of_wordlist[mullo_s73; sum_s92; sum_s94; sum_s95])` + SUBST_ALL_TAC THENL + [MAP_EVERY EXPAND_TAC ["xd"; "yd"] THEN + REWRITE_TAC[bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN + KARATSUBA12_TAC; + ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN + DISCARD_MATCHING_ASSUMPTIONS [`word a = b`]] THEN + + (*** The rest of the basic 4x4->8 multiply computation and its proof ***) + + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC + [96;97;98;99;100;101;104;106;108;110;111;112] (96--112) THEN + + MAP_EVERY ABBREV_TAC + [`l = bignum_of_wordlist[mullo_s3; sum_s22; sum_s104; sum_s106]`; + `h = bignum_of_wordlist[sum_s108; sum_s110; sum_s111; sum_s112]`] THEN SUBGOAL_THEN `2 EXP 256 * h + l = m * n` (SUBST1_TAC o SYM) THENL - [MAP_EVERY EXPAND_TAC ["h"; "l"; "m"; "n"] THEN - REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN + [DISCARD_STATE_TAC "s112" THEN MAP_EVERY EXPAND_TAC ["h"; "l"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN MAP_EVERY EXISTS_TAC [`512`; `&0:real`] THEN - REPLICATE_TAC 2 (CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC]) THEN - CONJ_TAC THENL [REAL_INTEGER_TAC; ALL_TAC] THEN + CONJ_TAC THENL [BOUNDER_TAC[]; ALL_TAC] THEN CONJ_TAC THENL + [MAP_EVERY EXPAND_TAC ["m"; "n"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN BOUNDER_TAC[]; + REWRITE_TAC[INTEGER_CLOSED]] THEN + SUBGOAL_THEN + `&m * &n:real = + (&1 + &2 pow 128) * (&q0 + &2 pow 128 * &q2 + &2 pow 256 * &q3) + + &2 pow 128 * + (&(bignum_of_wordlist [x_2; x_3]) - + &(bignum_of_wordlist [x_0; x_1])) * + (&(bignum_of_wordlist [y_0; y_1]) - + &(bignum_of_wordlist [y_2; y_3]))` + SUBST1_TAC THENL + [MAP_EVERY UNDISCH_TAC + [`2 EXP 128 * q1 + q0 = + bignum_of_wordlist[x_0; x_1] * bignum_of_wordlist[y_0; y_1]`; + `2 EXP 128 * q3 + q2 = + bignum_of_wordlist[x_2; x_3] * bignum_of_wordlist[y_2; y_3] + + q1`] THEN + MAP_EVERY EXPAND_TAC ["m"; "n"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN + CONV_TAC REAL_RING; + ASM_REWRITE_TAC[]] THEN + MAP_EVERY EXPAND_TAC ["h"; "l"; "q0"; "q2"; "q3"] THEN + REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES; bignum_of_wordlist] THEN ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN POP_ASSUM_LIST(K ALL_TAC) THEN - REWRITE_TAC[lemma1; lemma2] THEN REWRITE_TAC[WORD_XOR_MASK] THEN - REPEAT(COND_CASES_TAC THEN - ASM_REWRITE_TAC[BITVAL_CLAUSES; REAL_VAL_WORD_NOT]) THEN + REWRITE_TAC[WORD_XOR_MASK] THEN COND_CASES_TAC THEN + ASM_REWRITE_TAC[REAL_VAL_WORD_NOT; BITVAL_CLAUSES; DIMINDEX_64] THEN CONV_TAC WORD_REDUCE_CONV THEN CONV_TAC NUM_REDUCE_CONV THEN - REWRITE_TAC[BITVAL_CLAUSES; DIMINDEX_64] THEN - POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC THEN + REWRITE_TAC[BITVAL_CLAUSES] THEN DISCH_TAC THEN FIRST_ASSUM(MP_TAC o end_itlist CONJ o DESUM_RULE o CONJUNCTS) THEN - DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN - CONV_TAC(RAND_CONV REAL_POLY_CONV) THEN - FIRST_ASSUM(MP_TAC o end_itlist CONJ o filter(is_ratconst o rand o concl) o - DECARRY_RULE o CONJUNCTS) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN REAL_INTEGER_TAC; ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC)] THEN @@ -316,10 +487,10 @@ let BIGNUM_MUL_P256K1_CORRECT = time prove (*** Reduction from 8 digits to 5 digits, with fiddly hybrid muls ***) - ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC [126;132;134] (124--134) THEN + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC [115;121;123] (113--123) THEN SUBGOAL_THEN - `&2 pow 64 * &(val(sum_s134:int64)) + &(val(sum_s132:int64)):real = - &4294968273 * &(val(sum_s121:int64))` + `&2 pow 64 * &(val(sum_s123:int64)) + &(val(sum_s121:int64)):real = + &4294968273 * &(val(sum_s110:int64))` MP_TAC THENL [MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN MAP_EVERY EXISTS_TAC [`128`; `&0:real`] THEN @@ -343,10 +514,10 @@ let BIGNUM_MUL_P256K1_CORRECT = time prove (MP_TAC o end_itlist CONJ o rev o snd o chop_list 2) THEN STRIP_TAC THEN DISCH_TAC] THEN - ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC [135; 141; 143] (135--143) THEN + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC [124; 130; 132] (124--132) THEN SUBGOAL_THEN - `&2 pow 64 * &(val(sum_s143:int64)) + &(val(sum_s141:int64)):real = - &4294968273 * &(val(sum_s123:int64))` + `&2 pow 64 * &(val(sum_s132:int64)) + &(val(sum_s130:int64)):real = + &4294968273 * &(val(sum_s112:int64))` MP_TAC THENL [MATCH_MP_TAC EQUAL_FROM_CONGRUENT_REAL THEN MAP_EVERY EXISTS_TAC [`128`; `&0:real`] THEN @@ -370,13 +541,13 @@ let BIGNUM_MUL_P256K1_CORRECT = time prove (MP_TAC o end_itlist CONJ o rev o snd o chop_list 2) THEN STRIP_TAC THEN DISCH_TAC] THEN - ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC [144;145;146;147;149;150;151;152] - (144--152) THEN + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC [133;134;135;136;138;139;140;141] + (133--141) THEN RULE_ASSUM_TAC(REWRITE_RULE[COND_SWAP; GSYM WORD_BITVAL]) THEN ABBREV_TAC `ca = bignum_of_wordlist - [sum_s144; sum_s149; sum_s150; sum_s151; sum_s152]` THEN + [sum_s133; sum_s138; sum_s139; sum_s140; sum_s141]` THEN SUBGOAL_THEN `(4294968273 * h + l) DIV 2 EXP 256 + 1 <= 2 EXP 33` ASSUME_TAC THENL [REWRITE_TAC[ARITH_RULE `a + 1 <= b <=> a < b`] THEN @@ -393,30 +564,30 @@ let BIGNUM_MUL_P256K1_CORRECT = time prove (*** Quotient estimate computation ***) - SUBGOAL_THEN `ca DIV 2 EXP 256 = val(sum_s152:int64)` SUBST_ALL_TAC THENL + SUBGOAL_THEN `ca DIV 2 EXP 256 = val(sum_s141:int64)` SUBST_ALL_TAC THENL [EXPAND_TAC "ca" THEN CONV_TAC(LAND_CONV BIGNUM_OF_WORDLIST_DIV_CONV) THEN REFL_TAC; FIRST_ASSUM(ASSUME_TAC o MATCH_MP (ARITH_RULE `n + 1 < 2 EXP 64 ==> n < 2 EXP 64 - 1`))] THEN - ARM_STEPS_TAC BIGNUM_MUL_P256K1_EXEC [153] THEN - ABBREV_TAC `q:int64 = word_add sum_s152 (word 1)` THEN - SUBGOAL_THEN `val(sum_s152:int64) + 1 = val(q:int64)` SUBST_ALL_TAC THENL + ARM_STEPS_TAC BIGNUM_MUL_P256K1_EXEC [142] THEN + ABBREV_TAC `q:int64 = word_add sum_s141 (word 1)` THEN + SUBGOAL_THEN `val(sum_s141:int64) + 1 = val(q:int64)` SUBST_ALL_TAC THENL [EXPAND_TAC "q" THEN REWRITE_TAC[VAL_WORD_ADD; VAL_WORD_1] THEN ASM_SIMP_TAC[DIMINDEX_64; MOD_LT]; ALL_TAC] THEN (*** The rest of the computation, with more hybrid mul fiddling ***) - ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC (154--157) (154--157) THEN + ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC (143--146) (143--146) THEN SUBGOAL_THEN - `&2 pow 64 * &(val(sum_s157:int64)) + &(val(sum_s156:int64)) = + `&2 pow 64 * &(val(sum_s146:int64)) + &(val(sum_s145:int64)) = &4294968273 * &(val(q:int64))` MP_TAC THENL [ACCUMULATOR_POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN - CONV_TAC(LAND_CONV REAL_POLY_CONV) THEN EXPAND_TAC "mullo_s154" THEN + CONV_TAC(LAND_CONV REAL_POLY_CONV) THEN EXPAND_TAC "mullo_s143" THEN REWRITE_TAC[REAL_OF_NUM_CLAUSES; VAL_WORD; DIMINDEX_64] THEN ASM_SIMP_TAC[MOD_LT; ARITH_RULE `q <= 2 EXP 33 ==> 977 MOD 2 EXP 64 * q < 2 EXP 64`] THEN @@ -424,7 +595,7 @@ let BIGNUM_MUL_P256K1_CORRECT = time prove ACCUMULATOR_POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC] THEN ARM_ACCSTEPS_TAC BIGNUM_MUL_P256K1_EXEC - [158;159;160;161;163;164;165;166] (158--168) THEN + [147;148;149;150;152;153;154;155] (147--157) THEN ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC(LAND_CONV BIGNUM_EXPAND_CONV) THEN ASM_REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_UNIQ_BALANCED_REAL THEN @@ -434,17 +605,17 @@ let BIGNUM_MUL_P256K1_CORRECT = time prove (*** Comparison computation and then the rest is easy ***) - SUBGOAL_THEN `ca < val(q:int64) * p_256k1 <=> ~carry_s161` SUBST1_TAC THENL + SUBGOAL_THEN `ca < val(q:int64) * p_256k1 <=> ~carry_s150` SUBST1_TAC THENL [CONV_TAC SYM_CONV THEN MATCH_MP_TAC FLAG_FROM_CARRY_LT THEN EXISTS_TAC `256` THEN EXPAND_TAC "ca" THEN REWRITE_TAC[p_256k1; bignum_of_wordlist; GSYM REAL_OF_NUM_CLAUSES] THEN REWRITE_TAC[REAL_BITVAL_NOT] THEN - SUBGOAL_THEN `&(val(sum_s152:int64)):real = &(val(q:int64)) - &1` + SUBGOAL_THEN `&(val(sum_s141:int64)):real = &(val(q:int64)) - &1` SUBST1_TAC THENL [FIRST_X_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `n < 2 EXP 64 - 1 ==> n + 1 < 2 EXP 64`)) THEN UNDISCH_THEN - `word_add sum_s152 (word 1):int64 = q` (SUBST1_TAC o SYM) THEN + `word_add sum_s141 (word 1):int64 = q` (SUBST1_TAC o SYM) THEN SIMP_TAC[VAL_WORD_ADD; VAL_WORD_1; DIMINDEX_64; MOD_LT] THEN REWRITE_TAC[GSYM REAL_OF_NUM_CLAUSES] THEN REAL_ARITH_TAC; ACCUMULATOR_ASSUM_LIST(MP_TAC o end_itlist CONJ o DECARRY_RULE) THEN @@ -455,16 +626,16 @@ let BIGNUM_MUL_P256K1_CORRECT = time prove RULE_ASSUM_TAC(REWRITE_RULE[WORD_UNMASK_64]) THEN ACCUMULATOR_ASSUM_LIST(MP_TAC o end_itlist CONJ o DESUM_RULE) THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN - ASM_CASES_TAC `carry_s161:bool` THEN + ASM_CASES_TAC `carry_s150:bool` THEN ASM_REWRITE_TAC[BITVAL_CLAUSES] THEN CONV_TAC WORD_REDUCE_CONV THEN REAL_INTEGER_TAC]);; let BIGNUM_MUL_P256K1_SUBROUTINE_CORRECT = time prove (`!z x y m n pc stackpointer returnaddress. aligned 16 stackpointer /\ - nonoverlapping (word pc,0x2b4) (z,8 * 4) /\ + nonoverlapping (word pc,0x288) (z,8 * 4) /\ ALL (nonoverlapping (word_sub stackpointer (word 32),32)) - [(x,8 * 4); (y,8 * 4); (z,8 * 4); (word pc,0x2b4)] + [(x,8 * 4); (y,8 * 4); (z,8 * 4); (word pc,0x288)] ==> ensures arm (\s. aligned_bytes_loaded s (word pc) bignum_mul_p256k1_mc /\ read PC s = word pc /\ diff --git a/arm/proofs/bignum_neg_p25519.ml b/arm/proofs/bignum_neg_p25519.ml index a8152279..7f6aad76 100644 --- a/arm/proofs/bignum_neg_p25519.ml +++ b/arm/proofs/bignum_neg_p25519.ml @@ -50,7 +50,7 @@ let BIGNUM_NEG_P25519_EXEC = ARM_MK_EXEC_RULE bignum_neg_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let BIGNUM_NEG_P25519_CORRECT = time prove (`!z x n pc. diff --git a/arm/proofs/bignum_sqr_p25519.ml b/arm/proofs/bignum_sqr_p25519.ml index 7e9bc023..50f26e90 100644 --- a/arm/proofs/bignum_sqr_p25519.ml +++ b/arm/proofs/bignum_sqr_p25519.ml @@ -145,7 +145,7 @@ let BIGNUM_SQR_P25519_EXEC = ARM_MK_EXEC_RULE bignum_sqr_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let lemma1 = prove (`!(x0:num) x1 (y0:num) y1. diff --git a/arm/proofs/bignum_sqr_p25519_alt.ml b/arm/proofs/bignum_sqr_p25519_alt.ml index 0a393005..b43f3818 100644 --- a/arm/proofs/bignum_sqr_p25519_alt.ml +++ b/arm/proofs/bignum_sqr_p25519_alt.ml @@ -111,7 +111,7 @@ let BIGNUM_SQR_P25519_ALT_EXEC = ARM_MK_EXEC_RULE bignum_sqr_p25519_alt_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/arm/proofs/bignum_sub_p25519.ml b/arm/proofs/bignum_sub_p25519.ml index a863cef0..092e16b5 100644 --- a/arm/proofs/bignum_sub_p25519.ml +++ b/arm/proofs/bignum_sub_p25519.ml @@ -48,7 +48,7 @@ let BIGNUM_SUB_P25519_EXEC = ARM_MK_EXEC_RULE bignum_sub_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let BIGNUM_SUB_P25519_CORRECT = time prove (`!z x y m n pc. diff --git a/arm/secp256k1/bignum_mul_p256k1.S b/arm/secp256k1/bignum_mul_p256k1.S index c579f587..e92e8748 100644 --- a/arm/secp256k1/bignum_mul_p256k1.S +++ b/arm/secp256k1/bignum_mul_p256k1.S @@ -29,147 +29,217 @@ .text .balign 4 -// --------------------------------------------------------------------------- -// Macro computing [c,b,a] := [b,a] + (x - y) * (w - z), adding with carry -// to the [b,a] components but leaving CF aligned with the c term, which is -// a sign bitmask for (x - y) * (w - z). Continued add-with-carry operations -// with [c,...,c] will continue the carry chain correctly starting from -// the c position if desired to add to a longer term of the form [...,b,a]. -// -// c,h,l,t should all be different and t,h should not overlap w,z. -// --------------------------------------------------------------------------- - -#define muldiffnadd(b,a,x,y,w,z) \ - subs t, x, y; \ - cneg t, t, cc; \ - csetm c, cc; \ - subs h, w, z; \ - cneg h, h, cc; \ - mul l, t, h; \ - umulh h, t, h; \ - cinv c, c, cc; \ - adds xzr, c, #1; \ - eor l, l, c; \ - adcs a, a, l; \ - eor h, h, c; \ - adcs b, b, h +#define z x0 +#define x x1 +#define y x2 #define a0 x3 #define a1 x4 -#define a2 x5 -#define a3 x6 -#define b0 x7 -#define b1 x8 -#define b2 x9 -#define b3 x10 - -#define s0 x11 -#define s1 x12 -#define s2 x13 -#define s3 x14 -#define s4 x15 - -#define m x15 -#define q x15 - -#define t0 x11 -#define t1 x16 -#define t2 x12 -#define t3 x13 -#define t4 x14 -#define t5 x15 - -#define u0 x11 -#define u1 x16 -#define u2 x1 -#define u3 x2 -#define u4 x12 -#define u5 x13 -#define u6 x14 -#define u7 x15 - -#define c x17 -#define h x19 -#define l x20 -#define t x21 -#define d x21 +#define b0 x5 +#define b1 x6 + +#define u0 x7 +#define u1 x8 +#define u2 x9 +#define u3 x10 +#define u4 x11 +#define u5 x12 +#define u6 x13 +#define u7 x14 + +#define t x15 + +#define sgn x16 +#define ysgn x17 + +// These are aliases to registers used elsewhere including input pointers. +// By the time they are used this does not conflict with other uses. + +#define m0 y +#define m1 ysgn +#define m2 t +#define m3 x +#define u u2 + +// For the reduction stages, again aliasing other things but not the u's + +#define c x1 +#define h x2 +#define l x15 +#define d x16 +#define q x17 +#define a2 x19 +#define a3 x20 +#define b2 x21 +#define b3 x22 S2N_BN_SYMBOL(bignum_mul_p256k1): -stp x19, x20, [sp, #-16]! +// Preserve registers that are used in the reduction phase + + stp x19, x20, [sp, #-16]! stp x21, x22, [sp, #-16]! -// Load operands - - ldp a0, a1, [x1] - ldp b0, b1, [x2] - ldp a2, a3, [x1, #16] - ldp b2, b3, [x2, #16] - -// First accumulate all the "simple" products as [s4,s3,s2,s1,s0] - - mul s0, a0, b0 - mul s1, a1, b1 - mul s2, a2, b2 - mul s3, a3, b3 - - umulh m, a0, b0 - adds s1, s1, m - umulh m, a1, b1 - adcs s2, s2, m - umulh m, a2, b2 - adcs s3, s3, m - umulh m, a3, b3 - adc s4, m, xzr - -// Multiply by B + 1 to get [t5;t4;t3;t2;t1;t0] where t0 == s0 - - adds t1, s1, s0 - adcs t2, s2, s1 - adcs t3, s3, s2 - adcs t4, s4, s3 - adc t5, xzr, s4 - -// Multiply by B^2 + 1 to get [u6;u5;u4;u3;u2;u1;-]. Note that -// u0 == t0 == s0 and u1 == t1 - - adds u2, t2, t0 - adcs u3, t3, t1 - adcs u4, t4, t2 - adcs u5, t5, t3 - adcs u6, xzr, t4 - adc u7, xzr, t5 - -// Now add in all the "complicated" terms. - - muldiffnadd(u6,u5, a2,a3, b3,b2) - adc u7, u7, c - - muldiffnadd(u2,u1, a0,a1, b1,b0) - adcs u3, u3, c - adcs u4, u4, c - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd(u5,u4, a1,a3, b3,b1) - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd(u3,u2, a0,a2, b2,b0) - adcs u4, u4, c - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - - muldiffnadd(u4,u3, a0,a3, b3,b0) - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c - muldiffnadd(u4,u3, a1,a2, b2,b1) - adcs u5, u5, c - adcs u6, u6, c - adc u7, u7, c +// Multiply the low halves using Karatsuba 2x2->4 to get [u3,u2,u1,u0] + + ldp a0, a1, [x] + ldp b0, b1, [y] + + mul u0, a0, b0 + umulh u1, a0, b0 + mul u2, a1, b1 + umulh u3, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm sgn, cc + + adds u2, u2, u1 + adc u3, u3, xzr + + subs a0, b0, b1 + cneg a0, a0, cc + cinv sgn, sgn, cc + + mul t, a1, a0 + umulh a0, a1, a0 + + adds u1, u0, u2 + adcs u2, u2, u3 + adc u3, u3, xzr + + adds xzr, sgn, #1 + eor t, t, sgn + adcs u1, t, u1 + eor a0, a0, sgn + adcs u2, a0, u2 + adc u3, u3, sgn + +// Multiply the high halves using Karatsuba 2x2->4 to get [u7,u6,u5,u4] + + ldp a0, a1, [x, #16] + ldp b0, b1, [y, #16] + + mul u4, a0, b0 + umulh u5, a0, b0 + mul u6, a1, b1 + umulh u7, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm sgn, cc + + adds u6, u6, u5 + adc u7, u7, xzr + + subs a0, b0, b1 + cneg a0, a0, cc + cinv sgn, sgn, cc + + mul t, a1, a0 + umulh a0, a1, a0 + + adds u5, u4, u6 + adcs u6, u6, u7 + adc u7, u7, xzr + + adds xzr, sgn, #1 + eor t, t, sgn + adcs u5, t, u5 + eor a0, a0, sgn + adcs u6, a0, u6 + adc u7, u7, sgn + +// Compute sgn,[a1,a0] = x_hi - x_lo +// and ysgn,[b1,b0] = y_lo - y_hi +// sign-magnitude differences + + ldp a0, a1, [x, #16] + ldp t, sgn, [x] + subs a0, a0, t + sbcs a1, a1, sgn + csetm sgn, cc + + ldp t, ysgn, [y] + subs b0, t, b0 + sbcs b1, ysgn, b1 + csetm ysgn, cc + + eor a0, a0, sgn + subs a0, a0, sgn + eor a1, a1, sgn + sbc a1, a1, sgn + + eor b0, b0, ysgn + subs b0, b0, ysgn + eor b1, b1, ysgn + sbc b1, b1, ysgn + +// Save the correct sign for the sub-product + + eor sgn, ysgn, sgn + +// Add H' = H + L_top, still in [u7,u6,u5,u4] + + adds u4, u4, u2 + adcs u5, u5, u3 + adcs u6, u6, xzr + adc u7, u7, xzr + +// Now compute the mid-product as [m3,m2,m1,m0] + + mul m0, a0, b0 + umulh m1, a0, b0 + mul m2, a1, b1 + umulh m3, a1, b1 + + subs a1, a1, a0 + cneg a1, a1, cc + csetm u, cc + + adds m2, m2, m1 + adc m3, m3, xzr + + subs b1, b0, b1 + cneg b1, b1, cc + cinv u, u, cc + + mul b0, a1, b1 + umulh b1, a1, b1 + + adds m1, m0, m2 + adcs m2, m2, m3 + adc m3, m3, xzr + + adds xzr, u, #1 + eor b0, b0, u + adcs m1, b0, m1 + eor b1, b1, u + adcs m2, b1, m2 + adc m3, m3, u + +// Accumulate the positive mid-terms as [u7,u6,u5,u4,u3,u2] + + adds u2, u4, u0 + adcs u3, u5, u1 + adcs u4, u6, u4 + adcs u5, u7, u5 + adcs u6, u6, xzr + adc u7, u7, xzr + +// Add in the sign-adjusted complex term + + adds xzr, sgn, #1 + eor m0, m0, sgn + adcs u2, m0, u2 + eor m1, m1, sgn + adcs u3, m1, u3 + eor m2, m2, sgn + adcs u4, m2, u4 + eor m3, m3, sgn + adcs u5, m3, u5 + adcs u6, u6, sgn + adc u7, u7, sgn // Now we have the full 8-digit product 2^256 * h + l where // h = [u7,u6,u5,u4] and l = [u3,u2,u1,u0] diff --git a/common/components.ml b/common/components.ml index 02145b6b..af658df3 100644 --- a/common/components.ml +++ b/common/components.ml @@ -2517,6 +2517,32 @@ let (NONOVERLAPPING_TAC:tactic) = with Failure _ -> TAC_PROOF (g, SIMPLE_ARITH_TAC) in cache := th::!cache; th) in + let num_ty = `:num` + and ap_tm = `a':num` + and a1_tm = `a1:num` + and a2_tm = `a2:num` + and ai_tm = `a:int64` + and a_tm = `a:num` + and bp_tm = `b':num` + and bi_tm = `b:int64` + and b_tm = `b:num` + and i1_tm = `i1:num` + and i2_tm = `i2:num` + and mle_tm = `m <= 2 EXP 64` + and m_tm = `m:num` + and n1_tm = `n1:num` + and n2_tm = `n2:num` + and n_tm = `n:num` + and nx_tm = `nx:num` + and ny_tm = `ny:num` + and ppp_tm = `p':num#num` + and p1_tm = `p1:num#num` + and p2_tm = `p2:num#num` + and pp_tm = `p:num#num` + and p_tm = `p:num` + and x_tm = `x:int64` + and y_tm = `y:int64` in + let prove_le = let ADD_0_CONV = REWRITE_CONV [ (EQT_ELIM o REWRITE_CONV [ADD_CLAUSES]) `x + 0 = x /\ 0 + x = x`] @@ -2525,7 +2551,9 @@ let (NONOVERLAPPING_TAC:tactic) = ARITH_RULE `1 <= n <=> 0 < n`] and MULT_ASSOC4 = (EQT_ELIM o REWRITE_CONV [MULT_AC]) `(a * b) * (c * d):num = (a * c) * (b * d)` - and MULT_1 = (EQT_ELIM o REWRITE_CONV [MULT_CLAUSES]) `x = 1 * x` in + and MULT_1 = (EQT_ELIM o REWRITE_CONV [MULT_CLAUSES]) `x = 1 * x` + and mul_tm = `( * ):num->num->num` + and true_tm = `T` in let FACTOR_CONV t = let rec factor = function | Comb(Comb(Const("<=",_),t1),t2) -> gcd (factor t1) (factor t2) @@ -2549,8 +2577,8 @@ let (NONOVERLAPPING_TAC:tactic) = let i = factor t in if i = 1 then PART_MATCH lhs MULT_1 t else SYM (NUM_MULT_CONV ( - mk_comb (mk_comb (`( * ):num->num->num`, mk_numeral (Int n)), - mk_numeral (Int (i / n))))) in + mk_comb (mk_comb (mul_tm, mk_small_numeral n), + mk_small_numeral (i / n)))) in mk_theorem (factor t) t in let AFTER th k = EQ_MP (SYM th) (k (rhs (concl th))) in fun (asl:(string*thm)list) t -> @@ -2559,14 +2587,14 @@ let (NONOVERLAPPING_TAC:tactic) = (try PART_MATCH I LE_REFL t with Failure _ -> try PART_MATCH I LE_0 t with Failure _ -> AFTER (NUM_REDUCE_CONV t) (fun t -> - if t = `T` then TRUTH else + if t = true_tm then TRUTH else AFTER (FACTOR_CONV t) (fun t -> try PART_MATCH I LE_REFL t with Failure _ -> AFTER (ADD_1_LE_CONV t) (curry fallback asl)))) | _ -> failwith "prove_le") in let normalize = - let pth_num = SPECL [`a:num`; `2 EXP 64`] CONG_REFL + let pth_num = SPECL [a_tm; `2 EXP 64`] CONG_REFL and pth_int64 = prove (`(a:int64) = word (val a)`, REWRITE_TAC [WORD_VAL]) and pth_val = (UNDISCH_ALL o prove) @@ -2586,33 +2614,34 @@ let (NONOVERLAPPING_TAC:tactic) = let rec norm = function | Comb(Const("val",_),t) -> let th = norm t in - PROVE_HYP th (INST [t,`a:int64`; rand(rand(concl th)),`b:num`] pth_val) + PROVE_HYP th (INST [t,ai_tm; rand(rand(concl th)),b_tm] pth_val) | Comb(Const("word",_),t) -> let th = norm t in - PROVE_HYP th (INST [t,`a:num`; rand(rator(concl th)),`b:num`] pth_word) + PROVE_HYP th (INST [t,a_tm; rand(rator(concl th)),b_tm] pth_word) | Comb(Comb(Const("word_add",_),t1),t2) -> let th1 = norm t1 and th2 = norm t2 in (PROVE_HYP th1 o PROVE_HYP th2) - (INST [t1,`a:int64`; rand(rand(concl th1)),`a':num`; - t2,`b:int64`; rand(rand(concl th2)),`b':num`] pth_word_add) + (INST [t1,ai_tm; rand(rand(concl th1)),ap_tm; + t2,bi_tm; rand(rand(concl th2)),bp_tm] pth_word_add) | Comb(Comb(Const("+",_),t),b) -> let th = norm t in let t' = rand (rator (concl th)) in - PROVE_HYP th (INST [t,`a:num`; t',`a':num`; b,`b:num`] pth_add) - | t when type_of t = `:num` -> INST [t,`a:num`] pth_num - | t -> INST [t,`a:int64`] pth_int64 in + PROVE_HYP th (INST [t,a_tm; t',ap_tm; b,b_tm] pth_add) + | t when type_of t = num_ty -> INST [t,a_tm] pth_num + | t -> INST [t,ai_tm] pth_int64 in let pth1 = SYM (SPEC_ALL ADD_ASSOC) and pth2 = SYM (SPEC_ALL ADD_0) in let rec split_base = function | Comb(Comb(Const("+",_),Comb(Comb(Const("+",_),t1),t2)),t3) -> - CONV_RHS_RULE split_base (INST [t1,`m:num`; t2,`n:num`; t3,`p:num`] pth1) + CONV_RHS_RULE split_base (INST [t1,m_tm; t2,n_tm; t3,p_tm] pth1) | Comb(Comb(Const("+",_),_),_) as t -> REFL t - | t -> INST [t,`m:num`] pth2 in + | t -> INST [t,m_tm] pth2 in CONV_RULE (RATOR_CONV (RAND_CONV split_base)) o norm in + let is_le = is_binop `(<=):num->num->bool` in let prove_hyps f th = itlist (fun h -> - if is_binop `<=` h then PROVE_HYP (f h) else I) (hyp th) th in + if is_le h then PROVE_HYP (f h) else I) (hyp th) th in let prove_les asl = prove_hyps (prove_le asl) in let prove_contains = @@ -2636,8 +2665,8 @@ let (NONOVERLAPPING_TAC:tactic) = let th1 = normalize a1 and th2 = normalize a2 in let a,i1 = (rand F_F I) (dest_comb (rand (rator (concl th1)))) and i2 = rand (rand (rator (concl th2))) in - let th = INST [a,`a:num`; a1,`a1:num`; a2,`a2:num`; - i1,`i1:num`; i2,`i2:num`; n1,`n1:num`; n2,`n2:num`] pth in + let th = INST [a,a_tm; a1,a1_tm; a2,a2_tm; + i1,i1_tm; i2,i2_tm; n1,n1_tm; n2,n2_tm] pth in PROVE_HYP th1 (PROVE_HYP th2 (prove_les asl th)) in let base = @@ -2738,7 +2767,7 @@ let (NONOVERLAPPING_TAC:tactic) = with Failure _ -> failwith "NONOVERLAPPING_TAC: cmp" in let LE_TRANS' = UNDISCH_ALL (REWRITE_RULE [IMP_CONJ] - (SPECL [`m:num`; `n:num`; `2 EXP 64`] LE_TRANS)) + (SPECL [m_tm; n_tm; `2 EXP 64`] LE_TRANS)) and DISJ_NONOVERLAPPING_MODULO_SYM = MESON [NONOVERLAPPING_MODULO_SYM] `x = y \/ nonoverlapping_modulo n (val x,k) (val y,l) <=> y = x \/ nonoverlapping_modulo n (val y,l) (val x,k)` in @@ -2752,8 +2781,8 @@ let (NONOVERLAPPING_TAC:tactic) = let th = if b1 = b2 then let th1 = normalize e1 and th2 = normalize e2 in let i1,i2 = W f_f_ (rand o rand o rator o concl) (th1,th2) in - let th = INST [e1,`a1:num`; e2,`a2:num`; i1,`i1:num`; i2,`i2:num`; - n1,`n1:num`; n2,`n2:num`; b1,`a:num`] + let th = INST [e1,a1_tm; e2,a2_tm; i1,i1_tm; i2,i2_tm; + n1,n1_tm; n2,n2_tm; b1,a_tm] (if cmp i1 i2 then pth_lt else pth_gt) in let f h = try let n = tryfind (fun _,h -> @@ -2763,8 +2792,8 @@ let (NONOVERLAPPING_TAC:tactic) = if base e1' = b1 then n1' else if base e2' = b1 then n2' else fail () | _ -> fail ()) asl - and _,ls,_ = term_match [] `m <= 2 EXP 64` h in - prove_les asl (INST ((n,`n:num`)::ls) LE_TRANS') + and _,ls,_ = term_match [] mle_tm h in + prove_les asl (INST ((n,n_tm)::ls) LE_TRANS') with Failure _ -> prove_le asl h in PROVE_HYP th1 (PROVE_HYP th2 (prove_hyps f th)) else @@ -2793,9 +2822,9 @@ let (NONOVERLAPPING_TAC:tactic) = dest_comb o rand o rator o concl) (th1,th2) in if i1 = i2 then failwith "NONOVERLAPPING_TAC: same offset" else let nx,ny = (rand o rand F_F rand) (dest_comb (rand (concl h))) in - let f = prove_les asl o INST [e1,`a1:num`; e2,`a2:num`; - i1,`i1:num`; i2,`i2:num`; n1,`n1:num`; n2,`n2:num`; - nx,`nx:num`; ny,`ny:num`; x,`x:int64`; y,`y:int64`] in + let f = prove_les asl o INST [e1,a1_tm; e2,a2_tm; + i1,i1_tm; i2,i2_tm; n1,n1_tm; n2,n2_tm; + nx,nx_tm; ny,ny_tm; x,x_tm; y,y_tm] in let th = if cmp i1 i2 then try f dth_lt with Failure _ -> f dth_lt2 else try f dth_gt with Failure _ -> f dth_gt2 in @@ -2804,15 +2833,15 @@ let (NONOVERLAPPING_TAC:tactic) = let h = let p1' = lhand (concl h) in if p1 = p1' then h else - let th = INST [p1',`p:num#num`; p1,`p':num#num`; - rand (concl h),`p2:num#num`] pth_l in + let th = INST [p1',pp_tm; p1,ppp_tm; + rand (concl h),p2_tm] pth_l in let th = PROVE_HYP h th in PROVE_HYP (prove_contains asl p1 p1') th in let h = let p2' = rand (concl h) in if p2 = p2' then h else - let th = INST [p2',`p:num#num`; p2,`p':num#num`; - lhand (concl h),`p1:num#num`] pth_r in + let th = INST [p2',pp_tm; p2,ppp_tm; + lhand (concl h),p1_tm] pth_r in let th = PROVE_HYP h th in PROVE_HYP (prove_contains asl p2 p2') th in h in diff --git a/x86/proofs/bignum_add_p25519.ml b/x86/proofs/bignum_add_p25519.ml index 05f5ad13..36bedfcd 100644 --- a/x86/proofs/bignum_add_p25519.ml +++ b/x86/proofs/bignum_add_p25519.ml @@ -58,7 +58,7 @@ let BIGNUM_ADD_P25519_EXEC = X86_MK_CORE_EXEC_RULE bignum_add_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let BIGNUM_ADD_P25519_CORRECT = time prove (`!z x y m n pc. @@ -130,7 +130,7 @@ let BIGNUM_ADD_P25519_CORRECT = time prove REWRITE_TAC[GSYM NOT_LE; COND_SWAP] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[p_25519] THEN MATCH_MP_TAC(ARITH_RULE - `l + 2 EXP 255 = m + n + 19 ==> l = (m + n) - (2 EXP 255 - 19)`) THEN + `l + 2 EXP 255 = m + n + 19 ==> l = (m + n) - (57896044618658097711785492504343953926634992332820282019728792003956564819949)`) THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN REWRITE_TAC[bignum_of_wordlist; LEFT_ADD_DISTRIB; GSYM ADD_ASSOC] THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN REPEAT AP_TERM_TAC THEN diff --git a/x86/proofs/bignum_cmul_p25519.ml b/x86/proofs/bignum_cmul_p25519.ml index c2363523..fe09fba7 100644 --- a/x86/proofs/bignum_cmul_p25519.ml +++ b/x86/proofs/bignum_cmul_p25519.ml @@ -69,7 +69,7 @@ let BIGNUM_CMUL_P25519_EXEC = X86_MK_CORE_EXEC_RULE bignum_cmul_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/x86/proofs/bignum_cmul_p25519_alt.ml b/x86/proofs/bignum_cmul_p25519_alt.ml index 942f8958..ca6416be 100644 --- a/x86/proofs/bignum_cmul_p25519_alt.ml +++ b/x86/proofs/bignum_cmul_p25519_alt.ml @@ -74,7 +74,7 @@ let BIGNUM_CMUL_P25519_ALT_EXEC = X86_MK_CORE_EXEC_RULE bignum_cmul_p25519_alt_m (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/x86/proofs/bignum_mul_p25519.ml b/x86/proofs/bignum_mul_p25519.ml index c1b05993..92aae4d3 100644 --- a/x86/proofs/bignum_mul_p25519.ml +++ b/x86/proofs/bignum_mul_p25519.ml @@ -198,7 +198,7 @@ let BIGNUM_MUL_P25519_EXEC = X86_MK_CORE_EXEC_RULE bignum_mul_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/x86/proofs/bignum_mul_p25519_alt.ml b/x86/proofs/bignum_mul_p25519_alt.ml index f3899cf6..7b7586f6 100644 --- a/x86/proofs/bignum_mul_p25519_alt.ml +++ b/x86/proofs/bignum_mul_p25519_alt.ml @@ -176,7 +176,7 @@ let BIGNUM_MUL_P25519_ALT_EXEC = X86_MK_CORE_EXEC_RULE bignum_mul_p25519_alt_mc; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/x86/proofs/bignum_neg_p25519.ml b/x86/proofs/bignum_neg_p25519.ml index cb2cb651..83a7beb6 100644 --- a/x86/proofs/bignum_neg_p25519.ml +++ b/x86/proofs/bignum_neg_p25519.ml @@ -56,7 +56,7 @@ let BIGNUM_NEG_P25519_EXEC = X86_MK_CORE_EXEC_RULE bignum_neg_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let BIGNUM_NEG_P25519_CORRECT = time prove (`!z x n pc. diff --git a/x86/proofs/bignum_sqr_p25519.ml b/x86/proofs/bignum_sqr_p25519.ml index ad586435..8e97c26d 100644 --- a/x86/proofs/bignum_sqr_p25519.ml +++ b/x86/proofs/bignum_sqr_p25519.ml @@ -167,7 +167,7 @@ let BIGNUM_SQR_P25519_EXEC = X86_MK_CORE_EXEC_RULE bignum_sqr_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/x86/proofs/bignum_sqr_p25519_alt.ml b/x86/proofs/bignum_sqr_p25519_alt.ml index 62021a47..b75b6668 100644 --- a/x86/proofs/bignum_sqr_p25519_alt.ml +++ b/x86/proofs/bignum_sqr_p25519_alt.ml @@ -164,7 +164,7 @@ let BIGNUM_SQR_P25519_ALT_EXEC = X86_MK_CORE_EXEC_RULE bignum_sqr_p25519_alt_mc; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let p25519redlemma = prove (`!n. n <= (2 EXP 64 - 1) * (p_25519 - 1) diff --git a/x86/proofs/bignum_sub_p25519.ml b/x86/proofs/bignum_sub_p25519.ml index fe3ee342..0319d20e 100644 --- a/x86/proofs/bignum_sub_p25519.ml +++ b/x86/proofs/bignum_sub_p25519.ml @@ -52,7 +52,7 @@ let BIGNUM_SUB_P25519_EXEC = X86_MK_CORE_EXEC_RULE bignum_sub_p25519_mc;; (* Proof. *) (* ------------------------------------------------------------------------- *) -let p_25519 = new_definition `p_25519 = 2 EXP 255 - 19`;; +let p_25519 = new_definition `p_25519 = 57896044618658097711785492504343953926634992332820282019728792003956564819949`;; let BIGNUM_SUB_P25519_CORRECT = time prove (`!z x y m n pc. diff --git a/x86/proofs/instruction.ml b/x86/proofs/instruction.ml index 7e7d6b83..21bfd830 100644 --- a/x86/proofs/instruction.ml +++ b/x86/proofs/instruction.ml @@ -171,14 +171,14 @@ and zmm31 = define `zmm31 = Simdreg (word 31) Full_512`;; let opmaskreg_INDUCT,opmaskreg_RECURSION = define_type "opmaskreg = Opmaskreg (3 word)";; -let k0 = define `k0 = Opmaskreg (word 0)`;; -let k1 = define `k1 = Opmaskreg (word 1)`;; -let k2 = define `k2 = Opmaskreg (word 2)`;; -let k3 = define `k3 = Opmaskreg (word 3)`;; -let k4 = define `k4 = Opmaskreg (word 4)`;; -let k5 = define `k5 = Opmaskreg (word 5)`;; -let k6 = define `k6 = Opmaskreg (word 6)`;; -let k7 = define `k7 = Opmaskreg (word 7)`;; +let kmask0 = define `kmask0 = Opmaskreg (word 0)`;; +let kmask1 = define `kmask1 = Opmaskreg (word 1)`;; +let kmask2 = define `kmask2 = Opmaskreg (word 2)`;; +let kmask3 = define `kmask3 = Opmaskreg (word 3)`;; +let kmask4 = define `kmask4 = Opmaskreg (word 4)`;; +let kmask5 = define `kmask5 = Opmaskreg (word 5)`;; +let kmask6 = define `kmask6 = Opmaskreg (word 6)`;; +let kmask7 = define `kmask7 = Opmaskreg (word 7)`;; (* ------------------------------------------------------------------------- *) (* Condition codes for conditional operations. *) diff --git a/x86/proofs/x86.ml b/x86/proofs/x86.ml index 5fcdfa0e..1a506fa8 100644 --- a/x86/proofs/x86.ml +++ b/x86/proofs/x86.ml @@ -2537,6 +2537,16 @@ let (X86_BIGSTEP_TAC:thm->string->tactic) = (* Simulate a subroutine, instantiating it from the state. *) (* ------------------------------------------------------------------------- *) +let TWEAK_PC_OFFSET = + let conv = + GEN_REWRITE_CONV (RAND_CONV o RAND_CONV) [ARITH_RULE `pc = pc + 0`] + and tweakneeded tm = + match tm with + Comb(Comb(Const("bytes_loaded",_),Var(_,_)), + Comb(Const("word",_),Var("pc",_))) -> true + | _ -> false in + CONV_RULE(ONCE_DEPTH_CONV(conv o check tweakneeded));; + let X86_SUBROUTINE_SIM_TAC (machinecode,execth,offset,submachinecode,subth) = let subimpth = CONV_RULE NUM_REDUCE_CONV (REWRITE_RULE [LENGTH] @@ -2549,7 +2559,7 @@ let X86_SUBROUTINE_SIM_TAC (machinecode,execth,offset,submachinecode,subth) = let svar = mk_var(sname,`:x86state`) and svar0 = mk_var("s",`:x86state`) in let ilist = map (vsubst[svar,svar0]) ilist0 in - MP_TAC(SPECL ilist subth) THEN + MP_TAC(TWEAK_PC_OFFSET(SPECL ilist subth)) THEN ASM_REWRITE_TAC[C_ARGUMENTS; C_RETURN; SOME_FLAGS] THEN REWRITE_TAC[ALLPAIRS; ALL; PAIRWISE; NONOVERLAPPING_CLAUSES] THEN ANTS_TAC THENL @@ -2574,6 +2584,84 @@ let X86_SUBROUTINE_SIM_ABBREV_TAC tupper ilist0 = (tac n THEN ABBREV_TAC(mk_eq(mk_var(abn,type_of comp1),comp1))) (asl,w);; +(* ------------------------------------------------------------------------- *) +(* Simulate a macro, generating subgoal from a template *) +(* ------------------------------------------------------------------------- *) + +let X86_MACRO_SIM_ABBREV_TAC = + let dest_pc tm = + match tm with + Comb(Const("word",_),Var("pc",_)) -> 0 + | Comb(Const("word",_),Comb(Comb(Const("+",_),Var("pc",_)),n)) -> + dest_small_numeral n + | _ -> failwith "dest_pc" + and mk_pc = + let pat0 = `word pc:int64` + and patn = `word(pc + n):int64` + and pan = `n:num` in + fun n -> if n = 0 then pat0 + else vsubst[mk_small_numeral n,pan] patn + and grab_dest = + let pat = `read (memory :> bytes(p,8 * n))` in + fun th -> + let cortm = rand(body(lhand(repeat (snd o dest_imp) (concl th)))) in + hd(find_terms (can (term_match [] pat)) cortm) + and extract_offsets = + let rec exfn p acc l = + match l with + [] -> rev (p::acc) + | (n,_)::t -> exfn (p+n) (p::acc) t in + fun mc -> exfn 0 [] (decode_all(rand(concl mc))) in + let rec skip_to_offset p offl = + match offl with + [] -> failwith "skip_to_offset" + | (n::t) -> if n > p then failwith "skip_to_offset" + else if n = p then offl + else skip_to_offset p t in + let get_statenpc = + let fils = can (term_match [] `read RIP s = word n`) o concl o snd in + fun asl -> + let rips = concl(snd(find fils asl)) in + rand(lhand rips),dest_pc(rand rips) in + let simprule = + CONV_RULE (ONCE_DEPTH_CONV NORMALIZE_ADD_SUBTRACT_WORD_CONV) o + GEN_REWRITE_RULE ONCE_DEPTH_CONV + [WORD_RULE `word_add z (word 0):int64 = z`] in + fun mc -> + let offl = extract_offsets mc in + let execth = X86_MK_EXEC_RULE mc in + fun codelen localvars template core_tac prep ilist -> + let main_tac (asl,w) = + let svp,pc = get_statenpc asl in + let gv = genvar(type_of svp) in + let n = int_of_string(implode(tl(explode(fst(dest_var svp))))) + 1 in + let svn = mk_var("s"^string_of_int n,`:x86state`) in + let pc' = hd(snd(chop_list codelen (skip_to_offset pc offl))) in + let svs = svp::(mk_pc pc)::(mk_pc pc'):: + end_itlist (@) (map (C assoc localvars) ilist) in + let rawsg = simprule(SPECL svs (ASSUME template)) in + let insig = PURE_REWRITE_RULE + (filter (is_eq o concl) (map snd asl)) rawsg in + let subg = mk_forall(gv,vsubst[gv,svp] (concl(simprule insig))) in + let avoids = itlist (union o thm_frees o snd) asl (frees w) in + let abv = mk_primed_var avoids (mk_var(hd ilist,`:num`)) in + (SUBGOAL_THEN subg MP_TAC THENL + [X_GEN_TAC gv THEN POP_ASSUM_LIST(K ALL_TAC) THEN + REPEAT(GEN_TAC THEN DISCH_THEN(K ALL_TAC o SYM)) THEN + core_tac THEN NO_TAC; + ALL_TAC] THEN + DISCH_THEN(MP_TAC o SPEC svp) THEN + GEN_REWRITE_TAC (REPEATC o LAND_CONV) [FORALL_UNWIND_THM1] THEN + DISCH_THEN(fun subth -> + let dest = grab_dest subth in + X86_SUBROUTINE_SIM_TAC(mc,execth,0,mc,subth) [] n THEN + ABBREV_TAC (mk_eq(abv,mk_comb(dest,svn))))) + (asl,w) in + fun (asl,w) -> + let sv,_ = get_statenpc asl in + let n = int_of_string(implode(tl(explode(fst(dest_var sv))))) in + (X86_STEPS_TAC execth ((n+1)--(n+prep)) THEN main_tac) (asl,w);; + (* ------------------------------------------------------------------------- *) (* Fix up call/return boilerplate given core correctness. *) (* ------------------------------------------------------------------------- *)