Skip to content

HOL-Light: improve tooling and CI #1634

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Open
L-series wants to merge 2 commits into
base: main
Choose a base branch
from
Open

HOL-Light: improve tooling and CI #1634

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
218124d
testing: HOL-Light: add support for cross-proofing
L-series Mar 20, 2026
e6a3e47
lint: verify that all expected theorems are present
L-series Mar 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 30 additions & 30 deletions proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -992,7 +992,7 @@ let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf
];;
(*** BYTECODE END ***)

let KECCAK_F1600_X4_V8A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;

(*** Additional lazy/deferred rotations in the implementation, row-major ***)

Expand All @@ -1003,7 +1003,7 @@ let deferred_rotates = define
25; 8; 18; 1; 6;
10; 15; 56; 27; 36;
39; 41; 2; 62; 55]`;;
let KECCAK_F1600_X4_V8A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;

(* ------------------------------------------------------------------------- *)
(* Code length constants *)
Expand All @@ -1013,29 +1013,29 @@ let LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC =
REWRITE_CONV[keccak_f1600_x4_v8a_scalar_mc] `LENGTH keccak_f1600_x4_v8a_scalar_mc`
|> CONV_RULE (RAND_CONV LENGTH_CONV);;

let KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = 44`;;
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH = 44`;;

let KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = 48`;;
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH = 48`;;

let KECCAK_F1600_X4_V8A_SCALAR_CORE_START = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH`;;
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH`;;

let KECCAK_F1600_X4_V8A_SCALAR_CORE_END = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_CORE_END = LENGTH keccak_f1600_x4_v8a_scalar_mc - KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH`;;
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END = LENGTH keccak_f1600_x4_v8a_scalar_mc - KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH`;;

let LENGTH_SIMPLIFY_CONV =
REWRITE_CONV[LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC;
KECCAK_F1600_X4_V8A_SCALAR_CORE_START; KECCAK_F1600_X4_V8A_SCALAR_CORE_END;
KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH] THENC
KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START; KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END;
KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH] THENC
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;

(* ------------------------------------------------------------------------- *)
(* Correctness proof *)
(* ------------------------------------------------------------------------- *)

let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT = prove
(`!a rc A1 A2 A3 A4 pc stackpointer.
aligned 16 stackpointer /\
nonoverlapping (a,800) (stackpointer,216) /\
Expand All @@ -1044,15 +1044,15 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
[(word pc,LENGTH keccak_f1600_x4_v8a_scalar_mc); (rc,192)]
==> ensures arm
(\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_scalar_mc /\
read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_START) /\
read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START) /\
read SP s = stackpointer /\
C_ARGUMENTS [a; rc] s /\
wordlist_from_memory(a,25) s = A1 /\
wordlist_from_memory(word_add a (word 200),25) s = A2 /\
wordlist_from_memory(word_add a (word 400),25) s = A3 /\
wordlist_from_memory(word_add a (word 600),25) s = A4 /\
wordlist_from_memory(rc,24) s = round_constants)
(\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_END) /\
(\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END) /\
wordlist_from_memory(a,25) s = keccak 24 A1 /\
wordlist_from_memory(word_add a (word 200),25) s =
keccak 24 A2 /\
Expand All @@ -1071,7 +1071,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
MAP_EVERY X_GEN_TAC
[`a:int64`; `rc:int64`; `A1:int64 list`; `A2:int64 list`;
`A3:int64 list`; `A4:int64 list`; `pc:num`; `stackpointer:int64`] THEN
REWRITE_TAC[fst KECCAK_F1600_X4_V8A_SCALAR_EXEC] THEN
REWRITE_TAC[fst KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC] THEN
REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
ALL; ALLPAIRS; NONOVERLAPPING_CLAUSES] THEN
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
Expand Down Expand Up @@ -1131,7 +1131,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
MEMORY_128_FROM_64_TAC "a" 0 12 THEN
MEMORY_128_FROM_64_TAC "a" 200 12 THEN
ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--443) THEN
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--443) THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN
CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
Expand Down Expand Up @@ -1202,7 +1202,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[];
ALL_TAC] THEN

ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--386) THEN
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--386) THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
[REWRITE_TAC[GSYM CONJ_ASSOC];
Expand Down Expand Up @@ -1240,7 +1240,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC [1] THEN
ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC [1] THEN
VAL_INT64_TAC `i:num` THEN
ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV);

Expand Down Expand Up @@ -1294,7 +1294,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN
REWRITE_TAC[GSYM round_constants] THEN
ENSURES_INIT_TAC "s0" THEN
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--442) THEN
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--442) THEN

ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
[CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN
Expand Down Expand Up @@ -1369,7 +1369,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[];
ALL_TAC] THEN

ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--386) THEN
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--386) THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
[REWRITE_TAC[GSYM CONJ_ASSOC];
Expand Down Expand Up @@ -1409,7 +1409,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC [1] THEN
ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC [1] THEN
VAL_INT64_TAC `i:num` THEN
ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV);

Expand All @@ -1433,7 +1433,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN
REWRITE_TAC[GSYM round_constants] THEN
ENSURES_INIT_TAC "s0" THEN
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--83) THEN
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--83) THEN
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
Expand All @@ -1448,7 +1448,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
(* NOTE: This must be kept in sync with the CBMC specification
* in mlkem/src/fips202/native/aarch64/src/fips202_native_aarch64.h *)

let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_CORRECT = prove
(`!a rc A1 A2 A3 A4 pc stackpointer returnaddress.
aligned 16 stackpointer /\
nonoverlapping (a,800) (word_sub stackpointer (word 224),224) /\
Expand Down Expand Up @@ -1483,8 +1483,8 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove
(WORDLIST_FROM_MEMORY_CONV THENC
ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) in
CONV_TAC TWEAK_CONV THEN
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_SCALAR_EXEC
(CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_CORRECT))
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(11,11) KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC
(CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT))
`[D8; D9; D10; D11; D12; D13; D14; D15;
X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);;

Expand All @@ -1498,10 +1498,10 @@ needs "mlkem_native/aarch64/proofs/subroutine_signatures.ml";;
let full_spec,public_vars = mk_safety_spec
~keep_maychanges:false
(assoc "sha3_keccak4_f1600" subroutine_signatures)
KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT
KECCAK_F1600_X4_V8A_SCALAR_EXEC;;
KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_CORRECT
KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC;;

let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_SAFE = time prove
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_SUBROUTINE_SAFE = time prove
(`exists f_events.
forall e a rc pc stackpointer returnaddress.
aligned 16 stackpointer /\
Expand Down Expand Up @@ -1530,4 +1530,4 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_SAFE = time prove
[a,800; word_sub stackpointer (word 224),224])
(\s s'. true)`,
ASSERT_CONCL_TAC full_spec THEN
PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_SCALAR_EXEC);;
PROVE_SAFETY_SPEC_TAC ~public_vars:public_vars KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC);;
Loading
Loading