Skip to content

Commit e6a3e47

Browse files
L-seriesL-series
committed
lint: verify that all expected theorems are present
We add a check to the linting script called check-theorems that ensures that all HOL-Light proofs provide the expected set of theorems depending on the architecture. Signed-off-by: Andreas Hatziiliou <andreas.hatziiliou@savoirfairelinux.com>
1 parent 218124d commit e6a3e47

16 files changed

Lines changed: 339 additions & 265 deletions

‎proofs/hol_light/aarch64/proofs/keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm.ml‎

Lines changed: 30 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -992,7 +992,7 @@ let keccak_f1600_x4_v8a_scalar_mc = define_assert_from_elf
992992
];;
993993
(*** BYTECODE END ***)
994994

995-
let KECCAK_F1600_X4_V8A_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
995+
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x4_v8a_scalar_mc;;
996996

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

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

10081008
(* ------------------------------------------------------------------------- *)
10091009
(* Code length constants *)
@@ -1013,29 +1013,29 @@ let LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC =
10131013
REWRITE_CONV[keccak_f1600_x4_v8a_scalar_mc] `LENGTH keccak_f1600_x4_v8a_scalar_mc`
10141014
|> CONV_RULE (RAND_CONV LENGTH_CONV);;
10151015

1016-
let KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = new_definition
1017-
`KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH = 44`;;
1016+
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH = new_definition
1017+
`KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH = 44`;;
10181018

1019-
let KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = new_definition
1020-
`KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH = 48`;;
1019+
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH = new_definition
1020+
`KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH = 48`;;
10211021

1022-
let KECCAK_F1600_X4_V8A_SCALAR_CORE_START = new_definition
1023-
`KECCAK_F1600_X4_V8A_SCALAR_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH`;;
1022+
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START = new_definition
1023+
`KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START = KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH`;;
10241024

1025-
let KECCAK_F1600_X4_V8A_SCALAR_CORE_END = new_definition
1026-
`KECCAK_F1600_X4_V8A_SCALAR_CORE_END = LENGTH keccak_f1600_x4_v8a_scalar_mc - KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH`;;
1025+
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END = new_definition
1026+
`KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END = LENGTH keccak_f1600_x4_v8a_scalar_mc - KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH`;;
10271027

10281028
let LENGTH_SIMPLIFY_CONV =
10291029
REWRITE_CONV[LENGTH_KECCAK_F1600_X4_V8A_SCALAR_MC;
1030-
KECCAK_F1600_X4_V8A_SCALAR_CORE_START; KECCAK_F1600_X4_V8A_SCALAR_CORE_END;
1031-
KECCAK_F1600_X4_V8A_SCALAR_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_SCALAR_POSTAMBLE_LENGTH] THENC
1030+
KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START; KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END;
1031+
KECCAK_F1600_X4_V8A_SCALAR_HYBRID_PREAMBLE_LENGTH; KECCAK_F1600_X4_V8A_SCALAR_HYBRID_POSTAMBLE_LENGTH] THENC
10321032
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;
10331033

10341034
(* ------------------------------------------------------------------------- *)
10351035
(* Correctness proof *)
10361036
(* ------------------------------------------------------------------------- *)
10371037

1038-
let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
1038+
let KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORRECT = prove
10391039
(`!a rc A1 A2 A3 A4 pc stackpointer.
10401040
aligned 16 stackpointer /\
10411041
nonoverlapping (a,800) (stackpointer,216) /\
@@ -1044,15 +1044,15 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
10441044
[(word pc,LENGTH keccak_f1600_x4_v8a_scalar_mc); (rc,192)]
10451045
==> ensures arm
10461046
(\s. aligned_bytes_loaded s (word pc) keccak_f1600_x4_v8a_scalar_mc /\
1047-
read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_START) /\
1047+
read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_START) /\
10481048
read SP s = stackpointer /\
10491049
C_ARGUMENTS [a; rc] s /\
10501050
wordlist_from_memory(a,25) s = A1 /\
10511051
wordlist_from_memory(word_add a (word 200),25) s = A2 /\
10521052
wordlist_from_memory(word_add a (word 400),25) s = A3 /\
10531053
wordlist_from_memory(word_add a (word 600),25) s = A4 /\
10541054
wordlist_from_memory(rc,24) s = round_constants)
1055-
(\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_CORE_END) /\
1055+
(\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_HYBRID_CORE_END) /\
10561056
wordlist_from_memory(a,25) s = keccak 24 A1 /\
10571057
wordlist_from_memory(word_add a (word 200),25) s =
10581058
keccak 24 A2 /\
@@ -1071,7 +1071,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
10711071
MAP_EVERY X_GEN_TAC
10721072
[`a:int64`; `rc:int64`; `A1:int64 list`; `A2:int64 list`;
10731073
`A3:int64 list`; `A4:int64 list`; `pc:num`; `stackpointer:int64`] THEN
1074-
REWRITE_TAC[fst KECCAK_F1600_X4_V8A_SCALAR_EXEC] THEN
1074+
REWRITE_TAC[fst KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC] THEN
10751075
REWRITE_TAC[MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI; C_ARGUMENTS;
10761076
ALL; ALLPAIRS; NONOVERLAPPING_CLAUSES] THEN
10771077
DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
@@ -1131,7 +1131,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
11311131
MEMORY_128_FROM_64_TAC "a" 0 12 THEN
11321132
MEMORY_128_FROM_64_TAC "a" 200 12 THEN
11331133
ASM_REWRITE_TAC[WORD_ADD_0] THEN REPEAT STRIP_TAC THEN
1134-
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--443) THEN
1134+
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--443) THEN
11351135
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
11361136
[CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN
11371137
CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
@@ -1202,7 +1202,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
12021202
CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[];
12031203
ALL_TAC] THEN
12041204

1205-
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--386) THEN
1205+
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--386) THEN
12061206
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
12071207
REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
12081208
[REWRITE_TAC[GSYM CONJ_ASSOC];
@@ -1240,7 +1240,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
12401240
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
12411241
CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
12421242
CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
1243-
ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC [1] THEN
1243+
ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC [1] THEN
12441244
VAL_INT64_TAC `i:num` THEN
12451245
ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV);
12461246

@@ -1294,7 +1294,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
12941294
ASM_REWRITE_TAC[round_constants; CONS_11; GSYM CONJ_ASSOC] THEN
12951295
REWRITE_TAC[GSYM round_constants] THEN
12961296
ENSURES_INIT_TAC "s0" THEN
1297-
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--442) THEN
1297+
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--442) THEN
12981298

12991299
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
13001300
[CONV_TAC(LAND_CONV WORDLIST_FROM_MEMORY_CONV) THEN
@@ -1369,7 +1369,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
13691369
CONV_TAC(ONCE_DEPTH_CONV EL_CONV) THEN REWRITE_TAC[];
13701370
ALL_TAC] THEN
13711371

1372-
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC (1--386) THEN
1372+
ARM_STEPS_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC (1--386) THEN
13731373
ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN
13741374
REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
13751375
[REWRITE_TAC[GSYM CONJ_ASSOC];
@@ -1409,7 +1409,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
14091409
X_GEN_TAC `i:num` THEN STRIP_TAC THEN
14101410
CONV_TAC(ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV) THEN
14111411
CONV_TAC(ONCE_DEPTH_CONV NORMALIZE_RELATIVE_ADDRESS_CONV) THEN
1412-
ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_EXEC [1] THEN
1412+
ARM_SIM_TAC KECCAK_F1600_X4_V8A_SCALAR_HYBRID_EXEC [1] THEN
14131413
VAL_INT64_TAC `i:num` THEN
14141414
ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV WORD_NUM_RED_CONV);
14151415

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

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

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

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

0 commit comments

Comments
 (0)