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
94fad12
testing: HOL-Light: add support for cross-proofing
L-series Mar 20, 2026
3226ad6
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
6 changes: 3 additions & 3 deletions proofs/hol_light/aarch64/proofs/mlkem_rej_uniform.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1755,7 +1755,7 @@ let STRIP_EXISTS_ASSUM_TAC =
(* The main memory safety theorem. *)
(* ========================================================================= *)

let MLKEM_REJ_UNIFORM_MEMSAFE = prove
let MLKEM_REJ_UNIFORM_SAFE = prove
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was intentionally named this way and I would prefer to keep it like that because we do not have any constant time proofs at this time.
Can you implement it as: if mlkem_rej_uniform then MEMSAFE else SAFE? That would be better, I believe.

(`!res buf buflen table (inlist:(12 word)list) pc e stackpointer.
24 divides val buflen /\
8 * val buflen = 12 * LENGTH inlist /\
Expand Down Expand Up @@ -3086,7 +3086,7 @@ let MLKEM_REJ_UNIFORM_MEMSAFE = prove
(* Memory safety of the subroutine version. *)
(* ------------------------------------------------------------------------- *)

let MLKEM_REJ_UNIFORM_SUBROUTINE_MEMSAFE = time prove
let MLKEM_REJ_UNIFORM_SUBROUTINE_SAFE = time prove
(`!res buf buflen table (inlist:(12 word)list) pc e stackpointer returnaddress.
24 divides val buflen /\
8 * val buflen = 12 * LENGTH inlist /\
Expand Down Expand Up @@ -3119,6 +3119,6 @@ let MLKEM_REJ_UNIFORM_SUBROUTINE_MEMSAFE = time prove
REWRITE_CONV[wordlist_from_memory] in
CONV_TAC TWEAK_CONV THEN
ARM_ADD_RETURN_STACK_TAC MLKEM_REJ_UNIFORM_EXEC
(CONV_RULE TWEAK_CONV MLKEM_REJ_UNIFORM_MEMSAFE)
(CONV_RULE TWEAK_CONV MLKEM_REJ_UNIFORM_SAFE)
`[]:int64 list` 576 THEN
DISCHARGE_MEMSAFE_TAC);;
4 changes: 2 additions & 2 deletions proofs/hol_light/x86_64/proofs/mlkem_intt.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1206,7 +1206,7 @@ let MLKEM_INTT_CORRECT = prove
CONV_TAC INT_REDUCE_CONV]))
);;

let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT = prove
let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT = prove
(`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
aligned 32 a /\
aligned 32 zetas /\
Expand Down Expand Up @@ -1241,7 +1241,7 @@ let MLKEM_INTT_NOIBT_SUBROUTINE_CORRECT = prove
(* NOTE: This must be kept in sync with the CBMC specification
* in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)

let MLKEM_INTT_SUBROUTINE_CORRECT = prove
let MLKEM_INTT_SUBROUTINE_CORRECT = prove
(`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
aligned 32 a /\
aligned 32 zetas /\
Expand Down
2 changes: 1 addition & 1 deletion proofs/hol_light/x86_64/proofs/mlkem_mulcache_compute.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -259,7 +259,7 @@ let MLKEM_MULCACHE_COMPUTE_CORRECT = prove(
CONV_TAC INT_REDUCE_CONV])
);;

let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT = prove(
let MLKEM_MULCACHE_COMPUTE_NOIBT_SUBROUTINE_CORRECT = prove(
`!r a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
aligned 32 r /\
aligned 32 a /\
Expand Down
4 changes: 2 additions & 2 deletions proofs/hol_light/x86_64/proofs/mlkem_ntt.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1214,7 +1214,7 @@ let MLKEM_NTT_CORRECT = prove
CONV_TAC INT_REDUCE_CONV]))
);;

let MLKEM_NTT_NOIBT_SUBROUTINE_CORRECT = prove
let MLKEM_NTT_NOIBT_SUBROUTINE_CORRECT = prove
(`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
aligned 32 a /\
aligned 32 zetas /\
Expand Down Expand Up @@ -1250,7 +1250,7 @@ let MLKEM_NTT_NOIBT_SUBROUTINE_CORRECT = prove
(* NOTE: This must be kept in sync with the CBMC specification
* in mlkem/src/native/x86_64/src/arith_native_x86_64.h *)

let MLKEM_NTT_SUBROUTINE_CORRECT = prove
let MLKEM_NTT_SUBROUTINE_CORRECT = prove
(`!a zetas (zetas_list:int16 list) x pc stackpointer returnaddress.
aligned 32 a /\
aligned 32 zetas /\
Expand Down
45 changes: 45 additions & 0 deletions scripts/lint
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -295,6 +295,51 @@ gh_group_start "Check contracts"
check-contracts
gh_group_end

check-theorems()
{
local success=true
for arch in aarch64 x86_64; do
local proofs_dir="$ROOT/proofs/hol_light/$arch/proofs"
local proofs
proofs=$("$ROOT/proofs/hol_light/$arch/list_proofs.sh")

for routine in $proofs; do
local suffixes=("CORRECT" "SAFE" "SUBROUTINE_SAFE")
if [[ $arch == "x86_64" && ${routine} == "mlkem_rej_uniform" ]]; then
suffixes=("CORRECT")
Comment on lines +308 to +309
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is there this exceptions? There are memory safety proofs for this routine?

elif [[ $arch == "x86_64" ]]; then
suffixes+=("SUBROUTINE_CORRECT" "NOIBT_SUBROUTINE_CORRECT" "NOIBT_SUBROUTINE_SAFE")
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer Apr 3, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tried removing the SUBROUTINE_SAFE proof from the mlkem_poly_compress_d4.ml proof and the script did not catch it. Is that because NOIBT_SUBROUTINE_SAFE matches the SUBROUTINE_SAFE suffix? That should be fixed.

We can actually check the full theorem name, not just the suffix. It should be possible to derive the theorem names from the file names - we should enforce that and adjust theorem names where needed.

fi

for sfx in "${suffixes[@]}"; do
if ! grep -qE "_${sfx} = (time )?prove" "$proofs_dir/${routine}.ml"; then
gh_error "${routine}" "" "Missing theorem" "${routine}_${sfx} not found in ${routine}.ml for arch ${arch}"
success=false
fi
done

# Check for CHEAT_TAC usage (bypasses actual proving)
if grep -q "CHEAT_TAC" "$proofs_dir/${routine}.ml"; then
gh_error "${routine}" "" "CHEAT_TAC detected" "${routine}.ml uses CHEAT_TAC"
success=false
fi
done
done

if $success; then
info "Check HOL-Light theorems"
gh_summary_success "Check HOL-Light theorems"
else
error "Check HOL-Light theorems"
SUCCESS=false
gh_summary_failure "Check HOL-Light theorems"
fi
}

gh_group_start "Check HOL-Light theorems"
check-theorems
gh_group_end

if ! $SUCCESS; then
if $IN_GITHUB_CONTEXT; then
printf "%b%s%b\n" "${RED}" "The following checks failed, expand each for more details." "${NORMAL}"
Expand Down
24 changes: 18 additions & 6 deletions scripts/tests
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1017,7 +1017,9 @@ class Tests:

def hol_light(self):

if platform.machine().lower() in ["arm64", "aarch64"]:
if self.args.arch:
arch = self.args.arch
elif platform.machine().lower() in ["arm64", "aarch64"]:
arch = "aarch64"
elif platform.machine().lower() in ["x86_64"]:
arch = "x86_64"
Expand Down Expand Up @@ -1050,12 +1052,14 @@ class Tests:
os.remove(os.path.join(proof_dir, proof_target))
except FileNotFoundError:
pass

make_cmd = [
"make",
f"mlkem/{func}.correct",
]

p = subprocess.run(
[
"make",
f"mlkem/{func}.correct",
]
+ self.make_j(),
make_cmd,
cwd="proofs/hol_light/" + arch,
env=os.environ.copy(),
capture_output=(self.args.verbose is False),
Expand Down Expand Up @@ -1481,6 +1485,14 @@ def cli():
default=False,
)

hol_light_parser.add_argument(
"-a",
"--arch",
help="Architecture for which to list/run HOL_LIGHT proofs (aarch64 or x86_64).",
choices=["aarch64", "x86_64"],
default=None,
)

# func arguments
func_parser = cmd_subparsers.add_parser(
"func",
Expand Down
Loading