diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/.openspec.yaml b/openspec/changes/extend-orca-lang-neural-and-sparse/.openspec.yaml new file mode 100644 index 0000000..66da1ae --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/.openspec.yaml @@ -0,0 +1,2 @@ +schema: spec-driven +created: 2026-05-17 diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/design.md b/openspec/changes/extend-orca-lang-neural-and-sparse/design.md new file mode 100644 index 0000000..e28de09 --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/design.md @@ -0,0 +1,552 @@ +## Context + +Orca's grammar today is shaped by two artifact kinds: + +- `# machine` — state machines with `## context`, `## events`, + `## state ...`, `## transitions`, `## guards`, `## actions`, + optional `## effects`, optional `## properties`, optional + `## verification rules`. Types are primitive scalars (`string`, + `int`, `decimal`, `bool`) with optional/array modifiers, plus + array (`Field[]`) and optional (`string?`). +- `# decision_table` — typed condition/action grids with + `## conditions`, `## actions`, `## rules`, with numeric range + conditions (`int_range`, `decimal_range`) added via the + decision-tables-spec rollout. + +q-orca is a separate dialect. Its file extension is `.q.orca.md`; +its data model centers on qubits (`bit`, `qubit`), unitary +operators, and measurement outcomes. It has its own AST, parser, +verifier pipeline, and compile backends. The decision to keep +q-orca separate is sound: a qubit cannot type-unify with a +classical scalar, the operations are not composable with classical +transitions, and the verifier needs entanglement / unitarity / +superposition-leak checks that have no analog in the classical +world. + +The sm-sae benchmark wants Orca-shaped artifacts for SAE +compression and extraction techniques beyond the +quantum-encoding-only path that polygram currently emits. +Specifically: + +1. Neural artifacts — sae-forge's `NativeModel`, + concept-bottleneck networks, distilled-transformer carriers. + These are typed DAGs of layer ops with weights in sidecar + `*.safetensors` files. +2. Sparse artifacts — hierarchical SAEs, group-sparse codes. + These are cluster manifests plus sparse weight references. + +Both gaps share three features: +- **Classical data model.** Tensors are not qubits; layer ops + are not unitaries. A tensor type-unifies cleanly with the + existing primitive scalars (it just has rank and shape). +- **Sidecar binary references.** Weights live in `*.safetensors`, + not in the markdown. Both gaps need the same `weight_ref` + primitive. +- **Static invariants checkable without execution.** Shape + consistency, parameter counts, cluster completeness, sparsity + bounds — all are structural checks the verifier can run + without loading the binaries. + +The natural design instinct ("spin up `n-orca` and `s-orca` as +sister dialects to q-orca") is wrong on inspection. Dialect status +costs a full duplicate stack: parser, AST, verifier, compilers, +docs, examples, MCP tools. The cost is only worth paying when the +data model truly diverges. Here it does not — the divergence is +in *what the artifact represents*, not in the underlying types. +What's actually needed is new types and new sections inside the +existing grammar. + +## Goals / Non-Goals + +**Goals:** + +- One extension to `orca-lang`'s grammar and type system that + covers neural and sparse artifacts. +- Existing `*.orca.md` and `*.q.orca.md` artifacts SHALL parse + identically — zero regression. +- The three worked examples SHALL parse, verify, and round-trip + through the AST without loss. +- Each new invariant kind has a specified failure message and + error code, listed in `docs/error-catalog.md`. +- Verifier behavior is well-defined when binaries are absent + (warning, not error), so artifacts travel without their weights. +- Capability negotiation path so consumers that don't understand + the new sections continue to work. +- No changes to existing `# machine` or `# decision_table` + semantics. +- q-orca remains a separate dialect; this change does not modify + q-orca's grammar. + +**Non-Goals:** + +- No implementation. Spec-only deliverable. +- No inlining of tensor values in markdown. References are the + only supported mechanism; the parser SHALL reject inline tensor + literals with `INLINE_TENSOR_FORBIDDEN`. +- No compile back-ends or hardware targeting. Lives in + `add-neural-compile-targets`. +- No schema-versioning mechanism. Lives in + `add-orca-schema-version`; this change relies on its capability + advertisement once it lands. +- No runtime faithfulness check. The `## faithfulness` section is + *declarative*; running the test ships in + `add-runtime-faithfulness-harness`. +- No q-orca convergence. The neural/sparse extensions live + entirely in the classical dialect. +- No algebraic / probabilistic / circuit extensions. Each is its + own future change. + +## Decisions + +### D1. Extension, not new dialect + +**Decision:** Add types and sections to `orca-lang`. Do not +spawn `n-orca` or `s-orca`. + +**Rationale:** + +q-orca's separation is justified by data-model divergence: +qubits, unitaries, and measurement outcomes have no classical +analog. Neural and sparse artifacts share the classical data +model — tensors are just typed multi-dimensional arrays; layer +ops are pure functions; cluster manifests are partitions over +feature IDs. Spinning two new dialects would duplicate the +parser, AST, verifier pipeline, and tooling, and would make +hybrid artifacts (a transformer with a sparse output head) +require two parallel grammars in one workflow. + +Cross-references: + +- q-orca's dialect rationale lives in + `/Users/allans/code/q-orca-lang/openspec/specs/language/spec.md` + (the broader q-orca language spec) and is summarized in the + q-orca README under the heading "Why a separate dialect." +- Q-orca composition syntax (e.g. + `add-parameterized-invoke`) is built specifically because + q-orca's data model could not be merged into classical orca. + The same argument does not hold for tensors: a `tensor` field in a `## context` table behaves grammatically + identically to any other typed context field. + +**Alternatives considered:** + +- *Spin up `n-orca`.* Rejected — see above; duplicates the + pipeline for no data-model gain. A hybrid transformer + + sparse-head artifact would also need a third dialect or live + in two files glued by external tooling. +- *Spin up `s-orca`.* Same rejection. +- *Embed neural/sparse as a child-machine subtype invoked from + classical orca.* Rejected — the artifact is not a state + machine; forcing it into the machine grammar adds rote + states (`loaded → forward → done`) that obscure what the + artifact actually declares. + +### D2. Three new type-system primitives + +**Decision:** Add `tensor`, +`weight_ref`, and +`sparse_matrix` to the type grammar. +These are legal wherever a type appears (context table, weights +table, decision-table action types, future return types). + +**Grammar:** + +``` +tensor + dtype ::= f16 | bf16 | f32 | f64 | i8 | i16 | i32 | i64 | u8 | bool + shape ::= "[" dim ("," dim)* "]" + dim ::= integer | identifier // identifier = named symbolic dim + +weight_ref + path ::= string-literal // relative to artifact directory + sha256 ::= hex64 // 64-character hex digest + key ::= string-literal // tensor name inside the binary + +sparse_matrix + dtype ::= as above + shape ::= as above + format ::= COO | CSR +``` + +Named symbolic dimensions (e.g. +`tensor`) unify across operations +within an artifact — a transition consuming +`tensor` and producing +`tensor` declares that the operation +preserves these dimensions. Concrete integers and named dims may +mix: `tensor`. + +**Rationale:** + +- Tensor types must carry shape because shape consistency is the + primary static check; without it the verifier can only check + dtype, which is too weak to be useful. +- Symbolic dimensions are necessary to express + shape-preservation invariants that hold across arbitrary + batch / sequence sizes — concrete-only shapes would force the + artifact to commit to one set of dimensions. +- `weight_ref` is content-addressed because the same artifact + may be loaded from different storage locations (local, S3, + HF) and the hash is the integrity anchor, not the path. +- `sparse_matrix` carries format because the verifier needs to + evaluate `sparsity_bound` against the actual nnz, and the + binary loader needs format to decode the safetensor; bundling + these in the type avoids a parallel format-declaration + section. + +**Alternatives considered:** + +- *Single `tensor` type with optional + storage location.* Rejected — overloads tensor with two roles + (computed activation vs. stored parameter); the + trainable-flag, hash, and lifecycle of a stored weight are + distinct enough to deserve their own type. +- *Implicit shape (just `tensor`).* Rejected — kills the + `shape_consistency` invariant. +- *Format as a context field, not part of the type.* Rejected — + the format determines the binary layout; coupling it to the + type is the safest place. + +### D3. Four new sections + +**Decision:** Add `## weights`, `## cluster_manifest`, +`## faithfulness`, `## provenance` as peers to the existing +sections. + +**Table forms:** + +```markdown +## weights + +| name | type | weight_ref | trainable? | +|------|------|------------|------------| + +## cluster_manifest + +| cluster | features | size | +|---------|----------|------| + +## faithfulness + +| metric | threshold | distribution | reference | +|--------|-----------|--------------|-----------| + +## provenance + +| field | value | +|-------|-------| +| extraction_technique | sae_forge_v1 | +| version | 0.4.2 | +| config_hash | sha256:... | +| source_sae_hash | sha256:... | +| benchmark_score | 0.972 | +``` + +**Rationale:** + +- `## weights` is a flat table rather than embedded in + `## context` because weight rows have multiple metadata fields + (type, ref, trainability) that don't fit a single "Type" + column. +- `## cluster_manifest` is a table rather than nested YAML + because the existing parser is table-based and round-trips + cleanly; a YAML blob would force a second parsing layer. +- `## faithfulness` is declarative rather than executable + because spec-only — the actual numerical check runs at + build/run time. The verifier produces test scaffolding from + the declaration. +- `## provenance` is a key/value table because the field set + varies by extraction technique (some have benchmark scores, + some don't); a fixed table would be over-prescriptive. + Front-matter was considered but rejected — Orca files do not + use YAML front-matter today, and adding it here would create + a parsing surface that competes with the existing markdown + conventions. + +**Alternatives considered:** + +- *Folding weights into `## context`.* Rejected — context + fields are part of the machine's mutable state; weights are + fixed references. Mixing them blurs which fields are + trainable and which are activations. +- *Putting provenance in YAML front-matter.* Rejected — see + above. The repo's parser is markdown-section-based; + introducing YAML front-matter creates a parallel surface. + +### D4. Six new invariant kinds + +**Decision:** Extend `## verification rules` with the kinds in +the table below. The existing parser already accepts a bullet +list under `## verification rules`; the keys are added to the +invariant-kind enum and parsed by name with optional parameters. + +```markdown +## verification rules + +- shape_consistency +- sparsity_bound: 8 +- cluster_completeness +- decoder_norm_preservation: tolerance=0.01, reference=W_dec_baseline +- parameter_count: 10_240 +- faithfulness: kl_divergence <= 0.05 under distribution=imagenet_val against reference=teacher_model +``` + +| Kind | Parameters | Verifier action | +|------|------------|-----------------| +| `shape_consistency` | none | For every transition action whose signature involves tensor types, the declared output shape SHALL match each consumer's expected input shape. Symbolic dims unify by name; concrete dims unify by value. | +| `sparsity_bound: ` | int | For every `sparse_matrix` weight, the declared or referenced nnz-per-row SHALL be ≤ ``. | +| `cluster_completeness` | none | Every feature ID in the relevant tensor SHALL appear in exactly one cluster in `## cluster_manifest`. | +| `decoder_norm_preservation: tolerance=, reference=` | decimal, name | Declares that decoder column norms equal ``'s norms within ``. Verifier emits test scaffolding; numerical check runs at compile/run time. | +| `parameter_count: ` | int | Sum of element counts across all `## weights` rows (using each row's declared shape) SHALL equal ``. | +| `faithfulness: , , , ` | identifier, decimal, identifier, identifier | Same kind as the `## faithfulness` section row; allowed inline so machines that don't need a full section can declare a single faithfulness rule. The verifier emits test scaffolding only. | + +**Rationale:** + +- `shape_consistency` is the headline check that justifies the + whole shape-bearing tensor type. +- `sparsity_bound` is a pure structural check the verifier can + run from declarations alone — no binary needed. +- `cluster_completeness` is what polygram currently + hand-validates; promoting it to a first-class invariant means + the benchmark loses one bespoke validator. +- `decoder_norm_preservation` is declarative because the actual + norm check requires loading the binary. The verifier asserts + the *intent* and produces the scaffolding. +- `parameter_count` catches a class of bugs where the weights + table drifts from the artifact's headline parameter count. +- `faithfulness` is the formal declaration of the contract that + motivated the entire neural artifact pipeline. + +**Alternatives considered:** + +- *Embed shape checks implicitly in transition typing without + an opt-in keyword.* Rejected — would break existing machines + that have informal/loose context typing. Opt-in keeps the + change backwards-compatible. +- *Make `faithfulness` strictly a section, not also an inline + kind.* Rejected — single-rule artifacts shouldn't be forced + to spin up a whole section. + +### D5. Neural module = `# machine` with tensor-typed states + +**Decision:** A neural module is a `# machine` whose states are +named activation tensors (typed via `tensor<...>` in `## context`) +and whose transitions are layer operations referencing weights +via `weight_ref` action signatures. No new top-level construct. + +**Rationale:** + +The existing transition table is a typed DAG of operations — +that's exactly what a layer-by-layer neural module is. Forcing a +parallel construct would mean two ways to express the same +shape. Letting the existing grammar do the work means tensor +shapes flow through the verifier's existing transition-typing +machinery; we only add the type primitives. + +A neural module typically has: +- One `[initial]` state representing the input activation. +- One `[final]` state representing the output activation. +- No `## events` (or a single `forward` event), because the + forward pass is linear, not event-driven. +- No `## guards`, because there's no branching in a feedforward + module. (Branching neural modules — mixtures-of-experts, etc. + — *use* guards; this is an extra-credit shape, not a + required pattern.) + +This means a neural artifact does sometimes have a degenerate +state machine (linear chain, no events). That's acceptable. The +alternative — introducing a separate top-level construct for +neural DAGs — would split the language and force tooling to +handle two parallel artifact kinds. + +### D6. Standalone artifacts (sections-only documents) + +**Decision:** An `.orca.md` document MAY contain only the new +sections (`## weights`, `## cluster_manifest`, `## faithfulness`, +`## provenance`) with no `# machine` heading. The parser SHALL +treat this as a valid document whose AST is a +`SectionsOnlyArtifact` node. + +**Rationale:** + +A group-sparse SAE doesn't need transitions — it's a static +dictionary of features. Forcing a stub `# machine` heading +would be busywork that adds confusion ("what does this machine +*do*?"). The sections-only artifact is a clear, minimal shape +for dictionary-style artifacts. + +Round-trip rule: a sections-only artifact must contain at least +one of `## weights`, `## cluster_manifest`, or `## provenance`. +A document with only `## faithfulness` (and nothing else) is a +parse error — `EMPTY_ARTIFACT` — because faithfulness is a +contract *about* an artifact, not the artifact itself. + +### D7. Verifier behavior when binaries are absent + +**Decision:** If a `weight_ref`'s target binary is not present +in the artifact directory, the verifier emits +`WEIGHT_BINARY_MISSING` at **warning** severity, not error. +Hashes are checked only when the binary is present; mismatches +are `WEIGHT_HASH_MISMATCH` at error severity. Missing keys +inside a present binary are `WEIGHT_KEY_MISSING` at error +severity. + +**Rationale:** + +Artifacts are routinely passed around without their weight +binaries — for review, for static analysis, for diagrams. A +hard error in that case would make the verifier unusable for the +common review case. The contract is: if the binary is *there*, +its integrity is checked rigorously; if it's not, the absence is +reported but the artifact remains valid for static analysis. + +### D8. Capability negotiation (soft dependency on schema version) + +**Decision:** Consumers that load `.orca.md` and ignore unknown +sections continue to work. Consumers that want to use the new +sections opt in by declaring capability `neural-and-sparse-v1` at +load time. Until `add-orca-schema-version` lands, the convention +is documented but not enforced — consumers MAY assume default +support if they can parse the new sections, and SHOULD detect +unknown sections gracefully. + +**Rationale:** + +A versioning mechanism is a cross-cutting concern that deserves +its own change. The right hook here is to document the +capability name now so that +`add-orca-schema-version`'s capability advertisement has a +target string to use. + +## Risks / Trade-offs + +- **[Risk]** Adding tensor types to the type grammar may + destabilize existing type-grammar users (decision tables, + guards). → **Mitigation:** the new types are recognized only + by token shape (`tensor<...>`, `weight_ref<...>`, + `sparse_matrix<...>`); they don't overlap with existing + primitive scalars or `Field[]` syntax. Existing machines have + no `<>`-bracketed types and will parse identically. + +- **[Risk]** `## weights` with hundreds of rows could blow up + parse time and AST size. → **Mitigation:** weights are + declared per *named* tensor, not per element. A 10K-param + transformer typically has fewer than 20 weight rows; a large + model has at most a few hundred. The parser is linear in row + count; this is fine. If a future artifact has tens of + thousands of weight rows, the right answer is a glob + reference (out of scope), not optimizing the parser. + +- **[Risk]** Symbolic-dim unification across transitions could + surprise users when two ops use the same name for different + meanings. → **Mitigation:** symbolic dims are scoped to a + single machine; the verifier emits `SHAPE_NAME_REBINDING` if a + name's bound value diverges between two transitions. (This is + a sub-rule of `SHAPE_MISMATCH`.) Authors who want truly + independent dims use distinct names. + +- **[Risk]** `weight_ref` hashes are content-addressing the + binary as a whole, not per-tensor. If two artifacts share a + binary, both reference the same hash; if one's binary is + modified, both artifacts see `WEIGHT_HASH_MISMATCH`. → + **Mitigation:** by design, content-addressing means tampering + surfaces immediately on both consumers. The alternative + (per-tensor hashes) would require parsing safetensors to + compute a hash per key, which costs us static-only + checkability. + +- **[Risk]** `## provenance` table fields are open-ended. Two + extraction techniques could pick different field names for + the same concept. → **Mitigation:** the spec defines a small + required set (`extraction_technique`, `version`, + `config_hash`, `source_sae_hash` when applicable) and lets + techniques add their own fields below that. A registry of + field names can land later if convergence becomes important. + +- **[Trade-off]** Declarative `faithfulness` means the verifier + can't actually check that the artifact meets its declared + threshold — only that the declaration is well-formed. We + accept this; the spec is the contract, and the runtime + follow-up (`add-runtime-faithfulness-harness`) is what + enforces it numerically. A test-scaffold output keeps the + declaration from being purely decorative. + +- **[Trade-off]** Allowing sections-only artifacts (no + `# machine` heading) means consumers that hard-code "every + `.orca.md` has at least one machine" will break. → We accept + this; the same consumers already handle multi-machine files + via `---` separators, and adding a sections-only document + shape is a one-line check (`file.machines.length === 0 && + file.sections.length > 0`). The error message is clear. + +- **[Trade-off]** The change is "one coherent grammar + extension" rather than two smaller ones. A reviewer reading + only the neural example might find the sparse types unfamiliar + (and vice versa). → We accept this. The cost of splitting is + higher: shared types would be duplicated, the hybrid + transformer-with-sparse-head example would need to live in + two changes, and the dependency ordering would force + sequential rather than parallel review. + +## Migration Plan + +No migration. Existing `*.orca.md` and `*.q.orca.md` artifacts +SHALL parse identically — they declare none of the new types and +none of the new sections. + +**Regression test (required, lives in +`packages/orca-lang/tests/test-regression-existing-corpus.ts`):** + +Iterate over every `.orca.md` and `.q.orca.md` in +`packages/*/examples/` and `packages/*/orca/`. Parse with the +extended parser; the resulting AST SHALL be byte-identical to +the pre-extension AST under round-trip through +`ast-to-markdown`. If any file's AST changes, the test fails +and the extension has introduced an unintended grammar shift. + +**Rollback:** revert the change's commits. Artifacts that use +the new types or sections will fail to parse — the expected +rollback signal. + +## Open Questions + +1. **Is `## provenance` already partially covered by some other + convention?** Quick repo scan finds no front-matter handling + in the markdown parser and no provenance section in the + grammar spec. So provenance is genuinely new. **Confirmed: + no conflict.** If reviewers find a hidden convention I + missed, flag in PR review. + +2. **Should `weight_ref` allow URI schemes (`s3://...`, + `https://...`) or only relative paths?** Leaning relative + paths only — the verifier checks for binary presence in the + artifact directory; URIs would require a fetch step that + pulls runtime concerns into a static-analysis layer. + Resolver plug-ins can land in + `add-neural-compile-targets`. Defer. + +3. **Does the regression test need to cover artifacts produced + by the demos at runtime, or only checked-in examples?** + Leaning checked-in only. Runtime-produced artifacts aren't + stable enough to anchor a regression test. Defer. + +4. **How do symbolic dims interact with decision tables that + produce tensor-typed outputs?** Not in scope for this + change — DT action types are scalars today. If a future + change introduces tensor-typed DT outputs, symbolic-dim + unification rules carry over unchanged. + +5. **Should `sparse_matrix` support BSR (block sparse row) in + addition to COO/CSR?** Defer. Two formats cover sm-sae's + current needs; BSR can be added as a non-breaking enum + extension when an artifact demands it. + +6. **Naming: should the change be `extend-orca-lang-neural` + plus a follow-up `extend-orca-lang-sparse`?** Considered and + rejected at proposal time — see "Why" in `proposal.md`. The + type-system additions are shared, and the hybrid example + demonstrates why they belong in one coherent change. + +7. **Capability advertisement string.** Tentative name + `neural-and-sparse-v1`. Coordinate with the schema-version + change before final commitment. diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/examples/hybrid-transformer-sparse-head.orca.md b/openspec/changes/extend-orca-lang-neural-and-sparse/examples/hybrid-transformer-sparse-head.orca.md new file mode 100644 index 0000000..3cdddc2 --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/examples/hybrid-transformer-sparse-head.orca.md @@ -0,0 +1,112 @@ +# machine HybridTransformerSparseHead + +> Small transformer body + sparse output head in one artifact. +> The transformer body uses dense tensors and transitions; the +> output head uses a sparse matrix and a cluster manifest. This +> example demonstrates that `## transitions` and +> `## cluster_manifest` mix cleanly in a single file, and that +> one machine's `## verification rules` can combine dense and +> sparse invariants. + +## context + +| Field | Type | Default | +|------------|---------------------------------------|---------| +| input_ids | tensor | | +| embedded | tensor | | +| attended | tensor | | +| pooled | tensor | | +| features | tensor | | + +## events + +- forward + +## state input [initial] +> Token IDs in. + +## state embedded_state +> Embeddings applied. + +## state attended_state +> Self-attention block applied. + +## state pooled_state +> Mean-pooled across sequence dim. + +## state features_state [final] +> Sparse output head produces per-feature activations. + +## transitions + +| Source | Event | Guard | Target | Action | +|------------------|---------|-------|-------------------|--------------| +| input | forward | | embedded_state | embed | +| embedded_state | forward | | attended_state | attention | +| attended_state | forward | | pooled_state | mean_pool | +| pooled_state | forward | | features_state | sparse_head | + +## actions + +| Name | Signature | +|-------------|----------------------------| +| embed | `(ctx, event) -> Context` | +| attention | `(ctx, event) -> Context` | +| mean_pool | `(ctx, event) -> Context` | +| sparse_head | `(ctx, event) -> Context` | + +## weights + +| name | type | weight_ref | trainable? | +|-------------|-------------------------------------------------|-------------------------------------------------------------------------------------------------------|------------| +| W_embed | tensor | weight_ref<"hybrid.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "embed.weight"> | true | +| W_attn_qkv | tensor | weight_ref<"hybrid.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "attn.qkv"> | true | +| W_attn_o | tensor | weight_ref<"hybrid.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "attn.o"> | true | +| W_head | sparse_matrix | weight_ref<"hybrid.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "head.weight"> | true | + +## cluster_manifest + +| cluster | features | size | +|--------------|-----------------------|------| +| concrete | 0, 1, 2, 3, 4, 5 | 6 | +| abstract | 6, 7, 8, 9, 10, 11 | 6 | +| relational | 12, 13, 14, 15 | 4 | + +## provenance + +| field | value | +|----------------------|----------------------------------------------------------------------| +| extraction_technique | sae_forge_v1.distill+polygram_v2.group_sparse | +| version | 0.5.0 | +| config_hash | sha256:5555555555555555555555555555555555555555555555555555555555555555 | +| source_sae_hash | sha256:6666666666666666666666666666666666666666666666666666666666666666 | + +## faithfulness + +| metric | threshold | distribution | reference | +|---------------|-----------|---------------|--------------------| +| kl_divergence | 0.05 | imagenet_val | teacher_model | +| mse | 0.001 | imagenet_val | sae_dense_baseline | + +## verification rules + +- shape_consistency +- parameter_count: 327424 +- sparsity_bound: 4 +- cluster_completeness +- faithfulness: kl_divergence <= 0.05 under distribution=imagenet_val against reference=teacher_model + +> Notes: +> +> Symbolic dims `batch`, `seq`, `hidden`, `vocab`, `n_features` +> unify across the machine. `n_features` is bound to 16 by the +> cluster_manifest (6 + 6 + 4 = 16). `shape_consistency` walks +> the transition graph and checks that each layer's output type +> matches the next state's expected activation. `sparsity_bound` +> applies only to `W_head` (the only sparse_matrix in the +> artifact). `cluster_completeness` applies to the sparse head's +> output features. +> +> This artifact triggers `PROVENANCE_REQUIRED` if `## provenance` +> is omitted, because it has both `## weights` + `## faithfulness` +> AND `## cluster_manifest`. diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/examples/sparse-sae-16f.orca.md b/openspec/changes/extend-orca-lang-neural-and-sparse/examples/sparse-sae-16f.orca.md new file mode 100644 index 0000000..f61d52f --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/examples/sparse-sae-16f.orca.md @@ -0,0 +1,54 @@ +> Sections-only artifact: a 16-feature group-sparse SAE. +> No `# machine` heading — this artifact is a static dictionary, +> not a state machine. Demonstrates `## cluster_manifest`, +> sparse weight refs, and the `cluster_completeness` / +> `sparsity_bound` / `decoder_norm_preservation` invariants. + +## weights + +| name | type | weight_ref | trainable? | +|-------------|-----------------------------------------------|------------------------------------------------------------------------------------------------------|------------| +| W_enc | tensor | weight_ref<"sae-16f.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "encoder.weight"> | true | +| W_dec | sparse_matrix | weight_ref<"sae-16f.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "decoder.weight"> | true | +| b_enc | tensor | weight_ref<"sae-16f.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "encoder.bias"> | true | +| W_dec_baseline | sparse_matrix | weight_ref<"sae-16f-baseline.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "decoder.weight"> | false | + +## cluster_manifest + +| cluster | features | size | +|-----------|---------------|------| +| color | 0, 1, 2, 3 | 4 | +| shape | 4, 5, 6, 7 | 4 | +| texture | 8, 9, 10, 11 | 4 | +| motion | 12, 13, 14, 15 | 4 | + +## provenance + +| field | value | +|----------------------|----------------------------------------------------------------------| +| extraction_technique | polygram_v2.group_sparse | +| version | 1.2.0 | +| config_hash | sha256:3333333333333333333333333333333333333333333333333333333333333333 | +| source_sae_hash | sha256:4444444444444444444444444444444444444444444444444444444444444444 | + +## verification rules + +- cluster_completeness +- sparsity_bound: 4 +- decoder_norm_preservation: tolerance=0.01, reference=W_dec_baseline + +> Notes: +> +> The decoder is declared as `sparse_matrix` +> with `sparsity_bound: 4` — at most 4 nonzeros per feature row. +> `cluster_completeness` checks the partition: 16 features in +> 4 disjoint clusters of 4. The verifier emits +> CLUSTER_FEATURE_DUPLICATE if any feature appears twice, and +> CLUSTER_COVERAGE_GAP if any feature is unassigned. +> +> `decoder_norm_preservation` declares the scale-aware merge +> contract: the live decoder's column norms must match +> `W_dec_baseline`'s norms within 0.01. Because the verifier +> cannot compute norms without binaries present, it emits +> FAITHFULNESS_TEST_SCAFFOLD_REQUIRED at info severity — the +> runtime harness owes the actual check. diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/examples/tiny-transformer.orca.md b/openspec/changes/extend-orca-lang-neural-and-sparse/examples/tiny-transformer.orca.md new file mode 100644 index 0000000..69c28e7 --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/examples/tiny-transformer.orca.md @@ -0,0 +1,103 @@ +# machine TinyTransformer + +> A toy ~10K-parameter GPT-2-class transformer (1 layer, 2 attention +> heads, hidden=64, seq=8, vocab=64). States are activation +> tensors; transitions are layer operations. Weights are referenced +> from a sibling `tiny-transformer.safetensors`. Demonstrates +> tensor types, weight refs, parameter_count, and faithfulness. + +## context + +| Field | Type | Default | +|------------|---------------------------------------|---------| +| input_ids | tensor | | +| embedded | tensor | | +| attended | tensor | | +| mlp_out | tensor | | +| logits | tensor | | + +## events + +- forward + +## state input [initial] +> Token IDs available; no computation has run yet. + +## state embedded_state +> Token embeddings + positional embeddings applied. + +## state attended_state +> Self-attention output added back via residual. + +## state mlp_state +> Feed-forward MLP applied + residual + layer norm. + +## state logits_state [final] +> Output projection to vocab logits. + +## transitions + +| Source | Event | Guard | Target | Action | +|------------------|---------|-------|-------------------|------------| +| input | forward | | embedded_state | embed | +| embedded_state | forward | | attended_state | attention | +| attended_state | forward | | mlp_state | mlp_block | +| mlp_state | forward | | logits_state | unembed | + +## actions + +| Name | Signature | +|-----------|--------------------------------------------------------------------------------------------------------| +| embed | `(ctx, event) -> Context` | +| attention | `(ctx, event) -> Context` | +| mlp_block | `(ctx, event) -> Context` | +| unembed | `(ctx, event) -> Context` | + +## weights + +| name | type | weight_ref | trainable? | +|-----------|-----------------------------------------------|-----------------------------------------------------------------------------------------------------|------------| +| W_embed | tensor | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "embed.weight"> | true | +| W_pos | tensor | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "pos.weight"> | true | +| W_qkv | tensor | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "h.0.attn.qkv"> | true | +| W_attn_o | tensor | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "h.0.attn.o"> | true | +| W_mlp_in | tensor | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "h.0.mlp.in"> | true | +| W_mlp_out | tensor | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "h.0.mlp.out"> | true | +| W_unembed | tensor | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "unembed.weight"> | true | + +## provenance + +| field | value | +|----------------------|----------------------------------------------------------------------| +| extraction_technique | sae_forge_v1.distill | +| version | 0.4.2 | +| config_hash | sha256:1111111111111111111111111111111111111111111111111111111111111111 | +| source_sae_hash | sha256:2222222222222222222222222222222222222222222222222222222222222222 | +| benchmark_score | 0.972 | + +## faithfulness + +| metric | threshold | distribution | reference | +|---------------|-----------|---------------|----------------| +| kl_divergence | 0.05 | imagenet_val | teacher_model | + +## verification rules + +- shape_consistency +- parameter_count: 11392 +- faithfulness: kl_divergence <= 0.05 under distribution=imagenet_val against reference=teacher_model + +> Notes: +> +> Symbolic dims `batch`, `seq`, `hidden`, `vocab` unify across the +> machine. The parameter_count sum is purely the declared weight +> shapes: +> embed: 64*64 = 4096 +> pos: 8*64 = 512 +> qkv: 64*3*64 = 12288 → this dominates; the toy keeps it small +> by using a tied projection in the implementation, but the +> declaration is the full shape. +> The 11392 value here is illustrative; actual fixture will be +> recomputed by `parameter_count` once binaries land. The verifier +> emits PARAMETER_COUNT_MISMATCH if the sum does not match — that +> is the intended self-correcting behavior of the invariant. diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/proposal.md b/openspec/changes/extend-orca-lang-neural-and-sparse/proposal.md new file mode 100644 index 0000000..b03b559 --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/proposal.md @@ -0,0 +1,243 @@ +## Why + +Orca today covers two artifact shapes: state machines (`# machine`) +and decision tables (`# decision_table`). The sibling q-orca dialect +covers quantum primitives. The sm-sae benchmark +(github.com/jascal/sm-sae) wants Orca-shaped artifacts for a wider +range of SAE compression and extraction techniques than the +quantum-encoding-only path polygram currently emits. Two concrete +gaps: + +1. **Neural / distilled-transformer artifacts** (e.g. sae-forge's + `NativeModel`, concept-bottleneck networks). A typed DAG of + layer operations with weights stored in sidecar binaries. + Polygram emits these as bespoke files outside Orca's grammar + today; the benchmark wants them inside `.orca.md` so they share + the parser, verifier, and tooling pipeline. + +2. **Sparse / cluster-aware feature dictionaries** (e.g. + hierarchical SAEs, group-sparse codes). A cluster manifest plus + sparse weight references. Same story — currently expressed in + adjacent JSON sidecars; the benchmark wants the cluster + structure inside the orca artifact so that + `cluster_completeness`, `sparsity_bound`, and decoder-norm + preservation can be machine-checked alongside the rest of the + workflow. + +The instinct to spawn `n-orca` and `s-orca` as separate dialects +is wrong on inspection. q-orca's dialect status is justified +because qubits, unitary gates, and measurement outcomes are a +genuinely different data model — a qubit cannot type-unify with a +classical scalar, a unitary cannot type-unify with a tensor op, +and measurement statistics need their own vocabulary. Neural and +sparse artifacts, in contrast, share the classical data model: +they are typed DAGs over tensor-valued context. What they need is +new **types** (tensors, weight references, sparse matrices) and +new **sections** (weights, cluster manifests, faithfulness +assertions), not a parallel grammar. + +The right framing is therefore: one coherent grammar extension to +`orca-lang` that closes both gaps, with `# machine` and +`# decision_table` keeping their current semantics and q-orca +remaining a separate dialect. Splitting neural and sparse into two +changes would duplicate the type-system work (`tensor<...>`, +`weight_ref<...>`, `sparse_matrix<...>` are shared) and force +hybrid artifacts (transformer with a sparse output head) to span +two parallel grammars. + +This is planning-only. No code in this PR — the deliverable is +proposal + design + delta specs + tasks + three worked examples. + +## What Changes + +- **Language — types**: introduce three new type-system primitives + usable anywhere a type appears (context, weights table, return + types, decision-table action types): + - `tensor` — tensor with declared shape; shape may + include named symbolic dimensions for shape unification across + operations. + - `weight_ref` — content-addressed reference + to a tensor stored in a sibling binary (typically + `*.safetensors`). The grammar SHALL forbid inlining tensor + values in the markdown — references are the only supported + mechanism. + - `sparse_matrix` — sparse tensor with + `format ∈ {COO, CSR}`. +- **Language — sections**: four new top-level section types, + legal alongside existing ones in a `# machine` or as standalone + blocks in artifacts that contain only weights/clusters/faithfulness: + - `## weights` — declares external weights this artifact + references. Table form: `| name | type | weight_ref | trainable? |`. + - `## cluster_manifest` — named clusters with per-cluster + feature ID lists. Table form: `| cluster | features | size |`. + - `## faithfulness` — declarative assertions like `faithfulness + >= 0.95 under distribution D against reference R`. + - `## provenance` — extraction-technique ID, version, config + hash, source-SAE hash, optional benchmark scores. Required on + any artifact emitted by an extraction technique. +- **Language — invariants**: six new invariant kinds in + `## verification rules` that the verifier can evaluate + statically (parameter counts, shapes, cluster coverage, sparsity + bound, decoder-norm preservation declarations, faithfulness + declarations). +- **Language — extension to existing `## transitions` semantics**: + no new construct, but the types above are legal in transition + context/action signatures. A neural module expresses itself as a + `# machine` whose states are activation tensors (typed via + `tensor<...>`) and whose transitions are layer operations + (referencing weights via `weight_ref`). +- **AST**: new `TensorType`, `WeightRefType`, `SparseMatrixType` + type nodes; new `WeightDef`, `ClusterDef`, `ClusterManifestDef`, + `FaithfulnessDef`, `ProvenanceDef` section nodes; new + invariant-kind enum values on the existing verification-rules + AST. +- **Parser**: extend the type grammar to recognize the three new + type forms; extend section dispatch in the markdown parser to + handle the four new sections; recognize the new invariant-kind + keywords in `## verification rules`. +- **Verifier**: new shape-and-weights stage that runs after the + existing structural / completeness / determinism stages. Checks + the six new invariant kinds plus weight-reference integrity + (hashes match if the binary is present; absent binaries + surface a `WEIGHT_BINARY_MISSING` warning, not an error, since + artifacts are often handed around without their binaries). +- **Compiler**: out of scope. The XState/Mermaid backends already + ignore unknown context types; they SHALL continue to do so for + artifacts that use the new types, which keeps existing pipelines + passing through unaltered. +- **Examples**: three worked examples live under the change's + `examples/` directory and become canonical fixtures once + implementation lands: + 1. A tiny GPT-2-class transformer (~10K params) expressed as a + `# machine` with `## weights`, tensor-typed states, and + `faithfulness` / `parameter_count` invariants. + 2. A 16-feature group-sparse SAE expressed with + `## cluster_manifest`, `## weights` (sparse decoder), and + `cluster_completeness` / `sparsity_bound` invariants — no + transitions needed. + 3. A hybrid: small transformer with a sparse output head, + showing `## transitions` + `## cluster_manifest` in one file. + +## Capabilities + +### New Capabilities +None. This is a language/AST/verifier extension on existing +capabilities. No new file extension; no new top-level document +kind beyond what `# machine` and `# decision_table` already +provide (artifacts that contain only `## weights` + +`## cluster_manifest` + `## faithfulness` are valid standalone +documents under the same `.orca.md` extension, with no `# machine` +heading required). + +### Modified Capabilities + +- **`language`**: extended type grammar (three new type forms), + four new sections, six new invariant-kind keywords, one new + document-shape rule (sections-only artifact). +- **`verifier`**: new shape-and-weights stage plus six new + invariant-kind checks; new error/warning codes + (`SHAPE_MISMATCH`, `WEIGHT_HASH_MISMATCH`, + `WEIGHT_BINARY_MISSING`, `WEIGHT_KEY_MISSING`, + `CLUSTER_FEATURE_DUPLICATE`, `CLUSTER_COVERAGE_GAP`, + `SPARSITY_BOUND_VIOLATION`, `DECODER_NORM_DRIFT`, + `PARAMETER_COUNT_MISMATCH`, `FAITHFULNESS_TEST_SCAFFOLD_REQUIRED`, + `INLINE_TENSOR_FORBIDDEN`, `PROVENANCE_REQUIRED`). +- **`compiler`**: no new requirement. The change adds a + passthrough note: existing backends SHALL continue to ignore + unknown sections, preserving regression-safety for consumers + that don't yet understand the new sections. + +## Impact + +- `packages/orca-lang/src/parser/ast.ts` — add `TensorType`, + `WeightRefType`, `SparseMatrixType`, `WeightDef`, `ClusterDef`, + `ClusterManifestDef`, `FaithfulnessDef`, `ProvenanceDef`; extend + `InvariantKind` enum. ~120 LOC. +- `packages/orca-lang/src/parser/markdown-parser.ts` — type + grammar extension, four new section parsers, new invariant-kind + recognition. ~250 LOC + tests. +- `packages/orca-lang/src/verifier/shape-and-weights.ts` — new + verifier stage. ~350 LOC + tests. +- `packages/orca-lang/src/verifier/index.ts` — wire the new stage + into the pipeline after determinism, before properties checking. + ~10 LOC. +- `packages/orca-lang/docs/orca-md-grammar-spec.md` — document + the new type forms, sections, invariants in the canonical + grammar reference. +- `packages/orca-lang/examples/neural-tiny-transformer.orca.md`, + `packages/orca-lang/examples/sparse-sae-16f.orca.md`, + `packages/orca-lang/examples/hybrid-transformer-sparse-head.orca.md` + — three worked examples (drafts ship with this change in + `openspec/changes/extend-orca-lang-neural-and-sparse/examples/`; + promoted to package examples on implementation). +- `packages/orca-lang/tests/` — round-trip parse + verify on the + three examples; regression test confirming existing + `*.orca.md` and `*.q.orca.md` artifacts parse identically. +- `docs/error-catalog.md` — entries for the twelve new + error/warning codes. +- **No new runtime dependencies.** Runtime support (loading + weights, evaluating tensor ops, running faithfulness checks) + ships as a separate follow-up change. This spec defines only + the static grammar + verification surface. + +## Scope boundary + +In scope: +- Type grammar for `tensor<...>`, `weight_ref<...>`, + `sparse_matrix<...>`. +- Sections: `## weights`, `## cluster_manifest`, + `## faithfulness`, `## provenance`. +- Invariant kinds: `shape_consistency`, `sparsity_bound`, + `cluster_completeness`, `decoder_norm_preservation`, + `parameter_count`, `faithfulness`. +- Verifier-stage error and warning codes for each. +- AST + parser + static verifier behavior. +- Three worked examples (parse + verify, no implementation). +- Capability-negotiation note for downstream consumers. + +Explicitly **out of scope**: +- **Implementation.** This is a spec-only change. +- **Inlining weights into markdown.** Forbidden by design; the + spec explicitly rejects this as a non-goal and the verifier + emits `INLINE_TENSOR_FORBIDDEN` if encountered. +- **Compile back-ends / hardware targeting.** A separate change + (`add-neural-compile-targets`) will own emitting PyTorch / + ONNX / TFLite / safetensors-loading runtime glue. +- **Schema versioning.** A separate change + (`add-orca-schema-version`) will own version negotiation; this + change depends on it for the capability-negotiation flow but + does not itself introduce a schema field. +- **Algebraic / probabilistic / circuit extensions.** The + speculative `a-orca` / `p-orca` / `c-orca` family is out of + scope. The same logic applies — they are probably extensions, + not dialects — but each is its own future change. +- **q-orca convergence.** q-orca remains a separate dialect. + Its data model (qubits, unitaries, measurements) does not + type-unify with classical tensors; this change does not + attempt to merge them. +- **Runtime weight loading.** No runtime in this change. The + verifier validates hashes only when the binary is present in + the artifact directory; otherwise it emits a warning, not an + error. + +## Dependencies and follow-ups + +- **Depends on (soft)**: `add-orca-schema-version`. Capability + negotiation requires a version field. The spec lands without + it (consumers that load `.orca.md` and ignore unknown sections + continue to work; consumers that opt into the new sections do + so by capability advertisement). Versioning can land in parallel + and tighten the negotiation contract later. +- **Parked follow-ups (NOT this change)**: + - `add-neural-compile-targets` — PyTorch / ONNX / TFLite / + safetensors-loading runtime; weight binary lifecycle. + - `add-orca-schema-version` — version field + capability + advertisement; cross-cuts this change and others. + - `add-runtime-faithfulness-harness` — the actual numerical + check that a referenced reference model meets the declared + faithfulness threshold. The spec here describes only the + declarative form and the test-scaffold generation. + - `extend-orca-algebraic` (speculative `a-orca`), + `extend-orca-probabilistic` (`p-orca`), + `extend-orca-circuit` (`c-orca`) — each its own future + change once a concrete consumer surfaces. diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/specs/language/spec.md b/openspec/changes/extend-orca-lang-neural-and-sparse/specs/language/spec.md new file mode 100644 index 0000000..7000866 --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/specs/language/spec.md @@ -0,0 +1,239 @@ +## ADDED Requirements + +### Requirement: Tensor Type + +The parser SHALL accept `tensor` as a type +expression wherever a type appears (context table, weights table, +decision-table action types, action signatures). `dtype` SHALL be +one of `f16`, `bf16`, `f32`, `f64`, `i8`, `i16`, `i32`, `i64`, +`u8`, `bool`. `shape` SHALL be a bracketed comma-separated list +of dimensions where each dimension is either a non-negative +integer (concrete dim) or an identifier (named symbolic dim). +Symbolic dim names are scoped to a single machine. + +#### Scenario: Concrete-shape tensor in context + +- **WHEN** a `## context` row declares + `| activations | tensor | |` +- **THEN** the resulting `ContextField` carries a `TensorType` + with `dtype="f32"` and `shape=[128, 768]` + +#### Scenario: Symbolic-shape tensor + +- **WHEN** a `## context` row declares + `| activations | tensor | |` +- **THEN** the resulting `TensorType` has + `shape=["batch", "seq", "hidden"]` and the verifier MAY unify + these names across transitions within the same machine + +#### Scenario: Mixed concrete and symbolic dims + +- **WHEN** a type expression is `tensor` +- **THEN** the resulting `TensorType` has + `shape=["batch", 768]`; subsequent unifications bind `batch` + to a concrete value while requiring `768` to match exactly + +#### Scenario: Inline tensor literal rejected + +- **WHEN** a cell typed `tensor<...>` contains a numeric array + literal such as `[[0.1, 0.2], [0.3, 0.4]]` +- **THEN** the parser emits `INLINE_TENSOR_FORBIDDEN` — + references are the only supported mechanism for tensor values + +### Requirement: Weight Reference Type + +The parser SHALL accept `weight_ref` as a +type expression. `path` SHALL be a quoted relative path to a +sidecar binary (typically `*.safetensors`); `sha256` SHALL be a +64-character lowercase hexadecimal digest of the binary file; +`key` SHALL be a quoted identifier naming the tensor inside the +binary. + +#### Scenario: Well-formed weight_ref + +- **WHEN** a `## weights` row declares the type + `weight_ref<"weights.safetensors", "a3f1...e0", "transformer.h.0.attn.c_attn.weight">` +- **THEN** the resulting `WeightRefType` has the path, hash, and + key parsed into their respective string fields + +#### Scenario: Malformed hash length + +- **WHEN** a `weight_ref` declares `sha256="abc"` +- **THEN** the parser emits a structured error — hash must be a + 64-character hexadecimal string + +### Requirement: Sparse Matrix Type + +The parser SHALL accept `sparse_matrix` as +a type expression. `dtype` and `shape` follow the tensor-type +grammar. `format` SHALL be one of `COO`, `CSR`. + +#### Scenario: CSR sparse matrix in weights + +- **WHEN** a `## weights` row's type is + `sparse_matrix` +- **THEN** the resulting `SparseMatrixType` carries `dtype="f32"`, + `shape=[16, 512]`, and `format="CSR"` + +#### Scenario: Unknown format rejected + +- **WHEN** a type is `sparse_matrix` +- **THEN** the parser emits a structured error — only COO and + CSR are supported in this change + +### Requirement: Weights Section + +The parser SHALL accept an optional `## weights` section whose +table has columns `| name | type | weight_ref | trainable? |`. +Each row declares one named external tensor. `name` is an +identifier; `type` is `tensor<...>` or `sparse_matrix<...>`; +`weight_ref` is a `weight_ref<...>` type expression; `trainable?` +is `true` or `false` (default `false`). + +#### Scenario: Declared weight row + +- **WHEN** a machine has a `## weights` row + `| W_qkv | tensor | weight_ref<"w.safetensors", "<64-hex>", "qkv"> | true |` +- **THEN** the resulting `WeightDef` carries the name, the + tensor type, the weight reference, and `trainable=true` + +#### Scenario: Trainable column defaults to false + +- **WHEN** a `## weights` row omits the `trainable?` column +- **THEN** the resulting `WeightDef` has `trainable=false` + +### Requirement: Cluster Manifest Section + +The parser SHALL accept an optional `## cluster_manifest` +section whose table has columns `| cluster | features | size |`. +`cluster` is an identifier or quoted string; `features` is a +comma-separated list of feature IDs (integers or identifiers); +`size` is an integer that SHALL equal `features.length` +(parser-level check via `CLUSTER_SIZE_MISMATCH`). + +#### Scenario: Well-formed cluster row + +- **WHEN** the manifest has a row + `| color_cluster | 0, 1, 2, 3 | 4 |` +- **THEN** the resulting `ClusterDef` has + `name="color_cluster"`, `features=[0, 1, 2, 3]`, `size=4` + +#### Scenario: Size mismatch rejected + +- **WHEN** a row declares 4 features but `size=5` +- **THEN** the parser emits `CLUSTER_SIZE_MISMATCH` + +### Requirement: Faithfulness Section + +The parser SHALL accept an optional `## faithfulness` section +whose table has columns +`| metric | threshold | distribution | reference |`. Each row +declares one declarative faithfulness assertion. `metric` SHALL +be from the vocabulary `{kl_divergence, mse, cosine_similarity, +top1_accuracy, top5_accuracy}` (extensible in future changes); +`threshold` SHALL parse as a decimal; `distribution` and +`reference` SHALL be non-empty identifiers. + +#### Scenario: Well-formed faithfulness row + +- **WHEN** a row declares + `| kl_divergence | 0.05 | imagenet_val | teacher_model |` +- **THEN** the resulting `FaithfulnessDef` has + `metric="kl_divergence"`, `threshold=0.05`, + `distribution="imagenet_val"`, `reference="teacher_model"` + +### Requirement: Provenance Section + +The parser SHALL accept an optional `## provenance` section as +a two-column key/value table `| field | value |`. Field names +are arbitrary identifiers; the verifier later enforces that +required fields are present for extraction-technique-emitted +artifacts. + +#### Scenario: Well-formed provenance section + +- **WHEN** a `## provenance` section contains rows for + `extraction_technique`, `version`, `config_hash`, and + `benchmark_score` +- **THEN** the resulting `ProvenanceDef` carries a key/value + map with all four fields + +### Requirement: New Invariant Kinds in Verification Rules + +The parser SHALL recognize six new invariant kinds in the +`## verification rules` bullet list: +`shape_consistency`, `sparsity_bound: `, +`cluster_completeness`, +`decoder_norm_preservation: tolerance=, reference=`, +`parameter_count: `, and +`faithfulness: , , , `. + +#### Scenario: shape_consistency bullet + +- **WHEN** `## verification rules` contains the bullet + `- shape_consistency` +- **THEN** the resulting `InvariantDef` has + `kind="shape_consistency"` and no parameters + +#### Scenario: sparsity_bound with parameter + +- **WHEN** the bullet is `- sparsity_bound: 8` +- **THEN** the `InvariantDef` has `kind="sparsity_bound"` and + `params={maxNnzPerRow: 8}` + +#### Scenario: parameter_count with parameter + +- **WHEN** the bullet is `- parameter_count: 10_240` +- **THEN** the `InvariantDef` has `kind="parameter_count"` and + `params={expected: 10240}` (underscores in numeric literals + are stripped during parsing) + +#### Scenario: faithfulness invariant + +- **WHEN** the bullet is + `- faithfulness: kl_divergence <= 0.05 under distribution=imagenet_val against reference=teacher_model` +- **THEN** the `InvariantDef` has `kind="faithfulness"` and + `params={metric: "kl_divergence", threshold: 0.05, + distribution: "imagenet_val", reference: "teacher_model"}` + +### Requirement: Sections-Only Artifact + +The parser SHALL accept an `.orca.md` document that contains +none of `# machine`, `# decision_table`, or q-orca top-level +headings, but contains at least one of `## weights`, +`## cluster_manifest`, or `## provenance`. The resulting AST +node SHALL be a `SectionsOnlyArtifact`. A document with only +`## faithfulness` and no anchoring section SHALL be rejected +with `EMPTY_ARTIFACT`. + +#### Scenario: Dictionary-style sparse SAE parses as sections-only + +- **WHEN** an `.orca.md` document has only `## weights`, + `## cluster_manifest`, `## provenance`, and + `## verification rules` +- **THEN** the parser yields an `OrcaFile` with one + `SectionsOnlyArtifact`, no `MachineDef`, no + `DecisionTableDef` + +#### Scenario: Empty-artifact rejection + +- **WHEN** a document contains only `## faithfulness` +- **THEN** the parser emits `EMPTY_ARTIFACT` — faithfulness is + a contract about an artifact, not the artifact itself + +### Requirement: Backward-Compatible Parsing of Existing Artifacts + +Every existing `.orca.md` and `.q.orca.md` file that parsed +under the pre-extension grammar SHALL parse identically under +the extended grammar. The resulting AST SHALL round-trip +through `ast-to-markdown` to byte-identical output. The +extension is purely additive — no existing AST node shape, no +existing parsing rule, and no existing error code is modified. + +#### Scenario: Pre-extension machine round-trip unchanged + +- **WHEN** an existing machine (e.g. + `examples/payment-processor.orca.md`) is parsed under the + extended grammar and immediately serialized back via + `ast-to-markdown` +- **THEN** the output SHALL be byte-identical to the input diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/specs/verifier/spec.md b/openspec/changes/extend-orca-lang-neural-and-sparse/specs/verifier/spec.md new file mode 100644 index 0000000..63cd1b7 --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/specs/verifier/spec.md @@ -0,0 +1,313 @@ +## MODIFIED Requirements + +### Requirement: Verifier Pipeline Order + +The verifier SHALL run stages in the following order: +structural, completeness, determinism, **shape-and-weights +(new)**, properties. If the structural stage produces any +error, later stages SHALL be skipped. Otherwise, every +non-skipped stage SHALL run and their errors SHALL be merged +into a single result. The new shape-and-weights stage SHALL +run only on machines or sections-only artifacts that contain +at least one tensor type, weight reference, sparse matrix +type, or new section; otherwise it SHALL no-op so existing +artifacts incur zero verification cost. + +#### Scenario: Existing machine skips the new stage + +- **WHEN** a machine has no tensor types, no weight refs, no + sparse matrices, and none of the new sections +- **THEN** `verify()` SHALL skip the shape-and-weights stage + entirely; verification cost and error output SHALL be + identical to pre-extension behavior + +#### Scenario: Machine with tensor types runs the new stage + +- **WHEN** a machine has a `## weights` section with at least + one weight row +- **THEN** the shape-and-weights stage runs after determinism + and before properties + +## ADDED Requirements + +### Requirement: Shape Consistency Check + +The verifier SHALL evaluate `shape_consistency` invariants by +walking the `## transitions` table and unifying each +transition action's input tensor type against its source state's +declared activation type, and its output tensor type against +its target state's declared activation type. Symbolic dim names +SHALL unify by name; concrete dims SHALL unify by value. Errors: +- `SHAPE_MISMATCH` (error) — declared shape does not match + expected shape at a transition boundary. +- `SHAPE_NAME_REBINDING` (error) — a symbolic dim name binds + to two divergent concrete values across transitions in the + same machine. + +#### Scenario: Two transitions agree on a symbolic dim + +- **WHEN** a machine declares + `tensor` on both the input and output of + a `linear` transition, with `batch` bound elsewhere to `128` +- **THEN** the shape-consistency check passes for that + transition + +#### Scenario: Concrete dim mismatch + +- **WHEN** a transition action produces `tensor` + but the target state's activation is + `tensor` +- **THEN** the verifier emits `SHAPE_MISMATCH` at error severity + with a message naming the conflicting dim (index 1: expected + 512, got 768) + +#### Scenario: Symbolic dim rebinding + +- **WHEN** transition A binds `seq=128` and transition B in the + same machine binds `seq=64` for the same symbolic dim +- **THEN** the verifier emits `SHAPE_NAME_REBINDING` at error + severity + +### Requirement: Parameter Count Check + +The verifier SHALL evaluate `parameter_count: ` +invariants by summing `prod(shape)` across all `## weights` +rows. Rows whose shape contains unresolved symbolic dims at +verification time SHALL be skipped with a +`PARAMETER_COUNT_UNRESOLVED` warning, and the resulting +partial sum SHALL be compared against the declared expected +value. Errors: +- `PARAMETER_COUNT_MISMATCH` (error) — sum of resolved + weight-row element counts does not equal the declared value. +- `PARAMETER_COUNT_UNRESOLVED` (warning) — one or more rows + could not be summed due to unresolved symbolic dims. + +#### Scenario: Sum equals declared value + +- **WHEN** a machine declares two weight rows of shapes + `[10, 100]` and `[100, 1]` and the invariant + `- parameter_count: 1100` +- **THEN** the check passes silently + +#### Scenario: Mismatch + +- **WHEN** the rows total `1100` but the invariant is + `- parameter_count: 10240` +- **THEN** the verifier emits `PARAMETER_COUNT_MISMATCH` at + error severity, naming the actual and expected totals + +### Requirement: Sparsity Bound Check + +The verifier SHALL evaluate `sparsity_bound: ` +invariants by inspecting every `## weights` row of type +`sparse_matrix<...>` and comparing the declared or computed +nnz-per-row against the bound. If the binary is present, the +nnz is computed from the safetensor's indices; otherwise the +parser-declared metadata is used. Error: `SPARSITY_BOUND_VIOLATION` +(error). + +#### Scenario: Sparse decoder within bound + +- **WHEN** a sparse decoder has at most 4 nonzeros per row and + the invariant is `- sparsity_bound: 8` +- **THEN** the check passes silently + +#### Scenario: Bound exceeded + +- **WHEN** a sparse decoder has up to 12 nonzeros per row and + the invariant is `- sparsity_bound: 8` +- **THEN** the verifier emits `SPARSITY_BOUND_VIOLATION` at + error severity, identifying the offending row(s) + +### Requirement: Cluster Completeness Check + +The verifier SHALL evaluate `cluster_completeness` invariants +by computing the union of all clusters' feature lists in the +`## cluster_manifest` and comparing this set to the relevant +tensor's feature ID set (taken from the tensor's shape's +feature dim or a sidecar `feature_ids` field). Errors: +- `CLUSTER_FEATURE_DUPLICATE` (error) — a feature ID appears + in more than one cluster. +- `CLUSTER_COVERAGE_GAP` (error) — a feature ID exists in the + tensor but is not in any cluster. + +#### Scenario: Complete partition + +- **WHEN** four clusters of four features each cover features + 0–15 with no overlap and the tensor has 16 features +- **THEN** the check passes silently + +#### Scenario: Duplicate feature + +- **WHEN** feature 3 appears in both `cluster_a` and + `cluster_b` +- **THEN** the verifier emits `CLUSTER_FEATURE_DUPLICATE` at + error severity, naming the feature and both clusters + +#### Scenario: Coverage gap + +- **WHEN** the tensor has 16 features but feature 15 is in no + cluster +- **THEN** the verifier emits `CLUSTER_COVERAGE_GAP` at error + severity, naming the missing feature + +### Requirement: Decoder Norm Preservation Check (Declarative) + +The verifier SHALL evaluate `decoder_norm_preservation: +tolerance=, reference=` invariants structurally: the +named reference SHALL resolve to a declared weight or provenance +entry; the tolerance SHALL parse as a decimal. The numerical +check is out of scope (runs at build/run time in +`add-runtime-faithfulness-harness`). Verifier behavior: +- If both the artifact's decoder weight and the reference are + resolvable and both binaries are present, the verifier MAY + compute column norms and emit `DECODER_NORM_DRIFT` (error) + if any norm differs from the reference beyond tolerance. +- Otherwise, the verifier SHALL emit + `FAITHFULNESS_TEST_SCAFFOLD_REQUIRED` (info) noting that the + runtime harness is responsible for the actual check. + +#### Scenario: Reference resolves; binaries absent + +- **WHEN** the invariant is + `- decoder_norm_preservation: tolerance=0.01, reference=W_dec_baseline` + and `W_dec_baseline` resolves but its binary is not present +- **THEN** the verifier emits + `FAITHFULNESS_TEST_SCAFFOLD_REQUIRED` at info severity + +#### Scenario: Reference does not resolve + +- **WHEN** the invariant references `W_baseline` and no such + weight or provenance field is declared anywhere in the file +- **THEN** the verifier emits `DECODER_NORM_DRIFT` at error + severity, message `unresolved reference: W_baseline` + +### Requirement: Faithfulness Check (Declarative) + +The verifier SHALL validate `faithfulness` declarations +(whether they appear as a `## faithfulness` section row or as +an inline `## verification rules` bullet) structurally: +- `metric` SHALL be in the allowed vocabulary + (`kl_divergence`, `mse`, `cosine_similarity`, + `top1_accuracy`, `top5_accuracy`). Otherwise: + `FAITHFULNESS_DECLARATION_MALFORMED` (error). +- `threshold` SHALL parse as a decimal. +- `distribution` and `reference` SHALL be non-empty identifiers. + +If validation passes, the verifier SHALL emit +`FAITHFULNESS_TEST_SCAFFOLD_REQUIRED` at info severity, +recording that the runtime harness owes the actual numerical +check. + +#### Scenario: Well-formed faithfulness declaration + +- **WHEN** a row reads + `| kl_divergence | 0.05 | imagenet_val | teacher_model |` +- **THEN** the verifier emits + `FAITHFULNESS_TEST_SCAFFOLD_REQUIRED` at info severity + +#### Scenario: Unknown metric + +- **WHEN** the metric is `mahalanobis_distance` +- **THEN** the verifier emits + `FAITHFULNESS_DECLARATION_MALFORMED` at error severity + +### Requirement: Weight Reference Integrity Check + +The verifier SHALL check each `weight_ref` as follows: +1. Resolve `path` relative to the artifact directory. +2. If the binary is **absent**, emit `WEIGHT_BINARY_MISSING` + at **warning** severity and move on. The artifact remains + valid for static analysis. +3. If the binary is **present**, compute its sha256 digest. On + mismatch with the declared digest, emit + `WEIGHT_HASH_MISMATCH` at **error** severity. +4. If the binary is present and the hash matches, parse the + safetensors header and check that `key` is among its tensor + names. On miss, emit `WEIGHT_KEY_MISSING` at **error** + severity. + +#### Scenario: Binary absent — review-friendly behavior + +- **WHEN** `weight_ref` points to `weights.safetensors` and + that file does not exist next to the artifact +- **THEN** the verifier emits `WEIGHT_BINARY_MISSING` at + warning severity and continues; verification overall + succeeds (no errors) + +#### Scenario: Binary present, hash diverges + +- **WHEN** the binary exists but its sha256 differs from the + declared digest +- **THEN** the verifier emits `WEIGHT_HASH_MISMATCH` at error + severity + +#### Scenario: Binary present, key missing + +- **WHEN** the binary's hash matches but the declared `key` + does not appear among the binary's tensor names +- **THEN** the verifier emits `WEIGHT_KEY_MISSING` at error + severity + +### Requirement: Provenance Required-Set Check + +The verifier SHALL detect extraction-technique-emitted +artifacts heuristically: any artifact that contains `## weights` +*and* `## faithfulness`, or any artifact that contains +`## cluster_manifest`, is treated as extraction-technique +output. Such an artifact SHALL declare a `## provenance` +section containing at minimum `extraction_technique`, +`version`, and `config_hash`. Error: `PROVENANCE_REQUIRED` +(error). + +#### Scenario: Sparse SAE artifact requires provenance + +- **WHEN** an artifact has `## cluster_manifest` but no + `## provenance` section +- **THEN** the verifier emits `PROVENANCE_REQUIRED` at error + severity + +#### Scenario: Standalone machine with no extraction signal + +- **WHEN** an artifact has a `# machine` heading, no + `## weights`, no `## cluster_manifest` +- **THEN** no provenance is required; no error is emitted + +### Requirement: Inline Tensor Literals Forbidden + +The verifier SHALL re-affirm at stage entry that no +`weight_ref` cell or tensor-typed context value contains a raw +inline tensor literal. The primary check is performed at parse +time (`INLINE_TENSOR_FORBIDDEN`); the verifier re-checks defensively +and emits the same code at error severity if reached. + +#### Scenario: Defensive re-check + +- **WHEN** a malformed AST (constructed programmatically rather + than parsed) carries an inline tensor literal in a + tensor-typed slot +- **THEN** the verifier emits `INLINE_TENSOR_FORBIDDEN` at + error severity + +### Requirement: Capability Negotiation Note + +The verifier SHALL document, in its result metadata, whether +the artifact uses any feature from the +`neural-and-sparse-v1` capability set (new types or new +sections). Consumers MAY use this flag to decide whether to +load runtime modules required for downstream consumption. The +verifier does not itself reject artifacts based on consumer +capability — that contract belongs to the loading consumer. + +#### Scenario: Capability flag set when new sections present + +- **WHEN** an artifact uses `## weights` or any of the other + new sections +- **THEN** `verifyResult.capabilities` includes + `"neural-and-sparse-v1"` + +#### Scenario: Capability flag absent for existing-only artifacts + +- **WHEN** an artifact uses only pre-extension grammar +- **THEN** `verifyResult.capabilities` does not include + `"neural-and-sparse-v1"` diff --git a/openspec/changes/extend-orca-lang-neural-and-sparse/tasks.md b/openspec/changes/extend-orca-lang-neural-and-sparse/tasks.md new file mode 100644 index 0000000..70bb639 --- /dev/null +++ b/openspec/changes/extend-orca-lang-neural-and-sparse/tasks.md @@ -0,0 +1,257 @@ +## 1. AST + +- [ ] 1.1 Add `TensorType` node in + `packages/orca-lang/src/parser/ast.ts` with fields + `dtype: TensorDType`, `shape: Array` + (string entries = symbolic dim names). +- [ ] 1.2 Add `WeightRefType` node with fields + `path: string`, `sha256: string` (64-char hex), + `key: string`. +- [ ] 1.3 Add `SparseMatrixType` node with fields + `dtype: TensorDType`, `shape: Array`, + `format: 'COO' | 'CSR'`. +- [ ] 1.4 Add `WeightDef` (one row of `## weights`), + `ClusterDef` (one row of `## cluster_manifest`), + `ClusterManifestDef` (the whole section), `FaithfulnessDef` + (one row of `## faithfulness`), `ProvenanceDef` (whole + key/value table). +- [ ] 1.5 Extend `InvariantKind` enum with + `shape_consistency`, `sparsity_bound`, + `cluster_completeness`, `decoder_norm_preservation`, + `parameter_count`, `faithfulness`. Add parameter fields on + `InvariantDef` for the kinds that take parameters. +- [ ] 1.6 Add `SectionsOnlyArtifact` node for documents that + contain only `## weights` / `## cluster_manifest` / + `## faithfulness` / `## provenance` with no `# machine` + heading. Extend `OrcaFile` to hold a list of these alongside + `machines` and `decisionTables`. + +## 2. Parser + +- [ ] 2.1 Extend the type-grammar tokenizer in + `packages/orca-lang/src/parser/markdown-parser.ts` to + recognize `tensor<...>`, `weight_ref<...>`, + `sparse_matrix<...>`. Parse parameter lists inside `<...>` + with comma separation; reject malformed shapes with + structured errors. +- [ ] 2.2 Add section parser for `## weights` (table: + `| name | type | weight_ref | trainable? |`). Wire into the + section dispatch in the markdown parser. `trainable?` cell + accepts `true` / `false` (default `false`). +- [ ] 2.3 Add section parser for `## cluster_manifest` (table: + `| cluster | features | size |`). `features` cell is a + comma-separated list of feature IDs (integers or + identifiers); `size` is informational and SHALL match + `features.length` (parser-level check — + `CLUSTER_SIZE_MISMATCH` if not). +- [ ] 2.4 Add section parser for `## faithfulness` (table: + `| metric | threshold | distribution | reference |`). +- [ ] 2.5 Add section parser for `## provenance` (key/value + table with two columns `| field | value |`; arbitrary fields + allowed, with required-set check moved to the verifier). +- [ ] 2.6 Extend `## verification rules` bullet parser to + recognize the six new invariant kinds and their parameter + syntax (see the grammar table in + `specs/language/spec.md`). +- [ ] 2.7 Recognize a sections-only document: if no `# machine` + or `# decision_table` heading appears but at least one new + section does, build a `SectionsOnlyArtifact` instead of + raising `MISSING_MACHINE`. +- [ ] 2.8 Forbid inline tensor literals. If the parser + encounters anything that looks like a tensor literal (numeric + array in a cell that is typed `tensor<...>`), emit + `INLINE_TENSOR_FORBIDDEN`. References are the only supported + mechanism. +- [ ] 2.9 Unit tests in + `packages/orca-lang/tests/parser-neural-sparse.spec.ts` + covering: each new type with valid and malformed inputs, + each new section, the sections-only artifact shape, each new + invariant-kind keyword, and `INLINE_TENSOR_FORBIDDEN`. + +## 3. Verifier — shape-and-weights stage + +- [ ] 3.1 Create + `packages/orca-lang/src/verifier/shape-and-weights.ts` + exporting `checkShapeAndWeights(file: OrcaFile, + machine: MachineDef | SectionsOnlyArtifact) -> + VerificationResult`. +- [ ] 3.2 Implement `shape_consistency`: walk + `## transitions` rows; for each row whose action references a + tensor-typed input or output, unify the input type against + the source state's declared activation type and the output + type against the target state's declared activation type. + Symbolic dims unify by name; emit `SHAPE_MISMATCH` on + conflict and `SHAPE_NAME_REBINDING` if a name's bound value + diverges across two transitions. +- [ ] 3.3 Implement `parameter_count`: sum `prod(shape)` across + all `## weights` rows (skip rows with unresolved symbolic + dims and emit `PARAMETER_COUNT_UNRESOLVED` warning); compare + to declared expected value; emit `PARAMETER_COUNT_MISMATCH` + on inequality. +- [ ] 3.4 Implement `sparsity_bound`: for each `## weights` row + whose type is `sparse_matrix<...>`, check that the declared + nnz-per-row metadata (parsed from a sibling + `.nnz_per_row` field in the type's parameter list, or + computed from the binary if present) does not exceed the + declared bound. Emit `SPARSITY_BOUND_VIOLATION`. +- [ ] 3.5 Implement `cluster_completeness`: for the + `## cluster_manifest`, check that the union of all clusters' + feature lists covers exactly the feature ID set declared + in the relevant tensor's shape (or a sidecar + `feature_ids` field). Emit `CLUSTER_FEATURE_DUPLICATE` for + features appearing in more than one cluster; + `CLUSTER_COVERAGE_GAP` for features in the tensor but not in + any cluster. +- [ ] 3.6 Implement `decoder_norm_preservation`: emit + `DECODER_NORM_DRIFT` only if both the artifact and the + reference have binaries present and norms differ beyond + tolerance; otherwise emit + `FAITHFULNESS_TEST_SCAFFOLD_REQUIRED` info-level note that + the runtime harness must check this at build/run time. +- [ ] 3.7 Implement `faithfulness` (declarative): structural + validation only — metric is a known identifier (allowed + vocabulary: `kl_divergence`, `mse`, `cosine_similarity`, + `top1_accuracy`, `top5_accuracy`); threshold parses as + decimal; distribution and reference are non-empty + identifiers. Emit `FAITHFULNESS_DECLARATION_MALFORMED` + on validation failure; otherwise emit + `FAITHFULNESS_TEST_SCAFFOLD_REQUIRED` info-level note. +- [ ] 3.8 Implement weight-reference integrity: for each + `weight_ref`, check that `path` resolves relative to the + artifact directory. If absent, emit + `WEIGHT_BINARY_MISSING` at warning severity. If present, + compute the binary's sha256 and compare to the declared + digest; emit `WEIGHT_HASH_MISMATCH` at error severity on + inequality. If present and hash matches, attempt to look up + `key` inside the binary (using a safetensors header parse); + emit `WEIGHT_KEY_MISSING` at error severity if not found. +- [ ] 3.9 Implement provenance required-set check: if the + artifact's section set indicates extraction-technique output + (heuristic: has `## weights` *and* `## faithfulness`, OR has + `## cluster_manifest`), require a `## provenance` section + with at least `extraction_technique`, `version`, and + `config_hash`. Emit `PROVENANCE_REQUIRED` at error severity + if missing. +- [ ] 3.10 Wire the stage into + `packages/orca-lang/src/verifier/index.ts` after determinism + and before properties checking. Add + `VerifyOptions.skipShapeAndWeights` flag. +- [ ] 3.11 Unit tests in + `packages/orca-lang/tests/verifier-shape-and-weights.spec.ts` + covering every new error/warning code (happy path + failure + per code). + +## 4. Examples (3 worked artifacts) + +- [ ] 4.1 Author `examples/tiny-transformer.orca.md` — a + ~10K-parameter GPT-2-class transformer expressed as a + `# machine`. States are activation tensors with named symbolic + dims; transitions are attention / MLP / projection + operations referencing `weight_ref` entries in `## weights`. + `## verification rules` include `shape_consistency`, + `parameter_count: 10240`, and a `faithfulness` rule against + a reference teacher model. (A draft lives at + `openspec/changes/extend-orca-lang-neural-and-sparse/examples/tiny-transformer.orca.md`.) +- [ ] 4.2 Author `examples/sparse-sae-16f.orca.md` — a + 16-feature group-sparse SAE expressed as a + sections-only artifact: `## weights` (sparse decoder via + `sparse_matrix`), `## cluster_manifest` + partitioning the 16 features into 4 clusters of 4, + `## provenance` (extraction technique = `polygram_v2`), + `## verification rules` with `cluster_completeness`, + `sparsity_bound: 4`, and a `decoder_norm_preservation` rule. +- [ ] 4.3 Author `examples/hybrid-transformer-sparse-head.orca.md` + — a small transformer with a sparse output head, single + file: `# machine` with tensor-typed states + transitions + through the transformer body, plus `## weights`, + `## cluster_manifest` (for the sparse head's feature + partition), `## provenance`, `## verification rules` mixing + `shape_consistency`, `parameter_count`, `sparsity_bound`, + and `cluster_completeness`. Demonstrates that one artifact + cleanly mixes `## transitions` + `## cluster_manifest`. +- [ ] 4.4 Each example SHALL parse and verify under the + extended verifier with no errors (warnings allowed for + `WEIGHT_BINARY_MISSING` because binaries are not checked + into the spec change). Round-trip through `ast-to-markdown` + SHALL be byte-stable. + +## 5. Regression — existing corpus parses identically + +- [ ] 5.1 Author + `packages/orca-lang/tests/regression-existing-corpus.spec.ts` + that enumerates all `*.orca.md` and `*.q.orca.md` files + under `packages/*/examples/` and `packages/*/orca/`, + parses each with the extended parser, round-trips through + `ast-to-markdown`, and asserts byte-identical output to the + pre-extension baseline. (Baseline captured as a fixture + snapshot in the same test directory.) +- [ ] 5.2 Confirm zero changes to existing `MachineDef`, + `DecisionTableDef`, or any other existing AST node shape. + If an AST shape changes, halt and revisit the design — the + intent is purely additive. + +## 6. Documentation + +- [ ] 6.1 Update `packages/orca-lang/docs/orca-md-grammar-spec.md` + with sections for the new types, new sections, and new + invariants. Include a small example for each. +- [ ] 6.2 Update `docs/error-catalog.md` with entries for the + twelve new error/warning codes (see proposal). Each entry + includes cause, fix, and an example. +- [ ] 6.3 Add a "Capability negotiation" note in + `docs/orca-md-grammar-spec.md` describing the + `neural-and-sparse-v1` capability string and the + graceful-degradation contract for consumers that do not + understand the new sections. + +## 7. Spec sync + +- [ ] 7.1 Confirm `proposal.md`, `design.md`, and the three + `specs//spec.md` files are mutually consistent — + every requirement in a spec has a parameter / behavior in + design; every decision in design has a corresponding + requirement in some spec. +- [ ] 7.2 If `openspec validate` is wired in this repo + (it is not at the time of writing — see "Open questions" in + design), run `openspec validate + extend-orca-lang-neural-and-sparse --strict` and address any + issues. Otherwise, manually review against the q-orca repo's + conventions (which served as the template here). + +## 8. End-to-end verification + +- [ ] 8.1 Build the orca-lang package (`pnpm build`) and run + `pnpm test:lang` — all existing 135 tests SHALL pass. +- [ ] 8.2 Run the new parser, verifier, and regression test + suites — all SHALL pass. +- [ ] 8.3 Run `npx tsx src/index.ts verify` on each of the + three new examples and confirm clean output (errors empty; + only the expected `WEIGHT_BINARY_MISSING` warning where + binaries are absent). +- [ ] 8.4 `pnpm health-check` SHALL still pass end-to-end. + +## 9. Parked follow-ups (NOT this change) + +- [ ] 9.1 **Parked**: `add-neural-compile-targets` — emit + PyTorch, ONNX, TFLite, or safetensors-loading runtime glue + from a verified neural artifact. +- [ ] 9.2 **Parked**: `add-orca-schema-version` — version + field + capability advertisement, cross-cuts this change + and others. +- [ ] 9.3 **Parked**: `add-runtime-faithfulness-harness` — the + actual numerical check (loads binaries, runs the metric on + the named distribution, compares to threshold). This spec + describes only the declarative form and the + test-scaffolding output. +- [ ] 9.4 **Parked**: `extend-orca-algebraic` (`a-orca`), + `extend-orca-probabilistic` (`p-orca`), + `extend-orca-circuit` (`c-orca`) — each its own future + change when a concrete consumer surfaces. +- [ ] 9.5 **Parked**: glob references in `## weights` for + artifacts with thousands of weight rows. Current design is + one row per named tensor. +- [ ] 9.6 **Parked**: URI-scheme `weight_ref` paths + (`s3://...`, `https://...`). Current design is + relative paths only. +- [ ] 9.7 **Parked**: `sparse_matrix` block-sparse-row (BSR) + format. Current design supports COO and CSR only.