| # Reverse Quantum Walk over ER Bridge |
|
|
| [](LICENSE) |
| [](LICENSE) |
| [](LICENSE) |
| [](crates/) |
| [](crates/kani-verification/) |
| [](lean/) |
| [](agda/) |
| [](hardware/) |
| [](circuits/) |
| [](LICENSE) |
| [](https://github.com/SNAPKITTYWEST) |
|
|
| **Authors:** Jessica L. Westerhoff (SNAPKITTYWEST), Ahmad Ali Parr |
| **Trust:** Bel Esprit D'Accord Irrevocable Trust · EIN 42-697643 |
|
|
| > **Full sovereign stack for time-reversible quantum walk dynamics over an ER bridge.** |
| > Recurrence engine · Primitive Shattering Matrix · Kani model checking · Lean 4 · Agda · ZK circuits · SystemVerilog interlock |
|
|
| --- |
|
|
| ## What This Is |
|
|
| A **formally verified, hardware-grounded** implementation of reverse quantum walk dynamics over the ER = EPR bridge. |
|
|
| The core insight: replacing discrete finite-field R1CS constraints `A·B − C = 0 mod p` with continuous spatial constraints over ℝᴺ turns zero-knowledge logic into a CAD geometric solver engine. Every 256-bit scalar field element is **shattered** into 1-bit microbits satisfying `b·(1−b) = 0`, processed through a bit-serial full-adder array, and reconstructed with bounded drift. |
|
|
| --- |
|
|
| ## Architecture |
|
|
| ``` |
| 𝔽ₚ scalar field |
| ↓ Primitive Shattering Matrix |
| ↓ b·(1−b) = 0 (microbit invariant) |
| ↓ |
| MicrobitShard32 ──→ bit-serial full-adder ──→ reconstructed state |
| ↓ ↓ |
| RecurrenceState drift accumulator |
| x ∈ [-2·SCALE, 2·SCALE] ≤ TAU_R_MAX_DRIFT |
| L_eff ≤ L_EFF_MAX (interlock trips if exceeded) |
| ↓ |
| CAD Kernel (Newton-Raphson on C(X) = 0) |
| ↓ |
| Agda zero-sorry proof ──→ systemInvariant ≡ true |
| ``` |
|
|
| --- |
|
|
| ## Stack |
|
|
| | Layer | Files | What it does | |
| |---|---|---| |
| | **Rust engine** | `crates/engine/src/recurrence.rs` | Q16.16 fixed-point recurrence. `SCALE=65536`, `L_EFF_MAX=65530`, `TAU_R_MAX_DRIFT=1024`. Contraction: `L_eff < 1`. | |
| | **Primitive Shattering** | `crates/engine/src/microbit.rs` | Shatters 32-bit values into 32 `Microbit` shards. `b*(1-b)==0` enforced. NAND/XOR/AND/OR. `add_bounded()` with drift gate. | |
| | **CAD Kernel** | `crates/engine/src/cad_kernel.rs` | Newton-Raphson 2D constraint solver. Jacobian build + gradient projection. Replaces discrete R1CS with continuous `C(X)=0`. | |
| | **Kani** | `crates/kani-verification/src/lib.rs` | Model-checks all bounds: `l_eff ≤ L_EFF_MAX`, `drift ≤ TAU_R_MAX_DRIFT`. Run: `cargo kani` | |
| | **Lean 4** | `lean/Multiplicity/Dynamics/Contraction.lean` | `step_bounded` theorem — sorry pending (discharge: omega + linarith) | |
| | **Agda** | `agda/MultiplicityInvariants.agda` | 16-invariant conjunction from recurrence + Kani + Lean + crypto + CAD. `proof = refl`. | |
| | **Agda** | `agda/PrimitiveShattering.agda` | `Bit`, `shatter`, `reconstruct`, `driftCount`, `InterlockState`. `SystemInvariant` record. | |
| | **SystemVerilog** | `hardware/microbit_interlock.sv` | Bit-serial microbit interlock. Fails **closed** if `drift_accumulator > MAX_DRIFT_THRESHOLD`. | |
| | **Circom ZK** | `circuits/MicrobitFullAdder.circom` | `a*(1-a)===0` R1CS bit-validity. Quadratic carry: `cout <== a*b + cin*axorb`. | |
| | **Circom ZK** | `circuits/MicrobitAdderAndDrift.circom` | 32-bit ripple-carry + `LessEqThan(16)` drift gate. `interlockTripped = 1` on breach. | |
|
|
| --- |
|
|
| ## Primitive Shattering Matrix |
|
|
| Every 256-bit scalar field constraint across circuits is shattered into 1-bit boolean invariants: |
|
|
| | Primitive Circuit | Monolithic Constraint | Shattered Decomposition | Reconstructed Primitive | |
| |---|---|---|---| |
| | `DriftBound.circom` | `D_T ≤ τ_R` | `D = Σ bᵢ·2ⁱ`, carry gates | Bitwise Range Gate | |
| | `PrimeCheck.circom` | `aᵈ ≡ 1 mod n` | Bitwise Sieve Matrix | Sieved Bit-Mask | |
| | `UORMatMul.circom` | `C_ij = Σ A_ik·B_kj` | Carry-Save Grid | Bit-Sliced Accumulator | |
| | `ace.circom` | `L_eff·X ≤ X_max` | Full-Adder carry chain over Q16.16 limbs | Microbit ALU Interlock | |
|
|
| --- |
|
|
| ## Invariants |
|
|
| | Invariant | Value | Enforced by | |
| |---|---|---| |
| | Q16.16 scale | `SCALE = 65536` | Rust + Agda | |
| | Contraction bound | `L_eff ≤ 65530 (< 1)` | Rust + Kani + Lean 4 | |
| | Drift bound | `drift ≤ 1024` | Rust + Kani + SV + Circom | |
| | Bit validity | `b·(1−b) = 0` | Rust + Circom + Agda | |
| | Entropy bound | `H ≤ 0.20 nats` | Agda (NAND-encoded) | |
| | Spectral radius | `ρ < 1.0 − 1e-6` | Agda | |
| | Poseidon2 budget | `5087 R1CS` | Agda | |
| | Dilithium5 | `2592-byte PK / 4627-byte Sig` | Agda | |
|
|
| --- |
|
|
| ## Quick Start |
|
|
| ```bash |
| # Build Rust workspace |
| cargo build |
| |
| # Run Kani model checking (requires cargo-kani) |
| cargo kani |
| |
| # Check Lean 4 proofs (requires lake) |
| cd lean && lake build |
| |
| # Check Agda proofs (requires agda) |
| agda agda/MultiplicityInvariants.agda |
| agda agda/PrimitiveShattering.agda |
| |
| # Compile Circom circuits (requires circom + snarkjs) |
| cd circuits && circom MicrobitAdderAndDrift.circom --r1cs --wasm |
| ``` |
|
|
| --- |
|
|
| ## License |
|
|
| **Tri-License: BSL-1.1 / AGPL-3.0 / MPL-2.0 + Commercial** |
| © 2026 Bel Esprit D'Accord Irrevocable Trust · SNAPKITTYWEST |
| See [LICENSE](LICENSE) for full terms. |
|
|
| - Research / evaluation → BSL-1.1 (free) |
| - Network deployment / SaaS → AGPL-3.0 (mandatory copyleft) |
| - File-level modification → MPL-2.0 |
| - Commercial copyleft bypass → contact `licensing@snapkittywest.dev` |
|
|
