model.py

"""
Threshold Network for XOR Gate - Magnitude 7 (Proven Optimal)

Six equivalent solutions exist at magnitude 7. All compute XOR correctly.
Magnitudes 0-6 proven impossible via exhaustive Coq verification.
"""

import torch
from safetensors.torch import load_file


class ThresholdXOR:
    """
    XOR gate implemented as a 2-layer threshold network.
    Magnitude 7 - proven optimal by Coq exhaustive computation.
    """

    def __init__(self, weights_dict):
        self.l1_n1_weight = weights_dict['layer1.neuron1.weight']
        self.l1_n1_bias = weights_dict['layer1.neuron1.bias']
        self.l1_n2_weight = weights_dict['layer1.neuron2.weight']
        self.l1_n2_bias = weights_dict['layer1.neuron2.bias']
        self.l2_weight = weights_dict['layer2.weight']
        self.l2_bias = weights_dict['layer2.bias']

    def __call__(self, x1, x2):
        inputs = torch.tensor([float(x1), float(x2)])

        h1 = ((inputs * self.l1_n1_weight).sum() + self.l1_n1_bias >= 0).float()
        h2 = ((inputs * self.l1_n2_weight).sum() + self.l1_n2_bias >= 0).float()

        hidden = torch.tensor([h1, h2])
        output = ((hidden * self.l2_weight).sum() + self.l2_bias >= 0).float()

        return output

    @classmethod
    def from_safetensors(cls, path="solution1.safetensors"):
        return cls(load_file(path))


def forward(x1, x2, weights):
    """Forward pass with Heaviside activation."""
    inputs = torch.tensor([float(x1), float(x2)])

    h1 = ((inputs * weights['layer1.neuron1.weight']).sum() + weights['layer1.neuron1.bias'] >= 0).float()
    h2 = ((inputs * weights['layer1.neuron2.weight']).sum() + weights['layer1.neuron2.bias'] >= 0).float()

    hidden = torch.tensor([h1, h2])
    output = ((hidden * weights['layer2.weight']).sum() + weights['layer2.bias'] >= 0).float()

    return output


def verify_all_solutions():
    """Verify all 6 solutions compute XOR correctly."""
    print("Verifying all 6 magnitude-7 XOR solutions:")
    print("=" * 50)

    for i in range(1, 7):
        weights = load_file(f'solution{i}.safetensors')
        model = ThresholdXOR(weights)

        all_correct = True
        for x1 in [0, 1]:
            for x2 in [0, 1]:
                out = int(model(x1, x2).item())
                expected = x1 ^ x2
                if out != expected:
                    all_correct = False

        status = "OK" if all_correct else "FAIL"
        mag = sum(abs(v.item()) for v in weights.values() for v in [v] if v.numel() == 1)
        mag += sum(abs(v).sum().item() for v in weights.values() if v.numel() > 1)
        print(f"  Solution {i}: {status} (magnitude={mag:.0f})")

    print("=" * 50)


if __name__ == "__main__":
    verify_all_solutions()

    print("\nSolution 1 truth table:")
    print("-" * 25)
    weights = load_file("solution1.safetensors")
    model = ThresholdXOR(weights)

    for x1 in [0, 1]:
        for x2 in [0, 1]:
            out = int(model(x1, x2).item())
            expected = x1 ^ x2
            status = "OK" if out == expected else "FAIL"
            print(f"XOR({x1}, {x2}) = {out}  [{status}]")