HOL-Light: add rej_uniform_eta proofs for AArch64#1040

Open

jakemas wants to merge 6 commits into

mainfrom

add-hol-light-rej-uniform-eta4

Commits on Jun 3, 2026

HOL-Light: Add AArch64 rej_uniform_eta_{2,4} correctness, memory-safety proofs

jakemas
authored and
Ubuntu
committed
HOL-Light: address review on rej_uniform_eta_{2,4}

jakemas
authored and
Ubuntu
committed
HOL-Light: use named preamble/postamble offsets in rej_uniform_eta_{2,4}

jakemas
authored and
Ubuntu
committed
HOL-Light: hoist repeated rej_uniform_eta_{2,4} loop-body lemmas
jakemas
committed
HOL-Light: REJ_SAMPLE_ETA{2,4} take a (4 word) list at the natural bitwidth
jakemas
committed
HOL-Light: simplify REJ_SAMPLE_ETA4 to native (4 word) arithmetic
jakemas
committed