Rename from tiny-FullAdder-verified

README.md

@@ -0,0 +1,107 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+- arithmetic
+---
+
+# threshold-fulladder
+
+Adds three 1-bit inputs (a, b, carry_in), producing sum and carry_out. The core of ripple-carry adders.
+
+## Circuit
+
+```
+        a       b
+        │       │
+        └───┬───┘
+            ▼
+       ┌─────────┐
+       │   HA1   │  First half adder
+       └─────────┘
+        │       │
+       s1       c1
+        │        \
+        │    cin  \
+        └──┬──┘    \
+           ▼        \
+      ┌─────────┐    \
+      │   HA2   │     │
+      └─────────┘     │
+       │       │      │
+      sum      c2     │
+               │      │
+               └──┬───┘
+                  ▼
+              ┌──────┐
+              │  OR  │
+              └──────┘
+                  │
+                  ▼
+                cout
+```
+
+## Truth Table
+
+| a | b | cin | sum | cout |
+|---|---|-----|-----|------|
+| 0 | 0 | 0 | 0 | 0 |
+| 0 | 0 | 1 | 1 | 0 |
+| 0 | 1 | 0 | 1 | 0 |
+| 0 | 1 | 1 | 0 | 1 |
+| 1 | 0 | 0 | 1 | 0 |
+| 1 | 0 | 1 | 0 | 1 |
+| 1 | 1 | 0 | 0 | 1 |
+| 1 | 1 | 1 | 1 | 1 |
+
+Binary: a + b + cin = (cout × 2) + sum
+
+## Architecture
+
+| Component | Neurons |
+|-----------|---------|
+| HA1 (a + b) | 4 |
+| HA2 (s1 + cin) | 4 |
+| OR (c1, c2) | 1 |
+
+**Total: 9 neurons, 21 parameters, 4 layers**
+
+## Composition
+
+```
+s1, c1 = HalfAdder(a, b)
+sum, c2 = HalfAdder(s1, cin)
+cout = OR(c1, c2)
+```
+
+A carry propagates if either half adder produces one.
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+
+w = load_file('model.safetensors')
+
+def full_adder(a, b, cin):
+    # Implementation uses two half adders + OR
+    # See model.py for full implementation
+    pass
+```
+
+## Files
+
+```
+threshold-fulladder/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

@@ -0,0 +1,23 @@
+{
+  "model_type": "threshold_network",
+  "task": "full_adder",
+  "architecture": "3 -> (HA1 + HA2 + OR)",
+  "input_size": 3,
+  "inputs": ["a", "b", "cin"],
+  "outputs": ["sum", "cout"],
+  "num_neurons": 9,
+  "num_parameters": 21,
+  "depth": 4,
+  "activation": "heaviside",
+  "weight_constraints": "integer",
+  "verification": {
+    "method": "coq_proof",
+    "exhaustive": true,
+    "inputs_tested": 8
+  },
+  "accuracy": {
+    "all_inputs": "8/8",
+    "percentage": 100.0
+  },
+  "github": "https://github.com/CharlesCNorton/coq-circuits"
+}

model.py

@@ -0,0 +1,75 @@
+"""
+Threshold Network for Full Adder
+
+Adds three 1-bit inputs (a, b, cin), producing sum and carry outputs.
+Built from two half adders and an OR gate.
+"""
+
+import torch
+from safetensors.torch import load_file
+
+
+def heaviside(x):
+    return (x >= 0).float()
+
+
+class ThresholdFullAdder:
+    """
+    Full adder: sum = a XOR b XOR cin, cout = (a AND b) OR ((a XOR b) AND cin)
+    """
+
+    def __init__(self, weights_dict):
+        self.weights = weights_dict
+
+    def half_adder(self, prefix, a, b):
+        inputs = torch.tensor([float(a), float(b)])
+
+        # XOR for sum
+        or_out = heaviside((inputs * self.weights[f'{prefix}.sum.layer1.or.weight']).sum() +
+                           self.weights[f'{prefix}.sum.layer1.or.bias'])
+        nand_out = heaviside((inputs * self.weights[f'{prefix}.sum.layer1.nand.weight']).sum() +
+                             self.weights[f'{prefix}.sum.layer1.nand.bias'])
+        layer1 = torch.tensor([or_out, nand_out])
+        sum_out = heaviside((layer1 * self.weights[f'{prefix}.sum.layer2.weight']).sum() +
+                            self.weights[f'{prefix}.sum.layer2.bias'])
+
+        # AND for carry
+        carry_out = heaviside((inputs * self.weights[f'{prefix}.carry.weight']).sum() +
+                              self.weights[f'{prefix}.carry.bias'])
+
+        return int(sum_out.item()), int(carry_out.item())
+
+    def __call__(self, a, b, cin):
+        # First half adder: a + b
+        s1, c1 = self.half_adder('ha1', a, b)
+
+        # Second half adder: s1 + cin
+        sum_out, c2 = self.half_adder('ha2', s1, cin)
+
+        # Carry out = c1 OR c2
+        carry_inputs = torch.tensor([float(c1), float(c2)])
+        cout = heaviside((carry_inputs * self.weights['carry_or.weight']).sum() +
+                         self.weights['carry_or.bias'])
+
+        return int(sum_out), int(cout.item())
+
+    @classmethod
+    def from_safetensors(cls, path="model.safetensors"):
+        return cls(load_file(path))
+
+
+if __name__ == "__main__":
+    model = ThresholdFullAdder.from_safetensors("model.safetensors")
+
+    print("Full Adder Truth Table:")
+    print("-" * 40)
+    print("a | b | cin | sum | cout")
+    print("-" * 40)
+    for a in [0, 1]:
+        for b in [0, 1]:
+            for cin in [0, 1]:
+                s, cout = model(a, b, cin)
+                expected_sum = (a + b + cin) % 2
+                expected_cout = (a + b + cin) // 2
+                status = "OK" if (s == expected_sum and cout == expected_cout) else "FAIL"
+                print(f"{a} | {b} |  {cin}  |  {s}  |  {cout}    [{status}]")

model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:33c256206b93b37c9757e6c3cac3bbf3868f6995021b2872e812885719513651
+size 1452