Skip to content

spec: extend orca-lang with neural and sparse capabilities #11

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
jascal wants to merge 1 commit into from
Closed

spec: extend orca-lang with neural and sparse capabilities #11

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions openspec/changes/extend-orca-lang-neural-and-sparse/.openspec.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
schema: spec-driven
created: 2026-05-17
552 changes: 552 additions & 0 deletions openspec/changes/extend-orca-lang-neural-and-sparse/design.md
View file
Open in desktop

Large diffs are not rendered by default.

112 changes: 112 additions & 0 deletions ...end-orca-lang-neural-and-sparse/examples/hybrid-transformer-sparse-head.orca.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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<i32, [batch, seq]> | |
| embedded | tensor<f32, [batch, seq, hidden]> | |
| attended | tensor<f32, [batch, seq, hidden]> | |
| pooled | tensor<f32, [batch, hidden]> | |
| features | tensor<f32, [batch, n_features]> | |

## 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<f32, [vocab, hidden]> | weight_ref<"hybrid.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "embed.weight"> | true |
| W_attn_qkv | tensor<f32, [hidden, 3, hidden]> | weight_ref<"hybrid.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "attn.qkv"> | true |
| W_attn_o | tensor<f32, [hidden, hidden]> | weight_ref<"hybrid.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "attn.o"> | true |
| W_head | sparse_matrix<f32, [hidden, n_features], CSR> | 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`.
54 changes: 54 additions & 0 deletions ...spec/changes/extend-orca-lang-neural-and-sparse/examples/sparse-sae-16f.orca.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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<f32, [16, 512]> | weight_ref<"sae-16f.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "encoder.weight"> | true |
| W_dec | sparse_matrix<f32, [16, 512], CSR> | weight_ref<"sae-16f.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "decoder.weight"> | true |
| b_enc | tensor<f32, [16]> | weight_ref<"sae-16f.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "encoder.bias"> | true |
| W_dec_baseline | sparse_matrix<f32, [16, 512], CSR> | 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<f32, [16, 512], CSR>`
> 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.
103 changes: 103 additions & 0 deletions ...ec/changes/extend-orca-lang-neural-and-sparse/examples/tiny-transformer.orca.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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<i32, [batch, seq]> | |
| embedded | tensor<f32, [batch, seq, hidden]> | |
| attended | tensor<f32, [batch, seq, hidden]> | |
| mlp_out | tensor<f32, [batch, seq, hidden]> | |
| logits | tensor<f32, [batch, seq, vocab]> | |

## 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<f32, [vocab, hidden]> | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "embed.weight"> | true |
| W_pos | tensor<f32, [seq, hidden]> | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "pos.weight"> | true |
| W_qkv | tensor<f32, [hidden, 3, hidden]> | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "h.0.attn.qkv"> | true |
| W_attn_o | tensor<f32, [hidden, hidden]> | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "h.0.attn.o"> | true |
| W_mlp_in | tensor<f32, [hidden, 4, hidden]> | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "h.0.mlp.in"> | true |
| W_mlp_out | tensor<f32, [4, hidden, hidden]> | weight_ref<"tiny-transformer.safetensors", "0000000000000000000000000000000000000000000000000000000000000000", "h.0.mlp.out"> | true |
| W_unembed | tensor<f32, [hidden, vocab]> | 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.
Loading
Loading