Add docs/XML_METADATA.md
Browse files- docs/XML_METADATA.md +216 -0
docs/XML_METADATA.md
ADDED
|
@@ -0,0 +1,216 @@
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
+
# SnapKitty XML and Metadata Architecture
|
| 2 |
+
|
| 3 |
+
---
|
| 4 |
+
|
| 5 |
+
## XML Inventory
|
| 6 |
+
|
| 7 |
+
SnapKitty uses XML in six distinct roles. These are not collapsed.
|
| 8 |
+
|
| 9 |
+
### XML-001: ConstraintGraph (DAG Specification)
|
| 10 |
+
|
| 11 |
+
**Path:** `carry-agent/logic/constraint-graph.xml`
|
| 12 |
+
**Schema:** Custom β `<ConstraintGraph>` root with TypedSymbols, BooleanConstraints, RefinementPredicates, DAGNodes, TransformationRules, ProofConditions
|
| 13 |
+
**Purpose:** Machine-readable specification of a constraint DAG
|
| 14 |
+
**Role:** Intermediate representation β not configuration, not documentation
|
| 15 |
+
|
| 16 |
+
**Structure:**
|
| 17 |
+
```xml
|
| 18 |
+
<ConstraintGraph>
|
| 19 |
+
<TypedSymbols> <!-- emoji-typed named symbols -->
|
| 20 |
+
<BooleanConstraints> <!-- logical constraints including entropy <= 0.20 -->
|
| 21 |
+
<RefinementPredicates> <!-- per-symbol behavioral predicates -->
|
| 22 |
+
<DAGNodes> <!-- nodes with emoji labels + directed edges -->
|
| 23 |
+
<TransformationRules> <!-- input β output transform rules -->
|
| 24 |
+
<ProofConditions> <!-- formal proof obligations -->
|
| 25 |
+
</ConstraintGraph>
|
| 26 |
+
```
|
| 27 |
+
|
| 28 |
+
**Key example:**
|
| 29 |
+
```xml
|
| 30 |
+
<Constraint id="C4" expression="AND(entropy(S1) <= 0.20, entropy(S2) <= 0.20, entropy(S3) <= 0.20)"/>
|
| 31 |
+
```
|
| 32 |
+
|
| 33 |
+
**Consumed by:**
|
| 34 |
+
- `sovereign-xml-compiler/constraint_graph_svg.py` β SVG + executable pipeline dict
|
| 35 |
+
- `xslt/constraint-dsl-to-rust.xsl` β Rust source code
|
| 36 |
+
|
| 37 |
+
**Metadata type:** EXECUTABLE β the `BooleanConstraints` directly control what the generated Rust `validity_predicate` checks.
|
| 38 |
+
|
| 39 |
+
---
|
| 40 |
+
|
| 41 |
+
### XML-002: HyperKittyConstraintDSL (Full System Specification)
|
| 42 |
+
|
| 43 |
+
**Path:** Generated at runtime; parsed by `sovereign-shadow-compiler/hyperkitty_dsl/parser.py`
|
| 44 |
+
**Schema:** `<HyperKittyConstraintDSL version="...">` with Meta, GlyphTable, Nodes, Edges, Constraints, Invariants, EntropyBound
|
| 45 |
+
**Purpose:** Complete behavioral specification of a HyperKitty pipeline stage
|
| 46 |
+
**Role:** Specification + intermediate representation + code-generation input
|
| 47 |
+
|
| 48 |
+
**Key field:**
|
| 49 |
+
```python
|
| 50 |
+
@dataclass
|
| 51 |
+
class HKEntropyBound:
|
| 52 |
+
metric: str # e.g., "shannon_nats"
|
| 53 |
+
formula: str # e.g., "H(X)"
|
| 54 |
+
bound: float # parsed from "H <= 0.20" β 0.20
|
| 55 |
+
```
|
| 56 |
+
|
| 57 |
+
**Consumed by:**
|
| 58 |
+
- Python parser β `HKNode`, `HKEdge`, `HKConstraint`, `HKEntropyBound` objects β runtime
|
| 59 |
+
- XSLT transform β Rust code with `validity_predicate(entry.entropy_nats <= 0.20)`
|
| 60 |
+
|
| 61 |
+
**Metadata type:** EXECUTABLE β `HKEntropyBound.bound` is the runtime threshold, not documentation.
|
| 62 |
+
|
| 63 |
+
---
|
| 64 |
+
|
| 65 |
+
### XML-003: XSLT Transforms (Code Generation)
|
| 66 |
+
|
| 67 |
+
**Paths:** `xslt/*.xsl`
|
| 68 |
+
**Role:** Meta-programs β transform XML specifications into target code
|
| 69 |
+
|
| 70 |
+
| Transform | Input | Output |
|
| 71 |
+
|-----------|-------|--------|
|
| 72 |
+
| `constraint-dsl-to-rust.xsl` | `HyperKittyConstraintDSL` XML | Rust: Agent struct, UniverseLedger, `validity_predicate` |
|
| 73 |
+
| `agent-dsl-a.xsl` | `AGENT_MSG` XML | Dispatch XML with proof verification (checks 64-char proof field) |
|
| 74 |
+
| `agent-dsl-b.xsl` | `AGENT_MSG` XML | Second-pass dispatch transform |
|
| 75 |
+
| `qlg-to-rust.xsl` | QLG spec XML | Rust: routing certificate generation, witness vector selection |
|
| 76 |
+
| `sla-to-rust.xsl` | `SymbolicLedgerAlgebra` XML | Rust: Lambda type with balance axiom iota=-delta, omega invariant, `ENTROPY_NATS` constant |
|
| 77 |
+
| `generate-readme.xsl` | graph/spec XML | Markdown README documentation |
|
| 78 |
+
| `generate-site.xsl` | browser XML | HTML site pages |
|
| 79 |
+
|
| 80 |
+
**Generated `validity_predicate` (from constraint-dsl-to-rust.xsl):**
|
| 81 |
+
```rust
|
| 82 |
+
pub fn validity_predicate(entry: &JournalEntry) -> bool {
|
| 83 |
+
entry.delta_a + entry.delta_e == entry.delta_l + entry.delta_r
|
| 84 |
+
&& entry.entropy_nats <= 0.20
|
| 85 |
+
&& entry.proof_valid
|
| 86 |
+
}
|
| 87 |
+
```
|
| 88 |
+
|
| 89 |
+
The `0.20` entropy bound is embedded at code generation time from the XML spec. Changing the XML changes the generated code.
|
| 90 |
+
|
| 91 |
+
---
|
| 92 |
+
|
| 93 |
+
### XML-004: Higher-Order Contract (HOC) β Lean 4 Type Signatures in XML
|
| 94 |
+
|
| 95 |
+
**Path:** `seb/verification/lean4/SEB_CHAIN_DETERMINISM_INVARIANT.xml`
|
| 96 |
+
**Schema:** `<SEB_CHAIN_DETERMINISM_INVARIANT version="..." status="VERIFIED">` with HOC, TypeSignature (CDATA), Parameters, Returns, Preconditions, Postconditions
|
| 97 |
+
**Purpose:** Machine-readable formal contract that bridges XML spec and Lean 4 proof
|
| 98 |
+
**Role:** Polyglot specification β drives both documentation and formal verification
|
| 99 |
+
|
| 100 |
+
**The TypeSignature field contains a dependent type theory expression:**
|
| 101 |
+
```xml
|
| 102 |
+
<TypeSignature>
|
| 103 |
+
<![CDATA[
|
| 104 |
+
ChainDeterminism :
|
| 105 |
+
(PayloadSeq : List Payload) ->
|
| 106 |
+
(GenesisTip : Commitment) ->
|
| 107 |
+
(CommitmentFn : Commitment -> Payload -> Commitment) ->
|
| 108 |
+
Sigma (CommitmentSeq : List Commitment) .
|
| 109 |
+
(head CommitmentSeq = GenesisTip) /\
|
| 110 |
+
(forall (i : Fin ...) . step i = CommitmentFn step(i-1) payload(i)) /\
|
| 111 |
+
(forall OtherSeq . valid OtherSeq -> OtherSeq = CommitmentSeq)
|
| 112 |
+
]]>
|
| 113 |
+
</TypeSignature>
|
| 114 |
+
```
|
| 115 |
+
|
| 116 |
+
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.
|
| 117 |
+
|
| 118 |
+
**Metadata type:** EXECUTABLE at the verification level β the TypeSignature can be extracted and fed into a Lean 4 elaborator.
|
| 119 |
+
|
| 120 |
+
---
|
| 121 |
+
|
| 122 |
+
### XML-005: ConstraintGraph SVG (Visualization + Pipeline)
|
| 123 |
+
|
| 124 |
+
**Path:** `sovereign-xml-compiler/examples/constraint_graph.xml`
|
| 125 |
+
**Schema:** `<graph>` with `<node id="..." type="..."/>` and `<edge from="..." to="..."/>`
|
| 126 |
+
**Purpose:** Visual representation of the constraint DAG
|
| 127 |
+
|
| 128 |
+
**Compiled by** `constraint_graph_svg.py`:
|
| 129 |
+
1. Parses XML β node list + edge list
|
| 130 |
+
2. Validates: raises ValueError if cycle detected (DAG enforcement)
|
| 131 |
+
3. `_topological_sort()` β Kahn's algorithm
|
| 132 |
+
4. `_render_svg()` β SVG with node boxes + edge arrows
|
| 133 |
+
5. Returns both SVG string AND `{ "pipeline": [...sorted node ids...] }` dict
|
| 134 |
+
|
| 135 |
+
The pipeline dict is immediately executable β it IS the execution order.
|
| 136 |
+
|
| 137 |
+
---
|
| 138 |
+
|
| 139 |
+
### XML-006: System Prompt Template (Executable Metadata)
|
| 140 |
+
|
| 141 |
+
**Path:** `bob-ide/artifacts/bridges/xml-compiler-skeletons/sovereign_prompt.xml`
|
| 142 |
+
**Schema:** `<system_prompt>` with `<identity>`, `<logic_gates>`, `<execution_flow>`
|
| 143 |
+
**Purpose:** Template for generating agent system prompts
|
| 144 |
+
**Role:** Meta-program template β `{{IDENTITY}}`, `{{GATE_N_NAME}}` are substitution variables
|
| 145 |
+
|
| 146 |
+
**Metadata type:** EXECUTABLE when instantiated β the `<logic_gates>` become the agent's behavioral constraints; the `<execution_flow>` becomes the agent's procedure.
|
| 147 |
+
|
| 148 |
+
---
|
| 149 |
+
|
| 150 |
+
## Metadata Architecture: Descriptive vs. Executable
|
| 151 |
+
|
| 152 |
+
The distinction is non-trivial in SnapKitty:
|
| 153 |
+
|
| 154 |
+
### Descriptive Metadata (describes, does not control execution)
|
| 155 |
+
|
| 156 |
+
| Metadata | Where | Content |
|
| 157 |
+
|----------|-------|---------|
|
| 158 |
+
| `version="1.0"` attributes | XML files | Version tracking only |
|
| 159 |
+
| `status="VERIFIED"` | HOC files | Human-readable status |
|
| 160 |
+
| `description` text in HOC | XML | Documentation |
|
| 161 |
+
| HF model card frontmatter (`license:`, `tags:`) | README.md | Search/discovery |
|
| 162 |
+
| WORM chain `label` field | JSON events | Human-readable event description |
|
| 163 |
+
|
| 164 |
+
### Executable Metadata (controls computation)
|
| 165 |
+
|
| 166 |
+
| Metadata | Where | How it controls execution |
|
| 167 |
+
|----------|-------|--------------------------|
|
| 168 |
+
| `HKEntropyBound.bound = 0.20` | XML β Python | Runtime entropy threshold in `ConstraintPass.validate()` |
|
| 169 |
+
| `BooleanConstraint expression="..."` | XML | Becomes `validity_predicate` in generated Rust |
|
| 170 |
+
| `ENTROPY_NATS` constant in sla-to-rust.xsl | XML β Rust | Compiled into generated code as literal |
|
| 171 |
+
| `NodeType` in `<node type="Proof">` | XML | Determines position in pipeline execution order (Kahn's) |
|
| 172 |
+
| `proof` field length check in agent-dsl-a.xsl | XML β dispatch XML | Blocks dispatch if proof is not 64 chars |
|
| 173 |
+
| `HKNode.type` | XML β Python | Determines which constraint is applied to this node |
|
| 174 |
+
| `ICP-DAG node STATE` | MUMPS global | Controls AUTHORIZE/EXECUTE/HALT decision |
|
| 175 |
+
|
| 176 |
+
**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.
|
| 177 |
+
|
| 178 |
+
---
|
| 179 |
+
|
| 180 |
+
## XML β DAG Generation
|
| 181 |
+
|
| 182 |
+
The `constraint_graph_svg.py` compiler is the clearest example of XML driving DAG generation:
|
| 183 |
+
|
| 184 |
+
```
|
| 185 |
+
<graph> (XML specification)
|
| 186 |
+
<node id="input" type="Input"/>
|
| 187 |
+
<node id="proof" type="Proof"/>
|
| 188 |
+
<edge from="input" to="proof"/>
|
| 189 |
+
</graph>
|
| 190 |
+
β
|
| 191 |
+
_parse_graph_xml() (Python parser)
|
| 192 |
+
β
|
| 193 |
+
_topological_sort() (Kahn's algorithm)
|
| 194 |
+
β
|
| 195 |
+
{ "pipeline": ["input", "proof"] } (executable pipeline dict)
|
| 196 |
+
+
|
| 197 |
+
SVG visualization (rendered graph)
|
| 198 |
+
```
|
| 199 |
+
|
| 200 |
+
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.
|
| 201 |
+
|
| 202 |
+
---
|
| 203 |
+
|
| 204 |
+
## What Role Does Metadata Play?
|
| 205 |
+
|
| 206 |
+
**Short answer:** In SnapKitty, metadata drives both the specification and the execution. A single XML file can simultaneously:
|
| 207 |
+
|
| 208 |
+
1. Specify the DAG structure (nodes, edges, types)
|
| 209 |
+
2. Embed formal invariants (entropy bounds, balance axioms)
|
| 210 |
+
3. Generate Rust source code (via XSLT)
|
| 211 |
+
4. Drive Python runtime objects (via parser)
|
| 212 |
+
5. Produce SVG visualization (via constraint_graph_svg.py)
|
| 213 |
+
6. Provide formal type signatures for Lean 4 (via HOC CDATA blocks)
|
| 214 |
+
7. Document the system (via generate-readme.xsl)
|
| 215 |
+
|
| 216 |
+
This is the SnapKitty specification pattern: **XML as polyglot specification**.
|