|
Download docs/METAPROGRAMMING.md from Snapkitty/snapkitty-open-source: direct link, hf CLI and curl.
- Browser
- Download file 10.5 kB
-
https://huggingface.co/Snapkitty/snapkitty-open-source/resolve/main/docs/METAPROGRAMMING.md
- Command line
-
hf download hf://Snapkitty/snapkitty-open-source/docs/METAPROGRAMMING.md
-
curl -L -o METAPROGRAMMING.md https://huggingface.co/Snapkitty/snapkitty-open-source/resolve/main/docs/METAPROGRAMMING.md
10.5 kB
| # 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. | |