Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Lenngren-based X25519 for non-alt ARM code #108

Merged
merged 4 commits into from
Feb 15, 2024
Merged

Lenngren-based X25519 for non-alt ARM code #108

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
d0d5219
Specify the behavior of bignum_inv_p25519 in degenerate cases
jargh Feb 8, 2024
b2e7f4c
Refine ARM ABI specifications for Q8-Q15
jargh Feb 8, 2024
fc0b9bf
Switch non-alt ARM X25519 to unsaturated code following Lenngren
jargh Feb 9, 2024
f82da8f
Tweak attribution of SLOTHY work
jargh Feb 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2,312 changes: 1,487 additions & 825 deletions arm/curve25519/curve25519_x25519.S
View file
Open in desktop

Large diffs are not rendered by default.

2,440 changes: 1,552 additions & 888 deletions arm/curve25519/curve25519_x25519_byte.S
View file
Open in desktop

Large diffs are not rendered by default.

57 changes: 53 additions & 4 deletions arm/proofs/arm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,7 @@ let ARM_EXEC_CONV =
ONCE_DEPTH_CONV(EQT_INTRO o ORTHOGONAL_COMPONENTS_CONV) THENC
REWRITE_CONV[] THENC
ONCE_DEPTH_CONV(LAND_CONV DIMINDEX_CONV THENC NUM_DIV_CONV) THENC
GEN_REWRITE_CONV ONCE_DEPTH_CONV [GSYM BYTES64_WBYTES;
GEN_REWRITE_CONV ONCE_DEPTH_CONV [GSYM BYTES32_WBYTES; GSYM BYTES64_WBYTES;
GSYM BYTES128_WBYTES] THENC
GEN_REWRITE_CONV ONCE_DEPTH_CONV [qth] THENC
GEN_REWRITE_CONV ONCE_DEPTH_CONV [rth] THENC
Expand Down Expand Up @@ -713,6 +713,52 @@ let ARM_MACRO_SIM_ABBREV_TAC =
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);;

(* ------------------------------------------------------------------------- *)
(* Refinment of ENSURES_PRESERVED_TAC for special D register handling. *)
(* ------------------------------------------------------------------------- *)

let ENSURES_PRESERVED_DREG_TAC =
let pth = prove
(`read (Q8 :> bottomhalf) s = word_zx(read Q8 s) /\
read (Q9 :> bottomhalf) s = word_zx (read Q9 s) /\
read (Q10 :> bottomhalf) s = word_zx (read Q10 s) /\
read (Q11 :> bottomhalf) s = word_zx (read Q11 s) /\
read (Q12 :> bottomhalf) s = word_zx (read Q12 s) /\
read (Q13 :> bottomhalf) s = word_zx (read Q13 s) /\
read (Q14 :> bottomhalf) s = word_zx (read Q14 s) /\
read (Q15 :> bottomhalf) s = word_zx (read Q15 s)`,
CONV_TAC(ONCE_DEPTH_CONV COMPONENT_CANON_CONV) THEN
REWRITE_TAC[READ_COMPONENT_COMPOSE; READ_ZEROTOP_64;
bottomhalf; subword; read; FUN_EQ_THM] THEN
REWRITE_TAC[word_zx; DIV_1; EXP; WORD_MOD_SIZE])
and sth = prove
(`valid_component c /\
R ,, R = R /\
MAYCHANGE [c :> tophalf] subsumed R /\
ensures step P Q (R ,, MAYCHANGE [c])
==> ensures step P Q (R ,, MAYCHANGE [c :> bottomhalf])`,
REWRITE_TAC[MAYCHANGE_SING] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] ENSURES_FRAME_SUBSUMED) THEN
FIRST_ASSUM(fun th ->
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM th]) THEN
REWRITE_TAC[GSYM SEQ_ASSOC] THEN MATCH_MP_TAC SUBSUMED_SEQ THEN
REWRITE_TAC[SUBSUMED_REFL] THEN
FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP ASSIGNS_TOPHALF_BOTTOMHALF) THEN
MATCH_MP_TAC SUBSUMED_SEQ THEN ASM_REWRITE_TAC[SUBSUMED_REFL]) in
let alist = zip [`D8`; `D9`; `D10`; `D11`; `D12`; `D13`; `D14`; `D15`]
(map (lhand o lhand o concl) (CONJUNCTS pth)) in
let dregs = map fst alist in
fun pname ctm ->
if not (mem ctm dregs) then ENSURES_PRESERVED_TAC pname ctm else
let ctm' = assoc ctm alist in
ENSURES_PRESERVED_TAC pname ctm' THEN REWRITE_TAC[pth] THEN
TRY(REWRITE_TAC[SEQ_ASSOC] THEN MATCH_MP_TAC sth THEN
CONJ_TAC THENL [CONV_TAC VALID_COMPONENT_CONV; ALL_TAC] THEN
CONJ_TAC THENL [MAYCHANGE_IDEMPOT_TAC; ALL_TAC] THEN
CONJ_TAC THENL [SUBSUMED_MAYCHANGE_TAC THEN NO_TAC; ALL_TAC] THEN
REWRITE_TAC[GSYM SEQ_ASSOC]);;

(* ------------------------------------------------------------------------- *)
(* Fix up call/return boilerplate given core correctness. *)
(* ------------------------------------------------------------------------- *)
Expand Down Expand Up @@ -797,7 +843,8 @@ let ARM_ADD_RETURN_NOSTACK_TAC =
let ARM_ADD_RETURN_STACK_TAC =
let mono2lemma = MESON[]
`(!x. (!y. P x y) ==> (!y. Q x y)) ==> (!x y. P x y) ==> (!x y. Q x y)`
and sp_tm = `SP` and x30_tm = `X30` in
and sp_tm = `SP` and x30_tm = `X30`
and dqd_thm = WORD_BLAST `(word_zx:int128->int64)(word_zx(x:int64)) = x` in
fun execth coreth reglist stackoff ->
let regs = dest_list reglist in
let n = let n0 = length regs / 2 in
Expand Down Expand Up @@ -827,15 +874,17 @@ let ARM_ADD_RETURN_STACK_TAC =
ENSURES_EXISTING_PRESERVED_TAC sp_tm THEN
(if mem x30_tm regs then ENSURES_EXISTING_PRESERVED_TAC x30_tm
else ALL_TAC) THEN
MAP_EVERY (fun c -> ENSURES_PRESERVED_TAC ("init_"^fst(dest_const c)) c)
MAP_EVERY (fun c -> ENSURES_PRESERVED_DREG_TAC
("init_"^fst(dest_const c)) c)
(subtract regs [x30_tm]) THEN
REWRITE_TAC(!simulation_precanon_thms) THEN ENSURES_INIT_TAC "s0" THEN
ARM_STEPS_TAC execth (1--n) THEN
MP_TAC th) THEN
ARM_BIGSTEP_TAC execth ("s"^string_of_int(n+1)) THEN
REWRITE_TAC(!simulation_precanon_thms) THEN
ARM_STEPS_TAC execth ((n+2)--(2*n+2)) THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[];;
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[dqd_thm];;

(* ------------------------------------------------------------------------- *)
(* Handling more general branch targets *)
Expand Down
Loading