Initial commit: verified MOD-5 threshold circuit

README.md

@@ -0,0 +1,175 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- formal-verification
+- coq
+- mod5
+- modular-arithmetic
+- threshold-network
+- neuromorphic
+---
+
+# tiny-mod5-prover
+
+Formally verified neural network that computes the MOD-5 function (Hamming weight mod 5) on 8-bit inputs. This repository contains the model artifacts; for proof development and Coq source code, see [mod5-verified](https://github.com/CharlesCNorton/mod5-verified).
+
+## Overview
+
+This is a threshold network that computes `mod5(x) = HW(x) mod 5` for 8-bit binary inputs, where HW denotes Hamming weight (number of set bits). The network outputs 0, 1, 2, 3, or 4 corresponding to the five residue classes.
+
+**Key properties:**
+- 100% accuracy on all 256 possible inputs
+- Correctness proven in Coq via constructive algebraic proof
+- Weights constrained to integers
+- Heaviside step activation (x >= 0 -> 1, else 0)
+- Part of the verified MOD-m family: {MOD-2, MOD-3, MOD-5, ...}
+
+## Architecture
+
+| Layer | Neurons | Function |
+|-------|---------|----------|
+| Input | 8 | Binary input bits |
+| Hidden 1 | 9 | Thermometer encoding (HW >= k) |
+| Hidden 2 | 4 | MOD-5 detection |
+| Output | 5 | Classification (one-hot) |
+
+**Total: 18 neurons, 146 parameters**
+
+## Quick Start
+
+```python
+import torch
+from safetensors.torch import load_file
+
+weights = load_file('model.safetensors')
+
+def forward(x, weights):
+    x = x.float()
+    x = (x @ weights['layer1.weight'].T + weights['layer1.bias'] >= 0).float()
+    x = (x @ weights['layer2.weight'].T + weights['layer2.bias'] >= 0).float()
+    out = x @ weights['output.weight'].T + weights['output.bias']
+    return out.argmax(dim=-1)
+
+inputs = torch.tensor([[1, 0, 1, 1, 1, 0, 0, 0]], dtype=torch.float32)
+output = forward(inputs, weights)
+print(f"MOD-5 of [1,0,1,1,1,0,0,0]: {output.item()}")  # 4 (4 bits set, 4 mod 5 = 4)
+```
+
+## Weight Structure
+
+| Tensor | Shape | Values | Description |
+|--------|-------|--------|-------------|
+| `layer1.weight` | [9, 8] | All 1s | Thermometer encoding |
+| `layer1.bias` | [9] | [0, -1, ..., -8] | Threshold at HW >= k |
+| `layer2.weight` | [4, 9] | [0,1,1,1,1,-4,1,1,1] | MOD-5 detection |
+| `layer2.bias` | [4] | [-1, -2, -3, -4] | Class thresholds |
+| `output.weight` | [5, 4] | Various | Classification |
+| `output.bias` | [5] | [0, -1, -1, -1, -1] | Output thresholds |
+
+## Algebraic Insight
+
+The MOD-m construction uses weights `(1, 1, ..., 1, 1-m)` with `m-1` ones before the reset term.
+
+For MOD-5, the pattern `(1, 1, 1, 1, -4)` produces cumulative sums that cycle through `(0, 1, 2, 3, 4, 0, 1, 2, 3, 4, ...)`:
+
+```
+HW=0: cumsum = 0  ->  0 mod 5
+HW=1: cumsum = 1  ->  1 mod 5
+HW=2: cumsum = 2  ->  2 mod 5
+HW=3: cumsum = 3  ->  3 mod 5
+HW=4: cumsum = 4  ->  4 mod 5
+HW=5: cumsum = 0  ->  0 mod 5  (reset: 1+1+1+1-4=0)
+HW=6: cumsum = 1  ->  1 mod 5
+HW=7: cumsum = 2  ->  2 mod 5
+HW=8: cumsum = 3  ->  3 mod 5
+```
+
+## Formal Verification
+
+The network is proven correct in the Coq proof assistant with three independent proofs:
+
+**1. Exhaustive verification:**
+```coq
+Theorem network_correct_exhaustive : verify_all = true.
+Proof. vm_compute. reflexivity. Qed.
+```
+
+**2. Constructive verification (case analysis):**
+```coq
+Theorem network_correct_constructive : forall x0 x1 x2 x3 x4 x5 x6 x7,
+  predict [x0; x1; x2; x3; x4; x5; x6; x7] =
+  mod5 [x0; x1; x2; x3; x4; x5; x6; x7].
+```
+
+**3. Algebraic verification:**
+```coq
+Theorem cumsum_eq_mod5 : forall k,
+  (k <= 8)%nat -> cumsum k = Z.of_nat (Nat.modulo k 5).
+
+Theorem network_algebraic_correct : forall h,
+  (h <= 8)%nat ->
+  classify ... = Nat.modulo h 5.
+```
+
+All proofs are axiom-free ("Closed under the global context").
+
+## MOD-5 Distribution
+
+For 8-bit inputs (256 total):
+
+| Class | Count | Hamming Weights |
+|-------|-------|-----------------|
+| 0 | 57 | 0, 5 |
+| 1 | 36 | 1, 6 |
+| 2 | 36 | 2, 7 |
+| 3 | 57 | 3, 8 |
+| 4 | 70 | 4 |
+
+## The MOD-m Family
+
+| Model | Function | Neurons | Params | Weight Pattern |
+|-------|----------|---------|--------|----------------|
+| tiny-parity-prover | MOD-2 | 14 | 139 | (1, -1) |
+| tiny-mod3-prover | MOD-3 | 14 | 110 | (1, 1, -2) |
+| **tiny-mod5-prover** | MOD-5 | 18 | 146 | (1, 1, 1, 1, -4) |
+
+## Limitations
+
+- **Fixed input size**: 8 bits only (algebraic construction extends to any n)
+- **Binary inputs**: Expects {0, 1}, not continuous values
+- **No noise margin**: Heaviside threshold at exactly 0
+- **Not differentiable**: Cannot be fine-tuned with gradient descent
+
+## Files
+
+```
+tiny-mod5-prover/
+├── model.safetensors    # Network weights (146 params)
+├── model.py             # Inference code
+├── config.json          # Model metadata
+└── README.md            # This file
+```
+
+## Citation
+
+```bibtex
+@software{tiny_mod5_prover_2026,
+  title={tiny-mod5-prover: Formally Verified Threshold Network for MOD-5},
+  author={Norton, Charles},
+  url={https://huggingface.co/phanerozoic/tiny-mod5-prover},
+  year={2026},
+  note={Part of the verified MOD-m threshold circuit family}
+}
+```
+
+## Related
+
+- **Proof repository**: [mod5-verified](https://github.com/CharlesCNorton/mod5-verified)
+- **MOD-3 network**: [tiny-mod3-prover](https://huggingface.co/phanerozoic/tiny-mod3-prover)
+- **Parity network**: [tiny-parity-prover](https://huggingface.co/phanerozoic/tiny-parity-prover)
+
+## License
+
+MIT

config.json

@@ -0,0 +1,30 @@
+{
+  "model_type": "threshold_network",
+  "task": "mod5_classification",
+  "architecture": "8 -> 9 -> 4 -> 5",
+  "input_size": 8,
+  "hidden1_size": 9,
+  "hidden2_size": 4,
+  "output_size": 5,
+  "num_parameters": 146,
+  "num_neurons": 18,
+  "activation": "heaviside",
+  "weight_constraints": "integer",
+  "verification": {
+    "method": "coq_proof",
+    "exhaustive": true,
+    "constructive": true,
+    "algebraic": true,
+    "axiom_free": true
+  },
+  "accuracy": {
+    "all_inputs": "256/256",
+    "percentage": 100.0
+  },
+  "algebraic_insight": "Weights (1,1,1,1,-4) on thermometer encoding produce cumsum = HW mod 5",
+  "github": "https://github.com/CharlesCNorton/mod5-verified",
+  "related": {
+    "mod3_model": "https://huggingface.co/phanerozoic/tiny-mod3-prover",
+    "parity_model": "https://huggingface.co/phanerozoic/tiny-parity-prover"
+  }
+}

model.py

@@ -0,0 +1,119 @@
+"""
+Inference code for mod5-verified threshold network.
+
+This network computes MOD-5 (Hamming weight mod 5) on 8-bit binary inputs.
+"""
+
+import torch
+import torch.nn as nn
+from safetensors.torch import load_file
+
+
+def heaviside(x):
+    """Heaviside step function: 1 if x >= 0, else 0."""
+    return (x >= 0).float()
+
+
+class Mod5Network(nn.Module):
+    """
+    Verified threshold network for MOD-5 computation.
+
+    Architecture: 8 -> 9 -> 4 -> 5
+    - Layer 1: Thermometer encoding (9 neurons detect HW >= k)
+    - Layer 2: MOD-5 detection using (1,1,1,1,-4) weight pattern
+    - Output: 5-class classification
+    """
+
+    def __init__(self):
+        super().__init__()
+        self.layer1 = nn.Linear(8, 9)
+        self.layer2 = nn.Linear(9, 4)
+        self.output = nn.Linear(4, 5)
+
+    def forward(self, x):
+        """Forward pass with Heaviside activation."""
+        x = x.float()
+        x = heaviside(self.layer1(x))
+        x = heaviside(self.layer2(x))
+        x = self.output(x)
+        return x
+
+    def predict(self, x):
+        """Get predicted class (0, 1, 2, 3, or 4)."""
+        return self.forward(x).argmax(dim=-1)
+
+    @classmethod
+    def from_safetensors(cls, path):
+        """Load model from safetensors file."""
+        model = cls()
+        weights = load_file(path)
+
+        model.layer1.weight.data = weights['layer1.weight']
+        model.layer1.bias.data = weights['layer1.bias']
+        model.layer2.weight.data = weights['layer2.weight']
+        model.layer2.bias.data = weights['layer2.bias']
+        model.output.weight.data = weights['output.weight']
+        model.output.bias.data = weights['output.bias']
+
+        return model
+
+
+def mod5_reference(x):
+    """Reference implementation: Hamming weight mod 5."""
+    return (x.sum(dim=-1) % 5).long()
+
+
+def verify(model, verbose=True):
+    """Verify model on all 256 inputs."""
+    inputs = torch.zeros(256, 8)
+    for i in range(256):
+        for j in range(8):
+            inputs[i, j] = (i >> j) & 1
+
+    targets = mod5_reference(inputs)
+    predictions = model.predict(inputs)
+
+    correct = (predictions == targets).sum().item()
+
+    if verbose:
+        print(f"Verification: {correct}/256 ({100*correct/256:.1f}%)")
+
+        if correct < 256:
+            errors = (predictions != targets).nonzero(as_tuple=True)[0]
+            print(f"Errors at indices: {errors[:10].tolist()}")
+
+    return correct == 256
+
+
+def demo():
+    """Demonstration of MOD-5 computation."""
+    print("Loading mod5-verified model...")
+    model = Mod5Network.from_safetensors('model.safetensors')
+
+    print("\nVerifying on all 256 inputs...")
+    verify(model)
+
+    print("\nExample predictions:")
+    test_cases = [
+        [0, 0, 0, 0, 0, 0, 0, 0],
+        [1, 0, 0, 0, 0, 0, 0, 0],
+        [1, 1, 0, 0, 0, 0, 0, 0],
+        [1, 1, 1, 0, 0, 0, 0, 0],
+        [1, 1, 1, 1, 0, 0, 0, 0],
+        [1, 1, 1, 1, 1, 0, 0, 0],
+        [1, 1, 1, 1, 1, 1, 0, 0],
+        [1, 1, 1, 1, 1, 1, 1, 0],
+        [1, 1, 1, 1, 1, 1, 1, 1],
+    ]
+
+    for bits in test_cases:
+        x = torch.tensor([bits], dtype=torch.float32)
+        hw = sum(bits)
+        pred = model.predict(x).item()
+        expected = hw % 5
+        status = "OK" if pred == expected else "ERROR"
+        print(f"  {bits} -> HW={hw}, pred={pred}, expected={expected} [{status}]")
+
+
+if __name__ == '__main__':
+    demo()

model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:56840ae01951fd606bfc6aadb521629c1860752d8886efaad1ecd6bd2583707d
+size 1008