diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 7535be0..ad5e5c2 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -8,7 +8,7 @@ f14fd3c7ec25e96776c29a3899fe815c8899f70f00e8b820f1985d4ff784647c inventory-allo 8e2950712ce39ace9cffd3bb58a13984832ff7f3f43ba7b68aa2b1eaa2bc2116 inventory-allowlist.txt 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard -2b78361105984aa8e859758849a0886b5b768766fe9bb39dd04aa8ee24d38b6c lift-guard.sh +cad0ae17ce506e1defeab3b9799993b3a2251c055247695832ecae2c2617772f lift-guard.sh 1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py 1757e9c7d43aacc6d5930af62f6450ac336f7e881350ef0e5af35015442358dd MODEL-CORRESPONDENCE.txt 79a001107928713a22e679e4c4028549df76d0733455bb9937a4f438a0c315c8 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'(?