04 — Built-in dimensions
Eleven dimensions every Corvid program sees without declaring. The first eight drive the core effect system; the last three came online with Phase 20h’s typed model substrate and are documented in full in § 13. Each has a physical meaning, an algebraic archetype, an identity element, a constraint form, and a counter-design that shows what would break with any other rule.
| Dimension | Archetype | Value type | Identity | Constraint | Surface |
|---|---|---|---|---|---|
cost | Sum (Cumulative) | Cost | $0.00 | @budget($N) | § 4.1 |
trust | Max (Dominant) | Name lattice | autonomous | @trust(level) | § 4.2 |
reversible | LeastReversible (Conservative) | Bool | true | @reversible | § 4.3 |
data | Union (Accumulative) | Name set | none | @data(c₁, …) | § 4.4 |
latency | Max (Dominant) | Name lattice | instant | (no direct constraint) | § 4.5 |
confidence | Min (Weakest-link) | Number ∈ [0, 1] | 1.0 | @min_confidence(C) | § 4.6 |
tokens | Sum (Cumulative) | Number | 0 | @budget(tokens=T) | § 4.7 |
latency_ms | Sum (Cumulative) | Number | 0 | @budget(latency=M) | § 4.8 |
capability | Max (Dominant) | Name lattice | basic | requires: <level> on prompts | § 13.2 |
jurisdiction | Max (Dominant) | Name lattice | none | (model-field-only) | § 13.4 |
compliance | Union (Accumulative) | Name set | none | (model-field-only) | § 13.4 |
privacy_tier | Max (Dominant) | Name lattice | standard | (model-field-only) | § 13.4 |
Each dimension’s archetype is verified against its algebraic laws on every CI run via corvid test dimensions — the harness reports all 11 dimensions satisfy their archetype’s laws on every passing build. See 02 § 3.2 for the law suite and ../../crates/corvid-types/src/law_check.rs for the implementation.
4.1 cost — Sum
Physical meaning
Money that leaves an account when the chain executes. Each provider call pays. A chain that calls three prompts at $0.01, $0.02, $0.03 spends $0.06 total.
Composition
cost(f; g) = cost(f) + cost(g)Sum under addition. Associative, commutative, identity $0.00, monotonic for non-negative values (all costs are non-negative in practice).
Constraint
# expect: skip@budget($0.50)agent lookup(query: String) -> String: ...The checker computes the worst-case path through the agent’s body (branch max, loop multiplication) and fails when that path exceeds the declared bound. Unbounded loops emit a warning, not an error — the checker is honest that it can’t prove a bound when the loop length isn’t statically known.
Runtime behavior
Live-tracked per-token during streaming. When a streaming prompt’s cumulative cost crosses @budget, the runtime raises BudgetExceeded mid-stream rather than completing the over-budget call.
Counter-design
If cost composed by Max instead of Sum, a chain of three $0.10 calls would report $0.10, letting a @budget($0.20) agent overspend by 50%. See docs/effects-spec/counterexamples/composition/sum_with_max.cor.
4.2 trust — Max
Physical meaning
Authorization posture. A chain’s trust level is the strictest gate any step encounters. Levels form a total order:
autonomous < supervisor_required < human_requiredComposition
trust(f; g) = max(trust(f), trust(g)) in the trust latticeMax over the lattice. Associative, commutative, idempotent, identity autonomous.
Constraint
# expect: skip@trust(autonomous)agent safe_path(query: String) -> String: ...An agent declared @trust(autonomous) must compose to autonomous. The checker refuses to compile an agent whose body reaches any call with a stricter trust level unless the declared level is loosened.
Confidence-gated trust
A tool may declare trust: autonomous_if_confident(0.95). The compiler treats it as autonomous statically — the agent passes @trust(autonomous) — but at runtime the interpreter checks composed input confidence and activates the approval gate if confidence has dropped below 0.95. See 06 — Confidence-gated trust for the full runtime mechanism.
Counter-design
If trust composed by Min, an agent calling one autonomous tool and one human_required tool would report autonomous — bypassing the approval gate on the human-required call. See counterexamples/composition/max_with_min.cor.
4.3 reversible — LeastReversible
Physical meaning
Whether a chain can be rolled back. Reversibility is conservative: a chain is reversible iff every step is reversible. One irreversible step — a charged credit card, a deleted table, a sent email — makes the entire chain irreversible because the undo would need to reverse the one-way step.
Composition
reversible(f; g) = reversible(f) ∧ reversible(g)Logical AND. Associative, commutative, idempotent, identity true.
Constraint
# expect: skip@reversibleagent safe_preview(id: String) -> Plan: ...Every effect in the body must declare reversible: true. A single irreversible call in the chain fails the constraint with a hint naming the offending tool.
Counter-design
If reversible composed by OR, a chain logging to disk (reversible: true) that also drops a database table (reversible: false) would report true — the compiler would let a @reversible agent silently nuke production. See counterexamples/composition/and_with_or.cor.
4.4 data — Union
Physical meaning
Data categories that flow through a chain. A chain reading financial records then medical records has touched both categories — not either alone. The Union accumulates.
Well-known categories: none, public, pii, financial, medical, grounded. Users can declare more in corvid.toml if a dimension fork covers the domain (e.g. hipaa_phi, gdpr_special_category).
Composition
data(f; g) = data(f) ∪ data(g) (set union)Union over a Name set. Associative, commutative, idempotent, identity none.
Correctness note. The composition rule parses each side as a comma-separated set and merges. An earlier implementation used substring-based dedup; that version failed associativity ("pii" ⊕ ("financial" ⊕ "pii") ≠ ("pii" ⊕ "financial") ⊕ "pii") and was caught by the archetype law-check harness. See commit 66b3075 for the fix. The regression test lives in union_data_satisfies_semilattice_laws.
Constraint
# expect: skip@data(public, grounded)agent summarize(doc: String) -> Grounded<String>: ...The composed set must be a subset of the allowed set. Touching financial when not declared fails the constraint with a hint naming the offending call chain.
Grounding special case
A data: grounded entry is the marker that powers Grounded<T> return-type verification. See 03 § 5 and 05 — Grounding and provenance.
Counter-design
If data composed by intersection, a chain touching financial then medical would report ∅ — an audit would miss both categories. See counterexamples/composition/union_with_intersection.cor.
4.5 latency — Max
Physical meaning
The perceived latency class of a chain. Category lattice:
instant < fast < normal < slow < streaming(...)Chain-level perceived latency is the slowest step’s class — users feel the slow bit, not the average.
Composition
latency(f; g) = max(latency(f), latency(g))Max over the latency lattice. Associative, commutative, idempotent, identity instant.
The streaming variant composes specially: streaming(bounded(N)) ⊕ streaming(bounded(M)) = streaming(bounded(min(N, M))) — the tightest buffer dominates. See compose_latency_dimension in effects.rs.
Constraint
No direct @latency(...) constraint ships in v0.1. Users needing millisecond bounds use @budget(latency=M) on the latency_ms helper dimension instead.
Counter-design
If latency composed by Min, a chain with one fast and one slow step would report fast — hiding the slow bottleneck from every downstream analysis.
4.6 confidence — Min
Physical meaning
Statistical confidence of the chain’s output. Weakest-link semantic: a chain of inferences is no stronger than its weakest link. If a retrieval at 0.95 feeds a summarization at 0.70, the final answer cannot be claimed at more than 0.70.
Composition
confidence(f; g) = min(confidence(f), confidence(g))Min over Number ∈ [0, 1]. Associative, commutative, idempotent, identity 1.0.
Constraint
# expect: skip@min_confidence(0.90)agent high_confidence_path(query: String) -> String: ...The composed minimum must not fall below the declared floor. If the chain calls any step whose confidence is less than 0.90, the agent fails compilation.
Runtime interaction
Confidence also gates trust via autonomous_if_confident(T) — see §4.2 above and 06 — Confidence-gated trust.
Counter-design
If confidence composed by Mean, a chain retrieving at 0.99 (100 times) and fabricating at 0.20 (once) would report 0.97 — because Mean hides the fabrication. The output depends entirely on the fabrication, so reporting 0.97 is a lie. See counterexamples/composition/min_with_mean.cor.
4.7 Helper: tokens — Sum
Physical meaning
Token count consumed at the provider. Sums across prompts in the chain. Used as a secondary bound when @budget($...) isn’t precise enough — some providers cap tokens per context window separately from cost.
Composition
tokens(f; g) = tokens(f) + tokens(g)Identical archetype to cost but typed as plain Number, not Cost. Identity 0.
Constraint
# expect: skip@budget($1.00, tokens=50000)agent planner(query: String) -> Plan: ...Multi-dimensional @budget composes both bounds independently. Either bound firing fails the constraint.
4.8 Helper: latency_ms — Sum
Physical meaning
Wall-clock milliseconds. For sequential latency bounds where the exact ms matters (SLAs, end-to-end user-perceived latency), latency_ms sums across steps. Distinct from the latency category (fast/slow) which Max-composes.
Composition
latency_ms(f; g) = latency_ms(f) + latency_ms(g)Identity 0. Unlike latency which is idempotent, latency_ms is Sum — calling a 50 ms tool twice takes 100 ms in a sequential chain.
Constraint
# expect: skip@budget($0.50, latency=2000)agent interactive_response(query: String) -> String: ...Budget bound in milliseconds, same multi-dimensional form as tokens.
Note
Parallel execution isn’t yet modeled. When v0.2 adds spawn / join constructs, latency_ms over a parallel block will use max (the slowest branch dominates) — see ROADMAP Phase 22.
4.9 Model-substrate dimensions (Phase 20h)
capability, jurisdiction, compliance, and privacy_tier shipped in Phase 20h as built-in dimensions of the typed model substrate. They compose identically to the first eight — corvid test dimensions covers all eleven on every run. Full semantics, grammar (requires: / route: / progressive: / rollout), and worked examples live in § 13:
capability— Max over thebasic < standard < expertlattice.jurisdiction— Max over user-declared regulatory tier names.compliance— Union over comma-separated compliance tag sets.privacy_tier— Max overstandard < strict < air_gapped.
§ 13.4 documents two real trust_max bugs the law-check harness caught during this slice — the commutativity tie-break and the "none" identity absorption. Both fixes shipped alongside the dimension registrations.
4.10 Attack-surface review
Each built-in survives every bypass attempt we’ve tried. The current corpus of attempted bypasses lives in counterexamples/composition/. New attacks are added to counterexamples/ as bounty-driven regressions per 12 — Verification methodology.
Current attack coverage:
- Composition-rule confusion —
sum_with_max.cor,max_with_min.cor,and_with_or.cor,union_with_intersection.cor,min_with_mean.cor— all caught by the meta-verifier atcrates/corvid-driver/src/meta_verify.rs. - Unbounded loop cost hiding — caught by
CostWarningKind::UnboundedLoop. - Statically-dead-branch cost undercounting — caught by the worst-case path analysis (the checker treats
if false: expensive()as if the branch could execute). - Union substring-dedup non-associativity — caught in development by the law-check harness itself (commit
66b3075); the original implementation ran in production-adjacent tests without triggering this bug until 20g invention #7 landed. trust_maxcommutativity tie-break +"none"identity absorption — both caught in development by the law-check harness during slice D (commitb88307a).
The Union bug story is the clearest argument for algebraic law-checking as a first-class verification technique. No amount of example tests caught that the dedup was broken across reorder; only the archetype law check, running 10,000 random cases specifically for associativity, surfaced the counter-example. The trust_max fixes are the slice-D rerun of that lesson — law-check keeps finding bugs the example suite misses.
Next
05 — Grounding and provenance — the Grounded<T> type, runtime provenance chains, and cites ctx strictly verification.