| # SnapKitty Meta-Programming Systems |
|
|
| **Every code generator, template system, DSL, and schema in the repository.** |
|
|
| --- |
|
|
| ## Overview |
|
|
| SnapKitty uses meta-programming in four distinct layers: |
|
|
| | Layer | Purpose | Deterministic | Produces | |
| |-------|---------|:-------------:|---------| |
| | XSLT 1.0 | XML spec β Rust/C/HTML | Yes | Source code | |
| | Python compilers | XML/scene β SVG + pipeline | Yes | Visualization + execution order | |
| | DSL assembler (.rasm) | Assembly source β bytecode | Yes | Binary bytecode | |
| | Formal spec containers | XML wrapping type signatures | N/A | Archival + codegen routing | |
|
|
| --- |
|
|
| ## 1. XSLT Pipeline (7 + 1 Transforms) |
|
|
| **Location:** `xslt/` and `generated/` |
|
|
| Every XSLT transform is: |
| - XSLT 1.0 (maximum compatibility) |
| - Deterministic (pure functional transforms, no side effects) |
| - Annotated with `AUTO-GENERATED` comment in output |
| - Validated by embedding invariants in the generated code itself |
|
|
| ### constraint-dsl-to-rust.xsl |
|
|
| **Input:** `<HyperKittyConstraintDSL version="...">` XML |
| **Output:** Rust source β `Agent` struct, `UniverseLedger`, `validity_predicate` |
|
|
| **Generated invariants** (cannot be removed without changing the XML spec): |
| ```rust |
| pub fn validity_predicate(entry: &JournalEntry) -> bool { |
| entry.delta_a + entry.delta_e == entry.delta_l + entry.delta_r // balance |
| && entry.entropy_nats <= 0.20 // entropy bound |
| && entry.proof_valid // proof gate |
| } |
| ``` |
|
|
| The `0.20` is read from `<EntropyBound>` in the input XML at transform time. |
|
|
| ### sla-to-rust.xsl |
|
|
| **Input:** `<SymbolicLedgerAlgebra version="...">` XML |
| **Output:** Rust `Lambda` type with algebraic invariants baked in |
|
|
| ```rust |
| // AUTO-GENERATED from SymbolicLedgerAlgebra |
| impl Lambda { |
| pub fn new(s: u64, delta: i64, omega: i64) -> Self { |
| Self { s, delta, iota: -delta, omega } // iota = -delta: balance axiom |
| } |
| pub fn reconciliation(&self) -> i64 { self.delta + self.iota } // must == 0 |
| pub fn is_valid(&self) -> bool { self.reconciliation() == 0 } |
| } |
| pub const ENTROPY_NATS: f64 = 0.20; // from XML Meta/Entropy |
| ``` |
|
|
| The `ENTROPY_NATS` constant is extracted from the XML's `<Meta><Entropy>` field. |
|
|
| ### qlg-to-rust.xsl |
|
|
| **Input:** QLG spec XML |
| **Output:** Rust routing certificate generator |
|
|
| ```rust |
| // AUTO-GENERATED by qlg-to-rust.xsl |
| // Theorem: encode_produces_valid_frame holds by construction |
| pub fn generate_routing_certs(family: QLGFamily) -> Vec<QLGCertificate> { |
| // 6 witness vectors: Β±Pi, Β±Gamma, Β±Delta routes |
| ``` |
|
|
| The comment "Theorem: ... holds by construction" is the meta-program's assertion that the generated code satisfies a formal property. |
|
|
| ### agent-dsl-a.xsl (DSL-A) |
|
|
| **Input:** `<AGENT_MSG>` XML (per `dsl/agent-msg.dtd`) |
| **Output:** `<dispatch>` XML with proof verification inline |
|
|
| ```xml |
| <verified> |
| <xsl:choose> |
| <xsl:when test="string-length(proof) = 64">true</xsl:when> |
| <xsl:otherwise>false</xsl:otherwise> |
| </xsl:choose> |
| </verified> |
| ``` |
|
|
| A 64-character proof field = SHA-256 hex. The XSLT validates this structurally. |
|
|
| ### agent-dsl-b.xsl (DSL-B) |
|
|
| **Input:** `<RUNTIME_REQ>` XML |
| **Output:** Routing directive to `native/hyperkitty-c` or `wasm/pkg/` |
|
|
| This is the **backend selector** β the same XML request routes to different execution targets based on the `target` attribute (`c99 | wasm | auto`). |
|
|
| ### generate-readme.xsl + generate-site.xsl |
|
|
| **Input:** HyperKitty `hk:` namespace XML |
| **Output:** Markdown README (with badge tables, agent fabric table, status table) + HTML site |
|
|
| Documentation is generated from the same source as the code. When the XML spec changes, both documentation and implementation update together. |
|
|
| ### generate-native-config.xsl |
|
|
| **Input:** `QUANTUM-KITTY` XML |
| **Output:** C header `generated_config.h` with `hk_agent_*`, `hk_route_*`, `hk_ledger_config`, `hk_sla_bounds` structs |
|
|
| ```c |
| /* GENERATED FILE β do not edit by hand */ |
| ``` |
|
|
| --- |
|
|
| ## 2. Python XML Compilers |
|
|
| ### xml2svg.py β Scene Compiler |
|
|
| **Input β Output:** `<scene>` XML β SVG string |
| **Pipeline:** XML β `xml.etree.ElementTree` β `SVGNode` IR tree β SVG string |
| **Validated:** Tag whitelist (`{rect, circle, line, path, text, group}`) |
| **Role:** Visualization only β descriptive, not executable |
|
|
| ### constraint_graph_svg.py β DAG Compiler |
|
|
| **Input β Output:** `<graph>` XML β (SVG visualization, executable pipeline dict) |
|
|
| **The pipeline dict IS the execution order:** |
| ```python |
| { "pipeline": ["input", "memory", "retrieval", "transform", "constraint", "proof", "output"] } |
| ``` |
|
|
| This is the point where XML specification becomes an executable artifact. The topological ordering is Kahn's algorithm β cycle detection is structural validation. |
|
|
| --- |
|
|
| ## 3. .rasm Assembler (Full DSL Compiler Pipeline) |
|
|
| **DSL Name:** Resonance Assembly Language |
| **Location:** `snapkitty-resonance-isa/` |
| **Crates:** `abjad` (lexer/parser) β `ir` (lowering) β `assembler` (bytecode) |
|
|
| **8 opcodes (AβH):** |
| | Opcode | Name | Description | |
| |--------|------|-------------| |
| | A | LOAD | Load register from address | |
| | B | STORE | Store register to address | |
| | C | COMPARE | Compare against threshold | |
| | D | BRANCH | Conditional branch (fail-safe) | |
| | E | ENTER | Enter scope (first instruction) | |
| | F | FREEZE | WORM-seal state (immutable) | |
| | G | SIGNAL | Emit coherence signal, increment resonance | |
| | H | HALT | Terminate execution | |
|
|
| **Example program** (`examples/resonance.rasm`): |
| ``` |
| E field_core ; ENTER: open scope |
| A trust_vector ; LOAD: trust field |
| A entropy_register ; LOAD: entropy field |
| C entropy_register 0.21 ; COMPARE: entropy <= 0.21? |
| D fail_safe_branch ; BRANCH: if > threshold, jump |
| G resonance_signal ; SIGNAL: emit coherence pulse |
| F seal_state ; FREEZE: WORM seal |
| H ; HALT |
| ``` |
|
|
| The `0.21` threshold is the same invariant (`ENTROPY_THRESHOLD = 0.21`) enforced by the VM at runtime. |
|
|
| **Compilation pipeline:** |
| ``` |
| .rasm source |
| β |
| abjad/src/lib.rs (lexer: tokenize lines, skip comments) |
| β |
| ir/src/lib.rs (lowering: validate Enter at 0, Halt at end) |
| β |
| assembler/src/lib.rs (encode: ByteWord { opcode: u8, operand: hash }) |
| β |
| binary bytecode (Vec<ByteWord>) |
| β |
| vm/src/lib.rs (execute with entropy gate at 0.21) |
| ``` |
|
|
| **Validated:** Structural invariants (Enter at position 0, Halt at end) enforced in `ir` crate. |
|
|
| --- |
|
|
| ## 4. Formal Spec Containers (XML wrapping proofs) |
|
|
| ### SEB Chain Determinism Invariant |
|
|
| **Path:** `seb/verification/lean4/SEB_CHAIN_DETERMINISM_INVARIANT.xml` |
|
|
| A polyglot XML document that simultaneously contains: |
| 1. A mathematical description of the chain determinism property |
| 2. A complete Idris 2 module in a CDATA block (computable) |
| 3. Proof sketch (tactic steps: `simp`, `induction`, `rw`, `funext`) |
| 4. Codegen routing table: `Ada β seb_kernel.ads`, `Rust β code/T0/primitives`, `Erlang β seb_partition_mgr.erl` |
| 5. Test module in Idris 2 |
|
|
| This XML file is not executed directly. It is a **specification artifact** that routes different downstream consumers (Lean/Idris proof checkers, Rust/Ada/Erlang code generators, test frameworks) to the same formal source of truth. |
|
|
| ### System Schemas |
|
|
| **`schemas/agent.xsd`** β agent state machine (IDLE/ACTIVE/BLOCKED/COMPLETED/ERROR) with legal transitions |
| **`schemas/runtime-event.xsd`** β WORM event format with SHA-256 integrity |
| **`schemas/hyper-kitty-system.xsd`** β full system manifest |
|
|
| These are structural validators β consuming code that violates the schema fails at parse time. |
|
|
| --- |
|
|
| ## 5. Agent Prompt Templates |
|
|
| **Path:** `bob-ide/artifacts/bridges/xml-compiler-skeletons/sovereign_prompt.xml` |
|
|
| ```xml |
| <system_prompt> |
| <identity>{{IDENTITY}}</identity> |
| <logic_gates> |
| <gate><name>{{GATE_1_NAME}}</name> |
| <condition>{{GATE_1_CONDITION}}</condition> |
| <action>{{GATE_1_ACTION}}</action></gate> |
| </logic_gates> |
| <execution_flow> |
| <step><order>1</order><instruction>{{STEP_1}}</instruction></step> |
| </execution_flow> |
| </system_prompt> |
| ``` |
|
|
| Mustache-style template. When instantiated, the `<logic_gates>` become the agent's behavioral constraints. **This is executable metadata** β the template controls agent behavior when filled in. |
|
|
| --- |
|
|
| ## The Core Meta-Programming Pattern |
|
|
| SnapKitty's meta-programming follows a consistent pattern: |
|
|
| ``` |
| XML specification |
| β |
| ββββ XSLT transform βββ Source code (Rust/C/HTML/Markdown) |
| β (entropy bound baked into generated code) |
| β |
| ββββ Python parser βββ Runtime objects + execution order |
| β (entropy threshold as Python float) |
| β |
| ββββ Formal extractor ββ Lean 4 / Idris 2 type signatures |
| (proof obligations derived from spec) |
| ``` |
|
|
| **The invariant `H β€ 0.20` travels through all three paths:** |
| - In XSLT: embedded as literal `0.20` in generated `validity_predicate` |
| - In Python: parsed as `HKEntropyBound.bound = 0.20` controlling `ConstraintPass` |
| - In Lean 4: proved as the main theorem in `EntropyBound.lean` |
| - In .rasm: expressed as `C entropy_register 0.21` assembly instruction |
| - In Rust VM: hardcoded as `ENTROPY_THRESHOLD: f64 = 0.21` |
|
|
| **This is the strongest evidence that metadata is executable in SnapKitty:** the same mathematical constraint flows from the XML specification through code generation, formal proof, and assembly language, with the same numeric value appearing in all layers. |
|
|
| --- |
|
|
| ## What Is Generated Automatically? |
|
|
| | Artifact | Generator | From | |
| |----------|-----------|------| |
| | `UniverseLedger.rs` | `constraint-dsl-to-rust.xsl` | `HyperKittyConstraintDSL.xml` | |
| | `Lambda` Rust type | `sla-to-rust.xsl` | `SymbolicLedgerAlgebra.xml` | |
| | Routing cert Rust code | `qlg-to-rust.xsl` | QLG spec XML | |
| | `generated_config.h` | `generate-native-config.xsl` | `QUANTUM-KITTY.xml` | |
| | SVG visualization | `constraint_graph_svg.py` | `constraint_graph.xml` | |
| | Pipeline execution order | `constraint_graph_svg.py` | `constraint_graph.xml` | |
| | Binary bytecode | `.rasm` assembler | `.rasm` source file | |
| | Agent system prompts | Template instantiation | `sovereign_prompt.xml` | |
| | README + site docs | `generate-readme.xsl`, `generate-site.xsl` | HyperKitty XML | |
|
|
| **What is manually authored:** the XML specifications themselves, the XSLT stylesheets, the formal proofs, the Lean 4 + Agda source. |
|
|