| # SnapKitty XML and Metadata Architecture |
|
|
| --- |
|
|
| ## XML Inventory |
|
|
| SnapKitty uses XML in six distinct roles. These are not collapsed. |
|
|
| ### XML-001: ConstraintGraph (DAG Specification) |
|
|
| **Path:** `carry-agent/logic/constraint-graph.xml` |
| **Schema:** Custom β `<ConstraintGraph>` root with TypedSymbols, BooleanConstraints, RefinementPredicates, DAGNodes, TransformationRules, ProofConditions |
| **Purpose:** Machine-readable specification of a constraint DAG |
| **Role:** Intermediate representation β not configuration, not documentation |
|
|
| **Structure:** |
| ```xml |
| <ConstraintGraph> |
| <TypedSymbols> <!-- emoji-typed named symbols --> |
| <BooleanConstraints> <!-- logical constraints including entropy <= 0.20 --> |
| <RefinementPredicates> <!-- per-symbol behavioral predicates --> |
| <DAGNodes> <!-- nodes with emoji labels + directed edges --> |
| <TransformationRules> <!-- input β output transform rules --> |
| <ProofConditions> <!-- formal proof obligations --> |
| </ConstraintGraph> |
| ``` |
|
|
| **Key example:** |
| ```xml |
| <Constraint id="C4" expression="AND(entropy(S1) <= 0.20, entropy(S2) <= 0.20, entropy(S3) <= 0.20)"/> |
| ``` |
|
|
| **Consumed by:** |
| - `sovereign-xml-compiler/constraint_graph_svg.py` β SVG + executable pipeline dict |
| - `xslt/constraint-dsl-to-rust.xsl` β Rust source code |
|
|
| **Metadata type:** EXECUTABLE β the `BooleanConstraints` directly control what the generated Rust `validity_predicate` checks. |
|
|
| --- |
|
|
| ### XML-002: HyperKittyConstraintDSL (Full System Specification) |
|
|
| **Path:** Generated at runtime; parsed by `sovereign-shadow-compiler/hyperkitty_dsl/parser.py` |
| **Schema:** `<HyperKittyConstraintDSL version="...">` with Meta, GlyphTable, Nodes, Edges, Constraints, Invariants, EntropyBound |
| **Purpose:** Complete behavioral specification of a HyperKitty pipeline stage |
| **Role:** Specification + intermediate representation + code-generation input |
|
|
| **Key field:** |
| ```python |
| @dataclass |
| class HKEntropyBound: |
| metric: str # e.g., "shannon_nats" |
| formula: str # e.g., "H(X)" |
| bound: float # parsed from "H <= 0.20" β 0.20 |
| ``` |
|
|
| **Consumed by:** |
| - Python parser β `HKNode`, `HKEdge`, `HKConstraint`, `HKEntropyBound` objects β runtime |
| - XSLT transform β Rust code with `validity_predicate(entry.entropy_nats <= 0.20)` |
|
|
| **Metadata type:** EXECUTABLE β `HKEntropyBound.bound` is the runtime threshold, not documentation. |
|
|
| --- |
|
|
| ### XML-003: XSLT Transforms (Code Generation) |
|
|
| **Paths:** `xslt/*.xsl` |
| **Role:** Meta-programs β transform XML specifications into target code |
|
|
| | Transform | Input | Output | |
| |-----------|-------|--------| |
| | `constraint-dsl-to-rust.xsl` | `HyperKittyConstraintDSL` XML | Rust: Agent struct, UniverseLedger, `validity_predicate` | |
| | `agent-dsl-a.xsl` | `AGENT_MSG` XML | Dispatch XML with proof verification (checks 64-char proof field) | |
| | `agent-dsl-b.xsl` | `AGENT_MSG` XML | Second-pass dispatch transform | |
| | `qlg-to-rust.xsl` | QLG spec XML | Rust: routing certificate generation, witness vector selection | |
| | `sla-to-rust.xsl` | `SymbolicLedgerAlgebra` XML | Rust: Lambda type with balance axiom iota=-delta, omega invariant, `ENTROPY_NATS` constant | |
| | `generate-readme.xsl` | graph/spec XML | Markdown README documentation | |
| | `generate-site.xsl` | browser XML | HTML site pages | |
|
|
| **Generated `validity_predicate` (from constraint-dsl-to-rust.xsl):** |
| ```rust |
| pub fn validity_predicate(entry: &JournalEntry) -> bool { |
| entry.delta_a + entry.delta_e == entry.delta_l + entry.delta_r |
| && entry.entropy_nats <= 0.20 |
| && entry.proof_valid |
| } |
| ``` |
| |
| The `0.20` entropy bound is embedded at code generation time from the XML spec. Changing the XML changes the generated code. |
| |
| --- |
| |
| ### XML-004: Higher-Order Contract (HOC) β Lean 4 Type Signatures in XML |
| |
| **Path:** `seb/verification/lean4/SEB_CHAIN_DETERMINISM_INVARIANT.xml` |
| **Schema:** `<SEB_CHAIN_DETERMINISM_INVARIANT version="..." status="VERIFIED">` with HOC, TypeSignature (CDATA), Parameters, Returns, Preconditions, Postconditions |
| **Purpose:** Machine-readable formal contract that bridges XML spec and Lean 4 proof |
| **Role:** Polyglot specification β drives both documentation and formal verification |
|
|
| **The TypeSignature field contains a dependent type theory expression:** |
| ```xml |
| <TypeSignature> |
| <![CDATA[ |
| ChainDeterminism : |
| (PayloadSeq : List Payload) -> |
| (GenesisTip : Commitment) -> |
| (CommitmentFn : Commitment -> Payload -> Commitment) -> |
| Sigma (CommitmentSeq : List Commitment) . |
| (head CommitmentSeq = GenesisTip) /\ |
| (forall (i : Fin ...) . step i = CommitmentFn step(i-1) payload(i)) /\ |
| (forall OtherSeq . valid OtherSeq -> OtherSeq = CommitmentSeq) |
| ]]> |
| </TypeSignature> |
| ``` |
|
|
| This is the same property proved in Lean 4. The XML records the formal statement; the Lean file contains the proof. Status="VERIFIED" is metadata. |
|
|
| **Metadata type:** EXECUTABLE at the verification level β the TypeSignature can be extracted and fed into a Lean 4 elaborator. |
|
|
| --- |
|
|
| ### XML-005: ConstraintGraph SVG (Visualization + Pipeline) |
|
|
| **Path:** `sovereign-xml-compiler/examples/constraint_graph.xml` |
| **Schema:** `<graph>` with `<node id="..." type="..."/>` and `<edge from="..." to="..."/>` |
| **Purpose:** Visual representation of the constraint DAG |
|
|
| **Compiled by** `constraint_graph_svg.py`: |
| 1. Parses XML β node list + edge list |
| 2. Validates: raises ValueError if cycle detected (DAG enforcement) |
| 3. `_topological_sort()` β Kahn's algorithm |
| 4. `_render_svg()` β SVG with node boxes + edge arrows |
| 5. Returns both SVG string AND `{ "pipeline": [...sorted node ids...] }` dict |
|
|
| The pipeline dict is immediately executable β it IS the execution order. |
|
|
| --- |
|
|
| ### XML-006: System Prompt Template (Executable Metadata) |
|
|
| **Path:** `bob-ide/artifacts/bridges/xml-compiler-skeletons/sovereign_prompt.xml` |
| **Schema:** `<system_prompt>` with `<identity>`, `<logic_gates>`, `<execution_flow>` |
| **Purpose:** Template for generating agent system prompts |
| **Role:** Meta-program template β `{{IDENTITY}}`, `{{GATE_N_NAME}}` are substitution variables |
|
|
| **Metadata type:** EXECUTABLE when instantiated β the `<logic_gates>` become the agent's behavioral constraints; the `<execution_flow>` becomes the agent's procedure. |
|
|
| --- |
|
|
| ## Metadata Architecture: Descriptive vs. Executable |
|
|
| The distinction is non-trivial in SnapKitty: |
|
|
| ### Descriptive Metadata (describes, does not control execution) |
|
|
| | Metadata | Where | Content | |
| |----------|-------|---------| |
| | `version="1.0"` attributes | XML files | Version tracking only | |
| | `status="VERIFIED"` | HOC files | Human-readable status | |
| | `description` text in HOC | XML | Documentation | |
| | HF model card frontmatter (`license:`, `tags:`) | README.md | Search/discovery | |
| | WORM chain `label` field | JSON events | Human-readable event description | |
|
|
| ### Executable Metadata (controls computation) |
|
|
| | Metadata | Where | How it controls execution | |
| |----------|-------|--------------------------| |
| | `HKEntropyBound.bound = 0.20` | XML β Python | Runtime entropy threshold in `ConstraintPass.validate()` | |
| | `BooleanConstraint expression="..."` | XML | Becomes `validity_predicate` in generated Rust | |
| | `ENTROPY_NATS` constant in sla-to-rust.xsl | XML β Rust | Compiled into generated code as literal | |
| | `NodeType` in `<node type="Proof">` | XML | Determines position in pipeline execution order (Kahn's) | |
| | `proof` field length check in agent-dsl-a.xsl | XML β dispatch XML | Blocks dispatch if proof is not 64 chars | |
| | `HKNode.type` | XML β Python | Determines which constraint is applied to this node | |
| | `ICP-DAG node STATE` | MUMPS global | Controls AUTHORIZE/EXECUTE/HALT decision | |
|
|
| **Key principle:** In SnapKitty, metadata is not merely descriptive if it participates in a transformation chain that produces executable code or runtime decisions. The `HKEntropyBound.bound` is the canonical example β it is a number in an XML file that ends up as a literal in generated Rust code and as a runtime threshold in the Python constraint pass. |
|
|
| --- |
|
|
| ## XML β DAG Generation |
|
|
| The `constraint_graph_svg.py` compiler is the clearest example of XML driving DAG generation: |
|
|
| ``` |
| <graph> (XML specification) |
| <node id="input" type="Input"/> |
| <node id="proof" type="Proof"/> |
| <edge from="input" to="proof"/> |
| </graph> |
| β |
| _parse_graph_xml() (Python parser) |
| β |
| _topological_sort() (Kahn's algorithm) |
| β |
| { "pipeline": ["input", "proof"] } (executable pipeline dict) |
| + |
| SVG visualization (rendered graph) |
| ``` |
|
|
| The same XML produces both the visualization AND the executable execution order. This is the core of SnapKitty's XML architecture: one spec, multiple outputs. |
|
|
| --- |
|
|
| ## What Role Does Metadata Play? |
|
|
| **Short answer:** In SnapKitty, metadata drives both the specification and the execution. A single XML file can simultaneously: |
|
|
| 1. Specify the DAG structure (nodes, edges, types) |
| 2. Embed formal invariants (entropy bounds, balance axioms) |
| 3. Generate Rust source code (via XSLT) |
| 4. Drive Python runtime objects (via parser) |
| 5. Produce SVG visualization (via constraint_graph_svg.py) |
| 6. Provide formal type signatures for Lean 4 (via HOC CDATA blocks) |
| 7. Document the system (via generate-readme.xsl) |
|
|
| This is the SnapKitty specification pattern: **XML as polyglot specification**. |
|
|