diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 8318f00..f5ffeaf 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -8,7 +8,7 @@ a0082f3f5cad2feb8527edcb6efc50c211855eccffade29690d90bc78be8a945 inventory-allo 80cdd232c9a0f3078b2b712957e34797add5421b51bd695a151bf64a7855687a inventory-allowlist.txt 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard -2b78361105984aa8e859758849a0886b5b768766fe9bb39dd04aa8ee24d38b6c lift-guard.sh +cad0ae17ce506e1defeab3b9799993b3a2251c055247695832ecae2c2617772f lift-guard.sh 1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py cf86c955dd5b637bc9d673c4222684979f507a4e11e488ab514e654c49f4e569 MODEL-CORRESPONDENCE.txt 34c102ca7a38719ef8890b8dedd3f07c3f92e10ae4a1ce2c47a7db4d53523354 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'(?