Invariants

The AutonomyOps ADK enforces thirteen architectural invariants (INV-01–INV-13). Violating any invariant is a build-breaking failure. CI guardrails and failure injection tests detect violations automatically. No invariant may be relaxed without a signed-off Architecture Decision Record (ADR).

For the machine-readable traceability table (invariant → code module → CI guardrail → FI test), see Traceability → Invariant Map.

Summary Table

Inv

Name

Enforcement Layer

FI Coverage

INV-01

No Shared State

Startup path check + edge/ci/scan_prohibited

scan-only

INV-02

No Convergence Tracking

edge/ci/scan_prohibited (prohibited symbols)

scan-only

INV-03

No Leader Election

edge/ci/scan_prohibited + code review

scan-only

INV-04

Disk Ceiling

edge/storage/localstore.go, eviction, statfs

FI-C1-01, FI-C2-01, FI-C2-02

INV-05

Platform Assurance Binding

edge/assurance/assurance.go, cgroup v2 probe

FI-C1-05

INV-06

Local-Only Activation

Scheduler local-only params; code review

structural

INV-07

Bounded Memory

cgroup v2 + pool-bounded transport buffers

via INV-05 FI

INV-08

Idempotent Segment Receive

Segment ID dedup in local index

unit tests

INV-09

Authorization Boundary

mTLS + CRL in transport layer

FI-C3-02

INV-10

Mission-Layer Decoupling

edge/ci/scan_dependencies (import graph)

FI-C1-03

INV-11

Deterministic Relay

Lexicographic comparator, no PRNG in relay path

structural

INV-12

Bounded Retry

edge/retry/retry.go monotonic counter

FI-C4-01, FI-C4-02, FI-C4-03

INV-13

Bounded Per-Peer Ingest Quota

edge/quota/localquota.go token bucket

FI-C3-03

INV-01 — No Shared State

Statement: All persistent segment storage, peer metadata, and decision logs are local-root-only. No NFS, CIFS, cluster filesystem, distributed store, or shared-memory IPC mechanism is permitted.

Rationale: Shared state introduces coordination dependencies that violate the local-only decision authority model and create liveness hazards under network partition.

Code modules: edge/storage/localstore.go (local-root path check), edge/config/startup.go (startup abort on out-of-root path)

Enforcement:

  • Startup: path resolved against $EDGE_LOCAL_ROOT; out-of-root path → abort (exit code 2)

  • edge/ci/scan_prohibited — rejects NFS/CIFS/cluster-FS volume types in manifests and image layers

INV-02 — No Convergence Tracking

Statement: No convergence protocol, vector clock, CRDT, gossip, or anti-entropy mechanism may exist in any edge/ package.

Rationale: Convergence requires shared coordination state, which violates INV-01 and introduces undefined behaviour under network partition. The edge capability is designed for deterministic relay, not eventual consistency.

Enforcement:

  • edge/ci/scan_prohibited — prohibited symbols: raft, paxos, gossip_convergence, vector_clock, crdt, anti_entropy, and related patterns

INV-03 — No Leader Election

Statement: No node may be designated a leader, primary, or coordinator. All nodes are peers with identical role and authority.

Rationale: Leader election is a form of convergence coordination. It also creates a single point of failure incompatible with the autonomous node model.

Enforcement:

  • edge/ci/scan_prohibited — prohibited election/nomination patterns

  • Code-review checklist sign-off required for any change touching peer selection

INV-04 — Disk Ceiling

Statement: Disk usage never exceeds storage.disk_ceiling_bytes after any Write+fsync returns successfully. The runtime pre-evicts before the ceiling is reached. If pre-eviction cannot free sufficient space, writes are rejected with ErrCeilingExceeded.

Code modules: edge/storage/localstore.go (ceiling check, WithDiskUsedFunc), edge/eviction/local.go, edge/storage/recovery.go

Enforcement:

  • After every Write+fsync: kernel statfs check

  • Synchronous eviction triggered when usage approaches the configured threshold

  • ErrCeilingExceeded returned if post-eviction space is still insufficient

FI Tests:

  • FI-C1-01 TestFI_DiskCeiling_ErrCeilingExceeded

  • FI-C2-01 TestFI_DiskCeiling_ConcurrentWritesAtBoundary

  • FI-C2-02 TestFI_DiskCeiling_EvictionFailure_WriteRejectedCleanly

See also: Disk Ceiling

INV-05 — Platform Assurance Binding

Statement: High-durability mode requires a validated cgroup v2 memory + CPU controller. If the platform cannot provide cgroup v2 assurance at startup, the node logs a warning (edge.assurance.reduced) and refuses to enter high-durability mode.

Code modules: edge/assurance/assurance.go, edge/config/cgroup_linux.go, edge/config/cgroup_other.go

Enforcement:

  • Startup: cgroup v2 probe; absent → LogAssuranceReduced() + edge.assurance.reduced log; high-durability operations refused

FI Tests:

  • FI-C1-05 TestFI_Assurance_HighDurabilityUnavailable

  • TestFI_Assurance_ReducedEnvelopeLogged

See also: cgroup v2

INV-06 — Local-Only Activation

Statement: Activation functions accept only local-state parameters. No remote identifiers, fleet-wide tokens, external coordination primitives, or peer-sourced inputs may appear in activation function signatures.

Code modules: edge/scheduler/local.go, edge/scheduler/scheduler.go

Enforcement: Code review checklist; edge/ci/scan_prohibited (remote-state call patterns)

INV-07 — Bounded Memory

Statement: Memory usage is bounded by the configured resource envelope. cgroup v2 enforces this at the OS level when available. Transport layer transfer buffers are pool-bounded and never grow without bound as peer count scales.

Code modules: edge/storage/localstore.go, edge/transport/transport.go (pool-bounded buffers), edge/quota/localquota.go

Enforcement:

  • cgroup v2 memory controller (when present, via INV-05)

  • Load shedding on inbound when approaching memory ceiling

INV-08 — Idempotent Segment Receive

Statement: Receiving the same segment ID multiple times is safe and has no net effect after the first receive. Deduplication is handled locally; no peer coordination is required.

Code modules: edge/index/localindex.go, edge/storage/localstore.go

Enforcement:

  • Segment ID checked against local index before write

  • Duplicate segment → silently discarded; no error returned to peer

Tests: edge/storage/store_test.go, edge/index/localindex_test.go (unit)

INV-09 — Authorization Boundary

Statement: Segment exchange requires a mutually authenticated TLS connection (mTLS). No segment data is transmitted on unauthenticated or partially-authenticated connections. CRL/OCSP is checked locally for every connection.

Code modules: edge/transport/tcptls.go (mTLS), edge/transport/crl.go (CRL), edge/transport/conn.go

Enforcement:

  • mTLS handshake required and completed before any segment exchange begins

  • Revoked cert → ErrCertRevoked + connection closed immediately

FI Tests:

  • FI-C3-02 TestFI_Transport_RevokedCert_Rejected

  • TestFI_Transport_ValidCert_Passes

  • TestFI_Transport_ExpiredCert_Rejected

See also: Security → mTLS

INV-10 — Mission-Layer Decoupling

Statement: The edge/ module must not import adk/runtime, adk/policy, adk/orchestrator, or any mission-layer package. The edge capability operates independently of whatever agent framework (LangChain, custom, etc.) is running alongside it.

Code modules: edge/ (import isolation enforced at compile time)

Enforcement:

  • edge/ci/scan_dependencies — import-graph check runs on every PR; fails if prohibited imports found

  • Compile-time isolation (build will fail if imports are added)

FI Tests:

  • FI-C1-03 TestFI_MissionDecoupled_NoMissionImport

  • FI-C1-03 TestFI_MissionProcessKill_RelayUnaffected

  • Shell: FI-C1-03_mission_kill.sh

INV-11 — Deterministic Relay

Statement: Relay order and peer selection are fully deterministic for a given local state. No PRNG, wall-clock tie-breaking, or randomized selection is used in the relay path.

Code modules: edge/scheduler/local.go (lexicographic tie-breaking), edge/segment/segment.go

Enforcement:

  • edge/ci/scan_prohibited — PRNG/random call patterns flagged in relay code paths

  • Structural: no PRNG import in relay path

INV-12 — Bounded Retry

Statement: Each segment-relay attempt increments a monotonic counter associated with that segment. When MaxRetryCount is reached, the segment enters the EXHAUSTED terminal state and is never retried again. The counter does not reset on reconnect, timer expiry, or daemon restart (it is persisted in the local index).

Code modules: edge/retry/retry.go (Tracker, RetryExhausted terminal state)

Enforcement:

  • RecordAttempt() monotonically increments; no reset path

  • Terminal EXHAUSTED on reaching MaxRetryCount; subsequent calls return ErrRetryExhausted

FI Tests:

  • FI-C4-01 TestFI_RetryExhaustion_TerminalState

  • FI-C4-02 TestFI_RetryCount_Monotonic

  • FI-C4-03 TestFI_RetryExhausted_NoBeyondWindow

  • Shell: FI-C4-01_retry_exhaustion.sh

See also: Retries

INV-13 — Bounded Per-Peer Ingest Quota

Statement: Ingest from each peer is bounded by a rolling-window token bucket. When the per-peer quota is exceeded, ErrQuotaExceeded is returned and logged as edge.quota.exceeded. The peer session remains open; quota exhaustion is not a disconnection event.

Code modules: edge/quota/localquota.go (LocalEnforcer, rolling-window token bucket)

Enforcement:

  • Per-peer bucket checked on every ingest call

  • edge.quota.exceeded log entry on breach

FI Tests:

  • FI-C3-03 TestFI_Quota_EnforcedPerPeer

  • TestFI_Quota_PeerIsolation

Do Not Do

  • ❌ Do NOT add a convergence/gossip/CRDT import to any edge/ package — edge/ci/scan_prohibited catches this in CI

  • ❌ Do NOT designate any node as a leader, primary, or coordinator for any purpose

  • ❌ Do NOT reset a retry counter on reconnect or timeout — INV-12 requires monotonic persistence

  • ❌ Do NOT allow segment exchange before mTLS handshake completes — INV-09

  • ❌ Do NOT import adk/runtime, adk/policy, or adk/orchestrator from edge/ — INV-10

  • ❌ Do NOT use PRNG or wall-clock tie-breaking in the relay scheduler path — INV-11

ContractRefine Invariants (INV-CR-*)

The ContractRefine layer (Architecture) introduces a semantic preflight stage above the existing mechanical enforcement stack. The invariants below pin the safety + security properties operators rely on when a pre-execution contract verdict influences runtime behavior. They are scoped to the runtime/contract/ package and the /v1/preflight endpoint; they neither alter nor relax INV-01..INV-13.

The numbering range INV-CR-* is deliberately disjoint from INV-* so that traceability tools can filter either family independently.

INV-CR-1 — Preflight is opt-in by policy bundle

Statement: ContractRefine enforcement is advisory by default. A preflight verdict only blocks /v1/tool execution when (a) the active policy bundle’s manifest declares requires_preflight: true for the requested capability AND (b) the runtime config contract_refine.mode is enforce. Existing policy bundles that do not declare the flag are loaded unchanged and behave exactly as they did pre-#1020: the absent field is treated as requires_preflight: false, so no capability owned by the bundle requires a preflight header.

Rationale: Backward compatibility for existing bundles is load-bearing — operators must be able to upgrade the runtime without republishing every bundle. The mode ladder (disabled → advisory → enforce) mirrors the existing attestation.mode ladder operators are already familiar with.

Code modules: runtime/contract/ (verifier wiring), runtime/server.go (mode ladder), policy/ (bundle manifest field).

Enforcement:

  • Bundle loader treats the absent requires_preflight field as false. The loader MUST NOT reject a bundle for the field’s absence under any mode — including enforce — because doing so would break the upgrade-runtime-without-republishing-bundles backward-compatibility contract above

  • Mode ladder check at /v1/preflight entry: disabled ⇒ 503

  • Mode ladder check at /v1/tool entry: deny-on-missing-header is gated on mode == enforce AND bundle.manifest.requires_preflight == true for the requested capability. In advisory mode the header is consumed for WAL correlation but does not gate execution (see INV-CR-3 for the binding-check ladder)

  • Default (post-C12 #1032): the zero-value ContractRefineMode resolves to advisory via effectiveContractRefineMode (see runtime/server_preflight.go). Operators who want the pre-C12 silent posture set runtime.contract_refine.mode: disabled explicitly — the value is preserved when set, only the unset/zero case changed. The flip preserves backward compatibility for existing bundles + clients (header optional; requires_preflight absent ⇒ false); only the runtime’s “no opinion” behavior changed from 503 to “evaluate + log without enforcing”

INV-CR-2 — Verifier is fail-closed

Statement: A verifier that is unavailable, a resolver that returns an error, an unknown contract kind in the policy bundle, or a malformed PreflightRequest MUST resolve to outcome: deny with a reason in the contract: layer. A verdict of pass MUST NEVER be returned on any error path.

Rationale: Mirrors the existing fail-closed discipline at /v1/tool. Operators must be able to reason about the worst-case behavior of the preflight layer: a broken or misconfigured verifier blocks execution; it never silently approves it.

Code modules: runtime/contract/verifier.go, runtime/contract/resolvers.go, runtime/server.go (handlePreflight error path).

Enforcement:

  • Table-driven test in runtime/contract/verifier_test.go covers each error path and asserts outcome == "deny"

  • runtime/reasons_shape_test.go extended with the contract: layer including the verifier_unavailable, resolver_error, and introspector_error subreasons

INV-CR-3 — Preflight id is single-purpose and bounded

Statement: A preflight_id binds to exactly one (capability, normalized_params_hash) tuple and one expiry timestamp. It is not a generic capability token, not transferrable across capability kinds, and not extensible after issuance. The runtime’s response to a binding mismatch is mode-gated: enforce mode denies; advisory mode records the mismatch on the WAL and lets execution proceed.

Rationale: Prevents the preflight verdict from becoming an operator-side bypass token (a pass for one tool call must not be replayable to authorize a different one), while leaving operators a safe rollout posture in advisory where the binding signal can be observed in production traffic before being enforced.

Code modules: runtime/contract/binding.go (preflight-id issuance + binding check), runtime/server.go (handleTool binding verification + mode-gated enforcement).

Enforcement:

  • Binding check runs on every /v1/tool call that presents the X-Autonomy-Preflight-Id header, in every mode (disabled excepted — see below). The check evaluates capability match + normalized-params-hash match + not-expired

  • enforce mode: a binding mismatch ⇒ deny with contract: preflight_binding_mismatch. This is the GA posture.

  • advisory mode: a binding failure emits a full autonomy.decision WAL frame with outcome=deny and reason=contract: preflight_* under the same audit_id the /v1/tool request will use, but the request CONTINUES to the policy layer with Action.Preflight=nil (no wire-level 403). The operator opts into this posture to observe the deny signal in production traffic before flipping to enforce.

  • disabled mode: the header is ignored entirely (/v1/preflight returns 503; no preflight_id can have been issued)

  • Expiry-window default ≤ a small constant (workplan §6 specifies the exact bound). Expiry past the window is treated identically to mismatch by the rules above

INV-CR-4 — Reason shape conformance

Statement: Every reason string produced by the ContractRefine layer matches the canonical <layer>: <subreason> regex enforced by runtime/reasons_shape_test.go. The layer prefix is always contract. Subreasons are lowercase ASCII; underscores are permitted after the first character.

Rationale: ADK observability and audit tooling parses reason strings across all layers under one regex. A new layer that violates the contract corrupts every downstream consumer.

Code modules: runtime/contract/reasons.go, runtime/reasons_shape_test.go.

Enforcement:

  • Unit test asserts every subreason in the contract: allow-list matches the regex

  • The allow-list is the single source of truth; runtime code may not emit a subreason that is absent from it

INV-CR-5 — Determinism

Statement: Same PreflightRequest bytes + same resolver outputs + same policy bundle ⇒ same PreflightDecision bytes, modulo the freshly generated preflight_id and audit_id (both of which are explicitly excluded from the determinism check).

Rationale: Operators must be able to reproduce a preflight verdict offline from the WAL record. Non-determinism in the verifier breaks audit reproducibility and lets unrelated state (wall-clock, randomness, external services) leak into the governance verdict.

Code modules: runtime/contract/verifier.go (the exported contract.DefaultVerifier), runtime/contract/types.go, runtime/contract/repair.go.

Enforcement:

  • Determinism test in runtime/contract/verifier_test.go runs the verifier twice on identical inputs and asserts byte-identical decisions (after id elision)

  • The verifier MUST NOT read wall-clock except via an injected clock the test can pin; MUST NOT call math/rand or crypto/rand outside id generation

INV-CR-6 — Refinement is bounded

Statement: At most one repair attempt per preflight session is allowed by default. The bound is configurable up to a small constant ≤ 3. Beyond that, the verifier returns outcome: deny with reason contract: repair_exhausted. No unbounded refinement loop is permitted.

Rationale: ContractRefine is not a planner and not a model-in-loop. Repair hints exist to let a deterministic caller correct a structurally invalid plan once; they do not exist to drive an open-ended search.

Code modules: runtime/contract/session.go, runtime/contract/verifier.go.

Enforcement:

  • Session counter incremented on each repair_required outcome

  • Counter ≥ bound ⇒ next call resolves to deny

  • Unit test pins the counter ladder

INV-CR-7 — No model-in-loop

Statement: The ContractRefine verifier MUST NOT call an LLM, an external network service, a non-deterministic library, or any resolver whose output is not a pure read-through of existing ADK substrate (attestation snapshot, rollback registry, policy bundle, lock fingerprint).

Rationale: Governance verdicts that depend on a model are not deterministic, not auditable offline, and not stable under model upgrades. ContractRefine sells a deterministic verifier as the differentiator vs prompt-engineering “guardrails”.

Code modules: runtime/contract/ (entire package).

Enforcement:

  • Static check (CI grep) for net/http.Client.Do, openai., langchain imports inside runtime/contract/

  • Import-graph review on every PR touching the package

INV-CR-8 — Correlation discipline

Statement: Every autonomy.preflight WAL event carries lock_fingerprint, policy_ref, preflight_id, and audit_id attributes. The same audit_id MUST appear on the matching autonomy.decision WAL event when the preflight is consumed at /v1/tool.

Rationale: Forward traceability — intent stated → preflight verdict → tool decision — is one of the GTM claims ContractRefine ships. The join is unverifiable if either side drops the correlation key.

Code modules: telemetry/emitter.go (new EventKind constant — this is where the enum lives), telemetry/events.go (per-kind builder helper), runtime/server.go (handlePreflight emit, handleTool join).

Enforcement:

  • Telemetry test asserts attribute presence on both event kinds

  • Join test: emit a preflight, consume at /v1/tool, query the WAL for events with the shared audit_id, assert both event kinds are returned

INV-CR-9 — No bypass of mechanical layers

Statement: A preflight verdict of pass MUST NOT bypass policy evaluation, attestation, allowlist, or egress-DLP at /v1/tool. ContractRefine is additive. A pass preflight permits the caller to attempt the tool call; it does not pre-approve the call.

Rationale: Operators rely on layered defense. A preflight verdict is a semantic statement about the plan; mechanical layers enforce identity, shape, and resource constraints independently. The two must stack, not substitute.

Code modules: runtime/server.go (handleTool ordering), runtime/contract/ (no enforcement-bypass code path exposed).

Enforcement:

  • Integration test wires a verifier that always returns pass AND a policy that always denies, asserts the call denies

  • Unit test pins the ordering of pipeline stages in handleTool

Multi-Modal Policy invariants (target — epic #747)

Note

Status — target invariants for the Phase 1 substrate INV-MM-1 through INV-MM-7 below are TARGET invariants for the multi-modal policy authoring substrate. The substrate they constrain — the policy/ir/ package, policy_frontend fields on the inner + outer manifests, widened runtime.Decision, the --with-explainability CLI flag — does not exist in the repository yet. Each Enforcement section names the planned test or CI gate that will pin the invariant once the substrate lands; today none of those tests or gates exist.

Each invariant carries a **Status:** line at the top of its Enforcement section naming the child PR that lands it. The pattern matches how INV-CR-1 .. INV-CR-9 were specified during the #1020 epic — written into the architecture doc first so subsequent PRs have a single design contract to implement against. As the substrate lands, this banner will narrow to “INV-MM-N is enforced; INV-MM-M is still planned” until all seven are live.

INV-MM-1 — Ternary outcome preservation

Statement: Phase 1 of the multi-modal policy epic ships no new runtime.Outcome enum values. Allow, Deny, and Defer remain the closed set. A pure-Rego policy that never references the Phase 2 outcomes (audit_only, require_approval, rate_limited, sandboxed) continues to produce Allow/Deny/Defer exactly as it does today, with byte-identical WAL events except for the optional explainability fields listed in INV-MM-6.

Rationale: Operators upgrading across the Phase 1 cut must see no behavioral change in their existing Rego bundles. The Phase 2 outcome additions ride a separate epic with its own backward-compat gate (manifest schema v1.4); shipping them mixed in with Phase 1 would muddle the upgrade story.

Code modules: runtime/decision.go (Outcome enum), policy/evaluator.go (Rego → Outcome mapping).

Enforcement:

  • Status: existing policy/evaluator_test.go suite already covers Allow / Deny / undefined → Deny / non-bool → Deny / eval-error → Deny fail-closed semantics today. The “ternary outcome preservation” half of this invariant is therefore enforced today by definition — no new test required for C01–C07. The “no new Outcome values in Phase 1” half is enforced by the fact that no child PR on this epic touches runtime/decision.go’s Outcome enum.

  • Planned (Phase 2): an assertion in runtime/decision_test.go that the Outcome enum has exactly 3 values, so the Phase 2 PR that adds audit_only etc. must update the assertion (and the manifest version bump) in lockstep.

INV-MM-2 — Evaluator is fail-closed

Statement: The existing policy/evaluator.go fail-closed contract is preserved verbatim: undefined results, non-bool values, and evaluation errors all resolve to Deny. Only data.autonomy.allow == true produces Allow. The IR → Rego backend MUST emit Rego that the unchanged evaluator gates correctly on this contract.

Rationale: Production governance depends on the operator’s ability to reason about worst-case behavior: a broken IR program, a corrupted Rego module, or an evaluator error MUST NOT silently approve calls.

Code modules: policy/evaluator.go (evaluator unchanged), policy/ir/compiler (Rego backend MUST emit fail-closed shape; lands in C03).

Enforcement:

  • Status: the evaluator-side half is enforced today — existing fail-closed tests in policy/evaluator_test.go cover undefined / non-bool / eval-error → Deny. Every child PR on this epic MUST run these unchanged.

  • Planned (C03): a new test in policy/ir/compiler_test.go compiles a corrupted IR program and asserts the generated Rego still gates fail-closed (i.e. data.autonomy.allow remains false or undefined). Does not exist today.

INV-MM-3 — Runtime is sole authority

Statement: All policy decisions flow through runtime.Interceptor.Allow. Adapters MUST NOT short-circuit on the frontend used to author the policy bundle, MUST NOT cache decisions indexed by frontend, and MUST NOT inspect BundleManifest.policy_frontend to alter call behavior. The frontend is a build-time concern; the runtime sees only signed, verified Rego.

Rationale: Mirrors INV-09 (Authorization Boundary) and the ContractRefine INV-CR-9 commitment. Allowing adapters to behave differently based on the authoring frontend would partition the governance surface — operators could no longer reason about a single deterministic decision per (action, input) pair.

Code modules: runtime/server.go (handleTool), runtime/interceptor.go (Interceptor interface), policy/builder.go (manifest writer; reads forbidden in adapters).

Enforcement:

  • Status: trivially enforced today because BundleManifest.policy_frontend does not exist yet — no adapter CAN read it. The invariant becomes active when C04 lands the field.

  • Planned (C04): add a ci/test_arch_invariant.sh sub-check forbidding BundleManifest.PolicyFrontend reads in cmd/autonomy/commands/, runtime/exec/, and any *_adapter.go file. The check lands in the same PR as the field so the gate protects the field from day one.

  • Code review: any if manifest.PolicyFrontend == ... outside policy/, bundle/, and operator-facing CLI display paths fails review.

INV-MM-4 — IR-to-Rego compile is deterministic

Statement: Compiling the same IR program produces byte-identical Rego output across runs, across hosts, and across operator environments. The compiler MUST NOT read the wall clock, MUST NOT call math/rand or crypto/rand, and MUST NOT depend on filesystem entry ordering. Generated identifier names MUST derive from the IR program’s content (rule IDs or deterministic hashes of rule positions), never from process state.

Rationale: Two operators on different hosts building the same IR program MUST produce the same bundle_hash (which the bundle signer covers). Non-determinism in the compiler breaks the signed-bundle supply chain.

Code modules: policy/ir/compiler.go (lands in C03).

Enforcement:

  • Status: not enforced today — the substrate does not exist. C03 will land both the compiler AND the gates below in the same PR.

  • Planned (C03): property test TestIRToRego_Deterministic in policy/ir/compiler_test.go compiles a random IR program N times and asserts byte-identical output.

  • Planned (C03): a go vet-style check (in ci/ or as a build tag) forbids time.Now(), math/rand, crypto/rand, and os.ReadDir (which is order-undefined on some filesystems) inside the policy/ir/compiler build target.

INV-MM-5 — Frontend provenance is recorded on both manifest layers

Statement: The policy_frontend field is recorded on both the inner policy.BundleManifest (read by the runtime + autonomy policy inspect|load|eval) AND the outer bundle.Manifest schema v1.3 (read by OCI consumers + bundle inspect|verify without unpacking). bundle.Manifest.Validate() cross-checks the two values at verify time; mismatch fails closed.

Rationale: The runtime / autonomy policy CLI paths never read the outer bundle.Manifest; OCI / bundle inspect paths never unpack the inner manifest. Recording on only one layer leaves the other surface blind to frontend provenance, which Phase 1’s explainability output depends on. Cross-checking at verify catches a tampered bundle whose inner and outer manifests disagree.

Code modules: policy/builder.go (inner BundleManifest writer), bundle/manifest.go (outer schema v1.3 + cross-check), bundle/verify.go. All gain the policy_frontend field in C04.

Enforcement:

  • Status: not enforced today — neither manifest carries policy_frontend, and no tamper-check exists in bundle/verify.go. C04 lands the field on both layers AND the gates below.

  • Planned (C04): test in bundle/verify_test.go constructs a tampered bundle with mismatched policy_frontend on inner vs outer manifests and asserts verify fails with a documented sentinel error.

  • Planned (C04): test in policy/builder_test.go asserts a v1.2 (legacy, no field) and a v1.3 bundle both load cleanly; legacy defaults to "rego".

INV-MM-6 — Explainability metadata survives end-to-end

Statement: When a policy emits a decision with MatchedRule, EvaluationTrace, or RemediationHint populated, those fields survive from policy.Eval through runtime.Interceptor.Allow into the WAL decision event and out through autonomy wal inspect --kind decision. Widening any one of these layers without the others MUST fail CI.

Rationale: The Phase 1 acceptance criterion is “rule origin visible to operators.” Widening only the runtime Decision struct without widening the WAL event schema means the IR knows the rule origin but the operator never sees it. Widening only the WAL without the CLI means the field is in the event but wal inspect strips it. The end-to-end pin makes the contract observable as a single invariant.

Code modules: runtime/decision.go (Decision struct; widens in C05), policy/evaluator.go (populates; widens in C05), runtime/server.go (forwards; widens in C06), telemetry/events.go (event schema; widens in C06), cmd/autonomy/commands/wal.go (renders; widens in C06), cmd/autonomy/commands/audit_cmd.go (adds --with-explainability flag in C06).

Enforcement:

  • Status: not enforced today — none of the explainability fields exist on runtime.Decision, in the WAL event schema, or in the CLI surface. C05 widens the runtime contract; C06 widens the WAL + CLI surfaces. The end-to-end pin (the load-bearing claim of this invariant) only becomes verifiable after both PRs land.

  • Planned (C06): integration test in runtime/server_test.go posts a tool call with a YAML-authored bundle, asserts the decision WAL frame carries matched_rule.id AND matched_rule.source_file.

  • Planned (C06): CLI test asserts autonomy wal inspect --kind decision displays those fields when present.

  • Planned (C06): a drift test pins that every field added to runtime.Decision is also present in the WAL event schema (telemetry/events.go) — adding a field to one without the other fails CI.

INV-MM-7 — IR is the only contract between frontends and backends

Statement: Frontends (YAML, JSON, NL, Graph) MUST NOT call the Rego backend directly. Backends (Rego today; CEL, WASM, native in v2) MUST NOT inspect the originating frontend’s syntax. The IR Go types in policy/ir/ are the only shared substrate. A new frontend adds a compiler frontend → ir.Program; a new backend adds a compiler ir.Program → <target>.

Rationale: N frontends × M backends ⇒ N×M compilers without an IR. With the IR, it’s N+M. The IR is also the architectural pin that lets Phase 1 ship YAML without needing to redesign for the future Graph frontend.

Code modules: policy/ir/ (interface definition; lands in C02), all policy/<frontend>/ compilers (policy/yamldsl/ lands in C03), policy/ir/compiler.go (Rego backend; lands in C03).

Enforcement:

  • Status: not enforced today — none of the packages exist. C02 + C03 land the substrate AND the gates below. The discipline is documented now so any reviewer can hold the implementing PRs to it.

  • Planned (C03): add a ci/test_arch_invariant.sh sub-check forbidding any policy/<frontend>/ package from importing policy/ir/compiler or any backend package — they import only policy/ir (the types).

  • Planned (C03): same check forbids any backend from importing any policy/<frontend>/ package.

INV-MM-8 — preflight surfaces are frontend-orthogonal

Statement: The ContractRefine surfaces shipped by epic #1020 — policy.BundleManifest.RequiresPreflight (manifest-layer binding gate) and the input.preflight shape (Rego rules read the verified PreflightDecision) — behave identically regardless of which frontend (rego, yaml-dsl, future json-rules / nl / graph) authored the bundle. Frontend choice MUST NOT change which /v1/tool calls the runtime binding gate fires on, MUST NOT change the input.preflight shape Rego rules consume, and MUST NOT introduce any code path that branches on policy_frontend to alter preflight enforcement.

Rationale: Without this pin, operators who migrate a requires_preflight: true bundle from Rego to YAML could see behavior change in ways the YAML author never wrote. The two ContractRefine surfaces are deliberately at orthogonal layers (manifest field for the runtime’s binding gate; input contract for the policy evaluator); the IR is supposed to slot into the policy evaluator’s input contract unchanged, so a YAML rule expressing input.preflight.outcome == "pass" MUST compile to a Rego predicate that evaluates identically to the hand-written form. The invariant makes this load-bearing as a single observable property.

Code modules: policy/builder.go (BundleManifest holds both RequiresPreflight and the planned PolicyFrontend field; the two MUST stay independent), runtime/server.go (handleTool’s binding gate reads RequiresPreflight; MUST NOT read PolicyFrontend), policy/evaluator.go (populates input.preflight from runtime.Action.Preflight; MUST treat every Rego bundle identically regardless of its origin frontend), policy/ir/compiler.go (lands C03; lowers field: preflight.<...> predicates to the equivalent Rego input.preflight.<...> access).

Enforcement:

  • Status: the RequiresPreflight half is already enforced today by virtue of INV-MM-3 — adapters MUST NOT read BundleManifest.PolicyFrontend, which means they cannot branch on it to change RequiresPreflight behavior. The CI sub-check planned in INV-MM-3 covers this leg.

  • Planned (C03): the IR → Rego property test fixture set includes preflight-bound predicates (e.g. field: preflight.outcome, value: pass) and asserts the generated Rego accesses input.preflight.outcome identically to a hand-written predicate. This pins the input.preflight half.

  • Planned (C04): integration test in policy/builder_test.go or a sibling test file constructs a YAML-authored bundle with requires_preflight: true AND policy_frontend: yaml-dsl, signs/verifies it, then drives /v1/tool with and without the X-Autonomy-Preflight-Id header. Asserts the binding gate fires identically to a Rego-authored bundle’s gate behavior (the C08 test in runtime/server_preflight_binding_test.go is the reference shape).

  • Planned (C03): a small drift test that constructs a YAML rule expressing input.preflight.outcome == "pass" and asserts the emitted Rego is byte-identical (modulo deterministic identifier hashing) to a hand-written Rego predicate with the same semantics.

See Also