Upload README.md with huggingface_hub

README.md

@@ -0,0 +1,106 @@
+---
+license: mit
+tags:
+- formal-verification
+- coq
+- threshold-logic
+- neuromorphic
+- arithmetic
+- adder
+---
+
+# tiny-RippleCarry2Bit-verified
+
+Formally verified 2-bit ripple carry adder. Chains two full adders to add two 2-bit numbers with 100% accuracy.
+
+## Architecture
+
+| Component | Value |
+|-----------|-------|
+| Inputs | 4 (a1, a0, b1, b0) |
+| Outputs | 3 (cout, s1, s0) |
+| Neurons | 8 (2 full adders × 4 neurons each) |
+| Parameters | 24 (2 full adders × 12 params each) |
+| Layers | 2 (chained full adders) |
+| Activation | Heaviside step |
+
+## Key Properties
+
+- 100% accuracy (16/16 input combinations correct)
+- Coq-proven correctness
+- Compositional construction from verified full adders
+- Produces 3-bit output (sum can be 0-6, requiring 3 bits)
+- Compatible with neuromorphic hardware
+
+## Circuit Structure
+
+```
+a1 a0    b1 b0
+ |  |     |  |
+ |  +--+--+  |
+ |     |     |
+ |   FA0 (cin=0)
+ |     |     |
+ |    s0    c0
+ |     |     |
+ +--+--+-----+
+    |
+   FA1
+    |
+   s1  c1
+```
+
+First full adder adds least significant bits (a0 + b0 + 0), producing sum bit s0 and carry c0. Second full adder adds most significant bits with the carry (a1 + b1 + c0), producing s1 and final carry cout.
+
+## Usage
+
+```python
+import torch
+from safetensors.torch import load_file
+
+weights = load_file('ripplecarry2bit.safetensors')
+
+def full_adder_sim(a, b, cin):
+    sum_out = a ^ b ^ cin
+    carry_out = (a & b) | (cin & (a ^ b))
+    return sum_out, carry_out
+
+def ripple_carry_2bit(a1, a0, b1, b0):
+    s0, c0 = full_adder_sim(a0, b0, 0)
+    s1, cout = full_adder_sim(a1, b1, c0)
+    return cout, s1, s0
+
+# Test
+print(ripple_carry_2bit(1, 1, 1, 0))  # 3 + 2 = 5 -> (1, 0, 1)
+print(ripple_carry_2bit(1, 0, 1, 0))  # 2 + 2 = 4 -> (1, 0, 0)
+print(ripple_carry_2bit(0, 1, 0, 1))  # 1 + 1 = 2 -> (0, 1, 0)
+```
+
+## Verification
+
+**Coq Theorem**:
+```coq
+Theorem ripple_carry_2bit_correct : forall a1 a0 b1 b0,
+  ripple_carry_2bit a1 a0 b1 b0 = ripple_carry_2bit_spec a1 a0 b1 b0.
+```
+
+Proven axiom-free via exhaustive case analysis on all 16 input combinations.
+
+Full proof: [coq-circuits/Arithmetic/RippleCarry2Bit.v](https://github.com/CharlesCNorton/coq-circuits/blob/main/coq/Arithmetic/RippleCarry2Bit.v)
+
+## Properties
+
+- **Commutative**: Adding A + B equals B + A
+- **Identity**: Adding 0 preserves the value
+- **Compositional**: Built from two verified FullAdder circuits
+
+## Citation
+
+```bibtex
+@software{tiny_ripplecarry2bit_verified_2025,
+  title={tiny-RippleCarry2Bit-verified: Formally Verified 2-Bit Ripple Carry Adder},
+  author={Norton, Charles},
+  url={https://huggingface.co/phanerozoic/tiny-RippleCarry2Bit-verified},
+  year={2025}
+}
+```