diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 948e487..600f534 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -8,7 +8,7 @@ a0fb8a1a99bc991870b493796bf7bfe09463413298d83c6ae73a269712f96b55 inventory-allo 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard -2b78361105984aa8e859758849a0886b5b768766fe9bb39dd04aa8ee24d38b6c lift-guard.sh +cad0ae17ce506e1defeab3b9799993b3a2251c055247695832ecae2c2617772f lift-guard.sh 1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py 855134c50bc2ce374eb935058f808264ea6de5ee328ef766956e7e54366f75fe MODEL-CORRESPONDENCE.txt 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean diff --git a/verification/lift-guard.sh b/verification/lift-guard.sh index 0ef0a9c..c670242 100755 --- a/verification/lift-guard.sh +++ b/verification/lift-guard.sh @@ -90,7 +90,13 @@ reads = set(re.findall(r'\$\{?([A-Za-z_][A-Za-z0-9_]*)', payload)) # check.sh's Phase 1b. Not lifted today, which made it latent, not absent. for expr in (re.findall(r'\$\(\((.*?)\)\)', payload, re.S) + re.findall(r'(?