Delete test_equivalence.py with huggingface_hub

test_equivalence.py

@@ -1,477 +0,0 @@
-"""
-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)