Skip to content

HOL-Light: Avoid hardcoded lengths in HOL-Light proof scripts #1218

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

Merged
merged 1 commit into from
Oct 7, 2025
Merged

HOL-Light: Avoid hardcoded lengths in HOL-Light proof scripts #1218

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
38 changes: 33 additions & 5 deletions proofs/hol_light/arm/proofs/keccak_f1600_x1_scalar.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -310,6 +310,32 @@ let keccak_f1600_x1_scalar_mc = define_assert_from_elf

let KECCAK_F1600_X1_SCALAR_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x1_scalar_mc;;

(* ------------------------------------------------------------------------- *)
(* Code length constants *)
(* ------------------------------------------------------------------------- *)

let LENGTH_KECCAK_F1600_X1_SCALAR_MC =
REWRITE_CONV[keccak_f1600_x1_scalar_mc] `LENGTH keccak_f1600_x1_scalar_mc`
|> CONV_RULE (RAND_CONV LENGTH_CONV);;

let KECCAK_F1600_X1_SCALAR_PREAMBLE_LENGTH = new_definition
`KECCAK_F1600_X1_SCALAR_PREAMBLE_LENGTH = 28`;;

let KECCAK_F1600_X1_SCALAR_POSTAMBLE_LENGTH = new_definition
`KECCAK_F1600_X1_SCALAR_POSTAMBLE_LENGTH = 32`;;

let KECCAK_F1600_X1_SCALAR_CORE_START = new_definition
`KECCAK_F1600_X1_SCALAR_CORE_START = KECCAK_F1600_X1_SCALAR_PREAMBLE_LENGTH`;;

let KECCAK_F1600_X1_SCALAR_CORE_END = new_definition
`KECCAK_F1600_X1_SCALAR_CORE_END = LENGTH keccak_f1600_x1_scalar_mc - KECCAK_F1600_X1_SCALAR_POSTAMBLE_LENGTH`;;

let LENGTH_SIMPLIFY_CONV =
REWRITE_CONV[LENGTH_KECCAK_F1600_X1_SCALAR_MC;
KECCAK_F1600_X1_SCALAR_CORE_START; KECCAK_F1600_X1_SCALAR_CORE_END;
KECCAK_F1600_X1_SCALAR_PREAMBLE_LENGTH; KECCAK_F1600_X1_SCALAR_POSTAMBLE_LENGTH] THENC
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;

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

let deferred_rotates = define
Expand Down Expand Up @@ -339,21 +365,22 @@ let KECCAK_F1600_X1_SCALAR_CORRECT = prove
nonoverlapping (a,200) (stackpointer,32) /\
ALLPAIRS nonoverlapping
[(a,200); (stackpointer,32)]
[(word pc,0x480); (rc,192)]
[(word pc,LENGTH keccak_f1600_x1_scalar_mc); (rc,192)]
==> ensures arm
(\s. aligned_bytes_loaded s (word pc) keccak_f1600_x1_scalar_mc /\
read PC s = word (pc + 0x1c) /\
read PC s = word (pc + KECCAK_F1600_X1_SCALAR_CORE_START) /\
read SP s = stackpointer /\
C_ARGUMENTS [a; rc] s /\
wordlist_from_memory(a,25) s = A /\
wordlist_from_memory(rc,24) s = round_constants)
(\s. read PC s = word(pc + 0x460) /\
(\s. read PC s = word(pc + KECCAK_F1600_X1_SCALAR_CORE_END) /\
wordlist_from_memory(a,25) s = keccak 24 A)
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
MAYCHANGE [X19; X20; X21; X22; X23; X24;
X25; X26; X27; X28; X29; X30] ,,
MAYCHANGE [memory :> bytes(a,200);
memory :> bytes(stackpointer,32)])`,
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
MAP_EVERY X_GEN_TAC
[`a:int64`; `rc:int64`; `A:int64 list`; `pc:num`; `stackpointer:int64`] THEN
REWRITE_TAC[fst KECCAK_F1600_X1_SCALAR_EXEC] THEN
Expand Down Expand Up @@ -461,7 +488,7 @@ let KECCAK_F1600_X1_SCALAR_SUBROUTINE_CORRECT = prove
nonoverlapping (a,200) (word_sub stackpointer (word 128),128) /\
ALLPAIRS nonoverlapping
[(a,200); (word_sub stackpointer (word 128),128)]
[(word pc,0x480); (rc,192)]
[(word pc,LENGTH keccak_f1600_x1_scalar_mc); (rc,192)]
==> ensures arm
(\s. aligned_bytes_loaded s (word pc) keccak_f1600_x1_scalar_mc /\
read PC s = word pc /\
Expand All @@ -475,8 +502,9 @@ let KECCAK_F1600_X1_SCALAR_SUBROUTINE_CORRECT = prove
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
MAYCHANGE [memory :> bytes(a,200);
memory :> bytes(word_sub stackpointer (word 128),128)])`,
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in
CONV_TAC TWEAK_CONV THEN
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(7,7) KECCAK_F1600_X1_SCALAR_EXEC
(CONV_RULE TWEAK_CONV KECCAK_F1600_X1_SCALAR_CORRECT)
(CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X1_SCALAR_CORRECT))
`[X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 128);;
38 changes: 33 additions & 5 deletions proofs/hol_light/arm/proofs/keccak_f1600_x1_v84a.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,32 @@ let keccak_f1600_x1_v84a_mc = define_assert_from_elf

let KECCAK_F1600_X1_V84A_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x1_v84a_mc;;

(* ------------------------------------------------------------------------- *)
(* Code length constants *)
(* ------------------------------------------------------------------------- *)

let LENGTH_KECCAK_F1600_X1_V84A_MC =
REWRITE_CONV[keccak_f1600_x1_v84a_mc] `LENGTH keccak_f1600_x1_v84a_mc`
|> CONV_RULE (RAND_CONV LENGTH_CONV);;

let KECCAK_F1600_X1_V84A_PREAMBLE_LENGTH = new_definition
`KECCAK_F1600_X1_V84A_PREAMBLE_LENGTH = 20`;;

let KECCAK_F1600_X1_V84A_POSTAMBLE_LENGTH = new_definition
`KECCAK_F1600_X1_V84A_POSTAMBLE_LENGTH = 24`;;

let KECCAK_F1600_X1_V84A_CORE_START = new_definition
`KECCAK_F1600_X1_V84A_CORE_START = KECCAK_F1600_X1_V84A_PREAMBLE_LENGTH`;;

let KECCAK_F1600_X1_V84A_CORE_END = new_definition
`KECCAK_F1600_X1_V84A_CORE_END = LENGTH keccak_f1600_x1_v84a_mc - KECCAK_F1600_X1_V84A_POSTAMBLE_LENGTH`;;

let LENGTH_SIMPLIFY_CONV =
REWRITE_CONV[LENGTH_KECCAK_F1600_X1_V84A_MC;
KECCAK_F1600_X1_V84A_CORE_START; KECCAK_F1600_X1_V84A_CORE_END;
KECCAK_F1600_X1_V84A_PREAMBLE_LENGTH; KECCAK_F1600_X1_V84A_POSTAMBLE_LENGTH] THENC
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;

(*** Introduce ghost variables for Qn given Dn register reads in a list ***)

let GHOST_SUBREGLIST_TAC =
Expand All @@ -144,18 +170,19 @@ let GHOST_SUBREGLIST_TAC =

let KECCAK_F1600_X1_V84A_CORRECT = prove
(`!a rc A pc.
ALL (nonoverlapping (a,200)) [(word pc,0x1ac); (rc,192)]
ALL (nonoverlapping (a,200)) [(word pc,LENGTH keccak_f1600_x1_v84a_mc); (rc,192)]
==> ensures arm
(\s. aligned_bytes_loaded s (word pc) keccak_f1600_x1_v84a_mc /\
read PC s = word (pc + 0x14) /\
read PC s = word (pc + KECCAK_F1600_X1_V84A_CORE_START) /\
C_ARGUMENTS [a; rc] s /\
wordlist_from_memory(a,25) s = A /\
wordlist_from_memory(rc,24) s = round_constants)
(\s. read PC s = word(pc + 0x194) /\
(\s. read PC s = word(pc + KECCAK_F1600_X1_V84A_CORE_END) /\
wordlist_from_memory(a,25) s = keccak 24 A)
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,,
MAYCHANGE [memory :> bytes(a,200)])`,
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
MAP_EVERY X_GEN_TAC
[`a:int64`; `rc:int64`; `A:int64 list`; `pc:num`] THEN
REWRITE_TAC[fst KECCAK_F1600_X1_V84A_EXEC] THEN
Expand Down Expand Up @@ -246,7 +273,7 @@ let KECCAK_F1600_X1_V84A_SUBROUTINE_CORRECT = prove
nonoverlapping (a,200) (word_sub stackpointer (word 64),64) /\
ALLPAIRS nonoverlapping
[(a,200); (word_sub stackpointer (word 64),64)]
[(word pc,0x1ac); (rc,192)]
[(word pc,LENGTH keccak_f1600_x1_v84a_mc); (rc,192)]
==> ensures arm
(\s. aligned_bytes_loaded s (word pc) keccak_f1600_x1_v84a_mc /\
read PC s = word pc /\
Expand All @@ -260,8 +287,9 @@ let KECCAK_F1600_X1_V84A_SUBROUTINE_CORRECT = prove
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
MAYCHANGE [memory :> bytes(a,200);
memory :> bytes(word_sub stackpointer (word 64),64)])`,
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
let TWEAK_CONV = ONCE_DEPTH_CONV WORDLIST_FROM_MEMORY_CONV in
CONV_TAC TWEAK_CONV THEN
ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(5,5) KECCAK_F1600_X1_V84A_EXEC
(CONV_RULE TWEAK_CONV KECCAK_F1600_X1_V84A_CORRECT)
(CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X1_V84A_CORRECT))
`[D8; D9; D10; D11; D12; D13; D14; D15]` 64);;
40 changes: 35 additions & 5 deletions proofs/hol_light/arm/proofs/keccak_f1600_x2_v84a.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,26 +183,55 @@ let keccak_f1600_x2_v84a_mc = define_assert_from_elf

let KECCAK_F1600_X2_V84A_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x2_v84a_mc;;

(* ------------------------------------------------------------------------- *)
(* Code length constants *)
(* ------------------------------------------------------------------------- *)

let LENGTH_KECCAK_F1600_X2_V84A_MC =
REWRITE_CONV[keccak_f1600_x2_v84a_mc] `LENGTH keccak_f1600_x2_v84a_mc`
|> CONV_RULE (RAND_CONV LENGTH_CONV);;

let KECCAK_F1600_X2_V84A_PREAMBLE_LENGTH = new_definition
`KECCAK_F1600_X2_V84A_PREAMBLE_LENGTH = 20`;;

let KECCAK_F1600_X2_V84A_POSTAMBLE_LENGTH = new_definition
`KECCAK_F1600_X2_V84A_POSTAMBLE_LENGTH = 24`;;

let KECCAK_F1600_X2_V84A_CORE_START = new_definition
`KECCAK_F1600_X2_V84A_CORE_START = KECCAK_F1600_X2_V84A_PREAMBLE_LENGTH`;;

let KECCAK_F1600_X2_V84A_CORE_END = new_definition
`KECCAK_F1600_X2_V84A_CORE_END = LENGTH keccak_f1600_x2_v84a_mc - KECCAK_F1600_X2_V84A_POSTAMBLE_LENGTH`;;

let LENGTH_SIMPLIFY_CONV =
REWRITE_CONV[LENGTH_KECCAK_F1600_X2_V84A_MC;
KECCAK_F1600_X2_V84A_CORE_START; KECCAK_F1600_X2_V84A_CORE_END;
KECCAK_F1600_X2_V84A_PREAMBLE_LENGTH; KECCAK_F1600_X2_V84A_POSTAMBLE_LENGTH] THENC
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;

let KECCAK_F1600_X2_V84A_EXEC = ARM_MK_EXEC_RULE keccak_f1600_x2_v84a_mc;;

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

let KECCAK_F1600_X2_V84A_CORRECT = prove
(`!a rc A A' pc.
ALL (nonoverlapping (a,400)) [(word pc,0x284); (rc,192)]
ALL (nonoverlapping (a,400)) [(word pc,LENGTH keccak_f1600_x2_v84a_mc); (rc,192)]
==> ensures arm
(\s. aligned_bytes_loaded s (word pc) keccak_f1600_x2_v84a_mc /\
read PC s = word (pc + 0x14) /\
read PC s = word (pc + KECCAK_F1600_X2_V84A_CORE_START) /\
C_ARGUMENTS [a; rc] s /\
wordlist_from_memory(a,25) s = A /\
wordlist_from_memory(word_add a (word 200),25) s = A' /\
wordlist_from_memory(rc,24) s = round_constants)
(\s. read PC s = word(pc + 0x26c) /\
(\s. read PC s = word(pc + KECCAK_F1600_X2_V84A_CORE_END) /\
wordlist_from_memory(a,25) s = keccak 24 A /\
wordlist_from_memory(word_add a (word 200),25) s = keccak 24 A')
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
MAYCHANGE [Q8; Q9; Q10; Q11; Q12; Q13; Q14; Q15] ,,
MAYCHANGE [memory :> bytes(a,400)])`,
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
MAP_EVERY X_GEN_TAC
[`a:int64`; `rc:int64`; `A:int64 list`; `A':int64 list`; `pc:num`] THEN
REWRITE_TAC[fst KECCAK_F1600_X2_V84A_EXEC] THEN
Expand Down Expand Up @@ -318,7 +347,7 @@ let KECCAK_F1600_X2_V84A_SUBROUTINE_CORRECT = prove
nonoverlapping (a,400) (word_sub stackpointer (word 64),64) /\
ALLPAIRS nonoverlapping
[(a,400); (word_sub stackpointer (word 64),64)]
[(word pc,0x284); (rc,192)]
[(word pc,LENGTH keccak_f1600_x2_v84a_mc); (rc,192)]
==> ensures arm
(\s. aligned_bytes_loaded s (word pc) keccak_f1600_x2_v84a_mc /\
read PC s = word pc /\
Expand All @@ -335,11 +364,12 @@ let KECCAK_F1600_X2_V84A_SUBROUTINE_CORRECT = prove
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
MAYCHANGE [memory :> bytes(a,400);
memory :> bytes(word_sub stackpointer (word 64),64)])`,
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
let TWEAK_CONV =
ONCE_DEPTH_CONV
(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:(5,5) KECCAK_F1600_X2_V84A_EXEC
(CONV_RULE TWEAK_CONV KECCAK_F1600_X2_V84A_CORRECT)
(CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X2_V84A_CORRECT))
`[D8; D9; D10; D11; D12; D13; D14; D15]` 64);;
39 changes: 34 additions & 5 deletions proofs/hol_light/arm/proofs/keccak_f1600_x4_v8a_scalar.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -999,6 +999,33 @@ 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;;

(* ------------------------------------------------------------------------- *)
(* Code length constants *)
(* ------------------------------------------------------------------------- *)

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_POSTAMBLE_LENGTH = new_definition
`KECCAK_F1600_X4_V8A_SCALAR_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_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 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
NUM_REDUCE_CONV THENC REWRITE_CONV [ADD_0];;

(* ------------------------------------------------------------------------- *)
(* Correctness proof *)
Expand All @@ -1010,18 +1037,18 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
nonoverlapping (a,800) (stackpointer,216) /\
ALLPAIRS nonoverlapping
[(a,800); (stackpointer,216)]
[(word pc,0xf20); (rc,192)]
[(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 + 0x2c) /\
read PC s = word (pc + KECCAK_F1600_X4_V8A_SCALAR_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 + 0xef0) /\
(\s. read PC s = word(pc + KECCAK_F1600_X4_V8A_SCALAR_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 @@ -1036,6 +1063,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_CORRECT = prove
MAYCHANGE [memory :> bytes(a,800);
memory :> bytes(stackpointer,40);
memory :> bytes(word_add stackpointer (word 208),8)])`,
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
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
Expand Down Expand Up @@ -1419,7 +1447,7 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove
nonoverlapping (a,800) (word_sub stackpointer (word 224),224) /\
ALLPAIRS nonoverlapping
[(a,800); (word_sub stackpointer (word 224),224)]
[(word pc,0xf20); (rc,192)]
[(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 /\
Expand All @@ -1442,12 +1470,13 @@ let KECCAK_F1600_X4_V8A_SCALAR_SUBROUTINE_CORRECT = prove
(MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,,
MAYCHANGE [memory :> bytes(a,800);
memory :> bytes(word_sub stackpointer (word 224),224)])`,
CONV_TAC LENGTH_SIMPLIFY_CONV THEN
let TWEAK_CONV =
ONCE_DEPTH_CONV
(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 KECCAK_F1600_X4_V8A_SCALAR_CORRECT)
(CONV_RULE TWEAK_CONV (CONV_RULE LENGTH_SIMPLIFY_CONV KECCAK_F1600_X4_V8A_SCALAR_CORRECT))
`[D8; D9; D10; D11; D12; D13; D14; D15;
X19; X20; X21; X22; X23; X24; X25; X26; X27; X28; X29; X30]` 224);;
Loading