Initial commit: verified MOD-7 threshold circuit

README.md

@@ -0,0 +1,80 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- formal-verification
+- coq
+- mod7
+- modular-arithmetic
+- threshold-network
+- neuromorphic
+---
+
+# tiny-mod7-prover
+
+Formally verified neural network that computes the MOD-7 function (Hamming weight mod 7) on 8-bit inputs. For Coq source code, see [mod7-verified](https://github.com/CharlesCNorton/mod7-verified).
+
+## Overview
+
+Threshold network computing `mod7(x) = HW(x) mod 7` for 8-bit binary inputs. Outputs 0-6 corresponding to the seven residue classes.
+
+**Key properties:**
+- 100% accuracy on all 256 possible inputs
+- Correctness proven in Coq (axiom-free)
+- Integer weights, Heaviside activation
+- Part of the verified MOD-m family
+
+## Architecture
+
+| Layer | Neurons | Function |
+|-------|---------|----------|
+| Input | 8 | Binary input bits |
+| Hidden 1 | 9 | Thermometer encoding |
+| Hidden 2 | 6 | MOD-7 detection |
+| Output | 7 | Classification |
+
+**Total: 22 neurons, 190 parameters**
+
+## Algebraic Insight
+
+For MOD-m, use weights `(1, 1, ..., 1, 1-m)` with `m-1` ones before the reset.
+
+MOD-7 uses `(1, 1, 1, 1, 1, 1, -6)`:
+```
+HW=0: cumsum=0, HW=1: cumsum=1, ..., HW=6: cumsum=6
+HW=7: cumsum=0 (reset: 1+1+1+1+1+1-6=0)
+HW=8: cumsum=1
+```
+
+## Formal Verification
+
+```coq
+Theorem network_correct_exhaustive : verify_all = true.
+Theorem network_correct_constructive : forall x0 x1 x2 x3 x4 x5 x6 x7,
+  predict [x0; x1; x2; x3; x4; x5; x6; x7] = mod7 [x0; x1; x2; x3; x4; x5; x6; x7].
+Theorem cumsum_eq_mod7 : forall k,
+  (k <= 8)%nat -> cumsum k = Z.of_nat (Nat.modulo k 7).
+```
+
+All proofs axiom-free.
+
+## 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) |
+| **tiny-mod7-prover** | MOD-7 | 22 | 190 | (1, 1, 1, 1, 1, 1, -6) |
+
+## Related
+
+- [mod7-verified](https://github.com/CharlesCNorton/mod7-verified) — Coq proofs
+- [tiny-mod5-prover](https://huggingface.co/phanerozoic/tiny-mod5-prover)
+- [tiny-mod3-prover](https://huggingface.co/phanerozoic/tiny-mod3-prover)
+- [tiny-parity-prover](https://huggingface.co/phanerozoic/tiny-parity-prover)
+
+## License
+
+MIT

config.json

@@ -0,0 +1,31 @@
+{
+  "model_type": "threshold_network",
+  "task": "mod7_classification",
+  "architecture": "8 -> 9 -> 6 -> 7",
+  "input_size": 8,
+  "hidden1_size": 9,
+  "hidden2_size": 6,
+  "output_size": 7,
+  "num_parameters": 190,
+  "num_neurons": 22,
+  "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,1,1,-6) on thermometer encoding produce cumsum = HW mod 7",
+  "github": "https://github.com/CharlesCNorton/mod7-verified",
+  "related": {
+    "mod5_model": "https://huggingface.co/phanerozoic/tiny-mod5-prover",
+    "mod3_model": "https://huggingface.co/phanerozoic/tiny-mod3-prover",
+    "parity_model": "https://huggingface.co/phanerozoic/tiny-parity-prover"
+  }
+}

model.py

@@ -0,0 +1,68 @@
+"""
+Inference code for mod7-verified threshold network.
+
+This network computes MOD-7 (Hamming weight mod 7) on 8-bit binary inputs.
+"""
+
+import torch
+import torch.nn as nn
+from safetensors.torch import load_file
+
+
+def heaviside(x):
+    return (x >= 0).float()
+
+
+class Mod7Network(nn.Module):
+    """
+    Verified threshold network for MOD-7 computation.
+    Architecture: 8 -> 9 -> 6 -> 7
+    """
+
+    def __init__(self):
+        super().__init__()
+        self.layer1 = nn.Linear(8, 9)
+        self.layer2 = nn.Linear(9, 6)
+        self.output = nn.Linear(6, 7)
+
+    def forward(self, x):
+        x = x.float()
+        x = heaviside(self.layer1(x))
+        x = heaviside(self.layer2(x))
+        return self.output(x)
+
+    def predict(self, x):
+        return self.forward(x).argmax(dim=-1)
+
+    @classmethod
+    def from_safetensors(cls, path):
+        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 mod7_reference(x):
+    return (x.sum(dim=-1) % 7).long()
+
+
+def verify(model):
+    inputs = torch.zeros(256, 8)
+    for i in range(256):
+        for j in range(8):
+            inputs[i, j] = (i >> j) & 1
+    targets = mod7_reference(inputs)
+    predictions = model.predict(inputs)
+    correct = (predictions == targets).sum().item()
+    print(f"Verification: {correct}/256 ({100*correct/256:.1f}%)")
+    return correct == 256
+
+
+if __name__ == '__main__':
+    model = Mod7Network.from_safetensors('model.safetensors')
+    verify(model)

model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:18f19f668565235b040177e936da5a4cdf4062357e965c46115a13d9965ad621
+size 1184