The rules every other document must obey. A design that violates one of these must either change or amend the principle here, explicitly, via the decisions register.
Ordinary synchronous digital hardware is expressible in the safe subset. The compiler prevents or flags: accidental truncation, signedness mistakes, clock/reset-domain violations, exclusive-resource conflicts, invalid stage connections, protocol misuse, missing arbitration, speculative values reaching irrevocable effects, uninitialized state reaching architectural state. Escapes exist but are granular — unsafe clock_crossing, unsafe timing, unsafe primitive, unsafe proof_assumption, ... — each invalidating only its own guarantees, and the compiler reports the aggregate unsafe surface per design.
Safety is never an optimization level: no profile, mode, or objective vector may strengthen or weaken any judgment or evidence gate (D-070). There is no "-O0 is safer."
Abstractions must not conceal registers, combinational depth, replication, buffering, arbitration, memory ports, latency, throughput, or fanout. "Zero-cost abstraction" means: lowers to hardware an expert would reasonably write by hand — not "costs nothing." Every abstraction answers what did I just build? with an inspectable structure report. Storage is never inserted invisibly; arbitration is never chosen silently; iteration is never ambiguous between replication, unrolling, pipelining, and sequential reuse.
Every lowering step either preserves, transforms, discharges, explicitly weakens, or explicitly invalidates each semantic fact — never silently drops it (mechanism: the semantic ledger, 07-compiler-architecture.md). Provenance is mandatory: any register, wire, assertion, or critical path answers "which source expression, comptime call, contract, or pass created you?"
Internally, value shape, time, usage, protocol, effects/authority, and refinements are separate judgments with separate laws (02-type-system-core.md). Externally, the surface syntax presents them as one coherent declaration and one diagnostic vocabulary. Neither direction may leak: no mega-generic types in source, no cross-judgment soup in error messages.
Comptime constructs architecture; the optimizer chooses among semantics-preserving implementations; proofs constrain both. Canonical architectural operations (Reduce, Arbitrate, Buffer, CrossClock, Reorder, Commit, ...) remain first-class IR nodes carrying their laws — comptime must not pre-lower them into primitive soup, and users must not implement structural optimization via type-level gymnastics. This is a hard rule from day one because it cannot be retrofitted (decision D-022).
Comptime code cannot read the clock, the network, or undeclared files; cannot depend on environment or iteration-order nondeterminism; declares its effects; and has tracked, reportable cost (steps, memory, generated nodes). Same source + same inputs = same hardware, forever (decision D-021).
No fact is silently promoted to truth. Physical properties (frequency, area, power), unbounded properties (liveness, fairness), and external components (vendor primitives) carry explicit evidence tags — Estimated, Tested, BoundedProved, InductivelyProved, TranslationValidated, Measured — and consumers (optimizer legality, release gates, agents) state the minimum evidence they require (06-refinements-and-evidence.md).
The trusted computing base is the parser, typechecker, comptime evaluator, IR verifier, lowering passes, and contract compiler. Agent output — code, properties, rewrites, tests — is untrusted input, admitted only through type checking, translation validation, equivalence checking, simulation, and formal properties (09-agent-system.md).
Every rejection names the violated judgment, the conflicting facts with source locations, and a set of concrete candidate repairs. A diagnostic an agent cannot act on programmatically is a bug. Diagnostic quality is a gating criterion for shipping any new judgment: a check whose failures can't be explained in the shared vocabulary doesn't ship (this is the direct mitigation for the multi-judgment error-message risk, open-problems.md OP-5).
Every doc separates committed design from north star. Committed sections may only depend on committed sections. A north-star feature that would change a committed interface must record that pressure in open-problems.md or the roadmap, not silently shape the committed design.
Phase sequencing favors dogfooding: Strata's own components (FIFOs, arbiters, the test infrastructure's harnesses) are the first verification targets; the agent layer's first job is working on Strata designs. With an agent-amplified team of 1–3 humans (D-008), tooling that multiplies agents is on the critical path, not a nice-to-have.
A guarantee is meaningful only with its assumptions, validity scope, owner, and expiry conditions. Fault occurrence is not detection; correction is not containment; a source timing fact is not a bound netlist exception; a generated assurance graph is not evidence. Every cross-layer artifact records what it depends on and what invalidates it. Composition rejects circular assumption ownership and reports uncovered residue rather than converting missing evidence into trust.
Faults, progress, memory models, observer-relative security, power, reconfiguration, DFT, and assurance do not each become a new universal term judgment. The foundational semantics expose only reusable concepts—identity, lineage, invalidation, events, observations, denotation, and authority. Domain contract families and verification packages build on them. A component that declares no health, memory-model, power, or observer contract does not acquire those annotations or proof obligations.