Fix list of rules for violated rules

CKS-Systems · Nov 21, 2024 · 2d04c83 · 2d04c83
1 parent d78d04f
commit 2d04c83
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 20 deletions.
diff --git a/programs/manifest/justfile b/programs/manifest/justfile
@@ -125,6 +125,7 @@ verify-remote RULE *OPTS: build-sbf
 
 clean:
 	rm -f *.dot *.png *.svg
+	rm -f log_verification*
 	rm -Rf emv-*
 	rm -Rf .certora_internal
 	rm -f log.txt

diff --git a/programs/manifest/rules-rb-tree.json b/programs/manifest/rules-rb-tree.json
@@ -185,24 +185,6 @@
       "expected_result": "Verified",
       "prover_options": [],
       "cargo_features": []
-    },
-    {
-      "name": "rule_swap_parent_left_child",
-      "expected_result": "Violated",
-      "prover_options": [],
-      "cargo_features": []
-    },
-    {
-      "name": "rule_swap_right_child_parent",
-      "expected_result": "Violated",
-      "prover_options": [],
-      "cargo_features": []
-    },
-    {
-      "name": "rule_swap_left_child_parent",
-      "expected_result": "Violated",
-      "prover_options": [],
-      "cargo_features": []
     }
   ]
 }
diff --git a/programs/manifest/verify-manifest.py b/programs/manifest/verify-manifest.py
@@ -217,8 +217,6 @@ def clean() -> None:
         ''' Call `just clean`. '''
         subprocess.run(["just", "clean"], check=True, capture_output=True)
 
-# TODO: @phreppo - should sanity rules be added?
-
 
 # Parse the CLI options
 parser = argparse.ArgumentParser(