HANERMA/test_firewall.py at main · Electroiscoding/HANERMA · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
"""Test the Z3 Mathematical Firewall"""
import importlib.util
import os
import sys

# Bypass broken hanerma.__init__
spec = importlib.util.spec_from_file_location(
    "symbolic_reasoner",
    os.path.join(os.path.dirname(__file__), "src", "hanerma", "reliability", "symbolic_reasoner.py"),
)
reasoner_mod = importlib.util.module_from_spec(spec)
sys.modules["hanerma.reliability.symbolic_reasoner"] = reasoner_mod
spec.loader.exec_module(reasoner_mod)

SymbolicReasoner = reasoner_mod.SymbolicReasoner
ContradictionError = reasoner_mod.ContradictionError

reasoner = SymbolicReasoner()

# 1. Valid Assertions
print("\n--- Testing Valid Assertions ---")
valid_assertions = [
    {"fact": "user_age", "operator": ">=", "value": 18},
    {"fact": "credit_score", "operator": ">", "value": 700},
    {"fact": "is_employed", "operator": "==", "value": True}
]
reasoner.compiler.compile_and_check(valid_assertions)
print("✓ Valid assertions passed Z3 solver (SAT)")

# 2. Contradiction 1: Numeric bounds
print("\n--- Testing Mathematical Contradiction ---")
try:
    contradiction = [
        {"fact": "target_price", "operator": ">", "value": 150.0},
        {"fact": "target_price", "operator": "<", "value": 100.0}
    ]
    reasoner.compiler.compile_and_check(contradiction)
    print("❌ ERROR: Z3 failed to catch contradiction!")
except ContradictionError as e:
    print(f"✓ Z3 Caught Contradiction: {e}")

# 3. Contradiction 2: Boolean mismatch
print("\n--- Testing Boolean Contradiction ---")
try:
    bool_contradiction = [
        {"fact": "is_admin", "operator": "==", "value": True},
        {"fact": "is_admin", "operator": "==", "value": False}
    ]
    reasoner.compiler.compile_and_check(bool_contradiction)
    print("❌ ERROR: Z3 failed to catch boolean contradiction!")
except ContradictionError as e:
    print(f"✓ Z3 Caught Boolean Contradiction: {e}")

# 4. Contradiction 3: Type Mismatch (int vs bool)
print("\n--- Testing Type Sort Mismatch ---")
try:
    type_contradiction = [
        {"fact": "status", "operator": "==", "value": 404},
        {"fact": "status", "operator": "==", "value": True}
    ]
    reasoner.compiler.compile_and_check(type_contradiction)
    print("❌ ERROR: Z3 failed to catch Sort mismatch!")
except ContradictionError as e:
    print(f"✓ Z3 Caught Type/Sort Mismatch: {e}")

print("\nSLICE 4 VERIFIED ✓")