plurigrid Geb (+1)
Categorical computation via S-expressions. Compile categories to ZK circuits.
Trit: +1 (PLUS - generative categorical semantics) Language: Common Lisp (core), Idris2 (verified) Target: Vampir IR → ZK proofs
DeepWiki vs Repo Divergence Analysis
| DeepWiki Claims | Actual Repo State | Divergence |
|---|---|---|
| "Yoneda Categories" | Not prominent in src/ | HIGH |
| "Bicartesian Categories" | ✓ coprod, prod in geb.lisp |
LOW |
| "Polynomial Functors" | ✓ src/poly/poly.lisp full impl |
LOW |
| "Simply Typed Lambda" | ✓ src/lambda/ exists |
LOW |
| "Vampir IR Generation" | ✓ src/vampir/ exists |
LOW |
Key Finding: Core is src/geb/geb.lisp with morphism algebra, not abstract Yoneda.
Core Architecture (from geb.lisp)
;; Substrate objects (types)
so0 ; Initial object (void)
so1 ; Terminal object (unit)
(coprod x y) ; Coproduct (sum type)
(prod x y) ; Product (pair type)
;; Substrate morphisms
(init obj) ; 0 → A
(terminal obj) ; A → 1
(inject-left a b) ; A → A+B
(inject-right a b) ; B → A+B
(project-left a b) ; A×B → A
(project-right a b) ; A×B → B
(comp f g) ; g;f composition
(pair f g) ; ⟨f,g⟩ : A → B×C
(case f g) ; [f,g] : A+B → C
(distribute a b c) ; A×(B+C) → (A×B)+(A×C)
Polynomial Functors (poly.lisp)
;; Polynomial operations on ℕ
poly:ident ; identity polynomial P(x) = x
poly:compose ; P ∘ Q
poly:+ ; P + Q
poly:* ; P × Q
poly:/ ; P ÷ Q (integer division)
poly:- ; P - Q
poly:mod ; P mod Q
poly:if-zero ; conditional on zero
poly:if-lt ; conditional on less-than
;; Evaluation (gapply = generic apply)
(gapply (+ ident ident) 5) ; → 10
(gapply (* ident ident) 5) ; → 25
S-expression Specs (src/specs/)
src/specs/
├── bitc-printer.lisp ; Bit-level circuit printer
├── bitc.lisp ; Bit-level circuit semantics
├── extension-printer.lisp ; Extension types printer
├── extension.lisp ; User extensions
├── geb-printer.lisp ; Geb → S-exp serialization
├── geb.lisp ; Core Geb spec
├── lambda-printer.lisp ; Lambda calc printer
├── lambda.lisp ; STLC embedding
├── poly-printer.lisp ; Polynomial printer
├── poly.lisp ; Polynomial spec
├── seqn-printer.lisp ; Sequence printer
└── seqn.lisp ; Sequence representation
Vampir Compilation Pipeline
Geb Morphism → SeqN (sequences) → BitC (bit circuits) → Vampir IR → ZK Proof
↑ ↑ ↑ ↑
High-level Flattening Bit-blasting PLONK/etc
Obstruction Hot Potato Integration
Geb Morphisms as Obstruction Passing
The Aptos obstruction_hot_potato.move maps directly to Geb categorical semantics:
;; Obstruction as Geb type
(define obstruction-type
(prod
(prod so1 so1) ; (sexp, trit)
(prod so1 so1))) ; (h1_class, color)
;; Pass obstruction = morphism from source to target
(define (pass-obstruction source target obs)
(comp
;; Nullify on source (inject-left to void)
(inject-left (obstruction-type obs) so0)
;; VCG payment extraction
(vcg-extract (h1-class obs))
;; Commit on target (inject-right from void)
(inject-right so0 (obstruction-type obs))))
;; Cross-chain: Aptos → Anoma bridge morphism
(define (aptos-to-anoma-bridge obs)
(pair
(nullify-on-aptos obs) ; Left: burn on Aptos
(mint-on-anoma obs))) ; Right: mint on Anoma
Spectral Gap → Monad Connection
The open-games skill shows: spectral gap + Möbius inversion → Free monad.
Geb provides the categorical semantics for this monad:
;; Free monad on ObstructionF as Geb type
(define obstruction-free
(coprod
so1 ; Pure: no obstruction
(prod obstruction-type ; Roll: obstruction + continuation
obstruction-free)))
;; Cofree comonad (dual) for observations
(define observation-cofree
(prod
so1 ; Extract: current observation
(prod observation-cofree ; Minus neighbor
(prod observation-cofree ; Ergodic neighbor
observation-cofree)))) ; Plus neighbor
VCG Payment as Geb Morphism
;; VCG externality = H¹ × base_cost × multiplier
(define (vcg-payment h1-class)
(geb.poly:*
(geb.poly:* h1-class base-cost)
vcg-multiplier))
;; Roughgarden CS364A L7: truthful declaration is dominant
(define vcg-mechanism
(lambda (declared-h1 actual-h1)
(if (= declared-h1 actual-h1)
(vcg-payment declared-h1) ; Truthful: optimal
(abort)))) ; Lie: revert
Juvix Type Compilation
-- Obstruction type compiles to Geb
type Obstruction := mkObstruction {
sexp : ByteArray;
trit : GF3; -- Compiles to (coprod so1 (coprod so1 so1))
h1Class : Nat;
color : Word64
};
-- Intent for cross-chain pass
passIntent : Obstruction -> ChainId -> ChainId -> Intent
passIntent obs src tgt :=
Intent.compose
(Intent.nullify src obs) -- Geb: inject-left
(Intent.commit tgt obs); -- Geb: inject-right
GF(3) Sexp Neighborhood
| Skill | Trit | Bridge to Geb |
|---|---|---|
| lispsyntax-acset | 0 | S-exp ↔ ACSet bidirectional |
| slime-lisp | -1 | REPL for Common Lisp Geb |
| geiser-chicken | +1 | Scheme sexp coloring |
| discopy | 0 | String diagrams → morphisms |
| cider-clojure | +1 | EDN/sexp nREPL |
| borkdude | +1 | Babashka sexp runtime |
| crdt-vterm | 0 | CRDT sexp terminal sharing |
Exhaustive Sexp Skill Neighborhood
GEB (+1)
│
│ compiles to
▼
┌────────────────────────────────────────────────────────┐
│ SEXP SKILLS │
├────────────────────────────────────────────────────────┤
│ │
│ COMMON LISP SCHEME │
│ ┌─────────────┐ ┌─────────────┐ │
│ │ slime-lisp │ │ geiser- │ │
│ │ (-1) │ │ chicken (+1)│ │
│ └──────┬──────┘ └──────┬──────┘ │
│ │ │ │
│ └─────────┬───────────────┘ │
│ │ │
│ ▼ │
│ ┌─────────────────────────────────────┐ │
│ │ lispsyntax-acset (0) │ │
│ │ S-exp ↔ ACSet bidirectional │ │
│ │ Specter navigation │ │
│ └─────────────────────────────────────┘ │
│ │ │
│ ┌─────────┴─────────┐ │
│ │ │ │
│ ▼ ▼ │
│ ┌─────────────┐ ┌─────────────┐ │
│ │ cider- │ │ borkdude │ │
│ │ clojure (+1)│ │ (+1) │ │
│ └─────────────┘ └─────────────┘ │
│ │
│ CRDT / COLLAB CONFIG LANGS │
│ ┌─────────────┐ ┌─────────────┐ │
│ │ crdt-vterm │ │ cue-lang │ │
│ │ (0) │ │ (+1) │ │
│ └─────────────┘ │ nickel (0) │ │
│ │ hof (-1) │ │
│ └─────────────┘ │
│ │
└────────────────────────────────────────────────────────┘
Usage
# Clone and load
git clone https://github.com/anoma/geb
cd geb
sbcl --load geb.asd
# In REPL
(asdf:load-system :geb)
(in-package :geb.main)
# Example: evaluate morphism
(dom (comp (inject-left so1 so1) (terminal so1)))
; → SO1
# Polynomial evaluation
(geb.poly:gapply (geb.poly:+ geb.poly:ident 1) 5)
; → 6
Files
- Core:
anoma/geb/src/geb/geb.lisp - Poly:
anoma/geb/src/poly/poly.lisp - Vampir:
anoma/geb/src/vampir/ - Idris verified:
anoma/geb/geb-idris/
End-of-Skill Interface
Integration with Anoma Intents
;; Intent as Geb morphism
;; "I give X, I want Y" = morphism from X to Y
(define intent-morphism
(pair
(inject-left resource-x resource-y) ; Nullify X
(inject-right resource-x resource-y))) ; Commit Y
;; Solver composes intents
(define matched-transaction
(comp intent-a intent-b))
;; Compile to ZK proof
(geb-to-vampir matched-transaction)
GF(3) Triads with Anoma
geb (+1) ⊗ solver-fee (-1) ⊗ open-games (0) = 0 ✓
└─ Categorical semantics └─ VCG payment └─ Game coordination
geb (+1) ⊗ intent-sink (-1) ⊗ ihara-zeta (0) = 0 ✓
└─ Intent types └─ Nullification └─ Non-backtracking
Related Skills
| Skill | Trit | Relationship |
|---|---|---|
| intent-sink | -1 | Nullifies Geb-typed intents |
| solver-fee | -1 | Extracts from Geb morphism matches |
| gay-mcp | +1 | Colors Geb types/morphisms |
| discopy | 0 | DisCoPy string diagrams ≅ Geb |
Trit: +1 (PLUS - generative) Key Property: Categorical computation in S-expressions, compiles to ZK Anoma Role: Intent types and morphism semantics
Autopoietic Marginalia
The interaction IS the skill improving itself.
Every use of this skill is an opportunity for worlding:
- MEMORY (-1): Record what was learned
- REMEMBERING (0): Connect patterns to other skills
- WORLDING (+1): Evolve the skill based on use
Add Interaction Exemplars here as the skill is used.