F-*** doctrine invariants
Load-bearing rules the code keeps true and the tests pin. A comment
citing F-xxx is claiming this page's statement at that site. The
-a5 suffix marks the audit-5 refinement of the base invariant.
F-001
Verdict monotonicity. On the decision path, an enforcement layer may
only keep or harden the verdict (ALLOW < REQUIRE_CONFIRMATION <
ABSTAIN); relaxations exist only through the provenance-checked
override sites on a frozen allowlist. Enforced by enforce_monotone
(trace_helpers.py) around every layer of the gate decision stack,
and by the trace grammar test.
F-001-a5
A caller-declared input risk is untrusted input: it may harden the
verdict or add a signal, never weaken anything. Enforced in
kernel/gate/input_risk.py and the input-risk gate (harden-only
outside the graded posture).
F-002
Unknown switching safety fails closed: when the T1 condition cannot
be evaluated, the turn is treated as unsafe, never as safe. Enforced
in the gate switching layer; production invariants hold whatever the
constructor (api/os.py).
F-003
The validity envelope's hard_block is a real, computed signal (it
used to be hardcoded False, leaving the enforcement machinery dead).
Enforced by hard_block_policy.py and its table version.
F-003-a5
A configuration override that would relax a production invariant is refused at construction, not silently accepted.
F-004
The tool registry freezes after bootstrap: freeze_tools() pins the
surface and returns its fingerprint; later mutation is refused.
F-004-a5
Production invariants hold whatever the constructor arguments; the
single enforcement point is CognitiveOSConfig/CognitiveOS.
F-005
An envelope that could not be built is unknown validity, and unknown
validity gates nothing open: the verdict fails closed to ABSTAIN
(decision_stack.py).
F-006
The input-risk policy never relaxes a real veto, and an exception inside the gate forces ABSTAIN (fail-closed), never a pass-through.
F-007
The composed run commitment: what arvis did is exactly what arvis can
prove it did (api/commitment.py).
F-007-a5
The commitment inputs are exactly: registry manifest fingerprint, effective config fingerprint, active policy tables fingerprint, and the digest of the redacted syscall journals.
F-008
The runtime mode set is closed: unknown mode strings are refused at
coercion instead of silently running with a permissive posture
(api/runtime_mode.py).
F-008-a5
Every effect syscall journals a pre-effect audit intent through the outbox; a missing intent reads as a ghost signal, never as silence.
F-009
force_tool only selects the tool; execution authority is never
implied and requires force_execution=True explicitly
(api/runtime_controls.py).
F-009-a5
An effect capability cannot exist without its governance: registering
an EFFECT syscall without an access resolver is refused at import
time (syscall_registry.py).
F-012
REQUIRED audit commitment needs the trace machinery: combined with
enable_trace=False it is a configuration contradiction and is
refused (api/os.py).
F-013
The audit artifact detaches at commitment time: the stored IR is
rebuilt from the exact hashed bytes, so no upstream alias can diverge
the payload from its committed digest (cognitive_result_view.py).
F-014
A tool that runs past its declared timeout has its late result
REJECTED (deadline on result acceptance, not an interruption; the
effect may still have happened and the refusal says so)
(errors/tool_runtime.py).
F-015
How a missing audit commitment is handled is an explicit policy
(AuditCommitmentPolicy), never an implicit default.
F-016
Retry requires idempotence: a tool whose spec does not declare it is
never retried (tools/retry_policy.py).
F-017 and F-018
Host-provided tool gates: in the PRODUCTION profile a tool declaring
required_consent or data_egress is denied when the matching gate
is missing (deny-by-default); other profiles leave the decision to
the host (api/os.py).
F-018-a5
The redaction policy is part of the commitment composition: effect parameters are redacted before hashing, and the redaction policy itself is versioned.
F-019
In the PRODUCTION profile the tool registry freezes automatically at
the first run; late registration is refused by the frozen registry
itself (api/os.py).
F-020
A payload that violates the tool's declared input_schema never
reaches the tool (errors/tool_runtime.py).