Rename from tiny-HalfAdder-verified

README.md

@@ -0,0 +1,108 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+- arithmetic
+---
+
+# threshold-halfadder
+
+Adds two 1-bit inputs, producing sum and carry. The building block for all multi-bit adders.
+
+## Circuit
+
+```
+      a       b
+      │       │
+      ├───┬───┤
+      │   │   │
+      ▼   │   ▼
+  ┌──────┐│┌──────┐
+  │  OR  │││ NAND │
+  └──────┘│└──────┘
+      │   │   │
+      └───┼───┘
+          ▼               a   b
+      ┌──────┐            │   │
+      │ AND  │            └─┬─┘
+      └──────┘              ▼
+          │            ┌──────┐
+          ▼            │ AND  │
+        sum            └──────┘
+                           │
+                           ▼
+                        carry
+```
+
+The sum output uses XOR (2 layers), the carry uses AND (1 layer).
+
+## Truth Table
+
+| a | b | sum | carry |
+|---|---|-----|-------|
+| 0 | 0 | 0 | 0 |
+| 0 | 1 | 1 | 0 |
+| 1 | 0 | 1 | 0 |
+| 1 | 1 | 0 | 1 |
+
+Binary: a + b = (carry × 2) + sum
+
+## Components
+
+| Output | Function | Neurons | Layers |
+|--------|----------|---------|--------|
+| sum | XOR(a, b) | 3 | 2 |
+| carry | AND(a, b) | 1 | 1 |
+
+**Total: 4 neurons, 12 parameters**
+
+## Arithmetic
+
+The half adder computes a + b where a, b ∈ {0, 1}:
+
+- 0 + 0 = 0 (sum=0, carry=0)
+- 0 + 1 = 1 (sum=1, carry=0)
+- 1 + 0 = 1 (sum=1, carry=0)
+- 1 + 1 = 2 (sum=0, carry=1)
+
+The carry represents the 2s place.
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+import torch
+
+w = load_file('model.safetensors')
+
+def half_adder(a, b):
+    inp = torch.tensor([float(a), float(b)])
+
+    # XOR for sum
+    or_out = int((inp @ w['xor.layer1.or.weight'] + w['xor.layer1.or.bias']).sum() >= 0)
+    nand_out = int((inp @ w['xor.layer1.nand.weight'] + w['xor.layer1.nand.bias']).sum() >= 0)
+    xor_inp = torch.tensor([float(or_out), float(nand_out)])
+    sum_out = int((xor_inp @ w['xor.layer2.weight'] + w['xor.layer2.bias']).sum() >= 0)
+
+    # AND for carry
+    carry_out = int((inp @ w['carry.weight'] + w['carry.bias']).sum() >= 0)
+
+    return sum_out, carry_out
+```
+
+## Files
+
+```
+threshold-halfadder/
+├── model.safetensors
+├── model.py
+├── config.json
+└── README.md
+```
+
+## License
+
+MIT

config.json

@@ -0,0 +1,22 @@
+{
+  "model_type": "threshold_network",
+  "task": "half_adder",
+  "architecture": "2 -> (XOR:2->2->1, AND:1)",
+  "input_size": 2,
+  "outputs": ["sum", "carry"],
+  "num_neurons": 4,
+  "num_parameters": 12,
+  "depth": 2,
+  "activation": "heaviside",
+  "weight_constraints": "integer",
+  "verification": {
+    "method": "coq_proof",
+    "exhaustive": true,
+    "inputs_tested": 4
+  },
+  "accuracy": {
+    "all_inputs": "4/4",
+    "percentage": 100.0
+  },
+  "github": "https://github.com/CharlesCNorton/coq-circuits"
+}

model.py

@@ -0,0 +1,60 @@
+"""
+Threshold Network for Half Adder
+
+Adds two 1-bit inputs, producing sum (XOR) and carry (AND) outputs.
+Sum uses 2-layer XOR, Carry uses single AND neuron.
+"""
+
+import torch
+from safetensors.torch import load_file
+
+
+def heaviside(x):
+    return (x >= 0).float()
+
+
+class ThresholdHalfAdder:
+    """
+    Half adder: sum = a XOR b, carry = a AND b
+    """
+
+    def __init__(self, weights_dict):
+        self.weights = weights_dict
+
+    def __call__(self, a, b):
+        inputs = torch.tensor([float(a), float(b)])
+
+        # Sum = XOR (2-layer)
+        or_out = heaviside((inputs * self.weights['sum.layer1.or.weight']).sum() +
+                           self.weights['sum.layer1.or.bias'])
+        nand_out = heaviside((inputs * self.weights['sum.layer1.nand.weight']).sum() +
+                             self.weights['sum.layer1.nand.bias'])
+        layer1 = torch.tensor([or_out, nand_out])
+        sum_out = heaviside((layer1 * self.weights['sum.layer2.weight']).sum() +
+                            self.weights['sum.layer2.bias'])
+
+        # Carry = AND (single neuron)
+        carry_out = heaviside((inputs * self.weights['carry.weight']).sum() +
+                              self.weights['carry.bias'])
+
+        return int(sum_out.item()), int(carry_out.item())
+
+    @classmethod
+    def from_safetensors(cls, path="model.safetensors"):
+        return cls(load_file(path))
+
+
+if __name__ == "__main__":
+    model = ThresholdHalfAdder.from_safetensors("model.safetensors")
+
+    print("Half Adder Truth Table:")
+    print("-" * 30)
+    print("a | b | sum | carry")
+    print("-" * 30)
+    for a in [0, 1]:
+        for b in [0, 1]:
+            s, c = model(a, b)
+            expected_s = a ^ b
+            expected_c = a & b
+            status = "OK" if (s == expected_s and c == expected_c) else "FAIL"
+            print(f"{a} | {b} |  {s}  |   {c}    [{status}]")

model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:646d37de6dcc9da2b95118e8f1066dd7fb6fe274b4a354187641035272c0b053
+size 624