Upload README.md with huggingface_hub
Browse files
README.md
ADDED
|
@@ -0,0 +1,153 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
---
|
| 2 |
+
license: mit
|
| 3 |
+
tags:
|
| 4 |
+
- threshold-logic
|
| 5 |
+
- neuromorphic
|
| 6 |
+
- computer-architecture
|
| 7 |
+
- coq
|
| 8 |
+
- turing-complete
|
| 9 |
+
---
|
| 10 |
+
|
| 11 |
+
# 8bit-threshold-computer
|
| 12 |
+
|
| 13 |
+
A complete 8-bit computer implemented entirely in threshold logic neurons. All computation uses weighted sums with Heaviside step activation - no traditional logic gates.
|
| 14 |
+
|
| 15 |
+
## Architecture
|
| 16 |
+
|
| 17 |
+
| Component | Specification |
|
| 18 |
+
|-----------|---------------|
|
| 19 |
+
| Registers | 4 × 8-bit (R0, R1, R2, R3) |
|
| 20 |
+
| Memory | 256 bytes |
|
| 21 |
+
| Program Counter | 8-bit |
|
| 22 |
+
| Instruction Width | 16-bit |
|
| 23 |
+
| ALU Operations | 16 |
|
| 24 |
+
| Status Flags | Z, N, C, V |
|
| 25 |
+
| Circuits | 93 verified |
|
| 26 |
+
| Parameters | 2,377 |
|
| 27 |
+
|
| 28 |
+
## Instruction Set
|
| 29 |
+
|
| 30 |
+
### ALU Operations (opcode 0-12)
|
| 31 |
+
| Op | Mnemonic | Operation |
|
| 32 |
+
|----|----------|-----------|
|
| 33 |
+
| 0 | ADD | dest = src1 + src2 |
|
| 34 |
+
| 1 | SUB | dest = src1 - src2 |
|
| 35 |
+
| 2 | AND | dest = src1 & src2 |
|
| 36 |
+
| 3 | OR | dest = src1 \| src2 |
|
| 37 |
+
| 4 | XOR | dest = src1 ^ src2 |
|
| 38 |
+
| 5 | NOT | dest = ~src1 |
|
| 39 |
+
| 6 | SHL | dest = src1 << 1 |
|
| 40 |
+
| 7 | SHR | dest = src1 >> 1 |
|
| 41 |
+
| 8 | INC | dest = src1 + 1 |
|
| 42 |
+
| 9 | DEC | dest = src1 - 1 |
|
| 43 |
+
| 10 | CMP | flags = src1 - src2 |
|
| 44 |
+
| 11 | NEG | dest = -src1 |
|
| 45 |
+
| 12 | MOV | dest = src1 |
|
| 46 |
+
| 13 | LDI | dest = immediate |
|
| 47 |
+
|
| 48 |
+
### Control Flow (opcode 14)
|
| 49 |
+
| Cond | Mnemonic | Condition |
|
| 50 |
+
|------|----------|-----------|
|
| 51 |
+
| 0 | JMP | unconditional |
|
| 52 |
+
| 1 | JZ | Z = 1 |
|
| 53 |
+
| 2 | JNZ | Z = 0 |
|
| 54 |
+
| 3 | JC | C = 1 |
|
| 55 |
+
| 4 | JNC | C = 0 |
|
| 56 |
+
| 5 | JN | N = 1 |
|
| 57 |
+
| 6 | JP | N = 0 |
|
| 58 |
+
| 7 | JV | V = 1 |
|
| 59 |
+
|
| 60 |
+
### Extended Operations (opcode 15)
|
| 61 |
+
| Sub | Mnemonic | Operation |
|
| 62 |
+
|-----|----------|-----------|
|
| 63 |
+
| 0 | NOP | no operation |
|
| 64 |
+
| 1 | LD | load from memory |
|
| 65 |
+
| 2 | ST | store to memory |
|
| 66 |
+
| 3 | PUSH | push to stack |
|
| 67 |
+
| 4 | POP | pop from stack |
|
| 68 |
+
| 5 | CALL | call subroutine |
|
| 69 |
+
| 6 | RET | return |
|
| 70 |
+
|
| 71 |
+
## Usage
|
| 72 |
+
|
| 73 |
+
```python
|
| 74 |
+
from safetensors.torch import load_file
|
| 75 |
+
|
| 76 |
+
weights = load_file("neural_computer.safetensors")
|
| 77 |
+
|
| 78 |
+
# All operations use threshold neurons:
|
| 79 |
+
# output = 1 if sum(weight * input) + bias >= 0 else 0
|
| 80 |
+
```
|
| 81 |
+
|
| 82 |
+
## Example Programs
|
| 83 |
+
|
| 84 |
+
**Sum 1 to 10:**
|
| 85 |
+
```asm
|
| 86 |
+
LDI R0, 0 ; sum = 0
|
| 87 |
+
LDI R1, 10 ; counter = 10
|
| 88 |
+
ADD R0, R0, R1 ; sum += counter
|
| 89 |
+
DEC R1, R1 ; counter--
|
| 90 |
+
JNZ 4 ; loop if counter > 0
|
| 91 |
+
; Result: R0 = 55
|
| 92 |
+
```
|
| 93 |
+
|
| 94 |
+
**Fibonacci:**
|
| 95 |
+
```asm
|
| 96 |
+
LDI R0, 1 ; fib(n-2)
|
| 97 |
+
LDI R1, 1 ; fib(n-1)
|
| 98 |
+
LDI R2, 6 ; iterations
|
| 99 |
+
ADD R3, R0, R1 ; fib(n) = fib(n-2) + fib(n-1)
|
| 100 |
+
MOV R0, R1
|
| 101 |
+
MOV R1, R3
|
| 102 |
+
DEC R2, R2
|
| 103 |
+
JNZ 6
|
| 104 |
+
; Result: R1 = 21 (fib(8))
|
| 105 |
+
```
|
| 106 |
+
|
| 107 |
+
## Verification
|
| 108 |
+
|
| 109 |
+
Circuit weights derived from Coq proofs. Each circuit proven correct using:
|
| 110 |
+
1. **Exhaustive verification** - all inputs tested
|
| 111 |
+
2. **Universal quantification** - symbolic proofs
|
| 112 |
+
3. **Algebraic characterization** - weight pattern correctness
|
| 113 |
+
|
| 114 |
+
Note: The extraction from Coq to weights is not itself formally verified. The proofs establish correctness of the circuit specifications; the weights are a faithful transcription.
|
| 115 |
+
|
| 116 |
+
## Circuit Categories
|
| 117 |
+
|
| 118 |
+
| Category | Count | Examples |
|
| 119 |
+
|----------|-------|----------|
|
| 120 |
+
| Boolean | 9 | AND, OR, XOR, NAND, NOR |
|
| 121 |
+
| Modular | 11 | MOD-2 through MOD-12 |
|
| 122 |
+
| Threshold | 13 | Majority, k-out-of-n |
|
| 123 |
+
| Arithmetic | 17 | Adders, comparators |
|
| 124 |
+
| Error | 11 | Parity, Hamming, CRC |
|
| 125 |
+
| Pattern | 10 | PopCount, symmetry |
|
| 126 |
+
| Combinational | 10 | Mux, encoder, decoder |
|
| 127 |
+
| ALU | 3 | Flags, control, ALU8Bit |
|
| 128 |
+
| Control | 9 | Jump, conditional, stack |
|
| 129 |
+
|
| 130 |
+
## Hardware Compatibility
|
| 131 |
+
|
| 132 |
+
Designed for neuromorphic processors:
|
| 133 |
+
- Intel Loihi
|
| 134 |
+
- IBM TrueNorth
|
| 135 |
+
- BrainChip Akida
|
| 136 |
+
|
| 137 |
+
All weights are integers. All activations are Heaviside step.
|
| 138 |
+
|
| 139 |
+
## Citation
|
| 140 |
+
|
| 141 |
+
```bibtex
|
| 142 |
+
@software{threshold_computer_2025,
|
| 143 |
+
title={8bit-threshold-computer: Turing-Complete Threshold Logic Computer},
|
| 144 |
+
author={Norton, Charles},
|
| 145 |
+
url={https://huggingface.co/phanerozoic/8bit-threshold-computer},
|
| 146 |
+
year={2025}
|
| 147 |
+
}
|
| 148 |
+
```
|
| 149 |
+
|
| 150 |
+
## Links
|
| 151 |
+
|
| 152 |
+
- [GitHub Repository](https://github.com/CharlesCNorton/coq-circuits)
|
| 153 |
+
- [Coq Proofs](https://github.com/CharlesCNorton/coq-circuits/tree/main/coq)
|