Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Source-To-Runtime Gates

A runtime-bearing milestone is not complete until the command a user would run succeeds. Documentation and generated artifacts do not replace executable source-to-runtime behavior.

The normal gate shape is:

flowchart LR
    Source[".str source"]
    Check["strata check"]
    Build["strata build"]
    Artifact[".mta artifact"]
    Run["mantle run"]
    Trace["observability trace"]

    Source --> Check --> Build --> Artifact --> Run --> Trace

For fail-closed runtime behavior, the source must check and build, and mantle run must fail only after Mantle validates the artifact and emits trace evidence for the failure. Source-level rejection gates are different: they must fail before build/lowering and must not leave a target artifact behind.

Canonical Gates

The canonical user-facing gate is:

just source-to-runtime-gates

The split entrypoints are available when only one side of the gate is needed:

just source-to-runtime-success-gates
just source-to-runtime-failure-gates

The maintained command list belongs in the executable gate definitions:

  • Justfile owns the commands a user or CI runner executes.
  • crates/strata-mantle-acceptance/tests/source_to_runtime_gates.rs is the root integration harness, with focused gate families under crates/strata-mantle-acceptance/tests/source_to_runtime_gates/.
  • docs/src/examples.md owns the curated list of runnable examples. The grouped example pages document the behavior each example demonstrates.

This page intentionally does not enumerate every runtime gate. When a new user-visible language or runtime behavior needs source-to-runtime proof, update the executable gate and document the example in the grouped example pages.

The language surface proof substrate checks that the agreed current-surface proof domains map to declared features and that those features point at the required parser, checker, lowering, boundary, artifact, runtime, diagnostics, example, test, fuzz, and bounded/property evidence classes where those classes apply. It also checks that each proof domain declares the proof obligations implied by those features. That substrate supports implementation claims; it does not replace this executable gate shape.

Representative Commands

The minimum success gate checks, builds, runs, and traces hello.str:

just run-example hello

A richer state/payload gate follows the same shape:

just run-example state_payload_match

The source-unit import gate starts at a root source file and proves that Strata, not Mantle, resolves the reachable dependency graph before lowering:

just run-example imports_main

The source contract data primitive gate proves immutable String and Bytes values survive source checking, lowering, Mantle artifact admission, runtime execution, and observability as typed primitive data rather than string dispatch:

just run-example source_contract_data_primitives

BDD scenario: Given immutable String and Bytes state/message values in a checked .str program, when Strata builds the typed .mta and Mantle runs it, then the trace and output show typed primitive data survived checking, lowering, admission, runtime branch evaluation, and process termination without source string dispatch.

The typed boundary contract gate proves protocol, port, component, and process-local PortConnect declarations check before lowering and run through Mantle-admitted typed IDs:

just run-example boundary_contracts_main

The component composition gate proves source-unit reachability plus typed component import binding before lowering, then runs the admitted artifact without runtime source-name resolution:

strata check examples/component_composition_main.str
strata build examples/component_composition_main.str
strata composition build examples/component_composition_main.str
strata composition admit target/strata/component_composition_main.component-composition.json --format json
strata composition bind-runtime \
  target/strata/component_composition_main.component-composition.json \
  target/strata/component_composition_main.mta \
  --output target/strata/component_composition_main.deployment-composition.json
mantle run target/strata/component_composition_main.mta \
  --composition-binding target/strata/component_composition_main.deployment-composition.json
strata target-requirements examples/component_composition_main.str --format json
mantle feature-declaration --format json
mantle admit target/strata/component_composition_main.mta --format json

This target-binding gate keeps the boundary explicit. Strata reports the typed runtime features required by the checked program, emits and admits the Strata-owned strata.checked_component_composition JSON artifact as checked-subset component-composition validation evidence, and then emits an explicit mantle.runtime_composition_binding deployment binding for the matching .mta. Mantle separately reports the typed features it currently supports, admits the .mta requirements before execution, and emits deployment, composition, and component-instance trace correlation only when the explicit binding is supplied. The checked composition artifact is not Mantle input; Mantle does not infer source composition, verify Strata composition safety, or dispatch from source names. Source imports, component names, authority labels, composition artifacts, deployment bindings, and report data remain diagnostics, provenance, review records, admission evidence, or observability correlation evidence; they are not runtime dispatch inputs.

The authority/effect admission-binding gate proves checked authority and exact effect facts cross the Strata/Mantle boundary as admitted typed artifacts and a matching runtime binding. The dynamic-local branch exercises effect_outcome_spawn_denied:

strata check examples/effect_outcome_spawn_denied.str
strata build examples/effect_outcome_spawn_denied.str
strata authority-effects build examples/effect_outcome_spawn_denied.str
strata authority-effects admit target/strata/effect_outcome_spawn_denied.authority-effect.json --format json
strata authority-effects policy build \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  --output target/strata/effect_outcome_spawn_denied.authority-policy.json
strata authority-effects policy admit \
  target/strata/effect_outcome_spawn_denied.authority-policy.json \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  --format json
strata authority-effects bind-runtime \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  target/strata/effect_outcome_spawn_denied.authority-policy.json \
  target/strata/effect_outcome_spawn_denied.mta \
  --output target/strata/effect_outcome_spawn_denied.authority-effect-binding.json
mantle run target/strata/effect_outcome_spawn_denied.mta \
  --authority-effect-binding target/strata/effect_outcome_spawn_denied.authority-effect-binding.json
strata authority-effects policy build \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  --deny-spawn-authority \
  --output target/strata/effect_outcome_spawn_denied.authority-deny-policy.json
strata authority-effects policy admit \
  target/strata/effect_outcome_spawn_denied.authority-deny-policy.json \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  --format json
strata authority-effects bind-runtime \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  target/strata/effect_outcome_spawn_denied.authority-deny-policy.json \
  target/strata/effect_outcome_spawn_denied.mta \
  --output target/strata/effect_outcome_spawn_denied.authority-effect-deny-binding.json
mantle run target/strata/effect_outcome_spawn_denied.mta \
  --authority-effect-binding target/strata/effect_outcome_spawn_denied.authority-effect-deny-binding.json

The same gate also exercises the lexical supervisor-child branch:

strata check examples/local_supervision_restart.str
strata build examples/local_supervision_restart.str
strata authority-effects build examples/local_supervision_restart.str
strata authority-effects admit target/strata/local_supervision_restart.authority-effect.json --format json
strata authority-effects policy build \
  target/strata/local_supervision_restart.authority-effect.json \
  --output target/strata/local_supervision_restart.authority-policy.json
strata authority-effects policy admit \
  target/strata/local_supervision_restart.authority-policy.json \
  target/strata/local_supervision_restart.authority-effect.json \
  --format json
strata authority-effects bind-runtime \
  target/strata/local_supervision_restart.authority-effect.json \
  target/strata/local_supervision_restart.authority-policy.json \
  target/strata/local_supervision_restart.mta \
  --output target/strata/local_supervision_restart.authority-effect-binding.json
mantle run target/strata/local_supervision_restart.mta \
  --authority-effect-binding target/strata/local_supervision_restart.authority-effect-binding.json

The same gate also exercises component authority surfaces with both explicit runtime sidecars supplied to Mantle:

strata check examples/component_composition_main.str
strata build examples/component_composition_main.str
strata composition build examples/component_composition_main.str
strata composition admit target/strata/component_composition_main.component-composition.json --format json
strata composition bind-runtime \
  target/strata/component_composition_main.component-composition.json \
  target/strata/component_composition_main.mta \
  --output target/strata/component_composition_main.deployment-composition.json
strata authority-effects build examples/component_composition_main.str
strata authority-effects admit target/strata/component_composition_main.authority-effect.json --format json
strata authority-effects policy build \
  target/strata/component_composition_main.authority-effect.json \
  --output target/strata/component_composition_main.authority-policy.json
strata authority-effects policy admit \
  target/strata/component_composition_main.authority-policy.json \
  target/strata/component_composition_main.authority-effect.json \
  --format json
strata authority-effects bind-runtime \
  target/strata/component_composition_main.authority-effect.json \
  target/strata/component_composition_main.authority-policy.json \
  target/strata/component_composition_main.mta \
  --output target/strata/component_composition_main.authority-effect-binding.json
mantle run target/strata/component_composition_main.mta \
  --composition-binding target/strata/component_composition_main.deployment-composition.json \
  --authority-effect-binding target/strata/component_composition_main.authority-effect-binding.json

This gate keeps the ownership split explicit. Strata emits and admits strata.checked_authority_effects facts from checked IR; Strata emits and admits the closed strata.authority_policy_decisions table over typed process authority IDs; the runtime binding then correlates those facts and decisions with a matching .mta. Mantle consumes only mantle.runtime_authority_effect_binding, only when supplied through --authority-effect-binding, and validates the binding before ArtifactLoaded or runtime side effects. Dynamic spawn and boundary port-connect decisions are enforced by typed IDs and traced with authority_policy_decision_id. Source labels, authority names, report text, and debug names remain diagnostics/provenance metadata and cannot retarget authority, policy, or effect facts.

An immutable source computation gate proves sequential source-local bindings are resolved before lowering while Mantle executes only typed artifact data:

just run-example function_local_bindings

A scalar computation gate proves typed scalar payloads, immutable process-local scalar functions, runtime scalar predicates, runtime-bound value conditionals, and Mantle execution of typed scalar templates:

just run-example runtime_scalar_priority

A selected return-match arm-prefix gate proves source-selected dispatch before Mantle executes typed runtime arm actions:

just run-example process_return_match_arm_runtime_if_prefix
just run-example process_return_match_arm_for_prefix
just run-example process_return_match_arm_for_if_prefix
just run-example process_return_match_arm_if_for_prefix

A runtime control-flow gate checks, builds, validates, runs, and traces typed Mantle execution:

just run-example runtime_guard_noop
just run-example runtime_scalar_priority
just run-example runtime_nested_if_actions
just run-example runtime_final_if_guarded_loop
just run-example runtime_final_if_nested_if_actions
just run-example runtime_final_if_nested_terminal_if
just run-example runtime_for_each
just run-example runtime_for_each_empty
just run-example runtime_for_each_if
just run-example runtime_for_each_nested_if_actions
just run-example runtime_guarded_for_each
just run-example runtime_guarded_ref_loop
just run-example runtime_guarded_ref_loop_jobs
just run-example runtime_loop_element_projection
just run-example effect_outcomes
just run-example effect_outcome_mailbox_full
just run-example effect_outcome_stopped_target
just run-example process_ref_stale_lifecycle
# Default-limit acceptance only; the exhausted/backend-unavailable branches use dedicated gates below.
just run-example effect_outcome_spawn_exhausted
just run-example effect_outcome_spawn_backend_unavailable
just run-example local_supervision_restart
just run-example local_supervision_permanent_stop
just run-example local_supervision_temporary
just run-example local_supervision_transient_restart
just run-example local_supervision_transient
just run-example local_supervision_inactive_send_outcome
just run-example local_supervision_inactive_crashed_send_outcome

just process-ref-lifecycle-gates runs process_ref_stale_lifecycle plus the trace-level assertion that a transported old runtime PID stops instead of retargeting to a newer same-definition worker.

run-example uses default runtime limits and policies. For effect_outcome_spawn_exhausted and effect_outcome_spawn_backend_unavailable, it proves the checked source still runs with available local spawn capacity/backend; the source-visible failure branches use the dedicated commands below.

The local spawn authority denial gate uses the same check/build path and then runs Mantle with a direct denial runtime limit. The authority/effect binding gate above is the product path for typed admitted spawn-authority policy:

just strata-check examples/effect_outcome_spawn_denied.str
just strata-build examples/effect_outcome_spawn_denied.str
just mantle-run-deny-spawn-authority target/strata/effect_outcome_spawn_denied.mta

The local spawn capacity exhaustion gate uses the same check/build path and then runs Mantle with a deliberately exhausted process limit:

just strata-check examples/effect_outcome_spawn_exhausted.str
just strata-build examples/effect_outcome_spawn_exhausted.str
just mantle-run-max-runtime-processes target/strata/effect_outcome_spawn_exhausted.mta 1

The local spawn backend-unavailable gate uses the same check/build path and then runs Mantle with the bounded local backend disabled before acceptance:

just strata-check examples/effect_outcome_spawn_backend_unavailable.str
just strata-build examples/effect_outcome_spawn_backend_unavailable.str
just mantle-run-disable-local-spawn-backend target/strata/effect_outcome_spawn_backend_unavailable.mta

The exhausted-spawn, backend-unavailable-spawn, stopped-target send, stale-process-ref send, and inactive-crashed-child send gates also assert effect_outcome_bound trace events. The denied-port-policy send-outcome gate instead proves fail-closed authority denial before source-visible outcome binding or delivery; runtime-unit and trace-validation coverage separately exercise closed-mailbox runtime causes. These trace events carry the numeric outcome_id, the spawn or send action kind, and the closed outcome_result category so the branch result is attributable to Mantle runtime cause rather than inferred only from output text. For stale process references, the proof combines the received payload_pid, the later stopped send outcome, and the absence of delivery to the newer runtime PID.

A source rejection gate must fail during checking and must not create a target artifact:

just strata-check examples/failures/effect_authority_missing.str
just strata-check examples/failures/source_local_binding_process_ref_carrier_enum.str
just strata-check examples/failures/scalar_overflow.str
just strata-check examples/failures/scalar_type_mismatch.str
just strata-check examples/failures/scalar_divide_by_zero.str
just strata-check examples/failures/scalar_runtime_divide_by_zero.str
just strata-check examples/failures/scalar_runtime_modulo_by_zero.str
just strata-check examples/failures/scalar_unsuffixed_literal.str

A runtime fail-closed gate checks and builds successfully, then returns non-zero from Mantle after writing trace evidence:

just run-example actor_panic_no_replay

Each successful mantle run command must validate the generated .mta, execute it, and emit an observability trace under target/strata/. Expected-failure gates must return non-zero with source diagnostics or runtime failure evidence at the layer being tested. Acceptance tests that read trace evidence validate the Mantle-owned JSONL trace schema before trusting the trace summary. That validation checks schema identity, exact per-event field sets, required fields, typed ID field shapes, grouped payload/loop fields, artifact_loaded first/no-repeat ordering, Mantle-contiguous spawned PID sequencing, u32 artifact typed-ID width, u16 branch path segments and bounded path length, non-entry spawn parent evidence, runtime PID-to-process-ID correlation, supervisor-child restart causality, and restart-window numeric bounds/coupling only; it does not make trace JSON an artifact boundary or a source semantics input.

When adding a new user-visible language or runtime behavior, add or update an example that follows this shape. A passing unit test is useful, but it does not replace a runnable source-to-runtime command when the behavior is user-facing.