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

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:

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

Properties

• Commutative: Adding A + B equals B + A
• Identity: Adding 0 preserves the value
• Compositional: Built from two verified FullAdder circuits

Citation

@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}
}