Appendix D. The engine profile: handler specs and fits (normative)

• The file is UTF-8 text read line by line. A line that is blank after trimming, or whose first non-space characters are # or //, is skipped.
• A top-level line starts in column 0. A body line starts with a space or a tab and belongs to the nearest preceding top-level block. A blank line ends a body.
• Tokens are separated by white space. A token that starts with " runs to the next " (no escapes); its value is the text between the quotes.
• Durations: hours are N or Nh; milliseconds are Nms, Ns (seconds) or N. N is a decimal integer.

File        = SpecLine { TopLine } .
SpecLine    = "spec" STRING VERSION .                VERSION = [ "v" ] MAJOR "." MINOR "." PATCH
TopLine     = ReasonLine | CurrencyLine | Objective | Constraint | Acceptance
            | Deliverable | Role | Dependency | Escalation | Flow | ChangeControl .
ReasonLine  = "reason" STRING [ "by" STRING ] .
CurrencyLine= "currency" { "max_age=" HOURS | "last_checked=" RFC3339
            | "toolchain." NAME "=" VALUE | "dep." NAME "=" VALUE } .
Objective   = "objective" ID STRING Body( "metric" NAME "target" VALUE | ReasonLine ) .
Constraint  = "constraint" ID ( "substrate" | "performance" | "regulatory"
            | "resource" | "compatibility" ) STRING Body( ReasonLine ) .
Acceptance  = "acceptance" ID "validates" ID
              Body( "property" STRING | "error_budget" NUMBER | ReasonLine ) .
Deliverable = "deliverable" ID "fulfills" ID
              Body( "schema" STRING | "description" STRING | "blast_radius" NAME | ReasonLine ) .
Role        = "role" ID STRING ( "execution_node" | "coordinator" | "ai_foreman"
            | "order_giver" ) Body( "blast_radius" NAME | ReasonLine ) .
Dependency  = "dependency" ID ( "node" | "crate" | "service" | "data" ) STRING
              Body( "input_schema" JSON | ReasonLine ) .
Escalation  = "escalation" ID { "from" ENDPOINT | "to" ENDPOINT | "timeout" MS }
              Body( ReasonLine ) .
Flow        = "flow" ID "from" ENDPOINT "to" ENDPOINT Body( ReasonLine ) .
ChangeControl = "change_control" { "approvers" LIST | "review_period" HOURS | "frozen" } .

Body(X) is zero or more body lines each of the form X. error_budget must lie strictly between 0 and 1. input_schema is JSON that may span body lines until its brackets balance. An unknown top-level keyword, an unknown constraint, role or dependency kind, a flow without from and to, a missing spec line, an error_budget out of range, a last_checked that is not RFC 3339 and invalid input_schema JSON are refused at parse time. The reference parser ignores unknown body keywords and unknown change_control words, and reads an unparsable duration as its default (24 h, 30 000 ms).

• spec NAME VERSION: the name and version of the spec. The version is recorded in the compiled graph's metadata (spec_version) and in the Form IR (FormIr.version). The version is not yet checked.
• reason WHY by AUTHOR: why an artifact exists. A top-level reason belongs to the spec; a body reason belongs to its block. A reason is recorded on the node or edge it explains and enters the log with every mutation that creates it. Reasons are data: they never change δ.
• currency: when the spec's toolchain and dependencies were last verified (last_checked), the versions seen then, and the maximum age max_age in hours. Parsing is not a check: without last_checked the record is unchecked. rce currency FILE --mark records a check by writing last_checked back into the file. A record is stale when it was never checked or is older than max_age; the promotion gate records a stale spec, and blocks on it when the engine's enforce_currency policy is on (off by default).
• objective, constraint, acceptance: requirements. Acceptance properties and their error budget feed the promotion gate; they do not change δ.
• deliverable D compiles to the node del_D (an executor and a sink), role R to role_R (kind executor, decision, escalation or source), dependency P to dep_P (a source). flow F from A to B compiles to the edge flow_F; escalation E from A to B timeout t to esc_E. An endpoint names a node id, a node name or a declared id; an unknown flow endpoint is refused by the compiler, an unknown escalation endpoint is a diagnostic.
• change_control: who may approve changes to the spec, the minimum review period, and whether the spec is frozen. These bind the engine's promotion path (spec mutations are logged and need an approver); they do not change δ.

A fit is a JSON object:

{ "handlers": { NODE: HandlerSpec | {"kind": "term", "term": TERM}
                       | {"kind": "recorded", "contract": C, "table": {SHA256: RESULT}} },
  "types":    { SOURCE_NODE: TYPE },
  "keys":     { SINK_NODE: [COLUMN, ...] },
  "reads":    { SINK_NODE: {"key": [FIELD, ...], "into": FIELD} },
  "joins":    { SINK_NODE: [ {"relation": REL, "key": [FIELD, ...], "into": FIELD,
                              "scan": BOOL}, ... ] } }

An object with any of the five fields above is a full fit, even when it holds only reads or joins; any other object is a bare map of handlers and is read as handlers alone. NODE is a compiled node id (role_R1, dep_DEP1, del_D1). types gives the input contract of a source; keys the key of a sink's relation (default: the input number seq and the index n within the step). A recorded entry is an oracle: a recorded input replays its result and an unseen one escalates as "oracle miss".

Each is applied before the body of every rule that writes the sink, to the state at the event's entry (pre-state, as in 6.4), in this order: the read, then the joins in list order.

• reads[S] = {key, into}: the row of S's own relation whose key is the payload fields key (in key-column order) is put into the input as field into, or null when there is none. The relation must exist and its key must have as many columns as key names.
• joins[S], an entry without scan: the row of relation relation keyed by the payload fields key, or null, into field into. The relation must exist and its key arity must match.
• an entry with "scan": true: every row of relation as an array, in canonical key order (code point order of the canonical JSON key); key is ignored.
• A payload that is not a record is passed unchanged. Joined rows and scans are typed as JSON. Each read or join is covered by the rule's SHA-256 id, and a rule with a read or a join is not monotone (CALM, form/laws.rs). A joins entry for a sink no rule writes is refused.
• Every target (reference δ, Rust, Python, JavaScript for XState and SCXML) applies them identically.

CALM tags (normative). Each rule's monotone tag is derived by form::laws::calm_reason, never declared, and laws::check refuses an IR whose tag differs. A rule is monotone only when it has no resolve, no read, no join and no scan. The reasons, by derivation:

The tag is conservative (sound, not complete): a join against an insert-only relation would be monotone in principle, but the profile does not prove insert-only, so it is not claimed. A Form is coordination-free (laws::coordination_free) iff every rule is monotone. Because every read, join and scan sees the entry state, the post-state of an input event does not depend on the order in which rules for different sinks run; only the output order does, and that is fixed by content hash (law 2). Tested in tests/form_joins.rs.

Σc has one region per node, Ready | Escalated. Σd has the logical clock, an input count and the typed relations of the sinks plus escalation and error. E is IN_<source>, TICK and RESOLVE_<node>. An input event normalizes the payload (6.3 N1), checks the source's contract (a mismatch is a reject output and an error row, not a refusal of the event) and runs the rules in content-hash order. A timeout is converted to ticks of a nominal 100 ms, rounded up; the clock is logical (6.3 N11). D is the canonical log of 6.1: entries {seq, event, prev_hash, state_hash, hash} chained by SHA-256. Every event is applied (no outcome field is needed), since a contract mismatch is an output, not a refusal. The numeric edges are those of 6.3, with one recorded difference: in this profile an integer above i64::MAX is "integer out of range" (D.10).

A handler spec and a module of sections 2 to 10 both denote a Form, but the profile has no expressions of its own: node behaviour comes only from fits. A fit term is a term of the Form IR (form/ir.rs), not an RCE expression. How an RCE module is used as a fit is not yet defined (9, open questions).

A brownfield lift (rce scan DIR --form, brownfield/lift.rs) reads existing Rust, Python, TypeScript or Go into a Form schema. Its guarantees are exactly these, each enforced by code and tests, and no other is claimed:

• L1 Labeled: every relation, region, event and transition carries a label that starts with "unproven"; a lifted element is never presented as checked.
• L2 Fail closed: a guard the lift cannot read is opaque, and Lifted::step refuses to step through it rather than guess.
• L3 Generated code agrees with the lift: code emitted from a lifted machine (--emit-machine) steps as Lifted::step (tested, tests/lift_emit.rs).
• L4 Evidence, not proof: agreement of the lift with the original program is tested on seeded runs of the original (tests/brownfield_lift.rs); its level is tested (8). A lift is an input to a gate, never an authority: what it proposes is admitted only through the checker and the gate, like any other proposal.

These are checked by crate::spec::rules (src/spec/rules.rs), run by rce check, and each diagnostic names its rule.

• W-HS-VER-1: the spec version is not MAJOR.MINOR.PATCH of decimal integers (an optional leading v is allowed).
• W-HS-VER-2 (compatibility, between an old and a new revision of one spec, rce diff): the version must not decrease; a revision that removes or modifies a declaration must increase MAJOR, or MINOR when MAJOR is 0; a revision that only adds declarations must increase at least MINOR; a revision with no change may keep the version. Flows are declarations here: a flow whose endpoints change is modified.
• W-HS-CUR-1: a max_age that is not a positive integer number of hours (N or Nh, N ≥ 1).
• W-HS-CUR-2 (staleness): at check time now, the currency record is stale when it was never checked or now - last_checked exceeds max_age hours. A stale spec is refused by rce check --strict and by the promotion gate when the engine's enforce_currency policy is on; otherwise it is reported as a warning naming W-HS-CUR-2.
• W-HS-REASON-1: the spec, or a declaration that compiles to a node or an edge (deliverable, role, dependency, flow, escalation), has no reason line, or a reason whose text is empty or unspecified.
• W-HS-DUR-1: a duration that is not a decimal integer with an allowed suffix (D.1).
• W-HS-KW-1: an unknown body keyword or change_control word.

• Integers in [2^63, 2^64) are u64 values, as in the language (6.3 N2): the u64 operators compute on them exactly, comparisons, sort, lmin, lmax, min and max order them exactly, and the f64 and f32 operators convert them to f64. The signed operators refuse them ("integer out of range"), which no well-typed program reaches, since a signed value is never at or above 2^63. A JSON integer beyond u64 is read as a float (form::num); no integer type of the language holds one.
• The cost model of extraction (est_j) and the gate's certificate are outside this appendix, except the break-even receipt of D.11.

Each promotion record (promoted or refused) carries a break-even receipt break_even with three terms and n* = J_build / (J_model_path - J_handler), the number of inputs after which the promoted handler has paid back its build:

• J_build: the est_j of the gear resolution that wrote the handler plus the coverage shadow run of the promotion path. Static checks (proof, kernel) are not priced and not included, so J_build and n* are lower bounds.
• J_model_path: joules per input on the model path, the est_j of one gear resolution (the price the retirement rule uses for savings).
• J_handler: joules per input of the handler, the shadow run's priced operations per sample plus one dispatch.

Each term is {j, basis} with basis one of est (a model of the work, including a model provider's own figure), reported (an OS or on-chip energy counter: RAPL, NVML, IOReport), measured (a wall or shunt meter on a named rail) or unpriced (no figure; j is null, never 0). The terms the engine fills today are est or unpriced: a gear receipt's est_j is an estimate by schema and is never relabeled from its free text. A figure without a basis is refused when a record is read, and the type that holds a term has no constructor from a bare number. n_star is {kind: unpriced} when any term is unpriced (it is never computed from the other terms or from a default), {kind: never} when J_model_path - J_handler <= 0, and otherwise {kind: value, n, inputs = ⌈n⌉}; its basis is the weakest of the three (unpriced < est < reported < measured). The promotion path's last step records the same figures as text. Implemented in src/runtime/break_even.rs, tested there and in the engine's promotion tests.

Readings: provenance, boundary and amortization (normative; P4, P5, P6 of the receipt field proposals of 13 Oct 2026). These rules apply to every term labeled reported or measured, in every receipt that holds one, and are checked where a term is built and where a record is read:

1. A reading carries provenance = {sampler, counter, interval_s, idle_baseline_w, machine, boundary}: the four names non-empty, interval_s finite and > 0, idle_baseline_w finite and >= 0 (0 when no baseline was subtracted). boundary says what the joules include (package, package+dram, rail:VDD_GPU). A reading without a valid provenance is refused; unknown fields in it are refused. Derivation: the label reported or measured claims that something was read; a reading that cannot be reproduced or compared (which counter, over what interval, against which baseline, on which machine, inside which boundary) does not support that claim, so a term that lacks it is not a reading, and labeling it one would be unsound.
2. A term labeled est or unpriced carries no provenance (nothing was read); one that does is refused.
3. A reading carries amortization, one of {kind: per_call}, {kind: batch_mean, n >= 1}, {kind: per_solved_task}. An est term may carry one; the engine's own estimates omit it.
4. Figures of different kinds are never added or subtracted: a sum of two terms whose amortization differs (absent counts as its own kind) is refused, and so is a break-even whose J_model_path and J_handler differ in kind (n* divides by their difference) or whose J_build is a mean (batch_mean or per_solved_task; J_build is a one-off total). Derivation: a batch mean added to a per-call figure, or a per-task figure subtracted from a per-input one, is arithmetic on different units; no result of it is a figure of either kind.
5. A sum of two readings keeps the weaker label only when both come from the same sampler, counter, machine and boundary (the intervals add); otherwise it is refused. A sum with an est term is est with no provenance (unpriced < est < reported < measured, as for n*).
6. A stored break-even receipt is re-derived from its terms when read; a stored n* that disagrees with them is refused.

The est wire form is unchanged ({"j": 2.5, "basis": "est"}), so no stored receipt changes meaning; no receipt in the repository holds a reading today. Implemented by Term, Provenance and Amortization in src/runtime/break_even.rs (no constructor makes a reading without provenance and amortization), tested there (p4_*, p6_*).

The receipt is a measurement record. It is not an input to δ, to any check, or to the decision to promote, so it does not change the meaning of any program or handler spec in any language version (C.15: receipts are version-independent).