Follow the launch: qubic.org/doge-countdown Hashrate Tracker: doge-stats.qubic.org/ #DogeMeetsQubic

Turns out we're all just math maximalists trying to break past the limitations everyone else thinks are inevitable. Great space @ModulusZK🩸🤝

Nobody would understand this, which is sort of the point when I say that @ModulusZK provides a solution to this problem, that removes all these inherent VM based complexities. What nobody in the ZK space has yet considered… is what happens when we’re right? (Zoom required 📷)

The best part about @ModulusZK is that we’ll deliver 100-1000X computation savings & 10-100X cheaper ZK with math that was first proved possible in the 1930s. That is the level of tunnel vision crypto has been built with to date… “Do you think that’s air you’re breathing now?”

We don't ask what Bitcoin can do for us. We answer what we can do for Bitcoin. moduluszk.medium.com/introdu…

“ $ZEC ” Naaa we’ll be fine! Unless they figure out how to add privacy and programmability to $BTC at its core network level we’ll be okay… “@ModulusZK” Ahh Zcash… Programmability and privacy directly on Bitcoin 🙄

ZK-FOL (or zkFOL) is a proposed soft fork for Bitcoin developed by @ModulusZK, a blockchain project focused on zero-knowledge (ZK) proofs for enhanced privacy, scalability, and functionality. It enables native privacy features and decentralized finance (DeFi) applications—such as swaps, loans, vaults, and yield farming—directly on Bitcoin without compromising its core security, determinism, or introducing new vulnerabilities. Key Concepts •Arithmetization of First-Order Logic (FOL): Traditional ZK systems rely on arithmetic circuits, which can be inefficient and error-prone. zkFOL instead arithmetizes first-order logic—a foundational tool in mathematics and computer science—directly into polynomials. This leverages a mathematical duality between logical validity and polynomial evaluation, allowing complex computations to be verified via ZK proofs more naturally and efficiently. •Bitcoin Integration: As a soft fork, zkFOL upgrades Bitcoin’s Script language to support these ZK-verified logical predicates. For example, a Uniswap-style automated market maker (AMM) can enforce the invariant (x \times y = k) as a verifiable logical rule, enabling DeFi without needing sidechains or external layers. •Broader Vision: ModulusZK (founded by the pseudonymous Mr. O’Modulus) positions zkFOL as part of “Layer X,” a universal proof-coordination infrastructure. This enhances existing blockchains like Bitcoin and Ethereum rather than creating competing networks. It critiques the “Circuit-First” paradigm in ZK tech, advocating for logic-based abstractions to reduce complexity and costs. Benefits and Innovations •Privacy and Security: Users can prove computations (e.g., transaction validity) without revealing inputs, addressing Bitcoin’s transparency limitations while maintaining its battle-tested security. •Efficiency: Proof generation is faster and smaller compared to circuit-based ZK, potentially 10x quicker with 90% size reduction in some contexts. •Expressiveness: Brings Ethereum-like functionality to Bitcoin, resolving the long-standing trade-off between Bitcoin’s rigidity and other chains’ vulnerabilities. This concept emerged in late 2025 discussions, building on ModulusZK’s zkEVM (zero-knowledge Ethereum Virtual Machine) work for Ethereum Layer 2 scaling. For more details, check ModulusZK’s resources or the soft fork proposal.

I came here to prove the impossible is possible & to give my community true freedom. And we’re almost done proving whats possible.

Goddammit I’m bullish on $CULT

I reviewed the paper and wrote an EDSL in Lean based on it. My implementation demonstrates how first-order logic compiles directly to polynomial constraints, providing the missing link between high-level cryptocurrency invariants and low-level zkSNARK circuits. By mapping logical formulas to R1CS, developers can specify complex financial systems declaratively while achieving cryptographic verifiability. The core insight: monetary invariants are logical statements. "Total supply remains constant" becomes ∀tx. sum(inputs) = sum(outputs). "No double spending" becomes ∀coin. spent(coin) ⇒ ¬spendable(coin). These specifications compile automatically to polynomial constraints, eliminating manual circuit construction—the primary barrier to zkEVM adoption. The polynomial semantics handles the full complexity of financial logic. Negation through sign gadgets enables expressing invalidity conditions—quantifiers over finite domains model transaction batches. The sparse polynomial representation keeps verification costs manageable even for complex state transitions. Most critically, conjunction's additive compilation means combining multiple invariants doesn't compound proof complexity, essential for composable financial protocols. The R1CS output integrates directly with existing zkSNARK toolchains (Groth16, PLONK, Halo2). A balance check requiring hundreds of hand-written constraints reduces to a single logical formula. The compiler handles witness generation, wire allocation, and constraint optimization automatically. Here's the code: -- ArithFOL.lean — Lean 4 EDSL for Gabbay-style arithmetised first-order logic -- Author: Charles Hoskinson License: MIT -- -- * Full polynomial semantics (truth ≙ 0) complete R1CS compiler. -- * Extra Poly utilities (pow / evaluate / degree / leadingCoeff / isZero / isConst). -- * Pretty R1CS printer and runnable examples at bottom. -- --------------------------------------------------------------------------- import Std.Data.RBMap.Lemmas open Std (RBMap) /-! ### Signature --------------------------------------------------------- -/ structure FuncSymbol where name : String := "" ; arity : Nat := 0 structure PredSymbol where name : String := "" ; arity : Nat := 0 /-! ### Syntax: de-Bruijn terms & formulas -------------------------------- -/ inductive Term : Nat → Type | var {n} : Fin n → Term n | const {n} : Rat → Term n | indet {n} : Term n -- distinguished X | add {n} : Term n → Term n → Term n | mul {n} : Term n → Term n → Term n | neg {n} : Term n → Term n | func {n} : (f : FuncSymbol) → (Fin f.arity → Term n) → Term n inductive Formula : Nat → Type | top {n} : Formula n | bot {n} : Formula n | eq {n} (t u : Term n) : Formula n | pred {n} (P : PredSymbol) (args : Fin P.arity → Term n) : Formula n | and {n} (φ ψ : Formula n) : Formula n | or {n} (φ ψ : Formula n) : Formula n | forall {n} (φ : Formula (n 1)) : Formula n | exists {n} (φ : Formula (n 1)) : Formula n | notG {n} (φ : Formula n) : Formula n -- sign-gadget ¬φ /-! ### Polynomial datatype ----------------------------------------------- -/ structure Poly where coeffs : RBMap Nat Rat compare deriving Repr, DecidableEq namespace Poly def zero : Poly := ⟨RBMap.empty⟩ def const (q : Rat) : Poly := if q = 0 then zero else ⟨RBMap.ofList [(0,q)]⟩ def X : Poly := ⟨RBMap.ofList [(1,1)]⟩ @[inline] def clean (m : RBMap Nat Rat compare) := m.fold (init:=RBMap.empty) (fun acc k v => if v=0 then acc else acc.insert k v) @[inline] def add (p q : Poly) : Poly := ⟨clean <| p.coeffs.fold (init:=q.coeffs) (fun m k v => m.insert k (v m.findD k 0))⟩ @[inline] def neg (p : Poly) : Poly := ⟨p.coeffs.fold (init:=RBMap.empty) (fun m k v => m.insert k (-v))⟩ @[inline] def mul (p q : Poly) : Poly := ⟨clean <| p.coeffs.fold (init:=RBMap.empty) (fun acc kp vp => q.coeffs.fold (init:=acc) (fun acc2 kq vq => let k := kp kq let c := acc2.findD k 0 vp*vq if c = 0 then acc2.erase k else acc2.insert k c))⟩ @[inline] def square (p : Poly) : Poly := p.mul p @[inline] def pow (p : Poly) : Nat → Poly | 0 => const 1 | 1 => p | n 1 => let q := pow p (n/2) let q2 := q.mul q if n % 2 = 0 then q2 else q2.mul p @[inline] def ratPow : Rat → Nat → Rat | _, 0 => 1 | r, 1 => r | r, n 1 => let half := ratPow r (n/2) let sq := half*half if n%2=0 then sq else sq*r @[inline] def evaluate (p : Poly) (x : Rat) : Rat := if x = 0 then p.coeffs.findD 0 0 else if x = 1 then p.coeffs.fold (init:=0) (fun acc _ v => acc v) else p.coeffs.fold (init:=0) (fun acc k v => acc v * ratPow x k) @[inline] def degree (p : Poly) : Option Nat := p.coeffs.fold (init:=none) (fun o k _ => match o with | none => some k | some d => some (max d k)) @[inline] def leadingCoeff (p : Poly) : Option Rat := match p.degree with | none => none | some d => p.coeffs.find? d @[inline] def isZero (p : Poly) : Bool := p.coeffs.isEmpty @[inline] def isConst (p : Poly) : Option Rat := if p.isZero then some 0 else if p.coeffs.size = 1 ∧ p.coeffs.min?.map (·.1) = some 0 then some (p.coeffs.findD 0 0) else none @[inline] def compose (p q : Poly) : Poly := p.coeffs.fold (init:=Poly.zero) (fun acc k c => acc.add (Poly.const c).mul (q.pow k)) end Poly /-! ### Environment -------------------------------------------------------- -/ structure Env (n : Nat) where varVal : Fin n → Rat domain : List Rat namespace Env def extend {n} (e : Env n) (a : Rat) : Env (n 1) := { varVal := fun | ⟨0,_⟩ => a | ⟨i 1,h⟩ => e.varVal ⟨i, Nat.lt_of_succ_lt_succ h⟩, domain := e.domain } end Env /-! ### Interpretation ----------------------------------------------------- -/ mutual def interpTerm {n} (ρ : Env n) : Term n → Poly | .var i => Poly.const (ρ.varVal i) | .const q => Poly.const q | .indet => Poly.X | .add s t => (interpTerm ρ s).add (interpTerm ρ t) | .mul s t => (interpTerm ρ s).mul (interpTerm ρ t) | .neg t => Poly.neg (interpTerm ρ t) | .func _ _ => Poly.zero def liftTerm {k} : Term k → Term (k 1) | .var i => .var ⟨i.val 1, Nat.succ_lt_succ i.isLt⟩ | .const q => .const q | .indet => .indet | .add s t => .add (liftTerm s) (liftTerm t) | .mul s t => .mul (liftTerm s) (liftTerm t) | .neg t => .neg (liftTerm t) | .func f as => .func f (fun i => liftTerm (as i)) def liftFormula {k} : Formula k → Formula (k 1) | .top => .top | .bot => .bot | .eq t u => .eq (liftTerm t) (liftTerm u) | .pred P as => .pred P (fun i => liftTerm (as i)) | .and φ ψ => .and (liftFormula φ) (liftFormula ψ) | .or φ ψ => .or (liftFormula φ) (liftFormula ψ) | .forall φ => .forall (liftFormula φ) | .exists φ => .exists (liftFormula φ) | .notG φ => .notG (liftFormula φ) def interpFormula {n} (ρ : Env n) : Formula n → Poly | .top => Poly.zero | .bot => Poly.const 1 | .eq t u => (interpTerm ρ t).add (Poly.neg (interpTerm ρ u)) |> Poly.square | .pred _ _ => Poly.const 1 | .and φ ψ => let p := interpFormula ρ φ let q := interpFormula ρ ψ p.square.add q.square | .or φ ψ => (interpFormula ρ φ).mul (interpFormula ρ ψ) | .forall φ => ρ.domain.foldl (init:=Poly.zero) fun acc a => acc.add ((interpFormula (ρ.extend a) φ).square) | .exists φ => match ρ.domain with | [] => Poly.const 1 | a :: _ => interpFormula (ρ.extend a) φ -- naive witness | .notG φ => let φ' := liftFormula φ let b : Term (n 1) := .var ⟨0, Nat.zero_lt_succ n⟩ let boolB := Formula.eq (.mul b (.add b (.const (-1)))) (.const 0) let conj0 := Formula.and (Formula.eq b (.const 0)) φ' let conj1 := Formula.and (Formula.eq b (.const 1)) Formula.top let gadget := Formula.and boolB (Formula.or conj0 conj1) let p0 := interpFormula (ρ.extend 0) gadget let p1 := interpFormula (ρ.extend 1) gadget p0.mul p1 end /-! ### R1CS infrastructure ---------------------------------------------- -/ structure Wire where id : Nat deriving Repr, DecidableEq, Ord instance : Ord Wire := ⟨fun a b => compare a.id b.id⟩ namespace Wire def X : Wire := ⟨0⟩ def one : Wire := ⟨1⟩ def zero : Wire := ⟨2⟩ end Wire structure Constraint where A B C : RBMap Wire Rat compare deriving Repr structure Ctx where next : Nat := 3 -- after reserved rows : List Constraint := [] powers : RBMap Nat Wire compare := {} polyWires : RBMap Poly Wire compare := {} namespace Ctx def fresh : StateM Ctx Wire := do let s ← get; set {s with next := s.next 1}; pure ⟨s.next⟩ def push (row : Constraint) : StateM Ctx Unit := modify fun s => {s with rows := row :: s.rows} -- wires for X^k, cached partial def getPower (k : Nat) : StateM Ctx Wire := do let s ← get; match s.powers.find? k with | some w => pure w | none => if k=0 then pure Wire.one else if k=1 then pure Wire.X else let wPrev ← getPower (k-1) let wk ← fresh push {A := RBMap.singleton Wire.X 1, B := RBMap.singleton wPrev 1, C := RBMap.singleton wk 1} modify fun s => {s with powers := s.powers.insert k wk} pure wk -- wires for arbitrary polynomial value partial def getPolyWire (p : Poly) : StateM Ctx Wire := do let s ← get; match s.polyWires.find? p with | some w => pure w | none => match p.isConst with | some 0 => pure Wire.zero | some 1 => pure Wire.one | _ => let w ← fresh compilePolyDef p w modify fun s => {s with polyWires := s.polyWires.insert p w} pure w -- emit rows for Σ c_k X^k = w partial def compilePolyDef (p : Poly) (w : Wire) : StateM Ctx Unit := do let mut lin := RBMap.singleton w (-1) for ⟨k,c⟩ in p.coeffs.toList do let wk ← getPower k lin := lin.insert wk (c lin.findD wk 0) push {A := lin, B := RBMap.singleton Wire.one 1, C := RBMap.empty} end Ctx /-- compile equality p=0 into rows -/ private def compilePolyEq (p : Poly) : StateM Ctx Unit := do if p.isZero then return () let w ← Ctx.getPolyWire p Ctx.push {A := RBMap.singleton w 1, B := RBMap.singleton Wire.one 1, C := RBMap.empty} /-- substitute concrete a into a 1-bound formula (for ∀/∃ instantiation) -/ def substFormula {n} (φ : Formula (n 1)) (a : Rat) : Formula n := Formula.eq (Term.const ((interpFormula ⟨fun _ => a, []⟩ φ).evaluate 0)) (Term.const 0) /-! full compilation ------------------------------------------------------ -/ open Ctx mutual partial def compileFormula (φ : Formula 0) (env : Env 0) : StateM Ctx Unit := match φ with | .top => return () | .bot => compilePolyEq (Poly.const 1) | .eq t u => let diff := (interpTerm env t).add (Poly.neg (interpTerm env u)) compilePolyEq diff | .pred _ _ => compilePolyEq (Poly.const 1) | .and φ ψ => compileFormula φ env >> compileFormula ψ env | .or φ ψ => -- enforce wφ · wψ = 0 let pφ := interpFormula env φ; let pψ := interpFormula env ψ let wφ ← getPolyWire pφ; let wψ ← getPolyWire pψ push {A := RBMap.singleton wφ 1, B := RBMap.singleton wψ 1, C := RBMap.empty} | .forall φ => -- all instantiations must be 0 for a in env.domain do compileFormula (substFormula φ a) env | .exists φ => -- naive witness = first element match env.domain with | [] => compilePolyEq (Poly.const 1) | a :: _ => compileFormula (substFormula φ a) env | .notG φ => compilePolyEq (interpFormula env (.notG φ)) end /-- Public entry: compile closed formula to R1CS rows. -/ def compileFormulaToR1CS (φ : Formula 0) (domain : List Rat := []) : List Constraint := let env : Env 0 := ⟨fun _ => 0, domain⟩ ((compileFormula φ env).run {}).2.rows.reverse /-! ### Pretty printer & validation -------------------------------------- -/ namespace Constraint def termStr (w : Wire) (c : Rat) : String := let wS := if w = Wire.X then "X" else if w = Wire.one then "1" else if w = Wire.zero then "0" else s!"w{w.id}" if c = 1 then wS else if c = -1 then s!"-{wS}" else s!"{c}·{wS}" def sideStr (m : RBMap Wire Rat compare) : String := if m.isEmpty then "0" else String.intercalate " " (m.toList.map (fun (w,c) => termStr w c)) def toString (c : Constraint) : String := s!"({sideStr c.A}) × ({sideStr c.B}) = {sideStr c.C}" end Constraint def validateR1CS (rows : List Constraint) (w : Wire → Rat) : Bool := rows.all fun c => let eval (m : RBMap Wire Rat compare) := m.fold (init:=0) fun acc i coeff => acc coeff * w i eval c.A * eval c.B = eval c.C ------------------- Give my regards to Gabbay> I enjoyed reading the paper and wish you guys well with your project

Thank you Charles. I’ve sent @Cardano_CF a DM btw as yours aren’t open & I’ve passed your message onto Jamie 🤝 many thanks for your time

Today is a good day to talk about $CULT DAO ✍🏻 pass on it

Always watch LunarCrush AltRank™ — it shows where attention and capital are moving together. $CULT’s AltRank™ has strengthened (with a rank of 1 being the strongest rank in the entire crypto market) twice this week, with social activity ramping up alongside rising volume and price. Even with price up 27.88% this week, @wearecultdao is gaining momentum again as AltRank™ continues to strengthen.

$52,000 Buy $49,000 Buy $29,000 Buy All these CULT DAO buys occurred TODAY. So what's up? Thoughts? SEEMS LIKE FOR THE PAST MONTH BUYS LIKE THIS KEEP COMING IN. I think it's TIME. No matter what you believe, the CULT DAO CHART IS ASCENDING. Are you coming with us?

$CULT @ModulusZK

@ModulusZK’s tech is being built by a computer scientist with a doctorate from University of Cambridge. wearecultdao.medium.com/cult… $CULT

We would like to welcome the following to @ModulusZK & of course, also, welcome to @wearecultdao 🤝🏽 🎭 Dr Jamie Gabbay as CTO Dr Tirath Virdee as Advisor for AI & Quantum Computing And Mauro Grandinetti as Advisor for Financial Ecosystem Strategy wearecultdao.medium.com/cult…

It’s time $CULT @wearecultdao

Believe in your $CULT family as I believe in your $CULT family. “The inches we need, are everywhere around us.” - Credit Al Pacino, Any given Sunday. #talkaboutcult

Omg it's happening.... I'm wayyy over in $WLFI discord and this just happened. I've never mentioned $CULT in there. Letsssssssssss goooooooooo cultdao.io #Moduluszk 🔥🔥🔥