Skip to content

Commit f8138ef

Browse files
author
Ubuntu
committed
Address review: rename files, move specs, remove aliases, add aarch64_utils dep
- Rename {.S,.ml} to poly_use_hint_{32,88}_aarch64_asm for PR #1058 consolidation - Move mldsa_use_hint_{32,88}_spec to common/mldsa_specs.ml for x86 sharing - Remove pointless IVAL_SMALL/VAL_IWORD_NUM aliases; use actual names - Add aarch64_utils.ml to CI needs for both proofs - Align comment style between _32 and _88 spec definitions - Update Makefile, dump_bytecode, subroutine_signatures, README Signed-off-by: Jake Massimo <jakemas@amazon.com>
1 parent 2f0dd55 commit f8138ef

10 files changed

Lines changed: 103 additions & 113 deletions

‎.github/workflows/hol_light.yml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -95,10 +95,10 @@ jobs:
9595
needs: ["aarch64_utils.ml"]
9696
- name: mldsa_poly_chknorm
9797
needs: ["aarch64_utils.ml"]
98-
- name: mldsa_poly_use_hint_32
99-
needs: ["mldsa_specs.ml", "subroutine_signatures.ml"]
100-
- name: mldsa_poly_use_hint_88
101-
needs: ["mldsa_specs.ml", "subroutine_signatures.ml"]
98+
- name: poly_use_hint_32_aarch64_asm
99+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
100+
- name: poly_use_hint_88_aarch64_asm
101+
needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
102102
- name: keccak_f1600_x1_scalar
103103
needs: ["keccak_spec.ml"]
104104
- name: keccak_f1600_x1_v84a

‎proofs/hol_light/README.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,8 +54,8 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
5454
- ML-DSA Arithmetic:
5555
* AArch64 poly_caddq: [mldsa_poly_caddq.S](aarch64/mldsa/mldsa_poly_caddq.S)
5656
* AArch64 poly_chknorm: [mldsa_poly_chknorm.S](aarch64/mldsa/mldsa_poly_chknorm.S)
57-
* AArch64 poly_use_hint (l=5,7): [mldsa_poly_use_hint_32.S](aarch64/mldsa/mldsa_poly_use_hint_32.S)
58-
* AArch64 poly_use_hint (l=4): [mldsa_poly_use_hint_88.S](aarch64/mldsa/mldsa_poly_use_hint_88.S)
57+
* AArch64 poly_use_hint (l=5,7): [poly_use_hint_32_aarch64_asm.S](aarch64/mldsa/poly_use_hint_32_aarch64_asm.S)
58+
* AArch64 poly_use_hint (l=4): [poly_use_hint_88_aarch64_asm.S](aarch64/mldsa/poly_use_hint_88_aarch64_asm.S)
5959
* AArch64 pointwise multiplication: [mldsa_pointwise.S](aarch64/mldsa/mldsa_pointwise.S)
6060
* AArch64 pointwise multiplication-accumulation (l=4): [mldsa_pointwise_acc_l4.S](aarch64/mldsa/mldsa_pointwise_acc_l4.S)
6161
* AArch64 pointwise multiplication-accumulation (l=5): [mldsa_pointwise_acc_l5.S](aarch64/mldsa/mldsa_pointwise_acc_l5.S)

‎proofs/hol_light/aarch64/Makefile‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,8 +57,8 @@ OBJ = mldsa/mldsa_ntt.o \
5757
mldsa/mldsa_pointwise.o \
5858
mldsa/mldsa_poly_caddq.o \
5959
mldsa/mldsa_poly_chknorm.o \
60-
mldsa/mldsa_poly_use_hint_32.o \
61-
mldsa/mldsa_poly_use_hint_88.o \
60+
mldsa/poly_use_hint_32_aarch64_asm.o \
61+
mldsa/poly_use_hint_88_aarch64_asm.o \
6262
mldsa/mldsa_pointwise_acc_l4.o \
6363
mldsa/mldsa_pointwise_acc_l5.o \
6464
mldsa/mldsa_pointwise_acc_l7.o \

proofs/hol_light/aarch64/mldsa/mldsa_poly_use_hint_32.S renamed to proofs/hol_light/aarch64/mldsa/poly_use_hint_32_aarch64_asm.S

File renamed without changes.

proofs/hol_light/aarch64/mldsa/mldsa_poly_use_hint_88.S renamed to proofs/hol_light/aarch64/mldsa/poly_use_hint_88_aarch64_asm.S

File renamed without changes.

‎proofs/hol_light/aarch64/proofs/dump_bytecode.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,12 @@ print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_caddq.o ===\n";;
3030
print_literal_from_elf "aarch64/mldsa/mldsa_poly_caddq.o";;
3131
print_string "==== bytecode end =====================================\n\n";;
3232

33-
print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_use_hint_32.o ===\n";;
34-
print_literal_from_elf "aarch64/mldsa/mldsa_poly_use_hint_32.o";;
33+
print_string "=== bytecode start: aarch64/mldsa/poly_use_hint_32_aarch64_asm.o ===\n";;
34+
print_literal_from_elf "aarch64/mldsa/poly_use_hint_32_aarch64_asm.o";;
3535
print_string "==== bytecode end =====================================\n\n";;
3636

37-
print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_use_hint_88.o ===\n";;
38-
print_literal_from_elf "aarch64/mldsa/mldsa_poly_use_hint_88.o";;
37+
print_string "=== bytecode start: aarch64/mldsa/poly_use_hint_88_aarch64_asm.o ===\n";;
38+
print_literal_from_elf "aarch64/mldsa/poly_use_hint_88_aarch64_asm.o";;
3939
print_string "==== bytecode end =====================================\n\n";;
4040

4141
print_string "=== bytecode start: aarch64/mldsa/mldsa_poly_chknorm.o ===\n";;

proofs/hol_light/aarch64/proofs/mldsa_poly_use_hint_32.ml renamed to proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml

Lines changed: 27 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,11 @@ needs "common/mldsa_specs.ml";;
1313
needs "aarch64/proofs/aarch64_utils.ml";;
1414

1515

16-
(**** print_literal_from_elf "aarch64/mldsa/mldsa_poly_use_hint_32.o";;
16+
(**** print_literal_from_elf "aarch64/mldsa/poly_use_hint_32_aarch64_asm.o";;
1717
****)
1818

19-
let mldsa_poly_use_hint_32_mc = define_assert_from_elf
20-
"mldsa_poly_use_hint_32_mc" "aarch64/mldsa/mldsa_poly_use_hint_32.o"
19+
let poly_use_hint_32_aarch64_asm_mc = define_assert_from_elf
20+
"poly_use_hint_32_aarch64_asm_mc" "aarch64/mldsa/poly_use_hint_32_aarch64_asm.o"
2121
(*** BYTECODE START ***)
2222
[
2323
0x529c0024; (* arm_MOV W4 (rvalue (word 57345)) *)
@@ -92,32 +92,7 @@ let mldsa_poly_use_hint_32_mc = define_assert_from_elf
9292
];;
9393
(*** BYTECODE END ***)
9494

95-
let MLDSA_USE_HINT_EXEC = ARM_MK_EXEC_RULE mldsa_poly_use_hint_32_mc;;
96-
97-
(* ========================================================================= *)
98-
(* Functional specification: UseHint for ML-DSA parameter sets 65/87 *)
99-
(* *)
100-
(* Constants: *)
101-
(* Q = 8380417 *)
102-
(* GAMMA2 = (Q-1)/32 = 261888 *)
103-
(* 2*GAMMA2 = 523776 *)
104-
(* Output range: [0, 15] *)
105-
(* *)
106-
(* This is the per-coefficient UseHint function from FIPS 204 Algorithm 38: *)
107-
(* 1. decompose: a1 = round_half_down(a / 523776), a0 = a - a1*523776 *)
108-
(* 2. if hint=0: return a1 mod 16 *)
109-
(* 3. if a0 > 0: return (a1 + 1) mod 16 *)
110-
(* 4. if a0 <= 0: return (a1 - 1) mod 16 *)
111-
(* ========================================================================= *)
112-
113-
let mldsa_use_hint_32_spec = new_definition
114-
`mldsa_use_hint_32_spec (a:num) (h:num) =
115-
let a1 = ((((a + 127) DIV 128) * 1025 + 2097152) DIV 4194304) MOD 16 in
116-
let a0:int = &a - &a1 * &523776 in
117-
let a0' = if a0 > &4190208 then a0 - &8380417 else a0 in
118-
if h = 0 then a1
119-
else if a0' > &0 then (a1 + 1) MOD 16
120-
else (a1 + 15) MOD 16`;;
95+
let POLY_USE_HINT_32_AARCH64_ASM_EXEC = ARM_MK_EXEC_RULE poly_use_hint_32_aarch64_asm_mc;;
12196

12297
(* Per-element word function matching the assembly computation *)
12398
let mldsa_use_hint_32_asm = new_definition
@@ -133,16 +108,13 @@ let mldsa_use_hint_32_asm = new_definition
133108
(* Functional correctness helper lemmas *)
134109
(* ========================================================================= *)
135110

136-
let IVAL_SMALL = MLDSA_IVAL_VAL;;
137-
let VAL_IWORD_NUM = VAL_IWORD_NUM_32;;
138-
139111
let WORD_2SMULH_NOSATURATE_32 = prove(
140112
`!a:int32. val a < 8380417
141113
==> word_2smulh a (word 1074791425:int32) : int32 =
142114
iword((&2 * &(val a) * &1074791425) div &2 pow 32)`,
143115
GEN_TAC THEN DISCH_TAC THEN
144116
REWRITE_TAC[word_2smulh; DIMINDEX_32] THEN
145-
ASM_SIMP_TAC[IVAL_SMALL] THEN
117+
ASM_SIMP_TAC[MLDSA_IVAL_VAL] THEN
146118
CONV_TAC WORD_REDUCE_CONV THEN
147119
REWRITE_TAC[iword_saturate; word_INT_MIN; word_INT_MAX; DIMINDEX_32] THEN
148120
CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC WORD_REDUCE_CONV THEN
@@ -172,11 +144,11 @@ let VAL_DECOMPOSE_A1 = prove(
172144
[MATCH_MP_TAC(ARITH_RULE `x <= y ==> x < y + 1`) THEN
173145
MATCH_MP_TAC DIV_MONO THEN ASM_ARITH_TAC; CONV_TAC NUM_REDUCE_CONV]; ALL_TAC] THEN
174146
REWRITE_TAC[INT_OF_NUM_CLAUSES] THEN SIMP_TAC[INT_OF_NUM_DIV] THEN
175-
CONV_TAC NUM_REDUCE_CONV THEN ASM_SIMP_TAC[VAL_IWORD_NUM] THEN
147+
CONV_TAC NUM_REDUCE_CONV THEN ASM_SIMP_TAC[VAL_IWORD_NUM_32] THEN
176148
ABBREV_TAC `t:int32 = iword(&((2 * val(a:int32) * 1074791425) DIV 4294967296))` THEN
177149
SUBGOAL_THEN `val(t:int32) = (2 * val(a:int32) * 1074791425) DIV 4294967296`
178150
ASSUME_TAC THENL
179-
[EXPAND_TAC "t" THEN MATCH_MP_TAC VAL_IWORD_NUM THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
151+
[EXPAND_TAC "t" THEN MATCH_MP_TAC VAL_IWORD_NUM_32 THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
180152
SUBGOAL_THEN `val(t:int32) < 2147483648` ASSUME_TAC THENL
181153
[ASM_REWRITE_TAC[]; ALL_TAC] THEN
182154
REWRITE_TAC[word_ishr_round] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC INT_REDUCE_CONV THEN
@@ -190,7 +162,7 @@ let VAL_DECOMPOSE_A1 = prove(
190162
TRANS_TAC LT_TRANS `(4194303 + 131072) DIV 262144 + 1` THEN CONJ_TAC THENL
191163
[MATCH_MP_TAC(ARITH_RULE `x <= y ==> x < y + 1`) THEN
192164
MATCH_MP_TAC DIV_MONO THEN ASM_ARITH_TAC; CONV_TAC NUM_REDUCE_CONV]; ALL_TAC] THEN
193-
ASM_SIMP_TAC[VAL_IWORD_NUM] THEN MATCH_MP_TAC VAL_IWORD_NUM THEN
165+
ASM_SIMP_TAC[VAL_IWORD_NUM_32] THEN MATCH_MP_TAC VAL_IWORD_NUM_32 THEN
194166
UNDISCH_THEN `val(t:int32) = (2 * val(a:int32) * 1074791425) DIV 4294967296`
195167
(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[]);;
196168

@@ -427,13 +399,13 @@ let ELEMENT_CORRECT_WORD = prove(
427399
(* Correctness proof (output bounds) *)
428400
(* ========================================================================= *)
429401

430-
let MLDSA_USE_HINT_CORRECT = prove
402+
let POLY_USE_HINT_32_AARCH64_ASM_CORRECT = prove
431403
(`!b a h x y pc.
432-
nonoverlapping (word pc, LENGTH mldsa_poly_use_hint_32_mc) (b, 1024) /\
404+
nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (b, 1024) /\
433405
nonoverlapping (b, 1024) (a, 1024) /\
434406
nonoverlapping (b, 1024) (h, 1024)
435407
==> ensures arm
436-
(\s. aligned_bytes_loaded s (word pc) mldsa_poly_use_hint_32_mc /\
408+
(\s. aligned_bytes_loaded s (word pc) poly_use_hint_32_aarch64_asm_mc /\
437409
read PC s = word pc /\
438410
C_ARGUMENTS [b; a; h] s /\
439411
(!i. i < 256 ==> val(x i) < 8380417) /\
@@ -455,7 +427,7 @@ let MLDSA_USE_HINT_CORRECT = prove
455427
`x:num->int32`; `y:num->int32`; `pc:num`] THEN
456428
REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
457429
NONOVERLAPPING_CLAUSES; ALL;
458-
fst MLDSA_USE_HINT_EXEC] THEN
430+
fst POLY_USE_HINT_32_AARCH64_ASM_EXEC] THEN
459431
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
460432
GLOBALIZE_PRECONDITION_TAC THEN
461433
CONV_TAC(RATOR_CONV(LAND_CONV(ONCE_DEPTH_CONV EXPAND_CASES_CONV))) THEN
@@ -474,7 +446,7 @@ let MLDSA_USE_HINT_CORRECT = prove
474446
DISCARD_MATCHING_ASSUMPTIONS [`read (memory :> bytes32 a) s = x`] THEN
475447

476448
(* Simulate 878 instructions (excluding RET) *)
477-
MAP_EVERY (fun n -> ARM_STEPS_TAC MLDSA_USE_HINT_EXEC [n] THEN
449+
MAP_EVERY (fun n -> ARM_STEPS_TAC POLY_USE_HINT_32_AARCH64_ASM_EXEC [n] THEN
478450
SIMD_SIMPLIFY_TAC[])
479451
(1--878) THEN
480452
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
@@ -519,13 +491,13 @@ let MLDSA_USE_HINT_CORRECT = prove
519491
(* Subroutine form *)
520492
(* ========================================================================= *)
521493

522-
let MLDSA_USE_HINT_SUBROUTINE_CORRECT = prove
494+
let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT = prove
523495
(`!b a h x y pc returnaddress.
524-
nonoverlapping (word pc, LENGTH mldsa_poly_use_hint_32_mc) (b, 1024) /\
496+
nonoverlapping (word pc, LENGTH poly_use_hint_32_aarch64_asm_mc) (b, 1024) /\
525497
nonoverlapping (b, 1024) (a, 1024) /\
526498
nonoverlapping (b, 1024) (h, 1024)
527499
==> ensures arm
528-
(\s. aligned_bytes_loaded s (word pc) mldsa_poly_use_hint_32_mc /\
500+
(\s. aligned_bytes_loaded s (word pc) poly_use_hint_32_aarch64_asm_mc /\
529501
read PC s = word pc /\
530502
read X30 s = returnaddress /\
531503
C_ARGUMENTS [b; a; h] s /\
@@ -541,10 +513,10 @@ let MLDSA_USE_HINT_SUBROUTINE_CORRECT = prove
541513
word(mldsa_use_hint_32_spec (val(x i)) (val(y i)))))
542514
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
543515
MAYCHANGE [memory :> bytes(b, 1024)])`,
544-
REWRITE_TAC[fst MLDSA_USE_HINT_EXEC] THEN
545-
ARM_ADD_RETURN_NOSTACK_TAC MLDSA_USE_HINT_EXEC
546-
(REWRITE_RULE[fst MLDSA_USE_HINT_EXEC]
547-
MLDSA_USE_HINT_CORRECT));;
516+
REWRITE_TAC[fst POLY_USE_HINT_32_AARCH64_ASM_EXEC] THEN
517+
ARM_ADD_RETURN_NOSTACK_TAC POLY_USE_HINT_32_AARCH64_ASM_EXEC
518+
(REWRITE_RULE[fst POLY_USE_HINT_32_AARCH64_ASM_EXEC]
519+
POLY_USE_HINT_32_AARCH64_ASM_CORRECT));;
548520

549521

550522
(* ========================================================================= *)
@@ -557,20 +529,20 @@ needs "aarch64/proofs/subroutine_signatures.ml";;
557529

558530
let full_spec,public_vars = mk_safety_spec
559531
~keep_maychanges:false
560-
(assoc "mldsa_poly_use_hint_32" subroutine_signatures)
561-
MLDSA_USE_HINT_SUBROUTINE_CORRECT
562-
MLDSA_USE_HINT_EXEC;;
532+
(assoc "poly_use_hint_32_aarch64_asm" subroutine_signatures)
533+
POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_CORRECT
534+
POLY_USE_HINT_32_AARCH64_ASM_EXEC;;
563535

564-
let MLDSA_USE_HINT_SUBROUTINE_SAFE = time prove
536+
let POLY_USE_HINT_32_AARCH64_ASM_SUBROUTINE_SAFE = time prove
565537
(`exists f_events.
566538
forall e b a h pc returnaddress.
567-
nonoverlapping (word pc,LENGTH mldsa_poly_use_hint_32_mc) (b,1024) /\
539+
nonoverlapping (word pc,LENGTH poly_use_hint_32_aarch64_asm_mc) (b,1024) /\
568540
nonoverlapping (b,1024) (a,1024) /\
569541
nonoverlapping (b,1024) (h,1024)
570542
==> ensures arm
571543
(\s.
572544
aligned_bytes_loaded s (word pc)
573-
mldsa_poly_use_hint_32_mc /\
545+
poly_use_hint_32_aarch64_asm_mc /\
574546
read PC s = word pc /\
575547
read X30 s = returnaddress /\
576548
C_ARGUMENTS [b; a; h] s /\
@@ -584,4 +556,4 @@ let MLDSA_USE_HINT_SUBROUTINE_SAFE = time prove
584556
[b,1024]))
585557
(\s s'. true)`,
586558
ASSERT_CONCL_TAC full_spec THEN
587-
PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars MLDSA_USE_HINT_EXEC);;
559+
PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars POLY_USE_HINT_32_AARCH64_ASM_EXEC);;

0 commit comments

Comments
 (0)