Design Principles

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.

P-1 · Safe by default, unsafe by declaration

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."

P-2 · Hardware cost stays visible

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.

P-3 · Meaning survives lowering

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?"

P-4 · Stratified judgments, unified surface

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.

P-5 · Architecture stays recognizable until an explicit lowering boundary

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).

P-6 · Elaboration is deterministic, effect-declared, and budgeted

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).

P-7 · Claims carry evidence

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).

P-8 · Deterministic tools are the trusted base; models are not

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).

P-9 · Diagnostics are the product

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).

P-10 · Two-track honesty

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.

P-11 · The platform builds itself

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.

P-12 · Assumptions, validity, and custody are first-class

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.

P-13 · Keep the semantic waist thin; make advanced contracts opt-in

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.