Upload test_equivalence.py with huggingface_hub

test_equivalence.py

@@ -0,0 +1,477 @@
+"""
+TEST #2: Formal Equivalence Checking
+=====================================
+Run 8-bit adder against Python's arithmetic for ALL 2^16 input pairs.
+Bit-for-bit comparison of every result and carry flag.
+
+A skeptic would demand: "Prove exhaustive correctness, not just sampling."
+"""
+
+import torch
+from safetensors.torch import load_file
+import time
+
+# Load circuits
+model = load_file('neural_computer.safetensors')
+
+def heaviside(x):
+    return (x >= 0).float()
+
+def eval_xor_arith(inp, prefix):
+    """Evaluate XOR for arithmetic circuits."""
+    w1_or = model[f'{prefix}.layer1.or.weight']
+    b1_or = model[f'{prefix}.layer1.or.bias']
+    w1_nand = model[f'{prefix}.layer1.nand.weight']
+    b1_nand = model[f'{prefix}.layer1.nand.bias']
+    w2 = model[f'{prefix}.layer2.weight']
+    b2 = model[f'{prefix}.layer2.bias']
+    h_or = heaviside(inp @ w1_or + b1_or)
+    h_nand = heaviside(inp @ w1_nand + b1_nand)
+    hidden = torch.tensor([h_or.item(), h_nand.item()])
+    return heaviside(hidden @ w2 + b2).item()
+
+def eval_full_adder(a, b, cin, prefix):
+    """Evaluate full adder, return (sum, carry_out)."""
+    inp_ab = torch.tensor([a, b], dtype=torch.float32)
+    ha1_sum = eval_xor_arith(inp_ab, f'{prefix}.ha1.sum')
+    w_c1 = model[f'{prefix}.ha1.carry.weight']
+    b_c1 = model[f'{prefix}.ha1.carry.bias']
+    ha1_carry = heaviside(inp_ab @ w_c1 + b_c1).item()
+    inp_ha2 = torch.tensor([ha1_sum, cin], dtype=torch.float32)
+    ha2_sum = eval_xor_arith(inp_ha2, f'{prefix}.ha2.sum')
+    w_c2 = model[f'{prefix}.ha2.carry.weight']
+    b_c2 = model[f'{prefix}.ha2.carry.bias']
+    ha2_carry = heaviside(inp_ha2 @ w_c2 + b_c2).item()
+    inp_cout = torch.tensor([ha1_carry, ha2_carry], dtype=torch.float32)
+    w_or = model[f'{prefix}.carry_or.weight']
+    b_or = model[f'{prefix}.carry_or.bias']
+    cout = heaviside(inp_cout @ w_or + b_or).item()
+    return int(ha2_sum), int(cout)
+
+def add_8bit(a, b):
+    """8-bit addition using ripple carry adder."""
+    carry = 0.0
+    result_bits = []
+    for i in range(8):
+        a_bit = (a >> i) & 1
+        b_bit = (b >> i) & 1
+        s, carry = eval_full_adder(float(a_bit), float(b_bit), carry,
+                                    f'arithmetic.ripplecarry8bit.fa{i}')
+        result_bits.append(s)
+    result = sum(result_bits[i] * (2**i) for i in range(8))
+    return result, int(carry)
+
+def compare_8bit(a, b):
+    """8-bit comparators."""
+    a_bits = torch.tensor([(a >> (7-i)) & 1 for i in range(8)], dtype=torch.float32)
+    b_bits = torch.tensor([(b >> (7-i)) & 1 for i in range(8)], dtype=torch.float32)
+
+    # Greater than
+    w_gt = model['arithmetic.greaterthan8bit.comparator']
+    gt = 1 if ((a_bits - b_bits) @ w_gt).item() > 0 else 0
+
+    # Less than
+    w_lt = model['arithmetic.lessthan8bit.comparator']
+    lt = 1 if ((b_bits - a_bits) @ w_lt).item() > 0 else 0
+
+    # Equal (neither gt nor lt)
+    eq = 1 if (gt == 0 and lt == 0) else 0
+
+    return gt, lt, eq
+
+# =============================================================================
+# EXHAUSTIVE TESTS
+# =============================================================================
+
+def test_addition_exhaustive():
+    """
+    Test ALL 65,536 addition combinations.
+    """
+    print("\n[TEST 1] Exhaustive 8-bit Addition: 256 x 256 = 65,536 cases")
+    print("-" * 60)
+
+    errors = []
+    start = time.perf_counter()
+
+    for a in range(256):
+        for b in range(256):
+            # Circuit result
+            result, carry = add_8bit(a, b)
+
+            # Python reference
+            full_sum = a + b
+            expected_result = full_sum % 256
+            expected_carry = 1 if full_sum > 255 else 0
+
+            # Compare
+            if result != expected_result:
+                errors.append(('result', a, b, expected_result, result))
+            if carry != expected_carry:
+                errors.append(('carry', a, b, expected_carry, carry))
+
+        # Progress every 32 rows
+        if (a + 1) % 32 == 0:
+            elapsed = time.perf_counter() - start
+            rate = ((a + 1) * 256) / elapsed
+            eta = (256 - a - 1) * 256 / rate
+            print(f"    Progress: {a+1}/256 rows ({(a+1)*256:,} tests) "
+                  f"| {rate:.0f} tests/sec | ETA: {eta:.1f}s")
+
+    elapsed = time.perf_counter() - start
+
+    print()
+    if errors:
+        print(f"  FAILED: {len(errors)} mismatches")
+        for e in errors[:10]:
+            print(f"    {e[0]}: {e[1]} + {e[2]} = {e[4]}, expected {e[3]}")
+    else:
+        print(f"  PASSED: 65,536 additions verified")
+        print(f"  Time: {elapsed:.2f}s ({65536/elapsed:.0f} tests/sec)")
+
+    return len(errors) == 0
+
+def test_comparators_exhaustive():
+    """
+    Test ALL 65,536 comparator combinations for GT, LT, EQ.
+    """
+    print("\n[TEST 2] Exhaustive 8-bit Comparators: 256 x 256 x 3 = 196,608 checks")
+    print("-" * 60)
+
+    errors = []
+    start = time.perf_counter()
+
+    for a in range(256):
+        for b in range(256):
+            gt, lt, eq = compare_8bit(a, b)
+
+            # Python reference
+            exp_gt = 1 if a > b else 0
+            exp_lt = 1 if a < b else 0
+            exp_eq = 1 if a == b else 0
+
+            if gt != exp_gt:
+                errors.append(('GT', a, b, exp_gt, gt))
+            if lt != exp_lt:
+                errors.append(('LT', a, b, exp_lt, lt))
+            if eq != exp_eq:
+                errors.append(('EQ', a, b, exp_eq, eq))
+
+        if (a + 1) % 32 == 0:
+            elapsed = time.perf_counter() - start
+            rate = ((a + 1) * 256) / elapsed
+            eta = (256 - a - 1) * 256 / rate
+            print(f"    Progress: {a+1}/256 rows | {rate:.0f} pairs/sec | ETA: {eta:.1f}s")
+
+    elapsed = time.perf_counter() - start
+
+    print()
+    if errors:
+        print(f"  FAILED: {len(errors)} mismatches")
+        for e in errors[:10]:
+            print(f"    {e[0]}({e[1]}, {e[2]}) = {e[4]}, expected {e[3]}")
+    else:
+        print(f"  PASSED: 196,608 comparisons verified (GT, LT, EQ for each pair)")
+        print(f"  Time: {elapsed:.2f}s")
+
+    return len(errors) == 0
+
+def test_boolean_exhaustive():
+    """
+    Exhaustive test of all 2-input Boolean gates (4 cases each).
+    """
+    print("\n[TEST 3] Exhaustive Boolean Gates: AND, OR, NAND, NOR, XOR, XNOR")
+    print("-" * 60)
+
+    gates = {
+        'and':  lambda a, b: a & b,
+        'or':   lambda a, b: a | b,
+        'nand': lambda a, b: 1 - (a & b),
+        'nor':  lambda a, b: 1 - (a | b),
+    }
+
+    errors = []
+
+    # Simple gates (single layer)
+    for gate_name, expected_fn in gates.items():
+        w = model[f'boolean.{gate_name}.weight']
+        bias = model[f'boolean.{gate_name}.bias']
+
+        for a in [0, 1]:
+            for b in [0, 1]:
+                inp = torch.tensor([float(a), float(b)])
+                result = int(heaviside(inp @ w + bias).item())
+                expected = expected_fn(a, b)
+
+                if result != expected:
+                    errors.append((gate_name.upper(), a, b, expected, result))
+
+    # XOR (two-layer)
+    for a in [0, 1]:
+        for b in [0, 1]:
+            inp = torch.tensor([float(a), float(b)])
+
+            w1_n1 = model['boolean.xor.layer1.neuron1.weight']
+            b1_n1 = model['boolean.xor.layer1.neuron1.bias']
+            w1_n2 = model['boolean.xor.layer1.neuron2.weight']
+            b1_n2 = model['boolean.xor.layer1.neuron2.bias']
+            w2 = model['boolean.xor.layer2.weight']
+            b2 = model['boolean.xor.layer2.bias']
+
+            h1 = heaviside(inp @ w1_n1 + b1_n1)
+            h2 = heaviside(inp @ w1_n2 + b1_n2)
+            hidden = torch.tensor([h1.item(), h2.item()])
+            result = int(heaviside(hidden @ w2 + b2).item())
+            expected = a ^ b
+
+            if result != expected:
+                errors.append(('XOR', a, b, expected, result))
+
+    # XNOR (two-layer)
+    for a in [0, 1]:
+        for b in [0, 1]:
+            inp = torch.tensor([float(a), float(b)])
+
+            w1_n1 = model['boolean.xnor.layer1.neuron1.weight']
+            b1_n1 = model['boolean.xnor.layer1.neuron1.bias']
+            w1_n2 = model['boolean.xnor.layer1.neuron2.weight']
+            b1_n2 = model['boolean.xnor.layer1.neuron2.bias']
+            w2 = model['boolean.xnor.layer2.weight']
+            b2 = model['boolean.xnor.layer2.bias']
+
+            h1 = heaviside(inp @ w1_n1 + b1_n1)
+            h2 = heaviside(inp @ w1_n2 + b1_n2)
+            hidden = torch.tensor([h1.item(), h2.item()])
+            result = int(heaviside(hidden @ w2 + b2).item())
+            expected = 1 - (a ^ b)  # XNOR = NOT XOR
+
+            if result != expected:
+                errors.append(('XNOR', a, b, expected, result))
+
+    # NOT (single input)
+    w = model['boolean.not.weight']
+    bias = model['boolean.not.bias']
+    for a in [0, 1]:
+        inp = torch.tensor([float(a)])
+        result = int(heaviside(inp @ w + bias).item())
+        expected = 1 - a
+        if result != expected:
+            errors.append(('NOT', a, '-', expected, result))
+
+    if errors:
+        print(f"  FAILED: {len(errors)} mismatches")
+        for e in errors:
+            print(f"    {e[0]}({e[1]}, {e[2]}) = {e[4]}, expected {e[3]}")
+    else:
+        print(f"  PASSED: All Boolean gates verified (AND, OR, NAND, NOR, XOR, XNOR, NOT)")
+        print(f"  Total: 26 truth table entries")
+
+    return len(errors) == 0
+
+def test_half_adder_exhaustive():
+    """
+    Exhaustive test of half adder (4 cases).
+    """
+    print("\n[TEST 4] Exhaustive Half Adder: 4 cases")
+    print("-" * 60)
+
+    errors = []
+
+    for a in [0, 1]:
+        for b in [0, 1]:
+            inp = torch.tensor([float(a), float(b)])
+
+            # Sum (XOR)
+            w1_or = model['arithmetic.halfadder.sum.layer1.or.weight']
+            b1_or = model['arithmetic.halfadder.sum.layer1.or.bias']
+            w1_nand = model['arithmetic.halfadder.sum.layer1.nand.weight']
+            b1_nand = model['arithmetic.halfadder.sum.layer1.nand.bias']
+            w2 = model['arithmetic.halfadder.sum.layer2.weight']
+            b2_sum = model['arithmetic.halfadder.sum.layer2.bias']
+
+            h_or = heaviside(inp @ w1_or + b1_or)
+            h_nand = heaviside(inp @ w1_nand + b1_nand)
+            hidden = torch.tensor([h_or.item(), h_nand.item()])
+            sum_bit = int(heaviside(hidden @ w2 + b2_sum).item())
+
+            # Carry (AND)
+            w_c = model['arithmetic.halfadder.carry.weight']
+            b_c = model['arithmetic.halfadder.carry.bias']
+            carry = int(heaviside(inp @ w_c + b_c).item())
+
+            # Expected
+            exp_sum = a ^ b
+            exp_carry = a & b
+
+            if sum_bit != exp_sum:
+                errors.append(('SUM', a, b, exp_sum, sum_bit))
+            if carry != exp_carry:
+                errors.append(('CARRY', a, b, exp_carry, carry))
+
+    if errors:
+        print(f"  FAILED: {len(errors)} mismatches")
+        for e in errors:
+            print(f"    HA.{e[0]}({e[1]}, {e[2]}) = {e[4]}, expected {e[3]}")
+    else:
+        print(f"  PASSED: Half adder verified (4 sum + 4 carry = 8 checks)")
+
+    return len(errors) == 0
+
+def test_full_adder_exhaustive():
+    """
+    Exhaustive test of full adder (8 cases).
+    """
+    print("\n[TEST 5] Exhaustive Full Adder: 8 cases")
+    print("-" * 60)
+
+    errors = []
+
+    for a in [0, 1]:
+        for b in [0, 1]:
+            for cin in [0, 1]:
+                sum_bit, cout = eval_full_adder(float(a), float(b), float(cin),
+                                                 'arithmetic.fulladder')
+
+                # Expected
+                total = a + b + cin
+                exp_sum = total % 2
+                exp_cout = total // 2
+
+                if sum_bit != exp_sum:
+                    errors.append(('SUM', a, b, cin, exp_sum, sum_bit))
+                if cout != exp_cout:
+                    errors.append(('COUT', a, b, cin, exp_cout, cout))
+
+    if errors:
+        print(f"  FAILED: {len(errors)} mismatches")
+        for e in errors:
+            print(f"    FA.{e[0]}({e[1]}, {e[2]}, {e[3]}) = {e[5]}, expected {e[4]}")
+    else:
+        print(f"  PASSED: Full adder verified (8 sum + 8 carry = 16 checks)")
+
+    return len(errors) == 0
+
+def test_2bit_adder_exhaustive():
+    """
+    Exhaustive test of 2-bit ripple carry adder (16 cases).
+    """
+    print("\n[TEST 6] Exhaustive 2-bit Adder: 4 x 4 = 16 cases")
+    print("-" * 60)
+
+    errors = []
+
+    for a in range(4):
+        for b in range(4):
+            # Use 2-bit ripple carry
+            carry = 0.0
+            result_bits = []
+
+            for i in range(2):
+                a_bit = (a >> i) & 1
+                b_bit = (b >> i) & 1
+                s, carry = eval_full_adder(float(a_bit), float(b_bit), carry,
+                                            f'arithmetic.ripplecarry2bit.fa{i}')
+                result_bits.append(s)
+
+            result = result_bits[0] + 2 * result_bits[1]
+            cout = int(carry)
+
+            exp_result = (a + b) % 4
+            exp_carry = 1 if (a + b) >= 4 else 0
+
+            if result != exp_result:
+                errors.append(('result', a, b, exp_result, result))
+            if cout != exp_carry:
+                errors.append(('carry', a, b, exp_carry, cout))
+
+    if errors:
+        print(f"  FAILED: {len(errors)} mismatches")
+        for e in errors:
+            print(f"    {e[0]}: {e[1]} + {e[2]} = {e[4]}, expected {e[3]}")
+    else:
+        print(f"  PASSED: 2-bit adder verified (16 results + 16 carries)")
+
+    return len(errors) == 0
+
+def test_4bit_adder_exhaustive():
+    """
+    Exhaustive test of 4-bit ripple carry adder (256 cases).
+    """
+    print("\n[TEST 7] Exhaustive 4-bit Adder: 16 x 16 = 256 cases")
+    print("-" * 60)
+
+    errors = []
+
+    for a in range(16):
+        for b in range(16):
+            carry = 0.0
+            result_bits = []
+
+            for i in range(4):
+                a_bit = (a >> i) & 1
+                b_bit = (b >> i) & 1
+                s, carry = eval_full_adder(float(a_bit), float(b_bit), carry,
+                                            f'arithmetic.ripplecarry4bit.fa{i}')
+                result_bits.append(s)
+
+            result = sum(result_bits[i] * (2**i) for i in range(4))
+            cout = int(carry)
+
+            exp_result = (a + b) % 16
+            exp_carry = 1 if (a + b) >= 16 else 0
+
+            if result != exp_result:
+                errors.append(('result', a, b, exp_result, result))
+            if cout != exp_carry:
+                errors.append(('carry', a, b, exp_carry, cout))
+
+    if errors:
+        print(f"  FAILED: {len(errors)} mismatches")
+        for e in errors[:10]:
+            print(f"    {e[0]}: {e[1]} + {e[2]} = {e[4]}, expected {e[3]}")
+    else:
+        print(f"  PASSED: 4-bit adder verified (256 results + 256 carries)")
+
+    return len(errors) == 0
+
+# =============================================================================
+# MAIN
+# =============================================================================
+
+if __name__ == "__main__":
+    print("=" * 70)
+    print(" TEST #2: FORMAL EQUIVALENCE CHECKING")
+    print(" Exhaustive verification against Python's arithmetic")
+    print("=" * 70)
+
+    results = []
+
+    results.append(("Boolean gates", test_boolean_exhaustive()))
+    results.append(("Half adder", test_half_adder_exhaustive()))
+    results.append(("Full adder", test_full_adder_exhaustive()))
+    results.append(("2-bit adder", test_2bit_adder_exhaustive()))
+    results.append(("4-bit adder", test_4bit_adder_exhaustive()))
+    results.append(("8-bit adder", test_addition_exhaustive()))
+    results.append(("Comparators", test_comparators_exhaustive()))
+
+    print("\n" + "=" * 70)
+    print(" SUMMARY")
+    print("=" * 70)
+
+    passed = sum(1 for _, r in results if r)
+    total = len(results)
+
+    for name, r in results:
+        status = "PASS" if r else "FAIL"
+        print(f"  {name:20s} [{status}]")
+
+    print(f"\n  Total: {passed}/{total} test categories passed")
+
+    total_checks = 26 + 8 + 16 + 32 + 512 + 65536*2 + 65536*3
+    print(f"  Individual checks: ~{total_checks:,}")
+
+    if passed == total:
+        print("\n  STATUS: EXHAUSTIVE EQUIVALENCE VERIFIED")
+    else:
+        print("\n  STATUS: EQUIVALENCE FAILURES DETECTED")
+
+    print("=" * 70)