From 641f7eb4c946aa2a89fe60e12bfba5e7dd580cf9 Mon Sep 17 00:00:00 2001 From: Jake Massimo Date: Tue, 18 Aug 2026 17:09:53 +0000 Subject: [PATCH] Add aarch64 constant-time (f_events) proof for rej_uniform_eta2 Signed-off-by: Jake Massimo --- .../mldsa_rej_uniform_eta2_aarch64_asm.ml | 1703 +++++++++++++++++ 1 file changed, 1703 insertions(+) diff --git a/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2_aarch64_asm.ml b/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2_aarch64_asm.ml index a559e52f04..3724ec1df3 100644 --- a/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2_aarch64_asm.ml +++ b/proofs/hol_light/aarch64/proofs/mldsa_rej_uniform_eta2_aarch64_asm.ml @@ -3201,3 +3201,1706 @@ let MLDSA_REJ_UNIFORM_ETA2_SUBROUTINE_MEMSAFE = time prove (CONV_RULE LENGTH_SIMPLIFY_CONV MLDSA_REJ_UNIFORM_ETA2_MEMSAFE)) `[]:int64 list` 576 THEN DISCHARGE_MEMSAFE_TAC);; + +(* ========================================================================= *) +(* Secret-independent-timing (constant-time) proof for *) +(* rej_uniform_eta2_aarch64_asm -- pq-code-package/mldsa-native issue #1160. *) +(* Adds the f_events clause (MLDSA_REJ_UNIFORM_ETA2_SUBROUTINE_SAFE) on top of *) +(* the functional-correctness + memory-safety theorems above. *) +(* ========================================================================= *) + +(* ------------------------------------------------------------------------- *) +(* THE SECURITY PROPERTY (leakage-up-to-the-reject-mask, NOT obliviousness). *) +(* *) +(* rej_uniform_eta2 produces the SECRET eta coefficients (part of s1/s2), so *) +(* its microarchitectural event trace must be independent of the secret *) +(* *values*. It is however variable-time: the trace legitimately depends on *) +(* WHICH candidate nibbles are accepted vs. rejected (the reject decision is *) +(* public — a statistically-independent function of the public XOF stream, *) +(* Round3 spec §5.5). So we prove leakage-up-to-the-reject-mask: the trace is *) +(* a function of the public pointers PLUS the per-nibble accept/reject mask, *) +(* and NOTHING else about the input (in particular, not the accepted values). *) +(* *) +(* This is exactly the upstream TODO in rej_uniform_eta2_aarch64_asm.ml: *) +(* "the event-generating function should take the set of in-bound indices *) +(* as an argument, but not the entire input data. This corresponds to *) +(* declassifying WHICH coefficients are in bounds vs out of bounds, but *) +(* not their values." *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* WHY THE VANILLA mk_safety_spec DOES NOT WORK HERE. *) +(* *) +(* gen_mk_safety_spec (s2n-bignum common/consttime.ml:135-148) derives *) +(* f_events' public arguments as ONLY the base pointers + size vars of the *) +(* mem-in/out/temp buffers, plus pc, the stack base pointer, and *) +(* returnaddress. For eta2 that is [res; buf; buflen; table; pc; *) +(* stackpointer; returnaddress] — the buffer CONTENTS are absent. The *) +(* resulting spec would assert e2 = f_events , i.e. FULL *) +(* data-obliviousness. That is FALSE for a rejection sampler: two inputs with *) +(* the same pointers but different reject patterns emit different traces *) +(* (different table-lookup addresses table+mask*16, different store *) +(* advances). No such data-dependent f_events precedent exists anywhere in *) +(* s2n-bignum (grep for f_events taking a list/mask arg = 0 hits), so this *) +(* spec is HAND-WRITTEN, adding the reject mask as an extra public argument. *) +(* ------------------------------------------------------------------------- *) + +(* ------------------------------------------------------------------------- *) +(* WHERE THE DATA-DEPENDENCE LIVES (from the .S, lines 54-91, loop8). *) +(* *) +(* prologue (sub sp,#0x240) + Lrej_uniform_eta2_initial_zero (8 iters): *) +(* zero the 512-byte stack scratch. FIXED trip count. PUBLIC. *) +(* Lrej_uniform_eta2_loop8 (the sampler, DATA-DEPENDENT): *) +(* ld1 {v0.8b},[x1],#8 read buf+8*i (addr FIXED) *) +(* cmhi v4,v30,v16 ; and v31 ; uaddlv -> w12 = 8-bit accept mask hi *) +(* cmhi v5 ... ; uaddlv -> w13 = 8-bit accept mask lo *) +(* ldr q24,[x3,x12,lsl#4] read table+mask1*16 (addr = mask1) *) +(* ldr q25,[x3,x13,lsl#4] read table+mask2*16 (addr = mask2) *) +(* cnt/uaddlv -> popcounts; tbl (compact); st1 [x7]; add x7,popcnt*2 *) +(* st1 {v16.8h},[x7] ; st1 {v17.8h},[x7] writes sp+2*ctr (addr = ctr) *) +(* add x9,ctr ; cmp x2,#8 ; b.hs loop8 trip count = f(mask,buflen)*) +(* Lrej_uniform_eta2_final_copy (16 iters): *) +(* Barrett reduce scratch -> centered eta; store to res. FIXED. PUBLIC. *) +(* *) +(* => The ONLY secret-dependent addresses/branches are: table+mask*16 reads, *) +(* sp+2*ctr stores, and the loop8 trip count. All three are functions of *) +(* the per-8-nibble accept masks (ctr = prefix popcount of the masks) and *) +(* the public buflen. Nothing depends on the accepted VALUES. *) +(* ------------------------------------------------------------------------- *) + +(* The public reject-mask projection: one accept/reject bit per nibble, with *) +(* the accepted values DISCARDED. Mirrors REJ_NIBBLES_ETA2 (which FILTERs the *) +(* same predicate to keep the accepted values = the SECRET); here we MAP the *) +(* predicate to keep only the decisions. From this bool list one recovers the *) +(* per-group 8-bit masks (pack 8 bits), the accepted counts (popcounts), and *) +(* hence every secret-dependent address/branch above — but not the values. *) +(* *) +(* NOTE: REJ_NIBBLES_ETA2 l = FILTER (\x. val x < 15) (NIBBLES_OF_BYTES l) *) +(* so LENGTH(REJ_NIBBLES_ETA2 l) = number of `true` in REJ_MASK_ETA2 l. *) +(* REJ_NIBBLES_ETA2 is NOT recoverable from REJ_MASK_ETA2 alone (the *) +(* accepted values are gone) — that is the whole point. *) + +let REJ_MASK_ETA2 = define + `REJ_MASK_ETA2 (l:byte list) : bool list = + MAP (\x:int16. val x < 15) (NIBBLES_OF_BYTES l)`;; + +(* ========================================================================= *) +(* *) +(* These are the "store-advance / trip-count" half of the mask bridge (the *) +(* and independently of the assembly (pure list facts). They express the *) +(* SECRET accepted-count (which drives niblen, every stack-store offset *) +(* sp+2*niblen, and the loop trip count) as a function of the PUBLIC reject *) +(* mask only — the accepted VALUES never appear. Migrate together with the *) +(* SUBROUTINE_SAFE theorem when the proof is closed. *) +(* ========================================================================= *) + +(* Abstract core: #elements passing P = #`true`s in the boolean image. *) +let LENGTH_FILTER_EQ_LENGTH_FILTER_MAP = prove + (`!(P:A->bool) xs. + LENGTH(FILTER (\b:bool. b) (MAP P xs)) = LENGTH(FILTER P xs)`, + GEN_TAC THEN LIST_INDUCT_TAC THEN + REWRITE_TAC[MAP; FILTER; LENGTH] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH]);; + +(* Reject mask distributes over APPEND (so a prefix mask composes cleanly; + mirrors REJ_NIBBLES_ETA2_APPEND for the value-free projection). *) +let REJ_MASK_ETA2_APPEND = prove + (`!l1 l2. REJ_MASK_ETA2(APPEND l1 l2) = + APPEND (REJ_MASK_ETA2 l1) (REJ_MASK_ETA2 l2)`, + REWRITE_TAC[REJ_MASK_ETA2; NIBBLES_OF_BYTES_APPEND; MAP_APPEND]);; + +(* THE store-advance / trip-count bridge: the number of ACCEPTED nibbles + (= niblen, driving all sp+2*niblen store offsets and the WOP trip count N) + equals the number of `true`s in the PUBLIC reject mask. Value-free: the RHS + mentions only REJ_MASK_ETA2 (public), never the accepted values. *) +let LENGTH_REJ_NIBBLES_ETA2_EQ_MASK = prove + (`!l:byte list. + LENGTH(REJ_NIBBLES_ETA2 l) = LENGTH(FILTER (\b:bool. b) (REJ_MASK_ETA2 l))`, + REWRITE_TAC[REJ_NIBBLES_ETA2; REJ_MASK_ETA2; + LENGTH_FILTER_EQ_LENGTH_FILTER_MAP]);; + +(* A clean public "accepted count" over a mask, additive over APPEND — the + form the f_events per-iteration store-offset witness will use. *) +let NUM_ACCEPTED = define + `NUM_ACCEPTED (m:bool list) = LENGTH(FILTER (\b:bool. b) m)`;; + +let NUM_ACCEPTED_APPEND = prove + (`!m1 m2. NUM_ACCEPTED(APPEND m1 m2) = NUM_ACCEPTED m1 + NUM_ACCEPTED m2`, + REWRITE_TAC[NUM_ACCEPTED; FILTER_APPEND; LENGTH_APPEND]);; + +(* Public table-index witness: the 8-bit LSB-first packing of an accept-mask + group. The compaction table (mldsa_rej_uniform_eta_table) is indexed by this + 0..255 value, so the loop's data-dependent table read decodes to + EventLoad (table + 16 * PACK_MASK8 ) — a function of the PUBLIC + mask only. Explicit 8-EL form (not nsum) to match the eventual hardware + value-bridge, whose shape mirrors UADDLV_COUNT_LEMMA (8 explicit bits). *) +let PACK_MASK8 = define + `PACK_MASK8 (bs:bool list) = + bitval(EL 0 bs) + 2 * bitval(EL 1 bs) + + 4 * bitval(EL 2 bs) + 8 * bitval(EL 3 bs) + + 16 * bitval(EL 4 bs) + 32 * bitval(EL 5 bs) + + 64 * bitval(EL 6 bs) + 128 * bitval(EL 7 bs)`;; + +let PACK_MASK8_BOUND = prove + (`!bs:bool list. PACK_MASK8 bs < 256`, + GEN_TAC THEN REWRITE_TAC[PACK_MASK8] THEN + MAP_EVERY (fun t -> MP_TAC(SPEC t BITVAL_BOUND)) + [`EL 0 (bs:bool list)`; `EL 1 (bs:bool list)`; `EL 2 (bs:bool list)`; + `EL 3 (bs:bool list)`; `EL 4 (bs:bool list)`; `EL 5 (bs:bool list)`; + `EL 6 (bs:bool list)`; `EL 7 (bs:bool list)`] THEN + ARITH_TAC);; + +(* ------------------------------------------------------------------------- *) +(* *) +(* table index; it drives the data-dependent table read *) +(* LDR Q24,[X3,X12,LSL#4] = EventLoad(table + 16 * val(idx0)). *) +(* idx0 = FMOV(UADDLV(AND(CMHI(Q30=15-per-lane, nibbles),Q31=[1;2;4;..;128]))) *) +(* i.e. the WEIGHTED 8-bit pack of the per-nibble accept mask (NOT popcount; *) +(* the eta2.ml:2744 "popcount-accumulator" comment is stale — the real bound *) +(* proof at 2754-2774 uses SUM_8_BIT_BOUND_POLY with weights <=128, val<256). *) +(* with the 8 per-nibble accept predicates (val nibble_k < 15) ABSTRACTED to *) +(* booleans b0..b7. Lane layout (from the word_join tree): b0 = highest lane = *) +(* weight 128, ..., b7 = lowest lane = weight 1. *) +(* *) +(* PACK companion to UADDLV_COUNT_LEMMA (aarch64_utils.ml:534, the POPCOUNT *) +(* used for the X9/X7 store advance). Proven UADDLV_COUNT_LEMMA-style: REPEAT *) +(* NUM_REDUCE_CONV (256 concrete cases, ~84s). *) +(* *) +(* SECRET-INDEPENDENCE LINK: in nibble order the accept bits b0..b7 of a *) +(* 4-byte group = REJ_MASK_ETA2 of that group, and 128*b0+64*b1+..+bitval b7 = *) +(* PACK_MASK8 (that group's mask) [PACK_MASK8 above]. So val(idx0) — hence the *) +(* table-read address table+16*val(idx0) — is a function of the PUBLIC reject *) +(* the 2nd 4 bytes; the same lemma applies.) *) +(* *) +(* NOTE(#1160): the LHS below is machine-generated (round-trip parse verified *) +(* pre-WORD_SUBWORD_AND uaddlv form; consider distributing WORD_SUBWORD_AND to *) +(* a per-lane form (as MEMSAFE does at eta2.ml:2578 for the popcount) before *) +(* migrating to canonical rej_uniform_eta2_aarch64_asm.ml. *) +(* ------------------------------------------------------------------------- *) + +let UADDLV_PACK_LEMMA = prove + (`!b0 b1 b2 b3 b4 b5 b6 b7. + (val (word_zx (word_subword ((word_add (word_subword ((word_and (word 664619068533544770747334646890102785:(128)word)) (word_join (word_join (word_join (word_neg (word (bitval b0):(16)word)) (word_neg (word (bitval b1):(16)word)):(32)word) (word_join (word_neg (word (bitval b2):(16)word)) (word_neg (word (bitval b3):(16)word)):(32)word):(64)word) (word_join (word_join (word_neg (word (bitval b4):(16)word)) (word_neg (word (bitval b5):(16)word)):(32)word) (word_join (word_neg (word (bitval b6):(16)word)) (word_neg (word (bitval b7):(16)word)):(32)word):(64)word):(128)word)) (0,16):(128)word)) ((word_add (word_subword ((word_and (word 664619068533544770747334646890102785:(128)word)) (word_join (word_join (word_join (word_neg (word (bitval b0):(16)word)) (word_neg (word (bitval b1):(16)word)):(32)word) (word_join (word_neg (word (bitval b2):(16)word)) (word_neg (word (bitval b3):(16)word)):(32)word):(64)word) (word_join (word_join (word_neg (word (bitval b4):(16)word)) (word_neg (word (bitval b5):(16)word)):(32)word) (word_join (word_neg (word (bitval b6):(16)word)) (word_neg (word (bitval b7):(16)word)):(32)word):(64)word):(128)word)) (16,16):(128)word)) ((word_add (word_subword ((word_and (word 664619068533544770747334646890102785:(128)word)) (word_join (word_join (word_join (word_neg (word (bitval b0):(16)word)) (word_neg (word (bitval b1):(16)word)):(32)word) (word_join (word_neg (word (bitval b2):(16)word)) (word_neg (word (bitval b3):(16)word)):(32)word):(64)word) (word_join (word_join (word_neg (word (bitval b4):(16)word)) (word_neg (word (bitval b5):(16)word)):(32)word) (word_join (word_neg (word (bitval b6):(16)word)) (word_neg (word (bitval b7):(16)word)):(32)word):(64)word):(128)word)) (32,16):(128)word)) ((word_add (word_subword ((word_and (word 664619068533544770747334646890102785:(128)word)) (word_join (word_join (word_join (word_neg (word (bitval b0):(16)word)) (word_neg (word (bitval b1):(16)word)):(32)word) (word_join (word_neg (word (bitval b2):(16)word)) (word_neg (word (bitval b3):(16)word)):(32)word):(64)word) (word_join (word_join (word_neg (word (bitval b4):(16)word)) (word_neg (word (bitval b5):(16)word)):(32)word) (word_join (word_neg (word (bitval b6):(16)word)) (word_neg (word (bitval b7):(16)word)):(32)word):(64)word):(128)word)) (48,16):(128)word)) ((word_add (word_subword ((word_and (word 664619068533544770747334646890102785:(128)word)) (word_join (word_join (word_join (word_neg (word (bitval b0):(16)word)) (word_neg (word (bitval b1):(16)word)):(32)word) (word_join (word_neg (word (bitval b2):(16)word)) (word_neg (word (bitval b3):(16)word)):(32)word):(64)word) (word_join (word_join (word_neg (word (bitval b4):(16)word)) (word_neg (word (bitval b5):(16)word)):(32)word) (word_join (word_neg (word (bitval b6):(16)word)) (word_neg (word (bitval b7):(16)word)):(32)word):(64)word):(128)word)) (64,16):(128)word)) ((word_add (word_subword ((word_and (word 664619068533544770747334646890102785:(128)word)) (word_join (word_join (word_join (word_neg (word (bitval b0):(16)word)) (word_neg (word (bitval b1):(16)word)):(32)word) (word_join (word_neg (word (bitval b2):(16)word)) (word_neg (word (bitval b3):(16)word)):(32)word):(64)word) (word_join (word_join (word_neg (word (bitval b4):(16)word)) (word_neg (word (bitval b5):(16)word)):(32)word) (word_join (word_neg (word (bitval b6):(16)word)) (word_neg (word (bitval b7):(16)word)):(32)word):(64)word):(128)word)) (80,16):(128)word)) ((word_add (word_subword ((word_and (word 664619068533544770747334646890102785:(128)word)) (word_join (word_join (word_join (word_neg (word (bitval b0):(16)word)) (word_neg (word (bitval b1):(16)word)):(32)word) (word_join (word_neg (word (bitval b2):(16)word)) (word_neg (word (bitval b3):(16)word)):(32)word):(64)word) (word_join (word_join (word_neg (word (bitval b4):(16)word)) (word_neg (word (bitval b5):(16)word)):(32)word) (word_join (word_neg (word (bitval b6):(16)word)) (word_neg (word (bitval b7):(16)word)):(32)word):(64)word):(128)word)) (96,16):(128)word)) (word_subword ((word_and (word 664619068533544770747334646890102785:(128)word)) (word_join (word_join (word_join (word_neg (word (bitval b0):(16)word)) (word_neg (word (bitval b1):(16)word)):(32)word) (word_join (word_neg (word (bitval b2):(16)word)) (word_neg (word (bitval b3):(16)word)):(32)word):(64)word) (word_join (word_join (word_neg (word (bitval b4):(16)word)) (word_neg (word (bitval b5):(16)word)):(32)word) (word_join (word_neg (word (bitval b6):(16)word)) (word_neg (word (bitval b7):(16)word)):(32)word):(64)word):(128)word)) (112,16):(128)word)))))))) (0,32):(32)word):(64)word)) = + 128 * bitval b0 + 64 * bitval b1 + 32 * bitval b2 + 16 * bitval b3 + + 8 * bitval b4 + 4 * bitval b5 + 2 * bitval b6 + bitval b7`, + REPEAT GEN_TAC THEN + MAP_EVERY BOOL_CASES_TAC [`b0:bool`;`b1:bool`;`b2:bool`;`b3:bool`; + `b4:bool`;`b5:bool`;`b6:bool`;`b7:bool`] THEN + REWRITE_TAC[BITVAL_CLAUSES] THEN + CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV) THEN CONV_TAC NUM_REDUCE_CONV);; + +(* The value bridge's weighted sum IS PACK_MASK8 of the accept-mask in NIBBLE *) +(* order. UADDLV_PACK_LEMMA's b0..b7 are in LANE order (b0 = highest lane = *) +(* byte3's high nibble = weight 128 ... b7 = lowest lane = byte0's low nibble = *) +(* weight 1). NIBBLES_OF_BYTES [byte0;byte1;byte2;byte3] lists nibbles low-first *) +(* per byte: [byte0-lo; byte0-hi; byte1-lo; ...; byte3-hi] = [b7;b6;b5;b4;b3;b2; *) +(* b1;b0]. Hence val(idx0) = PACK_MASK8 (REJ_MASK_ETA2 ) once *) +(* the abstract booleans are instantiated to (val nibble_k < 15) — the core *) +(* _SAFE proof does that instantiation using the eta2 nibble machinery. *) +let PACK_CONNECT = prove + (`!b0 b1 b2 b3 b4 b5 b6 b7:bool. + 128 * bitval b0 + 64 * bitval b1 + 32 * bitval b2 + 16 * bitval b3 + + 8 * bitval b4 + 4 * bitval b5 + 2 * bitval b6 + bitval b7 = + PACK_MASK8 [b7;b6;b5;b4;b3;b2;b1;b0]`, + REWRITE_TAC[PACK_MASK8] THEN + CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN ARITH_TAC);; + +(* ------------------------------------------------------------------------- *) +(* *) +(* misc.ml:2100). Its guard FAILS the unification if the per-iteration event *) +(* LHS contains ANY free variable that is not *syntactically* one of *) +(* f_ev_loop8's applied arguments. The hand-written f_events spec passes the *) +(* WHOLE reject mask (REJ_MASK_ETA2 inlist) as f_ev_loop8's mask argument. If *) +(* that argument stays the COMPOUND term (REJ_MASK_ETA2 inlist), then `frees` *) +(* extracts the atom `inlist`, which is NOT syntactically the compound arg, so *) +(* TEST (s124, live): unify `f_ev table mask i = [EventLoad(table+16* *) +(* PACK_MASK8(SUB_LIST(16*i,16) mask),16)]` SUCCEEDS with atomic `mask`, *) +(* but the same with the compound (REJ_MASK_ETA2 inlist) FAILS. *) +(* *) +(* `mask = REJ_MASK_ETA2 inlist` (atomic var). Then the postcondition *) +(* extracts e_loop = \i. f_ev_loop8 .. mask i (atomic). The loop-body mask *) +(* bridge must then rewrite every hardware `inlist`-form into a SUB_LIST of *) +(* the atomic `mask` via REJ_MASK_ETA2_SUB_LIST below: *) +(* idx0 = PACK_MASK8(REJ_MASK_ETA2(SUB_LIST(8*i,4) inlist)) *) +(* = PACK_MASK8(SUB_LIST(16*i,8) mask) *) +(* idx1 = PACK_MASK8(SUB_LIST(16*i+8,8) mask) *) +(* curlen (store advance base) = *) +(* NUM_ACCEPTED(REJ_MASK_ETA2(SUB_LIST(0,8*i) inlist)) *) +(* = NUM_ACCEPTED(SUB_LIST(0,16*i) mask) *) +(* The `inlist`-only parts (curlist = REJ_NIBBLES_ETA2 .., memory contents) *) +(* keep `inlist`; they never enter the event LHS. *) +(* ------------------------------------------------------------------------- *) + +(* byte-index SUB_LIST maps to a nibble-index SUB_LIST at 2x offset/length. *) +let NIBBLES_OF_BYTES_SUB_LIST = prove + (`!l a b. NIBBLES_OF_BYTES(SUB_LIST(a,b) l) = + SUB_LIST(2*a,2*b)(NIBBLES_OF_BYTES l)`, + LIST_INDUCT_TAC THEN REPEAT GEN_TAC THEN + MAP_EVERY (fun v -> STRUCT_CASES_TAC(SPEC v num_CASES)) [`a:num`;`b:num`] THEN + ASM_REWRITE_TAC[NIBBLES_OF_BYTES; NIBBLE_PAIR; SUB_LIST_CLAUSES; APPEND; + MULT_CLAUSES; ADD_CLAUSES; ARITH_RULE `2 * SUC n = SUC(SUC(2*n))`] THEN + ASM_REWRITE_TAC[SUB_LIST_CLAUSES; APPEND]);; + +(* General-offset MAP/SUB_LIST commutation (aarch64_utils' SUB_LIST_MAP is *) +(* prefix-only, (0,n)). *) +let SUB_LIST_MAP_GEN = prove + (`!(f:A->B) l a b. SUB_LIST(a,b)(MAP f l) = MAP f (SUB_LIST(a,b) l)`, + GEN_TAC THEN LIST_INDUCT_TAC THEN REPEAT GEN_TAC THEN + MAP_EVERY (fun v -> STRUCT_CASES_TAC(SPEC v num_CASES)) [`a:num`;`b:num`] THEN + ASM_REWRITE_TAC[MAP; SUB_LIST_CLAUSES]);; + +(* THE mask-level length-doubling commutation: converts a hardware *) +(* REJ_MASK_ETA2(SUB_LIST(a,b) inlist) into a SUB_LIST of the ATOMIC mask — *) +let REJ_MASK_ETA2_SUB_LIST = prove + (`!l a b. REJ_MASK_ETA2(SUB_LIST(a,b) l) = SUB_LIST(2*a,2*b)(REJ_MASK_ETA2 l)`, + REWRITE_TAC[REJ_MASK_ETA2; NIBBLES_OF_BYTES_SUB_LIST; SUB_LIST_MAP_GEN]);; + +(* ------------------------------------------------------------------------- *) +(* *) +(* The number of loop8 iterations is data-dependent but PUBLIC: a function of *) +(* the public buflen and the public reject mask ONLY (never the accepted *) +(* values). It equals MEMSAFE's WOP-defined N (rej_uniform_eta2_aarch64_asm *) +(* .ml:2442): the least n at which EITHER the input is exhausted *) +(* (val buflen < 8*(n+1)) OR the output is full (256 <= accepted-so-far). *) +(* Each loop iteration consumes 8 bytes = 16 nibbles, and the accepted count *) +(* after n iterations = NUM_ACCEPTED of the first 16n mask bits, because *) +(* LENGTH(REJ_NIBBLES_ETA2(SUB_LIST(0,8n) inlist)) = *) +(* NUM_ACCEPTED(SUB_LIST(0,16n)(REJ_MASK_ETA2 inlist)) [s117 count bridge]. *) +(* So this is exactly MEMSAFE's N whenever mask = REJ_MASK_ETA2 inlist, and *) +(* it is expressed WITHOUT reference to inlist (secret-independent). *) +(* ------------------------------------------------------------------------- *) + +let MLDSA_ETA2_LOOP8_TRIP = define + `MLDSA_ETA2_LOOP8_TRIP (buflen:int64) (mask:bool list) : num = + minimal n. val buflen < 8 * (n + 1) \/ + 256 <= NUM_ACCEPTED (SUB_LIST(0,16 * n) mask)`;; + +(* ------------------------------------------------------------------------- *) +(* *) +(* This is the analytical crux of loop8's DUAL-EXIT closure. loop8 exits *) +(* when EITHER the input is exhausted (remaining < 8, i.e. val buflen < *) +(* 8*(i+1)) OR the output is full (256 <= accepted so far). In the *) +(* prove PC = (if i+1 < TRIP then pc1 else pc2), which requires connecting *) +(* the two HARDWARE branch conditions (X2<8 at the bottom b.hs 0xf8; X9>=256 *) +(* at the top b.hs 0x6c) to the arithmetic predicate i+1 < TRIP. This lemma *) +(* is exactly that connector, derived from the minimality of TRIP: *) +(* - part 1 (the exit disjunction AT the trip point) tells the exit tail *) +(* WHICH branch fired (input-exhaust vs output-full = which EventJump *) +(* list the last iteration emits); *) +(* - part 2 (neither condition holds strictly BELOW the trip point) is the *) +(* "we execute iteration i" fact — it kills the top b.hs (curlen<256, so *) +(* 0x6c falls through to 0x70) and guarantees the bottom b.hs is taken *) +(* back to 0x68 for every non-final iteration, exactly MEMSAFE's *) +(* invariant conjuncts `curlen < 256` (eta2.ml:2504) and `8*(i+1) <= *) +(* buflen` (eta2.ml:2508), but stated over the PUBLIC atomic mask via the *) +(* s117 count bridge (LENGTH(REJ_NIBBLES_ETA2(SUB_LIST(0,8i) inlist)) = *) +(* NUM_ACCEPTED(SUB_LIST(0,16i)(REJ_MASK_ETA2 inlist))) rather than the *) +(* secret niblen. Pure arithmetic on `minimal` (MINIMAL); no SIMD. *) +(* ------------------------------------------------------------------------- *) + +let MLDSA_ETA2_LOOP8_TRIP_MINIMAL = prove + (`!(buflen:int64) (mask:(bool)list). + (val buflen < 8 * (MLDSA_ETA2_LOOP8_TRIP buflen mask + 1) \/ + 256 <= NUM_ACCEPTED(SUB_LIST(0,16 * MLDSA_ETA2_LOOP8_TRIP buflen mask) mask)) /\ + (!i. i < MLDSA_ETA2_LOOP8_TRIP buflen mask + ==> ~(val buflen < 8 * (i + 1)) /\ + ~(256 <= NUM_ACCEPTED(SUB_LIST(0,16 * i) mask)))`, + REPEAT GEN_TAC THEN REWRITE_TAC[MLDSA_ETA2_LOOP8_TRIP] THEN + SUBGOAL_THEN + `?n. val(buflen:int64) < 8 * (n + 1) \/ 256 <= NUM_ACCEPTED(SUB_LIST(0,16 * n) mask)` + ASSUME_TAC THENL + [EXISTS_TAC `val(buflen:int64)` THEN DISJ1_TAC THEN ARITH_TAC; ALL_TAC] THEN + FIRST_X_ASSUM(STRIP_ASSUME_TAC o REWRITE_RULE[MINIMAL]) THEN + ASM_REWRITE_TAC[] THEN + X_GEN_TAC `i:num` THEN DISCH_TAC THEN + REWRITE_TAC[GSYM DE_MORGAN_THM] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN + ASM_REWRITE_TAC[]);; + +(* ------------------------------------------------------------------------- *) +(* MATERIALIZED + mask-bridge demonstrated end-to-end (not just asserted). *) +(* *) +(* EVENT VOCABULARY (confirmed from arm/proofs/instruction.ml + live steps): *) +(* EventLoad (addr:int64, size:num) EventStore (addr:int64, size:num) *) +(* EventJump (pc:int64, pc_next:int64) -- all accumulate via CONS. *) +(* arm_Bcond (instruction.ml:997): EVERY conditional branch (taken OR not- *) +(* taken) emits CONS(EventJump(pc, pc_next)) where pc_next is the symbolic *) +(* `if then else `. A symbolic-condition branch steps *) +(* to a CLEAN `if`-term for BOTH read PC and the EventJump target. *) +(* *) +(* read events s = CONS (EventStore (sp + 2*curlen, 16)) [st1 0xdc]*) +(* (CONS (EventLoad (table + 16*val idx1, 16)) [ldr 0xb8]*) +(* (CONS (EventLoad (table + 16*val idx0, 16)) [ldr 0xb4]*) +(* (CONS (EventLoad (buf + 8*i, 8)) e0))) [ld1 0x74]*) +(* Second store (0xe4) is EventStore(sp + 2*(curlen + val len0), 16), after *) +(* `add x7,x7,x12,lsl#1`. So the full per-iteration f_ev_loop8 = the 3 loads*) +(* + 2 stores + the trailing branch EventJump(s), all as CONS on e0. *) +(* *) +(* MASK BRIDGE demonstrated LIVE (the s124 "integration asserted not *) +(* demonstrated" gap is now CLOSED at the compute half): after the MEMSAFE *) +(* simp chain (eta2.ml:2564-2569), the live idx0 = read X12 collapses to *) +(* EXACTLY UADDLV_PACK_LEMMA's LHS shape *) +(* val(word_zx(word_subword(word_add(...word_and Q31 *) +(* (word_join.. word_neg(word(bitval(val(word_subword nibbles0 (k,16))<15)))))))) *) +(* machinery + REJ_MASK_ETA2_SUB_LIST + `REJ_MASK_ETA2 inlist = mask` give *) +(* val idx0 = PACK_MASK8(SUB_LIST(16*i,8) mask) *) +(* val idx1 = PACK_MASK8(SUB_LIST(16*i+8,8) mask) *) +(* curlen = NUM_ACCEPTED(SUB_LIST(0,16*i) mask) *) +(* val len0 = NUM_ACCEPTED(SUB_LIST(16*i,8) mask) *) +(* mask), so f_ev_loop8 (a CONCRETIZE meta-var) auto-instantiates via *) +(* REJECT-MASK, demonstrated. (Accepted VALUES never enter the trace.) *) +(* *) +(* add x7; add x12; add x9; cmp x2,#8]. *) +(* BEFORE `add x7`. (b) stores need `nonoverlapping (word pc,372) *) +(* (stackpointer,576)` in context (from the theorem's ALL clause) AND the *) +(* 2nd store additionally needs val len0<=8 (UADDLV_BOUND_LEMMA) + the *) +(* MEMSAFE WORD_ADD_SHL1 rewrite (eta2.ml:2971) on the word_shl'd X7 offset, *) +(* else "could not prove updates will not modify the program code". *) +(* *) +(* `8 <= val(read X2 )`: *) +(* * remaining>=8 (input not exhausted): step 0x68 (cmp x9,x4), 0x6c (b.cs, *) +(* if val buflen < 8*(i+2) then else =8 list> *) +(* the theorem's loop8 leaf; connect 256<=val(curlen') and remaining bounds *) +(* to `i+1 ival(word m:int64) = &m`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `val(word m:int64) = m` ASSUME_TAC THENL + [REWRITE_TAC[VAL_WORD; DIMINDEX_64] THEN MATCH_MP_TAC MOD_LT THEN + ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `~bit 63 (word m:int64)` ASSUME_TAC THENL + [REWRITE_TAC[BIT_WORD; DIMINDEX_64] THEN + SUBGOAL_THEN `m DIV 2 EXP 63 = 0` SUBST1_TAC THENL + [MATCH_MP_TAC DIV_LT THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN + CONV_TAC NUM_REDUCE_CONV; ALL_TAC] THEN + ASM_REWRITE_TAC[IVAL_VAL; DIMINDEX_64; ARITH_RULE `64 - 1 = 63`; + BITVAL_CLAUSES] THEN + INT_ARITH_TAC);; + +(* The signed b.lt back-edge condition for the zero-init counter: given i<8 *) +(* (loop bound), the raw stepper flag condition on 32*(i+1) is equivalent to *) +(* the loop-continuation predicate i+1<8. This is what the loop-body PC leaf *) +let ZINIT_BRANCH = prove + (`!i. i < 8 ==> + (~(ival (word_add (word (32 * i)) (word 18446744073709551392):int64) < &0 <=> + ~(ival (word_add (word (32 * i)) (word 32):int64) - &256 = + ival (word_add (word (32 * i)) (word 18446744073709551392):int64))) + <=> i + 1 < 8)`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN + `ival (word_add (word (32 * i)) (word 32):int64) = &(32 * i) + &32` + SUBST1_TAC THENL + [SUBGOAL_THEN `word_add (word (32*i)) (word 32):int64 = word(32*i+32)` + SUBST1_TAC THENL [CONV_TAC WORD_RULE; ALL_TAC] THEN + SUBGOAL_THEN `ival(word(32*i+32):int64) = &(32*i+32)` + (fun th -> REWRITE_TAC[th; GSYM INT_OF_NUM_ADD]) THEN + MATCH_MP_TAC IVAL_WORD_SMALL THEN ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN + `ival (word_add (word (32 * i)) (word 18446744073709551392):int64) = + &(32 * i) - &224` + SUBST1_TAC THENL + [SUBGOAL_THEN + `word_add (word (32*i)) (word 18446744073709551392):int64 = + iword(&(32*i) - &224)` SUBST1_TAC THENL + [REWRITE_TAC[IWORD_INT_SUB; GSYM WORD_IWORD] THEN + REWRITE_TAC[WORD_RULE `word_sub a (b:int64) = word_add a (word_neg b)`] THEN + AP_TERM_TAC THEN CONV_TAC WORD_REDUCE_CONV; ALL_TAC] THEN + MATCH_MP_TAC IVAL_IWORD THEN REWRITE_TAC[DIMINDEX_64] THEN + ASM_SIMP_TAC[GSYM INT_OF_NUM_MUL; GSYM INT_OF_NUM_LT] THEN + ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `(&(32 * i) + &32) - &256 = &(32 * i) - &224:int` SUBST1_TAC THENL + [INT_ARITH_TAC; ALL_TAC] THEN + REWRITE_TAC[] THEN + REWRITE_TAC[INT_ARITH `(x:int) - &224 < &0 <=> x < &224`; + GSYM INT_OF_NUM_MUL; GSYM INT_OF_NUM_LT] THEN + ARITH_TAC);; + +(* The signed b.lt back-edge condition for the FINAL-COPY (fcopy) counter: given *) +(* i<16 (loop bound), the raw stepper flag condition on the post-increment *) +(* counter 16*(i+1) is equivalent to the loop-continuation predicate i+1<16. *) +(* This is FCOPY's analogue of ZINIT_BRANCH (32*(i+1) vs 8): 16*(i+1) vs 256, *) +(* -240 = word 18446744073709551376 (= 16 - 256 in two's complement). *) +let FCOPY_BRANCH = prove + (`!i. i < 16 ==> + (~(ival (word_add (word (16 * i)) (word 18446744073709551376):int64) < &0 <=> + ~(ival (word_add (word (16 * i)) (word 16):int64) - &256 = + ival (word_add (word (16 * i)) (word 18446744073709551376):int64))) + <=> i + 1 < 16)`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN + `ival (word_add (word (16 * i)) (word 16):int64) = &(16 * i) + &16` + SUBST1_TAC THENL + [SUBGOAL_THEN `word_add (word (16*i)) (word 16):int64 = word(16*i+16)` + SUBST1_TAC THENL [CONV_TAC WORD_RULE; ALL_TAC] THEN + SUBGOAL_THEN `ival(word(16*i+16):int64) = &(16*i+16)` + (fun th -> REWRITE_TAC[th; GSYM INT_OF_NUM_ADD]) THEN + MATCH_MP_TAC IVAL_WORD_SMALL THEN ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN + `ival (word_add (word (16 * i)) (word 18446744073709551376):int64) = + &(16 * i) - &240` + SUBST1_TAC THENL + [SUBGOAL_THEN + `word_add (word (16*i)) (word 18446744073709551376):int64 = + iword(&(16*i) - &240)` SUBST1_TAC THENL + [REWRITE_TAC[IWORD_INT_SUB; GSYM WORD_IWORD] THEN + REWRITE_TAC[WORD_RULE `word_sub a (b:int64) = word_add a (word_neg b)`] THEN + AP_TERM_TAC THEN CONV_TAC WORD_REDUCE_CONV; ALL_TAC] THEN + MATCH_MP_TAC IVAL_IWORD THEN REWRITE_TAC[DIMINDEX_64] THEN + ASM_SIMP_TAC[GSYM INT_OF_NUM_MUL; GSYM INT_OF_NUM_LT] THEN + ASM_ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `(&(16 * i) + &16) - &256 = &(16 * i) - &240:int` SUBST1_TAC THENL + [INT_ARITH_TAC; ALL_TAC] THEN + REWRITE_TAC[] THEN + REWRITE_TAC[INT_ARITH `(x:int) - &240 < &0 <=> x < &240`; + GSYM INT_OF_NUM_MUL; GSYM INT_OF_NUM_LT] THEN + ARITH_TAC);; + +(* ------------------------------------------------------------------------- *) +(* *) +(* These two word-arith lemmas are the ONLY analytical pieces (beyond the *) +(* already-landed MLDSA_ETA2_LOOP8_TRIP_MINIMAL) needed to discharge loop8's *) +(* *) +(* BOTTOM branch (0xf4 cmp x2,#8 ; 0xf8 b.cs 0x68), x2 = buflen-8*(i+1): *) +(* live form: read PC = if 8 <= val(word_sub buflen (word(8*(i+1)))) *) +(* then word(pc+104)[=0x68] else word(pc+252)[=0xfc] *) +(* LOOP8_BOT_VAL_BRIDGE turns the hw cond into ~(val buflen < 8*(i+2)) *) +(* (input-exhaust), given the invariant fact 8*(i+1) <= val buflen *) +(* (= MINIMAL part 2 at j=i, i.e. ~(val buflen < 8*(i+1))). *) +(* *) +(* TOP branch (0x68 cmp x9,x4=256 ; 0x6c b.cs 0xfc), x9 = curlen' = *) +(* word(NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask)): *) +(* live form: read PC = if 256 <= val(word(NUM_ACCEPTED(...))) *) +(* then word(pc+252)[=0xfc] else word(pc+112)[=0x70] *) +(* LOOP8_TOP_VAL_BRIDGE turns the hw cond into 256 <= NUM_ACCEPTED(...) *) +(* (output-full), given NUM_ACCEPTED(...) < 2^64 (from the loop invariant *) +(* conjunct curlen' < 256+8 that mirrors MEMSAFE's niblen<256, eta2.ml *) +(* :2504 — MUST be added to the loop8 UP2 invariant). *) +(* ------------------------------------------------------------------------- *) + +let LOOP8_TOP_VAL_BRIDGE = prove + (`!n. n < 2 EXP 64 ==> (256 <= val(word n:int64) <=> 256 <= n)`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `val(word n:int64) = n` SUBST1_TAC THENL + [MATCH_MP_TAC VAL_WORD_EQ THEN ASM_REWRITE_TAC[DIMINDEX_64]; ALL_TAC] THEN + REWRITE_TAC[]);; + +let LOOP8_BOT_VAL_BRIDGE = prove + (`!(buflen:int64) i. 8*(i+1) <= val buflen + ==> (8 <= val(word_sub buflen (word(8*(i+1))):int64) <=> ~(val buflen < 8*(i+2)))`, + REPEAT STRIP_TAC THEN + SUBGOAL_THEN `val(word(8*(i+1)):int64) = 8*(i+1)` ASSUME_TAC THENL + [MATCH_MP_TAC VAL_WORD_EQ THEN REWRITE_TAC[DIMINDEX_64] THEN + MP_TAC(ISPEC `buflen:int64` VAL_BOUND) THEN REWRITE_TAC[DIMINDEX_64] THEN + ASM_ARITH_TAC; ALL_TAC] THEN + ASM_SIMP_TAC[VAL_WORD_SUB_CASES] THEN ASM_ARITH_TAC);; + +(* ------------------------------------------------------------------------- *) +(* *) +(* This is the analytical core of the loop8 tail-close PC obligation. It *) +(* connects the TOP branch's hardware condition (256 <= curlen', where *) +(* curlen' = NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask) is the accepted count *) +(* after iteration i) to the loop-exit predicate ~(i+1 < TRIP), GIVEN the *) +(* BOTTOM branch fell through to the top check (input not exhausted at i+1, *) +(* i.e. ~(val buflen < 8*(i+2))). Both directions follow from *) +(* MLDSA_ETA2_LOOP8_TRIP_MINIMAL: *) +(* (<=) ~(i+1 i+1 = TRIP (with i) 256 <= curlen' with i+1 (256 <= NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask) <=> + ~(i + 1 < MLDSA_ETA2_LOOP8_TRIP buflen mask))`, + REPEAT GEN_TAC THEN STRIP_TAC THEN + MP_TAC(SPECL[`buflen:int64`;`mask:(bool)list`] MLDSA_ETA2_LOOP8_TRIP_MINIMAL) THEN + DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "PT2")) THEN + ASM_CASES_TAC `i + 1 < MLDSA_ETA2_LOOP8_TRIP buflen mask` THENL + [ASM_REWRITE_TAC[] THEN + USE_THEN "PT2" (MP_TAC o SPEC `i + 1`) THEN ANTS_TAC THENL + [ASM_REWRITE_TAC[]; DISCH_THEN(fun th -> REWRITE_TAC[CONJUNCT2 th])]; + SUBGOAL_THEN `i + 1 = MLDSA_ETA2_LOOP8_TRIP buflen mask` ASSUME_TAC THENL + [MAP_EVERY UNDISCH_TAC + [`i < MLDSA_ETA2_LOOP8_TRIP buflen mask`; + `~(i + 1 < MLDSA_ETA2_LOOP8_TRIP buflen mask)`] THEN ARITH_TAC; + ALL_TAC] THEN + ASM_REWRITE_TAC[] THEN + FIRST_ASSUM(DISJ_CASES_TAC o check (is_disj o concl)) THEN ASM_ARITH_TAC]);; + +(* =========================================================================== *) +(* *) +(* was RUN LIVE (light env) and is GREEN end-to-end. Confirmed: *) +(* *) +(* into the loop8 slot (in place of the f_ev_loop8 meta-var); the 6 other *) +(* oblivious segments keep their meta-vars. *) +(* postcond subgoals (mk_new_inv, consttime.ml:792 — does NOT require a *) +(* (0x68/0x6c) — produces read PC / read events in EXACTLY the shape of *) +(* the baked e_loop (verified: the two EventJump targets are public *) +(* if-terms that match by REFL; no need to resolve the top-branch if in *) +(* (a) PC: (if 256<=val(word(NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask))) *) +(* then word(pc+252) else word(pc+112)) *) +(* = word(if i+1 Option A is viable; drive the FULL loop8 body (the ~11-min SIMD compute *) +(* 0x70..0xf4, per the s125 recipe) in a DETACHED BATCH, entering the tail *) +(* the casehyp itself to `true`, losing it for the i+1=TRIP close) — keep a *) +(* assumptions). *) +(* *) +(* 5 compute events buf-load/2 table-loads/2 stores, mask-bridged per s125): *) +(* \i. if 8 <= val(word_sub buflen (word(8*(i+1))):int64) *) +(* then [EventJump(word(pc+108), *) +(* (if 256 <= val(word(NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask))) *) +(* then word(pc+252) else word(pc+112))); *) +(* EventJump(word(pc+248), word(pc+104))] (* CaseA: 2 jumps *) *) +(* else [EventJump(word(pc+248), word(pc+252))] (* CaseB: 1 jump *) *) +(* The loop8 UP2 invariant must add `NUM_ACCEPTED(SUB_LIST(0,16*i) mask) < 256` *) +(* (mirrors MEMSAFE niblen<256) so LOOP8_TOP_VAL_BRIDGE's <2^64 hyp discharges. *) +(* =========================================================================== *) + +(* =========================================================================== *) +(* *) +(* (Option A), now a real `prove` (NO SIMD, ~3s). It is the reusable second *) +(* X2 = buflen - 8*(i+1), X9 = curlen' = NUM_ACCEPTED(SUB_LIST(0,16*(i+1))mask),*) +(* the invariant registers threaded, events = e), it steps the two dual-exit *) +(* branches (0xf4 cmp x2,#8; 0xf8 b.cs 0x68 = bottom/input-exhaust ; then in *) +(* the input-not-exhausted arm 0x68 cmp x9,x4; 0x6c b.cs 0xfc = top/output-full)*) +(* and lands at word(pc + if i+1 ~(i+1= 256, so a <256 invariant conjunct would be FALSE there *) +(* and the body would be unprovable. Instead the tail lemma takes the loose *) +(* `NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask) < 2 EXP 64` as a HYPOTHESIS; step 2 *) +(* discharges it inside the SIMD body from `curlen < 256` (derived from i ensures arm + (\s. aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta2_mc /\ + read PC s = word (pc + 0xf4) /\ + read SP s = word_sub stackpointer (word 576) /\ + read X30 s = returnaddress /\ + read X0 s = res /\ + read X1 s = word_add buf (word(8*(i+1))) /\ + read X2 s = word_sub buflen (word(8*(i+1))) /\ + read X3 s = table /\ + read X4 s = word 256 /\ + read X7 s = word_add (word_sub stackpointer (word 576)) + (word(2 * NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask))) /\ + read X8 s = word_sub stackpointer (word 576) /\ + read X9 s = word (NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask)) /\ + read Q30 s = word 77885641318594292392624080437575695 /\ + read Q31 s = word 664619068533544770747334646890102785 /\ + read (memory :> bytes(table,4096)) s = tabval /\ + read (memory :> bytes(buf, val buflen)) s = bufval /\ + read events s = e) + (\s. read PC s = + word (pc + (if i + 1 < MLDSA_ETA2_LOOP8_TRIP buflen mask then 0x70 else 0xfc)) /\ + read SP s = word_sub stackpointer (word 576) /\ + read X30 s = returnaddress /\ + read X0 s = res /\ + read X1 s = word_add buf (word(8*(i+1))) /\ + read X2 s = word_sub buflen (word(8*(i+1))) /\ + read X3 s = table /\ + read X4 s = word 256 /\ + read X7 s = word_add (word_sub stackpointer (word 576)) + (word(2 * NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask))) /\ + read X8 s = word_sub stackpointer (word 576) /\ + read X9 s = word (NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask)) /\ + read Q30 s = word 77885641318594292392624080437575695 /\ + read Q31 s = word 664619068533544770747334646890102785 /\ + read (memory :> bytes(table,4096)) s = tabval /\ + read (memory :> bytes(buf, val buflen)) s = bufval /\ + read events s = + APPEND + (if 8 <= val(word_sub buflen (word(8*(i+1))):int64) + then [EventJump(word(pc+108), + (if 256 <= val(word(NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask)):int64) + then word(pc+252) else word(pc+112))); + EventJump(word(pc+248), word(pc+104))] + else [EventJump(word(pc+248), word(pc+252))]) e) + (\s s'. T)`, + REPEAT GEN_TAC THEN STRIP_TAC THEN + SUBGOAL_THEN `8 * (i + 1) <= val(buflen:int64)` ASSUME_TAC THENL + [MP_TAC(SPECL[`buflen:int64`;`mask:(bool)list`] MLDSA_ETA2_LOOP8_TRIP_MINIMAL) THEN + DISCH_THEN(MP_TAC o SPEC `i:num` o CONJUNCT2) THEN + ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN ARITH_TAC; + ALL_TAC] THEN + ENSURES_INIT_TAC "s0" THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (1--2) THEN + ASM_CASES_TAC `8 <= val(word_sub buflen (word(8*(i+1))):int64)` THENL + [UNDISCH_TAC `8 <= val(word_sub buflen (word(8*(i+1))):int64)` THEN + DISCH_THEN(fun th -> RULE_ASSUM_TAC(REWRITE_RULE[th]) THEN ASSUME_TAC th) THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (3--4) THEN + SUBGOAL_THEN + `256 <= val(word(NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask)):int64) <=> + ~(i + 1 < MLDSA_ETA2_LOOP8_TRIP buflen mask)` ASSUME_TAC THENL + [ASM_SIMP_TAC[LOOP8_TOP_VAL_BRIDGE] THEN + MATCH_MP_TAC LOOP8_OUTPUT_FULL_IFF THEN + ASM_MESON_TAC[LOOP8_BOT_VAL_BRIDGE]; + ALL_TAC] THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REWRITE_TAC[APPEND] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]; + SUBGOAL_THEN `val (buflen:int64) < 8 * (i + 2)` ASSUME_TAC THENL + [UNDISCH_TAC `~(8 <= val(word_sub buflen (word(8*(i+1))):int64))` THEN + ASM_SIMP_TAC[LOOP8_BOT_VAL_BRIDGE]; ALL_TAC] THEN + SUBGOAL_THEN `~(i + 1 < MLDSA_ETA2_LOOP8_TRIP buflen mask)` ASSUME_TAC THENL + [DISCH_TAC THEN + MP_TAC(SPECL[`buflen:int64`;`mask:(bool)list`] MLDSA_ETA2_LOOP8_TRIP_MINIMAL) THEN + DISCH_THEN(MP_TAC o SPEC `i + 1` o CONJUNCT2) THEN + ASM_REWRITE_TAC[ARITH_RULE `8 * ((i + 1) + 1) = 8 * (i + 2)`]; ALL_TAC] THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[APPEND]]);; + +(* ========================================================================= *) +(* REAL compute-lemma goal (closes the s125 "integration asserted not *) +(* demonstrated" gap for the compute half, now on a concrete `ensures arm` *) +(* whose postcond IS MLDSA_ETA2_LOOP8_TAIL_CLOSE's precond). *) +(* *) +(* (no per-step SIMD simplification) + the MEMSAFE batch simp chains is FAST: *) +(* Total interactive stepping to the 1st store ~30s (NOT 11 min). Only *) +(* whole compute prefix can be driven interactively OR in one modest batch. *) +(* *) +(* THE TARGET LEMMA (validated to type-check; postcond = TAIL_CLOSE precond *) +(* + 5 explicit mask-form events; composes with MLDSA_ETA2_LOOP8_TAIL_CLOSE *) +(* *) +(* MLDSA_ETA2_LOOP8_COMPUTE: *) +(* !res buf buflen table inlist mask pc i e stackpointer. *) +(* mask = REJ_MASK_ETA2 inlist /\ LENGTH inlist = val buflen /\ *) +(* 8*(i+1) <= val buflen /\ NUM_ACCEPTED(SUB_LIST(0,16*i) mask) < 256 /\ *) +(* nonoverlapping (word pc,372) (word_sub stackpointer (word 576),576) *) +(* + read events = APPEND [st2; st1; ldtab1; ldtab0; ldbuf] e) *) +(* (\s s'. T) *) +(* where the 5 events (newest-first) are, with *) +(* curlen = NUM_ACCEPTED(SUB_LIST(0,16*i) mask): *) +(* EventStore(sp-576 + 2*(curlen + NUM_ACCEPTED(SUB_LIST(16*i,8) mask)),16)*) +(* EventStore(sp-576 + 2*curlen, 16) *) +(* EventLoad (table + 16*PACK_MASK8(SUB_LIST(16*i+8,8) mask), 16) *) +(* EventLoad (table + 16*PACK_MASK8(SUB_LIST(16*i,8) mask), 16) *) +(* EventLoad (buf + 8*i, 8) *) +(* *) +(* EventStore(word_add(word_sub stackpointer(word 576))(word(2*curlen)),16)*) +(* *) +(* REMAINING (all "known recipe", to finish MLDSA_ETA2_LOOP8_COMPUTE): *) +(* (1) bounds val(len0)<=8 / val(len1)<=8: after the 2nd simp the goal is *) +(* match (len0's collapsed form differs from the raw cnt/uaddlv shape of *) +(* `val(read X12)=LENGTH lis0` (eta2.ml:2529-2536,2869) idiom. *) +(* (3) MASK BRIDGES (the crux; s125 recipe, all lemmas already landed): *) +(* loaded_d = num_of_wordlist(SUB_LIST(8*i,8) inlist) via *) +(* SUB_LIST_8_BYTES_FROM_INT64 (eta2.ml, needs 8*(i+1)<=LENGTH inlist); *) +(* b_k to nibble preds (VAL_WORD_ZX_BYTE16/BYTE_AND_15_MOD/BYTE_USHR4_ *) +(* len0/len1: LENGTH lis0 = NUM_ACCEPTED(REJ_MASK_ETA2(4-byte grp)) via *) +(* LENGTH_REJ_NIBBLES_ETA2_EQ_MASK + NUM_ACCEPTED + REJ_MASK_ETA2_SUB_ *) +(* (4) POSTCOND close: X9/X7 final via NUM_ACCEPTED_SUB_LIST_STEP (below) + *) +(* WORD_RULE; events via (3); memory (table/buf) preserved (only stack *) +(* written). Keep `mask` FOLDED throughout (atomic-mask discipline). *) +(* *) +(* CLOSE ] ; the per-iter e_loop = APPEND *) +(* ; APPEND_ASSOC bookkeeping between the two halves. *) +(* ========================================================================= *) + +(* Count-bridge for the loop8 per-iteration accepted count (final X9 value and *) +(* the 2nd stack-store address): the accepted-count after i+1 groups = the *) +(* count after i groups + the two 4-byte-half counts of group i. Pure list *) +let NUM_ACCEPTED_SUB_LIST_STEP = prove + (`!(mask:bool list) i. + NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask) = + NUM_ACCEPTED(SUB_LIST(0,16*i) mask) + + NUM_ACCEPTED(SUB_LIST(16*i,8) mask) + + NUM_ACCEPTED(SUB_LIST(16*i+8,8) mask)`, + REPEAT GEN_TAC THEN + ASSUME_TAC(REWRITE_RULE[ADD_CLAUSES; ARITH_RULE `8+8=16`] + (ISPECL[`mask:bool list`;`8`;`8`;`16*i:num`] SUB_LIST_SPLIT)) THEN + ASSUME_TAC(REWRITE_RULE[ADD_CLAUSES] + (ISPECL[`mask:bool list`;`16*i:num`;`16`;`0`] SUB_LIST_SPLIT)) THEN + ASM_REWRITE_TAC[ARITH_RULE `16*(i+1) = 16*i+16`; NUM_ACCEPTED_APPEND] THEN + ARITH_TAC);; + +(* Each 4-byte loop8 half-group accepts at most 8 nibbles (LENGTH bound). Used to *) +(* bound the per-iteration store advance so the 2nd stack store's address stays *) +let NUM_ACCEPTED_LE_8 = prove + (`!(m:bool list) a. NUM_ACCEPTED(SUB_LIST(a,8) m) <= 8`, + REPEAT GEN_TAC THEN REWRITE_TAC[NUM_ACCEPTED] THEN + MATCH_MP_TAC LE_TRANS THEN + EXISTS_TAC `LENGTH(SUB_LIST(a,8) (m:bool list))` THEN + REWRITE_TAC[LENGTH_FILTER; LENGTH_SUB_LIST] THEN ARITH_TAC);; + +(* ========================================================================= *) +(* *) +(* content): the loop8 SIMD reads 8 bytes into v0 then computes over them. *) +(* (i.e. after the leading `sub x2` = step 1, before step 2), so the load *) +(* folds to `read Q0 s2 = word_zx loaded_d` and read Q16 s9 (nibbles0) becomes *) +(* a PURE function of loaded_d. If loaded_d is abbreviated AFTER the ld1 *) +(* (s130's earlier drive), idx0's accept bits reference `read Q0 s2` (an opaque *) +(* register atom, NOT loaded_d) and WORD_BLAST cannot connect the nibbles to *) +(* loaded_d — the whole bridge stalls. This was the true blocker. *) +(* *) +(* 2. at s9 (BEFORE reabbrev), establish 16 nibble facts by WORD_BLAST *) +(* `word_subword (read Q16 s9) (16k,16):int16 = *) +(* word_zx(word_and/ushr (word_subword loaded_d (bp,8):byte) (word 15/4))` *) +(* via FIRST_ASSUM(SUBST1 the `read Q16 s9 = ` fact) THEN WORD_BLAST; *) +(* (bp = (k div 2)*8 for Q16 bytes 0-3, +32 for Q17 bytes 4-7; even k=and, *) +(* (These 16 facts survive because they mention only loaded_d + nibbles0.) *) +(* 4. mask-slice fact `SUB_LIST(16*i,8) mask = [8 loaded_d-nibble bools]`: *) +(* - SUB_LIST(8*i,8) inlist = [8 subwords loaded_d] via *) +(* - split with SUB_LIST_4_FROM_8; connect SUB_LIST(16*i,8) mask = *) +(* [REJ_MASK_ETA2;NIBBLES_OF_BYTES_4;MAP;VAL_WORD_NIBBLE_LT]). *) +(* ALL FIVE STEPS RAN CLEAN LIVE (s131). ⚠ Do NOT bulk-discard assumptions by *) +(* size (`>3000 chars`) — that also nukes the 6.4KB idx0/idx1 raw forms; discard*) +(* only the uxtl bigforms by matching the constant "1085102592571150095". *) +(* *) +(* REMAINING to finish MLDSA_ETA2_LOOP8_COMPUTE (NOT yet a landed prove): *) +(* — analogous but via the CNT/popcount form: POPCOUNT_AND_POWERS then *) +(* UADDLV_COUNT_LEMMA-style sum = NUM_ACCEPTED [8 bools] (mask slice); *) +(* val len<=8 is then free (NUM_ACCEPTED <= LENGTH <= 8); 2 stores (VERBOSE + *) +(* WORD_ADD_SHL1 + nonoverlapping (2nd-store-addr,16)(word pc,344) via *) +(* via the 4 bridges). Then compose with MLDSA_ETA2_LOOP8_TAIL_CLOSE. *) +(* ========================================================================= *) + +(* Cancel a prefix of known length off an APPEND equality. *) +let APPEND_EQ_LEN = prove + (`!l1 m1 l2 m2:A list. LENGTH l1 = LENGTH m1 + ==> (APPEND l1 l2 = APPEND m1 m2 <=> l1 = m1 /\ l2 = m2)`, + LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN + REWRITE_TAC[LENGTH; NOT_SUC; SUC_INJ; APPEND; CONS_11] THEN + REPEAT STRIP_TAC THEN ASM_MESON_TAC[]);; + +(* Split a known 8-element SUB_LIST into its two 4-element halves (the loop8 *) +(* group is 8 bytes = two 4-byte lanes feeding idx0 and idx1 respectively). *) +let SUB_LIST_4_FROM_8 = prove + (`!(l:A list) a x0 x1 x2 x3 x4 x5 x6 x7. + SUB_LIST(a,8) l = [x0;x1;x2;x3;x4;x5;x6;x7] + ==> SUB_LIST(a,4) l = [x0;x1;x2;x3] /\ SUB_LIST(a+4,4) l = [x4;x5;x6;x7]`, + REPEAT GEN_TAC THEN DISCH_TAC THEN + SUBGOAL_THEN `8 <= LENGTH(l:A list) - a` ASSUME_TAC THENL + [FIRST_ASSUM(MP_TAC o AP_TERM `LENGTH:A list->num`) THEN + REWRITE_TAC[LENGTH_SUB_LIST; LENGTH] THEN ARITH_TAC; ALL_TAC] THEN + SUBGOAL_THEN `APPEND (SUB_LIST(a,4)(l:A list)) (SUB_LIST(a+4,4) l) = + [x0;x1;x2;x3;x4;x5;x6;x7]` MP_TAC THENL + [FIRST_X_ASSUM(fun th -> REWRITE_TAC[SYM th]) THEN + MP_TAC(ISPECL[`l:A list`;`4`;`4`;`a:num`] SUB_LIST_SPLIT) THEN + REWRITE_TAC[ARITH_RULE `4+4=8`] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN REFL_TAC; + ALL_TAC] THEN + MP_TAC(ISPECL[`SUB_LIST(a,4)(l:A list)`;`[x0;x1;x2;x3]:A list`; + `SUB_LIST(a+4,4)(l:A list)`;`[x4;x5;x6;x7]:A list`] APPEND_EQ_LEN) THEN + ANTS_TAC THENL + [REWRITE_TAC[LENGTH_SUB_LIST; LENGTH] THEN CONV_TAC NUM_REDUCE_CONV THEN + ASM_ARITH_TAC; ALL_TAC] THEN + REWRITE_TAC[APPEND] THEN DISCH_THEN(fun th -> ONCE_REWRITE_TAC[GSYM th]) THEN + DISCH_THEN ACCEPT_TAC);; + +(* Expand the reject mask of an explicit 4-byte group into the 8 per-nibble *) +(* accept predicates (low then high nibble of each byte, matching the SIMD lane *) +(* order after the AND/USHR/ZIP/UXTL chain). *) +let MASK_SLICE_4 = prove + (`!(l:byte list) a b0 b1 b2 b3. + SUB_LIST(a,4) l = [b0;b1;b2;b3] + ==> REJ_MASK_ETA2(SUB_LIST(a,4) l) = + [val b0 MOD 16 < 15; val b0 DIV 16 < 15; val b1 MOD 16 < 15; val b1 DIV 16 < 15; + val b2 MOD 16 < 15; val b2 DIV 16 < 15; val b3 MOD 16 < 15; val b3 DIV 16 < 15]`, + REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REJ_MASK_ETA2; NIBBLES_OF_BYTES_4; MAP] THEN + REWRITE_TAC[VAL_WORD_NIBBLE_LT]);; + +(* ========================================================================= *) +(* all 4 bridges (idx0/idx1/len0/len1) proven on the real COMPUTE goal and all *) +(* 5 events materialised in ATOMIC-mask/PACK_MASK8 form. Only the postcond *) +(* clean-script pass from a landed prove. Option A is CONVERGING, not a dead- *) +(* end. Full validated recipe below; assemble it as ONE clean prove (avoid the *) +(* interactive fold back-and-forth that tangled s132's live state). *) +(* *) +(* ***THE ROOT-CAUSE FIX for the len0/len1 bridge (what s131 missed):*** the *) +(* PER-BIT BITBLAST rules `bit k (word_subword (word_neg (word (bitval b):16 *) +(* word)) (0,8):8 word) <=> b` (eta2.ml:1756-1759 / 2798-2801). s131's one-shot *) +(* (POPCOUNT_AND_POWERS + UADDLV_COUNT_LEMMA) omitted them and died on the *) +(* `bit k (word_subword (word_neg (word (bitval b):16 word)) (0,8):8 word) *) +(* <=> b`)) (0--7)) THEN *) +(* FIRST_ASSUM(SUBST1 that len0-LENGTH fact) THEN *) +(* th))]) THEN *) +(* REJ_MASK_ETA2_SUB_LIST] THEN *) +(* (len1 identical: nibbles1b, bytes (32,8)..(56,8), CONJUNCT2, 2*(8*i+4)=16*i+8).*) +(* *) +(* EXEC=MLDSA_REJ_UNIFORM_ETA2_EXEC. Goal = the COMPUTE statement below. *) +(* 5. PROVE_HW_ALL: 16 nibble facts word_subword nibbles0/1b (16k,16) = *) +(* word_zx(word_and/ushr (word_subword loaded_d (bp,8)) ...). Use MEMSAFE's *) +(* prove_hw BUT with the check restricted to a NON-`read` LHS (the word_join *) +(* 6. ***IDX BRIDGES HERE — BEFORE SIMP2*** (order fix; SIMP2's WORD_SUBWORD_AND *) +(* DISTRIBUTES the `word_and (word 664..)` weight const into per-lane *) +(* `word_and (word 2^k)` so UADDLV_PACK_LEMMA no longer matches). Establish *) +(* [ARITH`2*(8*i)=16*i`;ARITH`2*4=8`]; ALL] THEN *) +(* (idx1: sub4hi, 2*(8*i+4)=16*i+8.) These facts SURVIVE SIMP2. *) +(* [If you keep idx bridges AFTER SIMP2 instead, UADDLV_PACK_LEMMA fails; you *) +(* must abstract the distributed form to a fresh 256-case BOOL_CASES lemma *) +(* `IDX_DISTRIB_PACK` (s132 proved one live) — doing it BEFORE SIMP2 avoids *) +(* that entirely.] *) +(* (18--25); SIMP2 (eta2.ml:2578-2584); THEN the len0/len1 bridge + bounds + *) +(* len1` (NOT NUM_ACCEPTED) in the store-address arithmetic (see step 9). *) +(* base MUST be a plain var, else the store's nonoverlapping automation can't *) +(* match `word_add (word_sub sp 576) X`). *) +(* (word_add sp0 (word(2*(curlen+val len0))),16)(word pc,344) [NONOVERLAP- *) +(* X9=word_add(word curlen)(word_add len0 len1), events all in PACK/curlen/ *) +(* to split the postcond's NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask); then fold *) +(* X7 via ARITH assoc + WORD_RULE, X9 via `word_add(word c)(word_add a b) = *) +(* word(c+val a+val b)` (prove: len_k=word(val len_k) [WORD_VAL] then WORD_ *) +(* ***Preserve the val-len0=NUM_ACCEPTED facts to the very end — do NOT *) +(* RULE_ASSUM(GSYM lenfact) mid-drive (it rewrites the lenfact to a trivial *) +(* `val len0 = val len0` and you lose the link).*** *) +(* *) +(* MLDSA_ETA2_LOOP8_COMPUTE statement (validated to type-check + drive to *) +(* !res buf buflen table (inlist:byte list) mask pc i e stackpointer tabval. *) +(* mask = REJ_MASK_ETA2 inlist /\ LENGTH inlist = val buflen /\ *) +(* 8*(i+1) <= val buflen /\ NUM_ACCEPTED(SUB_LIST(0,16*i) mask) < 256 /\ *) +(* nonoverlapping (word pc,372)(word_sub stackpointer (word 576),576) *) +(* ==> ensures arm (PC=pc+112, loop8 inv @ i, buf=num_of_wordlist inlist, *) +(* table=tabval) (PC=pc+244, inv @ i+1 + read events = APPEND *) +(* [Store(sp0+2*(NA(0,16i)+NA(16i,8)));Store(sp0+2*NA(0,16i)); *) +(* Load(table+16*PACK_MASK8(SUB_LIST(16i+8,8) mask)); *) +(* Load(table+16*PACK_MASK8(SUB_LIST(16i,8) mask));Load(buf+8i)] e) *) +(* (\s s'. T) [sp0 = word_sub stackpointer (word 576)]. *) +(* THEN [apply COMPUTE (tabval:=num_of_wordlist table, *) +(* e_loop i = APPEND . *) +(* ========================================================================= *) + +(* ========================================================================= *) +(* *) +(* leakage-up-to-the-reject-mask security content): *) +(* so every one of the 5 emitted events (buf load, 2 table loads, 2 stores) is *) +(* an address that is a function of the PUBLIC (buf,table,sp,i,mask) only — *) +(* never the accepted values. Postcond = MLDSA_ETA2_LOOP8_TAIL_CLOSE's precond *) +(* at i+1 + those 5 events, so the loop8 body leaf composes as *) +(* *) +(* Corrections to the s132 recipe found while assembling this as one prove: *) +(* - len bridge: the popcount reduces to LOADED_D form (`word_zx(word_and *) +(* (word_subword loaded_d ..)(word 15))`), NOT `word_subword nibbles0 ..` *) +(* form, so you MUST fold it back to nibbles0 form (GSYM of the 16 nibble *) +(* forms). Folding the LENGTH form away with SUBST1 (keeping only the *) +(* NUM_ACCEPTED form) makes the 2nd stack store fail its program-code *) +(* non-modification check. *) +(* - the idx bridges must run BEFORE SIMP2 (SIMP2 distributes the Q31 weight *) +(* const so UADDLV_PACK_LEMMA stops matching). *) +(* - the nonoverlapping subgoal for the 2nd store needs explicit :int64 *) +(* annotations, val len0<=8 (NUM_ACCEPTED_LE_8) and curlen<256 in context. *) +(* ========================================================================= *) + +(* --- self-contained helper tactics for the COMPUTE proof --- *) +let bitblast8_compute = List.map (fun k -> BITBLAST_RULE (vsubst[mk_small_numeral k,`k:num`] + `bit k (word_subword (word_neg (word (bitval b):16 word)) (0,8):8 word) <=> b`)) (0--7);; + +(* rewrite the goal with (mk th) for every assumption where mk succeeds *) +let COLLECT_COMPUTE (mk:thm->thm) : tactic = fun (asl,w) -> + REWRITE_TAC(List.filter_map (fun (_,th) -> try Some(mk th) with _ -> None) asl) (asl,w);; + +let is_nibvar_compute v = (try let n = fst(dest_var v) in n="nibbles0"||n="nibbles1b" with _ -> false);; +let NIBGSYM_COMPUTE : tactic = COLLECT_COMPUTE (fun th -> + match lhs(concl th) with + | Comb(Comb(Const("word_subword",_),v),_) when is_nibvar_compute v -> GSYM th + | _ -> failwith "no");; +(* MASK_SLICE_4 applied to each SUB_LIST(_,4) assumption *) +let MASKSLICE_COMPUTE : tactic = COLLECT_COMPUTE (fun th -> MATCH_MP MASK_SLICE_4 th);; +let is_sub4_compute c = is_eq c && (try let (f,a)=strip_comb(lhs c) in + fst(dest_const f)="SUB_LIST" && dest_small_numeral(snd(dest_pair(hd a)))=4 with _ -> false);; +let SUB4GSYM_COMPUTE : tactic = COLLECT_COMPUTE (fun th -> if is_sub4_compute(concl th) then GSYM th else failwith "no");; + +(* find first assumption whose conclusion satisfies p, apply f to it *) +let W_ASM_COMPUTE p (f:thm->tactic) : tactic = fun (asl,w) -> + f (snd(List.find (fun (_,th) -> try p(concl th) with _ -> false) asl)) (asl,w);; + +(* the 16 per-nibble facts word_subword nibbles0/1b (16k,16) = word_zx(word_and/ushr..) *) +let PROVE_HW_ALL_COMPUTE : tactic = + let prove_hw name pos byte_pos op = + let rhs_inner = if op = "and" + then Printf.sprintf + "(word_and (word_subword (loaded_d:int64) (%d,8):byte) (word 15):byte)" byte_pos + else Printf.sprintf + "(word_ushr (word_subword (loaded_d:int64) (%d,8):byte) 4:byte)" byte_pos in + let goal_str = Printf.sprintf + "(word_subword (%s:int128) (%d,16)):int16 = word_zx %s :int16" name pos rhs_inner in + SUBGOAL_THEN (parse_term goal_str) ASSUME_TAC THENL + [FIRST_X_ASSUM(MP_TAC o SYM o check + (fun th -> let c = concl th in is_eq c && + (try fst(dest_var(rhs c)) = name with _ -> false) && + (match lhs c with Comb(Comb(Const("read",_),_),_)->false|_->true))) THEN + DISCH_THEN(fun th -> SUBST1_TAC th THEN ASSUME_TAC(SYM th)) THEN + CONV_TAC WORD_BLAST; + ALL_TAC] in + prove_hw "nibbles0" 0 0 "and" THEN prove_hw "nibbles0" 16 0 "ushr" THEN + prove_hw "nibbles0" 32 8 "and" THEN prove_hw "nibbles0" 48 8 "ushr" THEN + prove_hw "nibbles0" 64 16 "and" THEN prove_hw "nibbles0" 80 16 "ushr" THEN + prove_hw "nibbles0" 96 24 "and" THEN prove_hw "nibbles0" 112 24 "ushr" THEN + prove_hw "nibbles1b" 0 32 "and" THEN prove_hw "nibbles1b" 16 32 "ushr" THEN + prove_hw "nibbles1b" 32 40 "and" THEN prove_hw "nibbles1b" 48 40 "ushr" THEN + prove_hw "nibbles1b" 64 48 "and" THEN prove_hw "nibbles1b" 80 48 "ushr" THEN + prove_hw "nibbles1b" 96 56 "and" THEN prove_hw "nibbles1b" 112 56 "ushr";; + +(* the postcondition fold: normalise driven state + target to a common form *) +let POSTCOND_FOLD_COMPUTE : tactic = fun (asl,w) -> + let find p = snd(List.find (fun (_,th) -> try p(concl th) with _ -> false) asl) in + let maskeq = find (fun c -> c = `mask:(bool)list = REJ_MASK_ETA2 inlist`) in + let curleneq= find (fun c -> c = `NUM_ACCEPTED (SUB_LIST (0,16 * i) mask) = curlen`) in + let len0na = find (fun c -> c = `val(len0:int64) = NUM_ACCEPTED (SUB_LIST (16 * i,8) mask)`) in + let len1na = find (fun c -> c = `val(len1:int64) = NUM_ACCEPTED (SUB_LIST (16 * i + 8,8) mask)`) in + let is_lenlen v c = is_eq c && lhs c = v && + (try fst(dest_const(fst(strip_comb(rhs c))))="LENGTH" with _->false) in + let len0len = find (is_lenlen `val(len0:int64)`) in + let len1len = find (is_lenlen `val(len1:int64)`) in + (REWRITE_TAC[GSYM maskeq] THEN REWRITE_TAC[NUM_ACCEPTED_SUB_LIST_STEP] THEN + REWRITE_TAC[GSYM len0len; GSYM len1len] THEN REWRITE_TAC[curleneq] THEN + REWRITE_TAC[GSYM len0na; GSYM len1na] THEN + REWRITE_TAC[ARITH_RULE `8*(i+1) = 8*i+8`; APPEND] THEN + REPEAT CONJ_TAC THEN TRY(CONV_TAC WORD_RULE) THEN TRY REFL_TAC) (asl,w);; + +let MLDSA_ETA2_LOOP8_COMPUTE = prove + (`!res (buf:int64) (buflen:int64) (table:int64) (inlist:byte list) (mask:(bool)list) + (pc:num) (i:num) (e:(uarch_event)list) (stackpointer:int64) (tabval:num) + (returnaddress:int64). + mask = REJ_MASK_ETA2 inlist /\ + LENGTH inlist = val buflen /\ + 8 * (i + 1) <= val buflen /\ + NUM_ACCEPTED(SUB_LIST(0,16 * i) mask) < 256 /\ + ALL (nonoverlapping (word_sub stackpointer (word 576),576)) + [(word pc,372); (buf,val buflen); (table,4096)] + ==> ensures arm + (\s. aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta2_mc /\ + read PC s = word (pc + 0x70) /\ + read SP s = word_sub stackpointer (word 576) /\ + read X30 s = returnaddress /\ + read X0 s = res /\ + read X1 s = word_add buf (word(8 * i)) /\ + read X2 s = word_sub buflen (word(8 * i)) /\ + read X3 s = table /\ + read X4 s = word 256 /\ + read X7 s = word_add (word_sub stackpointer (word 576)) + (word(2 * NUM_ACCEPTED(SUB_LIST(0,16 * i) mask))) /\ + read X8 s = word_sub stackpointer (word 576) /\ + read X9 s = word (NUM_ACCEPTED(SUB_LIST(0,16 * i) mask)) /\ + read Q30 s = word 77885641318594292392624080437575695 /\ + read Q31 s = word 664619068533544770747334646890102785 /\ + read (memory :> bytes(table,4096)) s = tabval /\ + read (memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist /\ + read events s = e) + (\s. aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta2_mc /\ + read PC s = word (pc + 0xf4) /\ + read SP s = word_sub stackpointer (word 576) /\ + read X30 s = returnaddress /\ + read X0 s = res /\ + read X1 s = word_add buf (word(8 * (i + 1))) /\ + read X2 s = word_sub buflen (word(8 * (i + 1))) /\ + read X3 s = table /\ + read X4 s = word 256 /\ + read X7 s = word_add (word_sub stackpointer (word 576)) + (word(2 * NUM_ACCEPTED(SUB_LIST(0,16 * (i + 1)) mask))) /\ + read X8 s = word_sub stackpointer (word 576) /\ + read X9 s = word (NUM_ACCEPTED(SUB_LIST(0,16 * (i + 1)) mask)) /\ + read Q30 s = word 77885641318594292392624080437575695 /\ + read Q31 s = word 664619068533544770747334646890102785 /\ + read (memory :> bytes(table,4096)) s = tabval /\ + read (memory :> bytes(buf,val buflen)) s = num_of_wordlist inlist /\ + read events s = + APPEND + [EventStore (word_add (word_sub stackpointer (word 576)) + (word(2 * (NUM_ACCEPTED(SUB_LIST(0,16 * i) mask) + + NUM_ACCEPTED(SUB_LIST(16 * i,8) mask)))), 16); + EventStore (word_add (word_sub stackpointer (word 576)) + (word(2 * NUM_ACCEPTED(SUB_LIST(0,16 * i) mask))), 16); + EventLoad (word_add table + (word(16 * PACK_MASK8(SUB_LIST(16 * i + 8,8) mask))), 16); + EventLoad (word_add table + (word(16 * PACK_MASK8(SUB_LIST(16 * i,8) mask))), 16); + EventLoad (word_add buf (word(8 * i)), 8)] + e) + (\s s'. T)`, + REPEAT GEN_TAC THEN DISCH_THEN(MAP_EVERY ASSUME_TAC o CONJUNCTS) THEN + ABBREV_TAC `curlen = NUM_ACCEPTED(SUB_LIST(0,16 * i) mask)` THEN + GHOST_INTRO_TAC `nibbles1:int128` `read Q17` THEN + ENSURES_INIT_TAC "s0" THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC [1] THEN + ABBREV_TAC `loaded_d:int64 = read (memory :> bytes64 (word_add buf (word (8 * i)))) s1` THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC [2] THEN + ARM_VSTEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (3--9) THEN + REABBREV_TAC `nibbles0:int128 = read Q16 s9` THEN + REABBREV_TAC `nibbles1b:int128 = read Q17 s9` THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (10--17) THEN + RULE_ASSUM_TAC(CONV_RULE(TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV)) THEN + RULE_ASSUM_TAC(CONV_RULE WORD_REDUCE_CONV) THEN + RULE_ASSUM_TAC(REWRITE_RULE[word_ugt; relational2; GT; WORD_AND_MASK]) THEN + RULE_ASSUM_TAC(ONCE_REWRITE_RULE[COND_RAND]) THEN + RULE_ASSUM_TAC(CONV_RULE WORD_REDUCE_CONV) THEN + PROVE_HW_ALL_COMPUTE THEN + SUBGOAL_THEN + `SUB_LIST(8 * i,8) inlist = + [word_subword (loaded_d:int64) (0,8):byte; word_subword loaded_d (8,8); + word_subword loaded_d (16,8); word_subword loaded_d (24,8); + word_subword loaded_d (32,8); word_subword loaded_d (40,8); + word_subword loaded_d (48,8); word_subword loaded_d (56,8)]` + ASSUME_TAC THENL + [MP_TAC(SPECL[`buf:int64`;`val(buflen:int64)`;`inlist:byte list`;`i:num`;`s17:armstate`] + SUB_LIST_8_BYTES_FROM_INT64) THEN + ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN + FIRST_ASSUM(fun th -> STRIP_ASSUME_TAC(MATCH_MP SUB_LIST_4_FROM_8 th)) THEN + SUBGOAL_THEN `val(read X12 s17:int64) = PACK_MASK8(SUB_LIST(16 * i,8) mask)` ASSUME_TAC THENL + [W_ASM_COMPUTE (fun c -> is_eq c && lhs c = `read X12 s17:int64`) + (fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN + REWRITE_TAC[UADDLV_PACK_LEMMA; PACK_CONNECT] THEN AP_TERM_TAC THEN + SUBGOAL_THEN `SUB_LIST(16 * i,8) mask = REJ_MASK_ETA2(SUB_LIST(8 * i,4) inlist)` + SUBST1_TAC THENL + [REWRITE_TAC[REJ_MASK_ETA2_SUB_LIST] THEN + ASM_REWRITE_TAC[ARITH_RULE`2*(8*i)=16*i`; ARITH_RULE`2*4=8`]; ALL_TAC] THEN + MASKSLICE_COMPUTE THEN + ASM_REWRITE_TAC[VAL_WORD_ZX_BYTE16; BYTE_AND_15_MOD; BYTE_USHR4_DIV]; ALL_TAC] THEN + SUBGOAL_THEN `val(read X13 s17:int64) = PACK_MASK8(SUB_LIST(16 * i + 8,8) mask)` ASSUME_TAC THENL + [W_ASM_COMPUTE (fun c -> is_eq c && lhs c = `read X13 s17:int64`) + (fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN + REWRITE_TAC[UADDLV_PACK_LEMMA; PACK_CONNECT] THEN AP_TERM_TAC THEN + SUBGOAL_THEN `SUB_LIST(16 * i + 8,8) mask = REJ_MASK_ETA2(SUB_LIST(8 * i + 4,4) inlist)` + SUBST1_TAC THENL + [REWRITE_TAC[REJ_MASK_ETA2_SUB_LIST] THEN + ASM_REWRITE_TAC[ARITH_RULE`2*(8*i+4)=16*i+8`; ARITH_RULE`2*4=8`]; ALL_TAC] THEN + MASKSLICE_COMPUTE THEN + ASM_REWRITE_TAC[VAL_WORD_ZX_BYTE16; BYTE_AND_15_MOD; BYTE_USHR4_DIV]; ALL_TAC] THEN + MAP_EVERY REABBREV_TAC [`idx0:int64 = read X12 s17`; `idx1:int64 = read X13 s17`] THEN + MAP_EVERY ABBREV_TAC + [`tab0:int128 = read(memory :> bytes128(word_add table (word(16 * val(idx0:int64))))) s17`; + `tab1:int128 = read(memory :> bytes128(word_add table (word(16 * val(idx1:int64))))) s17`] THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (18--25) THEN + RULE_ASSUM_TAC(REWRITE_RULE[WORD_SUBWORD_AND]) THEN + RULE_ASSUM_TAC(CONV_RULE(TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV)) THEN + RULE_ASSUM_TAC(CONV_RULE WORD_REDUCE_CONV) THEN + RULE_ASSUM_TAC(REWRITE_RULE[word_ugt; relational2; GT; WORD_AND_MASK]) THEN + RULE_ASSUM_TAC(ONCE_REWRITE_RULE[COND_RAND]) THEN + RULE_ASSUM_TAC(CONV_RULE WORD_REDUCE_CONV) THEN + SUBGOAL_THEN `val(read X12 s25:int64) = + LENGTH(REJ_NIBBLES_ETA2 [word_subword (loaded_d:int64) (0,8):byte; + word_subword loaded_d (8,8); word_subword loaded_d (16,8); + word_subword loaded_d (24,8)])` ASSUME_TAC THENL + [W_ASM_COMPUTE (fun c -> is_eq c && lhs c = `read X12 s25:int64`) + (fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN + REWRITE_TAC[WORD_AND_0; WORD_POPCOUNT_0; ADD_CLAUSES] THEN + REWRITE_TAC[POPCOUNT_AND_POWERS] THEN REWRITE_TAC[UADDLV_COUNT_LEMMA] THEN + REWRITE_TAC bitblast8_compute THEN NIBGSYM_COMPUTE THEN + MP_TAC(SPECL[`nibbles0:int128`; `word_subword (loaded_d:int64) (0,8):byte`; + `word_subword (loaded_d:int64) (8,8):byte`; `word_subword (loaded_d:int64) (16,8):byte`; + `word_subword (loaded_d:int64) (24,8):byte`] COUNT_BRIDGE_ABSTRACT_4) THEN + ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN DISCH_THEN SUBST1_TAC THEN REFL_TAC; + ALL_TAC] THEN + SUBGOAL_THEN `val(read X12 s25:int64) = NUM_ACCEPTED(SUB_LIST(16 * i,8) mask)` ASSUME_TAC THENL + [ASM_REWRITE_TAC[] THEN + REWRITE_TAC[LENGTH_REJ_NIBBLES_ETA2_EQ_MASK; GSYM NUM_ACCEPTED] THEN AP_TERM_TAC THEN + SUB4GSYM_COMPUTE THEN REWRITE_TAC[REJ_MASK_ETA2_SUB_LIST] THEN + ASM_REWRITE_TAC[ARITH_RULE`2*(8*i)=16*i`; ARITH_RULE`2*4=8`]; ALL_TAC] THEN + SUBGOAL_THEN `val(read X13 s25:int64) = + LENGTH(REJ_NIBBLES_ETA2 [word_subword (loaded_d:int64) (32,8):byte; + word_subword loaded_d (40,8); word_subword loaded_d (48,8); + word_subword loaded_d (56,8)])` ASSUME_TAC THENL + [W_ASM_COMPUTE (fun c -> is_eq c && lhs c = `read X13 s25:int64`) + (fun th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN + REWRITE_TAC[WORD_AND_0; WORD_POPCOUNT_0; ADD_CLAUSES] THEN + REWRITE_TAC[POPCOUNT_AND_POWERS] THEN REWRITE_TAC[UADDLV_COUNT_LEMMA] THEN + REWRITE_TAC bitblast8_compute THEN NIBGSYM_COMPUTE THEN + MP_TAC(SPECL[`nibbles1b:int128`; `word_subword (loaded_d:int64) (32,8):byte`; + `word_subword (loaded_d:int64) (40,8):byte`; `word_subword (loaded_d:int64) (48,8):byte`; + `word_subword (loaded_d:int64) (56,8):byte`] COUNT_BRIDGE_ABSTRACT_4) THEN + ANTS_TAC THENL [ASM_REWRITE_TAC[]; ALL_TAC] THEN DISCH_THEN SUBST1_TAC THEN REFL_TAC; + ALL_TAC] THEN + SUBGOAL_THEN `val(read X13 s25:int64) = NUM_ACCEPTED(SUB_LIST(16 * i + 8,8) mask)` ASSUME_TAC THENL + [ASM_REWRITE_TAC[] THEN + REWRITE_TAC[LENGTH_REJ_NIBBLES_ETA2_EQ_MASK; GSYM NUM_ACCEPTED] THEN AP_TERM_TAC THEN + SUB4GSYM_COMPUTE THEN REWRITE_TAC[REJ_MASK_ETA2_SUB_LIST] THEN + ASM_REWRITE_TAC[ARITH_RULE`2*(8*i+4)=16*i+8`; ARITH_RULE`2*4=8`]; ALL_TAC] THEN + ABBREV_TAC `sp0:int64 = word_sub stackpointer (word 576)` THEN + MAP_EVERY REABBREV_TAC [`len0:int64 = read X12 s25`; `len1:int64 = read X13 s25`] THEN + FIRST_X_ASSUM(STRIP_ASSUME_TAC o REWRITE_RULE[ALL] o check + (fun th -> match concl th with Comb(Comb(Const("ALL",_),_),_) -> true | _ -> false)) THEN + SUBGOAL_THEN `val(len0:int64) <= 8` ASSUME_TAC THENL + [ASM_REWRITE_TAC[NUM_ACCEPTED_LE_8; REJ_NIBBLES_ETA2_LENGTH_4]; ALL_TAC] THEN + SUBGOAL_THEN `val(len1:int64) <= 8` ASSUME_TAC THENL + [ASM_REWRITE_TAC[NUM_ACCEPTED_LE_8; REJ_NIBBLES_ETA2_LENGTH_4]; ALL_TAC] THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (26--28) THEN + ARM_VERBOSE_STEP_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC "s29" THEN + FIRST_X_ASSUM(fun th -> if is_eq(concl th) && lhs(concl th) = `read X7 s29:int64` + then ASSUME_TAC(GEN_REWRITE_RULE RAND_CONV [WORD_ADD_SHL1] th) else failwith "no") THEN + SUBGOAL_THEN + `nonoverlapping (word_add sp0 (word(2*(curlen + val(len0:int64)))):int64,16) (word pc:int64,372)` + ASSUME_TAC THENL [NONOVERLAPPING_TAC; ALL_TAC] THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC [30] THEN + ARM_VERBOSE_STEP_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC "s31" THEN + FIRST_X_ASSUM(fun th -> if is_eq(concl th) && lhs(concl th) = `read X7 s31:int64` + then ASSUME_TAC(GEN_REWRITE_RULE RAND_CONV [WORD_ADD_SHL1] th) else failwith "no") THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (32--33) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN POSTCOND_FOLD_COMPUTE);; + +(* ========================================================================= *) +(* MLDSA_ETA2_LOOP8_COMPUTE o MLDSA_ETA2_LOOP8_TAIL_CLOSE. *) +(* *) +(* FAIL-FAST COMPOSITION VERIFIED (the s133 reviewer's one open question): *) +(* MLDSA_ETA2_LOOP8_TAIL_CLOSE's precond under *) +(* [bufval := num_of_wordlist inlist, e := APPEND <5 compute events> e]. *) +(* COMPUTE's postcond WITHOUT its two leading aligned/PC conjuncts.) *) +(* *) +(* The two side hyps are discharged from `i < TRIP` via TRIP_MINIMAL part 2 *) +(* (COMPUTE's `8*(i+1)<=buflen` and `NA(0,16i)<256`) and via *) +(* NUM_ACCEPTED_SUB_LIST_STEP + NUM_ACCEPTED_LE_8 (TAIL_CLOSE's `NA(0,16(i+1)) *) +(* < 2 EXP 64`, bounded by 255+8+8), keeping `mask` ATOMIC throughout (never *) +(* *) +(* Per-iteration public event trace *) +(* e_loop i = APPEND <2 dual-exit branch jumps> . *) +(* The goal is built PROGRAMMATICALLY from COMPUTE + TAIL_CLOSE (mirrors *) +(* UADDLV_PACK_LEMMA's machine-generated construction in this file) so the *) +(* two halves are guaranteed to line up by construction. *) +(* ========================================================================= *) +let MLDSA_ETA2_LOOP8_BODY = + let strip_PQR th = + let b = concl (SPEC_ALL th) in + let body = if is_imp b then rand b else b in + let (_,args) = strip_comb body in (el 1 args, el 2 args, el 3 args) in + let (cP,cQ,cR) = strip_PQR MLDSA_ETA2_LOOP8_COMPUTE in + let (tP,tQ,tR) = strip_PQR MLDSA_ETA2_LOOP8_TAIL_CLOSE in + let _,cQbody = dest_abs cQ in + let ev_compute = + rhs (find (fun c -> is_eq c && lhs c = `read events (s:armstate)`) + (conjuncts cQbody)) in + let subl = [`num_of_wordlist(inlist:byte list)`,`bufval:num`; + ev_compute,`e:(uarch_event)list`] in + let tQ_inst = subst subl tQ in + let c_hyps = conjuncts (lhand (concl (SPEC_ALL MLDSA_ETA2_LOOP8_COMPUTE))) in + let bl_hyps = list_mk_conj + [el 0 c_hyps; el 1 c_hyps; `i < MLDSA_ETA2_LOOP8_TRIP buflen mask`; last c_hyps] in + let ef,eargs = strip_comb (rand (concl (SPEC_ALL MLDSA_ETA2_LOOP8_COMPUTE))) in + let bl_ensures = list_mk_comb(ef, [el 0 eargs; el 1 eargs; tQ_inst; el 3 eargs]) in + let midstate = let sv,body = dest_abs cQ in + mk_abs(sv, list_mk_conj (tl (tl (conjuncts body)))) in + GEN_ALL(prove(mk_imp(bl_hyps, bl_ensures), + STRIP_TAC THEN + SUBGOAL_THEN + `~(val (buflen:int64) < 8 * (i + 1)) /\ + ~(256 <= NUM_ACCEPTED(SUB_LIST(0,16 * i) mask))` + STRIP_ASSUME_TAC THENL + [MATCH_MP_TAC(CONJUNCT2(SPECL[`buflen:int64`;`mask:(bool)list`] + MLDSA_ETA2_LOOP8_TRIP_MINIMAL)) THEN FIRST_ASSUM ACCEPT_TAC; + ALL_TAC] THEN + ENSURES_SEQUENCE_TAC `pc + 0xf4` midstate THEN + CONJ_TAC THENL + [ MATCH_MP_TAC MLDSA_ETA2_LOOP8_COMPUTE THEN + REPEAT CONJ_TAC THENL + [ FIRST_ASSUM ACCEPT_TAC; FIRST_ASSUM ACCEPT_TAC; + ASM_ARITH_TAC; ASM_ARITH_TAC; FIRST_ASSUM ACCEPT_TAC ]; + MATCH_MP_TAC MLDSA_ETA2_LOOP8_TAIL_CLOSE THEN + CONJ_TAC THENL + [ FIRST_ASSUM ACCEPT_TAC; + REWRITE_TAC[NUM_ACCEPTED_SUB_LIST_STEP] THEN + MP_TAC(SPECL[`mask:(bool)list`;`16 * i`] NUM_ACCEPTED_LE_8) THEN + MP_TAC(SPECL[`mask:(bool)list`;`16 * i + 8`] NUM_ACCEPTED_LE_8) THEN + CONV_TAC(ONCE_DEPTH_CONV NUM_REDUCE_CONV) THEN ASM_ARITH_TAC ] ]));; + +(* ========================================================================= *) +(* deep, with the exact next blocker pinned. *) +(* *) +(* TASK 1 (COMMITTED, gated): COMPUTE / TAIL_CLOSE / BODY above now carry *) +(* `read SP s = word_sub stackpointer (word 576)` + `read X30 s = *) +(* returnaddress` in BOTH pre and post (+ a `returnaddress` quantifier). *) +(* handling (COMPUTE re-proves ~54s; TAIL_CLOSE ~3s; BODY re-derives 0.2s *) +(* from its programmatic construction, unchanged). This makes the loop8 *) +(* *) +(* split; the remaining crux precisely pinned. Reproduction recipe: *) +(* (a) Modified CONCRETIZE lambda: splice BODY's per-iteration event delta *) +(* into the `f_ev_loop8` slot. delta i = APPEND <2 dual-exit jumps> *) +(* <5 compute events>, extracted from BODY's postcond `read events` *) +(* conjunct (rhs = APPEND A (APPEND B e); delta = APPEND A B), then *) +(* the outer lambda + subst in the OPEN body (NOT subst under the binder *) +(* — capture-avoiding subst won't match the bound-var'd f_ev_loop8_abs), *) +(* then re-abstract. Front (CONCRETIZE modified_lam THEN META_EXISTS *) +(* (APPEND epil (APPEND loop prol)) tail) tail2 /\ Q e2) <=> ... *) +(* APPEND (APPEND epil (APPEND loop prol)) (APPEND tail tail2) ...` *) +(* rebracket (bignum_copy_row_from_table.ml:771) — but apply it with *) +(* associates the 4-deep trace into `APPEND EPIL (APPEND L8 ACC)`, so *) +(* L8 with count = MLDSA_ETA2_LOOP8_TRIP buflen mask. *) +(* aligned/PC/events, tabval := num_of_wordlist eta_table, as `\i s.`) *) +(* `\s. aligned /\ PC=word(pc+112) /\ (GROUPED loopinv conjunction) /\ *) +(* e_loop) acc)` — this does NOT flat-match MLDSA_ETA2_LOOP8_BODY's *) +(* precond `\s. aligned /\ PC /\ SP /\ X30 /\ ...flat... /\ read events *) +(* directly (validated live — no match). The mismatch is (i) loopinv *) +(* grouped vs flat and (ii) events-exists vs a direct `read events s=e`. *) +(* mask bridges BODY was built to avoid. So the reuse path needs an *) +(* ENSURES precond/postcond MONOTONICITY bridge: instantiate BODY's `e` *) +(* and show P_goal ==> P_body (grouped=>flat, events-exists picks e) and *) +(* ========================================================================= *) + +(* ========================================================================= *) +(* *) +(* are `\s. program_decodes s /\ read PC s = word pc1 /\ (GROUPED loopinv) /\ *) +(* (APPEND e_front acc) /\ memaccess_inbounds e2 ...)}` (relational.ml:1974 *) +(* pth) — which does NOT flat-match MLDSA_ETA2_LOOP8_BODY's precond. *) +(* *) +(* BOTH pre AND post, but BODY's postcond (=TAIL_CLOSE's) DROPS aligned. *) +(* => augment TAIL_CLOSE/BODY with `aligned_bytes_loaded s (word pc) mc` *) +(* aligned so it re-proves for free, exactly like s135's SP/X30 augment). *) +(* pre, covar post, SAME `(\s s'.T)` frame — all of COMPUTE/TAIL_CLOSE/ *) +(* BODY use `(\s s'.T)`), instantiating P/Q to BODY_AL's pre/post with *) +(* acc)) e. Pre-strengthen: grouped=>flat + pick the events witness. *) +(* Post-weaken: PC bridge (word(pc+if..)=word(if..then pc+112..) via *) +(* with e_loop i = the per-iter delta), memaccess (see (3)). Body conjunct*) +(* (3) memaccess of the NEW e2 splits (MEMACCESS_INBOUNDS_APPEND) into the *) +(* per-iter delta memaccess (proven concretely) AND the pre's accumulated *) +(* memaccess. The latter is state-independent, so it is threaded via *) +(* => MI available in-context for the post; ~MI => the pre's `?e2 ... /\ *) +(* memaccess e2_pre` is unsatisfiable so the ensures is vacuous *) +(* (4) The per-iter delta memaccess: jumps (EventJumps) close via *) +(* the buf load needs `8*i+8<=val buflen` which MENTIONS `val` so *) +(* *) +(* MLDSA_ETA2_LOOP8_BODY_ADAPTED is stated with e_front/acc as FREE vars *) +(* its 3 ambient hyps (mask=REJ_MASK_ETA2 inlist, LENGTH inlist=val buflen, *) +(* ALL nonoverlapping) discharge from the main-proof context. conj2 is built *) +(* (no SIMD), guaranteeing the statement is exactly the shape the front emits. *) +(* ========================================================================= *) + +let TAIL_CLOSE_AL = + let th = SPEC_ALL MLDSA_ETA2_LOOP8_TAIL_CLOSE in + let hyps = lhand (concl th) in + let ens = rand (concl th) in + let args = snd(strip_comb ens) in + let p = el 1 args and q = el 2 args and c = el 3 args in + let sv,qb = dest_abs q in + let aligned = subst [sv,`s:armstate`] + `aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta2_mc` in + let q' = mk_abs(sv, mk_conj(aligned, qb)) in + let goal = mk_imp(hyps, list_mk_icomb "ensures" [`arm`;p;q';c]) in + GEN_ALL (prove(goal, + REPEAT GEN_TAC THEN STRIP_TAC THEN + SUBGOAL_THEN `8 * (i + 1) <= val(buflen:int64)` ASSUME_TAC THENL + [MP_TAC(SPECL[`buflen:int64`;`mask:(bool)list`] MLDSA_ETA2_LOOP8_TRIP_MINIMAL) THEN + DISCH_THEN(MP_TAC o SPEC `i:num` o CONJUNCT2) THEN + ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN ARITH_TAC; + ALL_TAC] THEN + ENSURES_INIT_TAC "s0" THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (1--2) THEN + ASM_CASES_TAC `8 <= val(word_sub buflen (word(8*(i+1))):int64)` THENL + [UNDISCH_TAC `8 <= val(word_sub buflen (word(8*(i+1))):int64)` THEN + DISCH_THEN(fun th -> RULE_ASSUM_TAC(REWRITE_RULE[th]) THEN ASSUME_TAC th) THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (3--4) THEN + SUBGOAL_THEN + `256 <= val(word(NUM_ACCEPTED(SUB_LIST(0,16*(i+1)) mask)):int64) <=> + ~(i + 1 < MLDSA_ETA2_LOOP8_TRIP buflen mask)` ASSUME_TAC THENL + [ASM_SIMP_TAC[LOOP8_TOP_VAL_BRIDGE] THEN + MATCH_MP_TAC LOOP8_OUTPUT_FULL_IFF THEN + ASM_MESON_TAC[LOOP8_BOT_VAL_BRIDGE]; + ALL_TAC] THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REWRITE_TAC[APPEND] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]; + SUBGOAL_THEN `val (buflen:int64) < 8 * (i + 2)` ASSUME_TAC THENL + [UNDISCH_TAC `~(8 <= val(word_sub buflen (word(8*(i+1))):int64))` THEN + ASM_SIMP_TAC[LOOP8_BOT_VAL_BRIDGE]; ALL_TAC] THEN + SUBGOAL_THEN `~(i + 1 < MLDSA_ETA2_LOOP8_TRIP buflen mask)` ASSUME_TAC THENL + [DISCH_TAC THEN + MP_TAC(SPECL[`buflen:int64`;`mask:(bool)list`] MLDSA_ETA2_LOOP8_TRIP_MINIMAL) THEN + DISCH_THEN(MP_TAC o SPEC `i + 1` o CONJUNCT2) THEN + ASM_REWRITE_TAC[ARITH_RULE `8 * ((i + 1) + 1) = 8 * (i + 2)`]; ALL_TAC] THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[APPEND]]));; + +let BODY_AL = + let strip_PQR th = + let b = concl (SPEC_ALL th) in + let body = if is_imp b then rand b else b in + let (_,args) = strip_comb body in (el 1 args, el 2 args, el 3 args) in + let (cP,cQ,cR) = strip_PQR MLDSA_ETA2_LOOP8_COMPUTE in + let (tP,tQ,tR) = strip_PQR TAIL_CLOSE_AL in + let _,cQbody = dest_abs cQ in + let ev_compute = + rhs (find (fun c -> is_eq c && lhs c = `read events (s:armstate)`) + (conjuncts cQbody)) in + let subl = [`num_of_wordlist(inlist:byte list)`,`bufval:num`; + ev_compute,`e:(uarch_event)list`] in + let tQ_inst = subst subl tQ in + let c_hyps = conjuncts (lhand (concl (SPEC_ALL MLDSA_ETA2_LOOP8_COMPUTE))) in + let bl_hyps = list_mk_conj + [el 0 c_hyps; el 1 c_hyps; `i < MLDSA_ETA2_LOOP8_TRIP buflen mask`; last c_hyps] in + let ef,eargs = strip_comb (rand (concl (SPEC_ALL MLDSA_ETA2_LOOP8_COMPUTE))) in + let bl_ensures = list_mk_comb(ef, [el 0 eargs; el 1 eargs; tQ_inst; el 3 eargs]) in + let midstate = let sv,body = dest_abs cQ in + mk_abs(sv, list_mk_conj (tl (tl (conjuncts body)))) in + GEN_ALL(prove(mk_imp(bl_hyps, bl_ensures), + STRIP_TAC THEN + SUBGOAL_THEN + `~(val (buflen:int64) < 8 * (i + 1)) /\ + ~(256 <= NUM_ACCEPTED(SUB_LIST(0,16 * i) mask))` + STRIP_ASSUME_TAC THENL + [MATCH_MP_TAC(CONJUNCT2(SPECL[`buflen:int64`;`mask:(bool)list`] + MLDSA_ETA2_LOOP8_TRIP_MINIMAL)) THEN FIRST_ASSUM ACCEPT_TAC; + ALL_TAC] THEN + ENSURES_SEQUENCE_TAC `pc + 0xf4` midstate THEN + CONJ_TAC THENL + [ MATCH_MP_TAC MLDSA_ETA2_LOOP8_COMPUTE THEN + REPEAT CONJ_TAC THENL + [ FIRST_ASSUM ACCEPT_TAC; FIRST_ASSUM ACCEPT_TAC; + ASM_ARITH_TAC; ASM_ARITH_TAC; FIRST_ASSUM ACCEPT_TAC ]; + MATCH_MP_TAC TAIL_CLOSE_AL THEN + CONJ_TAC THENL + [ FIRST_ASSUM ACCEPT_TAC; + REWRITE_TAC[NUM_ACCEPTED_SUB_LIST_STEP] THEN + MP_TAC(SPECL[`mask:(bool)list`;`16 * i`] NUM_ACCEPTED_LE_8) THEN + MP_TAC(SPECL[`mask:(bool)list`;`16 * i + 8`] NUM_ACCEPTED_LE_8) THEN + CONV_TAC(ONCE_DEPTH_CONV NUM_REDUCE_CONV) THEN ASM_ARITH_TAC ] ]));; + +let MLDSA_ETA2_LOOP8_BODY_ADAPTED = + let appty = `APPEND:(uarch_event)list->(uarch_event)list->(uarch_event)list` in + let body = SPEC_ALL BODY_AL in + let bargs = snd(strip_comb (rand (concl body))) in + let bP = el 1 bargs and bQ = el 2 bargs in + (* loop8_inv = BODY_AL-pre minus aligned/PC (front 2) and events (last) *) + let sv, bpbody = dest_abs bP in + let loop8_inv = mk_abs(`i:num`, mk_abs(sv, list_mk_conj (butlast (tl (tl (conjuncts bpbody)))))) in + (* e_loop = \i. APPEND jumps five (per-iter delta from BODY_AL-post events) *) + let _, bqbody = dest_abs bQ in + let ev_rhs = rhs (last (conjuncts bqbody)) in + let jumps, rest = dest_binary "APPEND" ev_rhs in + let five, _ = dest_binary "APPEND" rest in + let e_loop = mk_abs(`i:num`, mk_binop appty jumps five) in + let rr = `[(buf:int64),val(buflen:int64); (table:int64),4096; + word_sub (stackpointer:int64) (word 576),576]` in + let wr = `[word_sub (stackpointer:int64) (word 576),576; (res:int64),1024]` in + let mkinb e2v = list_mk_icomb "memaccess_inbounds" [e2v; rr; wr] in + let e_front = `f_ev_loop8_prol:(uarch_event)list` in + let acc = `f_ev_acc:(uarch_event)list` in + let enum_i = list_mk_comb(`ENUMERATEL:num->(num->(uarch_event)list)->(uarch_event)list`,[`i:num`; e_loop]) in + let e2_pre = mk_binop appty enum_i (mk_binop appty e_front acc) in + let eB = mk_binop appty e2_pre `e:(uarch_event)list` in + let bP_inst = subst [eB,`e:(uarch_event)list`] bP in + let bQ_inst = subst [eB,`e:(uarch_event)list`] bQ in + let mi = mkinb e2_pre in + let trip = `MLDSA_ETA2_LOOP8_TRIP buflen mask` in + let pc1 = `pc + 112` and pc2 = `pc + 252` in + let pre = + let e2 = `e2:(uarch_event)list` in + mk_abs(`s:armstate`, + list_mk_conj + [`aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta2_mc`; + `read PC s = word (pc+112)`; + list_mk_comb(loop8_inv,[`0`;`s:armstate`]); + mk_exists(e2, list_mk_conj [`read events s = APPEND e2 e`; mk_eq(e2,e_front); mkinb e2])]) in + let enum_trip = list_mk_comb(`ENUMERATEL:num->(num->(uarch_event)list)->(uarch_event)list`,[trip; e_loop]) in + let post_e2val = + mk_binop appty (mk_binop appty `f_ev_epil:(uarch_event)list` + (mk_binop appty enum_trip e_front)) acc in + let post = + let e2 = `e2:(uarch_event)list` in + mk_abs(`s:armstate`, + list_mk_conj + [`read PC s = returnaddress`; + mk_exists(e2, list_mk_conj [`read events s = APPEND e2 e`; mk_eq(e2,post_e2val); mkinb e2])]) in + let syn_goal = list_mk_icomb "ensures" [`arm`; pre; post; `\(s:armstate) (s':armstate). T`] in + let conj2 = + let (_,gls,_) = ENSURES_EVENTS_WHILE_UP2_TAC trip pc1 pc2 loop8_inv ([],syn_goal) in + el 2 (conjuncts (snd (hd gls))) in + let enum_i1 = list_mk_comb(`ENUMERATEL:num->(num->(uarch_event)list)->(uarch_event)list`,[`i+1`; e_loop]) in + let e2_post = mk_binop appty enum_i1 (mk_binop appty e_front acc) in + let ambient = list_mk_conj + [`mask = REJ_MASK_ETA2 inlist`; + `LENGTH (inlist:byte list) = val (buflen:int64)`; + `ALL (nonoverlapping (word_sub stackpointer (word 576),576)) + [(word pc,372); (buf:int64,val (buflen:int64)); (table:int64,4096)]`] in + prove(mk_imp(ambient, conj2), + REPEAT STRIP_TAC THEN + ASM_CASES_TAC mi THENL + [ MATCH_MP_TAC ENSURES_PREPOSTCONDITION_THM THEN + MAP_EVERY EXISTS_TAC [bP_inst; bQ_inst] THEN + REPEAT CONJ_TAC THENL + [ GEN_TAC THEN BETA_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[]; + GEN_TAC THEN BETA_TAC THEN STRIP_TAC THEN + UNDISCH_THEN `mask = REJ_MASK_ETA2 inlist` (K ALL_TAC) THEN + ASM_REWRITE_TAC[] THEN + CONJ_TAC THENL + [ AP_TERM_TAC THEN COND_CASES_TAC THEN ARITH_TAC; + EXISTS_TAC e2_post THEN REPEAT CONJ_TAC THENL + [ ASM_REWRITE_TAC[ENUMERATEL_ADD1] THEN REWRITE_TAC[APPEND; APPEND_ASSOC]; + REFL_TAC; + REWRITE_TAC[ENUMERATEL_ADD1] THEN REWRITE_TAC[APPEND; APPEND_ASSOC] THEN + REWRITE_TAC[MEMACCESS_INBOUNDS_APPEND] THEN + RULE_ASSUM_TAC(REWRITE_RULE[APPEND; APPEND_ASSOC; MEMACCESS_INBOUNDS_APPEND]) THEN + ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `8 * (i + 1) <= val(buflen:int64) /\ + NUM_ACCEPTED(SUB_LIST(0,16*i) mask) < 256` + STRIP_ASSUME_TAC THENL + [MP_TAC(SPEC `i:num` (CONJUNCT2(SPECL[`buflen:int64`;`mask:(bool)list`] + MLDSA_ETA2_LOOP8_TRIP_MINIMAL))) THEN ASM_REWRITE_TAC[] THEN ARITH_TAC; + ALL_TAC] THEN + ASSUME_TAC(SPECL[`mask:(bool)list`;`16*i`] NUM_ACCEPTED_LE_8) THEN + ASSUME_TAC(SPEC `SUB_LIST(16*i,8) (mask:(bool)list)` PACK_MASK8_BOUND) THEN + ASSUME_TAC(SPEC `SUB_LIST(16*i+8,8) (mask:(bool)list)` PACK_MASK8_BOUND) THEN + CONJ_TAC THENL + [ COND_CASES_TAC THEN DISCHARGE_MEMACCESS_INBOUNDS_TAC; + DISCHARGE_CONCRETE_MEMACCESS_INBOUNDS_TAC THEN + DISJ1_TAC THEN + GEN_REWRITE_TAC I [GSYM CONTAINED_MODULO_MOD2] THEN + GEN_REWRITE_TAC (BINOP_CONV o LAND_CONV o LAND_CONV o TOP_DEPTH_CONV) + [VAL_WORD_ADD; VAL_WORD; DIMINDEX_64] THEN + CONV_TAC(BINOP_CONV(LAND_CONV MOD_DOWN_CONV)) THEN + GEN_REWRITE_TAC I [CONTAINED_MODULO_MOD2] THEN + (MATCH_MP_TAC CONTAINED_MODULO_OFFSET_SIMPLE ORELSE + MATCH_MP_TAC CONTAINED_MODULO_SIMPLE) THEN + UNDISCH_TAC `8 * (i + 1) <= val(buflen:int64)` THEN ARITH_TAC ] ] ]; + MATCH_MP_TAC BODY_AL THEN ASM_REWRITE_TAC[] ]; + MATCH_MP_TAC ENSURES_PRECONDITION_THM THEN EXISTS_TAC `\s:armstate. F` THEN + CONJ_TAC THENL + [ GEN_TAC THEN BETA_TAC THEN STRIP_TAC THEN ASM_MESON_TAC[]; + REWRITE_TAC[ensures] THEN MESON_TAC[] ] ]);; + +(* Restore the recursive `STRIP_EXISTS_ASSUM_TAC` from s2n-bignum common/misc.ml, *) +(* which the constant-time proof below was developed against. The MEMSAFE section *) +(* (near line 2363) locally redefines STRIP_EXISTS_ASSUM_TAC to a *shallow* variant that *) +(* only splits the outermost conjunction of the chosen existential. The event-loop *) +(* leaves below feed `~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC)` an invariant of the *) +(* form `?e2. read events s = ... /\ e2 = ... /\ memaccess_inbounds e2 ...`; the shallow *) +(* variant leaves `e2 = ... /\ memaccess_inbounds e2 ...` conjoined, so *) +(* DISCHARGE_MEMACCESS_INBOUNDS_USING_ASM_TAC (which filters assumptions by head symbol) *) +(* cannot see the `memaccess_inbounds e2` fact and the discharge fails. The recursive *) +(* STRIP_ASSUME_TAC form splits it into a standalone assumption. *) +let STRIP_EXISTS_ASSUM_TAC = + FIRST_X_ASSUM (STRIP_ASSUME_TAC o (check (is_exists o concl)));; + +let MLDSA_REJ_UNIFORM_ETA2_SUBROUTINE_SAFE = + let appty = `APPEND:(uarch_event)list->(uarch_event)list->(uarch_event)list` in + let bodyth = SPEC_ALL BODY_AL in + let bargs = snd(strip_comb (rand (concl bodyth))) in + let bP = el 1 bargs and bQ = el 2 bargs in + let sv,bpbody = dest_abs bP in + let loop8_inv = + mk_abs(`i:num`, mk_abs(sv, list_mk_conj (butlast (tl (tl (conjuncts bpbody)))))) in + let _,bqbody = dest_abs bQ in + let ev_rhs = rhs (last (conjuncts bqbody)) in + let jumps,rest = dest_binary "APPEND" ev_rhs in + let five,_ = dest_binary "APPEND" rest in + let loop8_inv_real = + subst [`num_of_wordlist mldsa_rej_uniform_eta_table`,`tabval:num`] loop8_inv in + let orig_lam = + `\(res:int64)(buf:int64)(buflen:int64)(table:int64)(pc:num)(sp:int64) + (ra:int64)(mask:(bool)list). + APPEND + (APPEND + (APPEND + (APPEND + (f_ev_epi res buf buflen table pc sp ra mask) + (APPEND (ENUMERATEL 16 (\j. f_ev_fcopy res buf buflen table pc sp ra mask j)) + (f_ev_fcopy_prol res buf buflen table pc sp ra mask))) + (APPEND (ENUMERATEL (MLDSA_ETA2_LOOP8_TRIP buflen mask) + (\i. f_ev_loop8 res buf buflen table pc sp ra mask i)) + (f_ev_loop8_prol res buf buflen table pc sp ra mask))) + (APPEND (ENUMERATEL 8 (\k. f_ev_zinit res buf buflen table pc sp ra mask k)) + (f_ev_zinit_prol res buf buflen table pc sp ra mask))) + (f_ev_begin res buf buflen table pc sp ra mask) :(uarch_event)list` in + let lamvars,obody = strip_abs orig_lam in + let is_l8 t = is_abs t && + (let _,b = dest_abs t in is_comb b && + (let h = fst(strip_comb b) in is_var h && fst(dest_var h) = "f_ev_loop8")) in + let l8_old = find_term is_l8 obody in + let e_loop_lam = mk_abs(`i:num`, + subst [`sp:int64`,`stackpointer:int64`; `ra:int64`,`returnaddress:int64`] + (mk_binop appty jumps five)) in + let modified_lam = list_mk_abs(lamvars, subst [e_loop_lam,l8_old] obody) in + let REASSOC_LOOP8 = METIS[APPEND_ASSOC] + `(exists e2. P e2 /\ + e2 = APPEND (APPEND (APPEND epil (APPEND loop prol)) tail) tail2 /\ Q e2) + <=> + (exists e2. P e2 /\ + e2 = APPEND (APPEND epil (APPEND loop prol)) (APPEND tail tail2) /\ Q e2)` in + let REASSOC_FCOPY = METIS[APPEND_ASSOC] + `(exists e2. P e2 /\ + e2 = APPEND (APPEND fe (APPEND l8e l8p)) zb /\ Q e2) + <=> + (exists e2. P e2 /\ + e2 = APPEND fe (APPEND l8e (APPEND l8p zb)) /\ Q e2)` in + (* MINIMAL fcopy invariant (postcond doesn't constrain regs; omit X9/v-consts). *) + let fcopy_inv = + `\(i:num) s. read SP s = word_sub stackpointer (word 576) /\ + read X30 s = returnaddress /\ + read X0 s = word_add res (word(64 * i)) /\ + read X7 s = word_add (word_sub stackpointer (word 576)) (word(32 * i)) /\ + read X8 s = word_sub stackpointer (word 576) /\ + read X11 s = word(16 * i)` in + prove + (`?f_events:int64->int64->int64->int64->num->int64->int64-> + (bool list)->(uarch_event)list. + !res buf buflen table (inlist:byte list) pc e stackpointer returnaddress. + 8 divides val buflen /\ + 8 <= val buflen /\ + LENGTH inlist = val buflen /\ + ALL (nonoverlapping (word_sub stackpointer (word 576),576)) + [(word pc,LENGTH mldsa_rej_uniform_eta2_mc); + (buf,val buflen); (table,4096)] /\ + ALL (nonoverlapping (res,1024)) + [(word pc,LENGTH mldsa_rej_uniform_eta2_mc); + (word_sub stackpointer (word 576),576)] + ==> ensures arm + (\s. aligned_bytes_loaded s (word pc) mldsa_rej_uniform_eta2_mc /\ + read PC s = word pc /\ + read SP s = stackpointer /\ + read X30 s = returnaddress /\ + C_ARGUMENTS [res;buf;buflen;table] s /\ + read(memory :> bytes(table,4096)) s = + num_of_wordlist mldsa_rej_uniform_eta_table /\ + read(memory :> bytes(buf,val buflen)) s = + num_of_wordlist (inlist:byte list) /\ + read events s = e) + (\s. read PC s = returnaddress /\ + (?e2. + read events s = APPEND e2 e /\ + e2 = f_events res buf buflen table pc stackpointer + returnaddress (REJ_MASK_ETA2 inlist) /\ + memaccess_inbounds e2 + [buf,val buflen; table,4096; + word_sub stackpointer (word 576),576] + [word_sub stackpointer (word 576),576; res,1024])) + (\s s'. T)`, + (* ===================================================================== *) + (* bignum_copy_row_from_table.ml:635-880 (LEFT-leaning lambda association). *) + (* ===================================================================== *) + CONCRETIZE_F_EVENTS_TAC modified_lam THEN + REPEAT META_EXISTS_TAC THEN REPEAT GEN_TAC THEN + REWRITE_TAC[C_ARGUMENTS; NONOVERLAPPING_CLAUSES; ALL; + fst MLDSA_REJ_UNIFORM_ETA2_EXEC] THEN + REPEAT STRIP_TAC THEN + ABBREV_TAC `mask:(bool)list = REJ_MASK_ETA2 inlist` THEN + ENSURES_EVENTS_SEQUENCE_TAC `pc + 0x40` + `\s. read X30 s = returnaddress /\ read X0 s = res /\ read X1 s = buf /\ + read X2 s = buflen /\ read X3 s = table /\ + read SP s = word_sub stackpointer (word 576) /\ + read X7 s = word_sub stackpointer (word 576) /\ + read X8 s = word_sub stackpointer (word 576) /\ + read X11 s = word 0 /\ + read Q30 s = word 77885641318594292392624080437575695 /\ + read Q31 s = word 664619068533544770747334646890102785 /\ + read Q16 s = word 0 /\ + read (memory :> bytes (table,4096)) s = + num_of_wordlist mldsa_rej_uniform_eta_table /\ + read (memory :> bytes (buf,val buflen)) s = num_of_wordlist (inlist:byte list)` THEN + CONJ_TAC THENL [ + GHOST_INTRO_TAC `q31_init:int128` `read Q31` THEN + ENSURES_INIT_TAC "s0" THEN + ARM_STEPS_TAC MLDSA_REJ_UNIFORM_ETA2_EXEC (1--16) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REWRITE_TAC[WORD_INSERT_Q31] THEN + DISCHARGE_SAFETY_PROPERTY_TAC; + ALL_TAC] THEN + ENSURES_EVENTS_WHILE_UP2_TAC `8` `pc + 0x40` `pc + 0x5c` + `\(i:num) s. read SP s = word_sub stackpointer (word 576) /\ + read X30 s = returnaddress /\ read X0 s = res /\ read X1 s = buf /\ + read X2 s = buflen /\ read X3 s = table /\ + read X8 s = word_sub stackpointer (word 576) /\ + read X7 s = word_add (word_sub stackpointer (word 576)) (word (64 * i)) /\ + read X11 s = word (32 * i) /\ + read Q30 s = word 77885641318594292392624080437575695 /\ + read Q31 s = word 664619068533544770747334646890102785 /\ + read Q16 s = word 0 /\ + read (memory :> bytes (table,4096)) s = + num_of_wordlist mldsa_rej_uniform_eta_table /\ + read (memory :> bytes (buf,val buflen)) s = num_of_wordlist (inlist:byte list)` THEN + REPEAT CONJ_TAC THENL [ + ARITH_TAC; + ARM_SIM_TAC ~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC) + ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA2_EXEC (1--0) THEN + REWRITE_TAC[MULT_CLAUSES; WORD_ADD_0] THEN DISCHARGE_SAFETY_PROPERTY_TAC; + REPEAT STRIP_TAC THEN + ARM_SIM_TAC ~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC) + ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA2_EXEC (1--7) THEN + CONJ_TAC THENL + [ASM_SIMP_TAC[ZINIT_BRANCH] THEN REWRITE_TAC[COND_RAND] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN + CONJ_TAC THENL + [REWRITE_TAC[ARITH_RULE `64*(i+1)=64*i+64`] THEN CONV_TAC WORD_RULE; ALL_TAC] THEN + CONJ_TAC THENL + [REWRITE_TAC[ARITH_RULE `32*(i+1)=32*i+32`] THEN CONV_TAC WORD_RULE; ALL_TAC] THEN + DISCHARGE_SAFETY_PROPERTY_TAC; + ONCE_REWRITE_TAC[REASSOC_LOOP8] THEN + ENSURES_EVENTS_WHILE_UP2_TAC `MLDSA_ETA2_LOOP8_TRIP buflen mask` + `pc + 0x70` `pc + 0xfc` loop8_inv_real THEN + REPEAT CONJ_TAC THENL [ + SUBGOAL_THEN `NUM_ACCEPTED(SUB_LIST(0,16 * 0) (mask:(bool)list)) = 0` ASSUME_TAC THENL + [REWRITE_TAC[ARITH_RULE `16 * 0 = 0`; SUB_LIST_CLAUSES; NUM_ACCEPTED; FILTER; LENGTH]; + ALL_TAC] THEN + DISCH_TAC THEN + MP_TAC(CONJUNCT1(SPECL[`buflen:int64`;`mask:(bool)list`] + MLDSA_ETA2_LOOP8_TRIP_MINIMAL)) THEN + ASM_REWRITE_TAC[ARITH_RULE `8 * (0 + 1) = 8`] THEN ASM_ARITH_TAC; + ARM_SIM_TAC ~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC) + ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA2_EXEC (1--5) THEN + REWRITE_TAC[MULT_CLAUSES; SUB_LIST_CLAUSES; NUM_ACCEPTED; FILTER; LENGTH] THEN + REPEAT CONJ_TAC THEN TRY(CONV_TAC WORD_RULE) THEN DISCHARGE_SAFETY_PROPERTY_TAC; + MATCH_MP_TAC MLDSA_ETA2_LOOP8_BODY_ADAPTED THEN ASM_REWRITE_TAC[] THEN + REWRITE_TAC[ALL] THEN REPEAT CONJ_TAC THEN NONOVERLAPPING_TAC; + ONCE_REWRITE_TAC[REASSOC_FCOPY] THEN + ENSURES_EVENTS_WHILE_UP2_TAC `16` `pc + 0x11c` `pc + 0x168` fcopy_inv THEN + REPEAT CONJ_TAC THENL [ + ARITH_TAC; + ARM_SIM_TAC ~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC) + ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA2_EXEC (1--8) THEN + REWRITE_TAC[MULT_CLAUSES; WORD_ADD_0] THEN + REPEAT CONJ_TAC THEN TRY(CONV_TAC WORD_RULE) THEN DISCHARGE_SAFETY_PROPERTY_TAC; + REPEAT STRIP_TAC THEN + ARM_SIM_TAC ~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC) + ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA2_EXEC (1--19) THEN + CONJ_TAC THENL + [ASM_SIMP_TAC[FCOPY_BRANCH] THEN REWRITE_TAC[COND_RAND] THEN + COND_CASES_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN + CONJ_TAC THENL + [REWRITE_TAC[ARITH_RULE `64*(i+1)=64*i+64`; ARITH_RULE `32*(i+1)=32*i+32`; + ARITH_RULE `16*(i+1)=16*i+16`] THEN CONV_TAC WORD_RULE; ALL_TAC] THEN + CONJ_TAC THENL + [REWRITE_TAC[ARITH_RULE `64*(i+1)=64*i+64`; ARITH_RULE `32*(i+1)=32*i+32`; + ARITH_RULE `16*(i+1)=16*i+16`] THEN CONV_TAC WORD_RULE; ALL_TAC] THEN + CONJ_TAC THENL + [REWRITE_TAC[ARITH_RULE `64*(i+1)=64*i+64`; ARITH_RULE `32*(i+1)=32*i+32`; + ARITH_RULE `16*(i+1)=16*i+16`] THEN CONV_TAC WORD_RULE; ALL_TAC] THEN + DISCHARGE_SAFETY_PROPERTY_TAC; + ARM_SIM_TAC ~preprocess_tac:(TRY STRIP_EXISTS_ASSUM_TAC) + ~canonicalize_pc_diff:false MLDSA_REJ_UNIFORM_ETA2_EXEC (1--3) THEN + DISCHARGE_SAFETY_PROPERTY_TAC]]]);;