|
|
--- |
|
|
license: mit |
|
|
tags: |
|
|
- formal-verification |
|
|
- coq |
|
|
- threshold-logic |
|
|
- neuromorphic |
|
|
- functionally-complete |
|
|
--- |
|
|
|
|
|
# tiny-NOR-verified |
|
|
|
|
|
Formally verified NOR gate. Single threshold neuron computing negated disjunction with 100% accuracy. |
|
|
|
|
|
## Architecture |
|
|
|
|
|
| Component | Value | |
|
|
|-----------|-------| |
|
|
| Inputs | 2 | |
|
|
| Outputs | 1 | |
|
|
| Neurons | 1 | |
|
|
| Parameters | 3 | |
|
|
| Weights | [-1, -1] | |
|
|
| Bias | 0 | |
|
|
| Activation | Heaviside step | |
|
|
|
|
|
## Key Properties |
|
|
|
|
|
- 100% accuracy (4/4 inputs correct) |
|
|
- Coq-proven correctness |
|
|
- Single threshold neuron |
|
|
- Integer weights |
|
|
- Commutative: NOR(x,y) = NOR(y,x) |
|
|
- Functionally complete (can build any Boolean function) |
|
|
- Self-dual: NOR(x,x) = NOT(x) |
|
|
|
|
|
## Usage |
|
|
|
|
|
```python |
|
|
import torch |
|
|
from safetensors.torch import load_file |
|
|
|
|
|
weights = load_file('nor.safetensors') |
|
|
|
|
|
def nor_gate(x, y): |
|
|
# Heaviside: weighted_sum + bias >= 0 |
|
|
inputs = torch.tensor([float(x), float(y)]) |
|
|
weighted_sum = (inputs * weights['weight']).sum() + weights['bias'] |
|
|
return int(weighted_sum >= 0) |
|
|
|
|
|
# Test |
|
|
print(nor_gate(0, 0)) # 1 |
|
|
print(nor_gate(0, 1)) # 0 |
|
|
print(nor_gate(1, 0)) # 0 |
|
|
print(nor_gate(1, 1)) # 0 |
|
|
``` |
|
|
|
|
|
## Verification |
|
|
|
|
|
**Coq Theorem**: |
|
|
```coq |
|
|
Theorem nor_correct : forall x y, nor_circuit x y = negb (orb x y). |
|
|
``` |
|
|
|
|
|
Proven axiom-free with properties: |
|
|
- Commutativity |
|
|
- Self-duality (NOR(x,x) = NOT(x)) |
|
|
- Functional completeness |
|
|
- Identity with false gives NOT |
|
|
- Absorption with true gives false |
|
|
|
|
|
Full proof: [coq-circuits/Boolean/NOR.v](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/Boolean/NOR.v) |
|
|
|
|
|
## Circuit Operation |
|
|
|
|
|
Input combination produces weighted sum: |
|
|
- (0,0): 0*(-1) + 0*(-1) + 0 = 0 >= 0 → 1 |
|
|
- (0,1): 0*(-1) + 1*(-1) + 0 = -1 < 0 → 0 |
|
|
- (1,0): 1*(-1) + 0*(-1) + 0 = -1 < 0 → 0 |
|
|
- (1,1): 1*(-1) + 1*(-1) + 0 = -2 < 0 → 0 |
|
|
|
|
|
Fires only when both inputs are false. |
|
|
|
|
|
## Functional Completeness |
|
|
|
|
|
NOR is functionally complete - any Boolean function can be built from NOR gates alone. This makes it particularly important for circuit composition. |
|
|
|
|
|
## Citation |
|
|
|
|
|
```bibtex |
|
|
@software{tiny_nor_prover_2025, |
|
|
title={tiny-NOR-verified: Formally Verified NOR Gate}, |
|
|
author={Norton, Charles}, |
|
|
url={https://huggingface.co/phanerozoic/tiny-NOR-verified}, |
|
|
year={2025} |
|
|
} |
|
|
``` |
|
|
|
