# proposal/01-design-principles.md · versecafe/strata

[View on GitCafe](https://git.cafe/versecafe/strata/blob/7a7a1544c70f936a726ff076a85218064160dee5/proposal/01-design-principles.md)

Repository: [versecafe/strata](https://git.cafe/versecafe/strata)

Visibility: public

Requested revision: 7a7a1544c70f936a726ff076a85218064160dee5

Requested commit: 7a7a1544c70f936a726ff076a85218064160dee5

Commit: 7a7a1544c70f936a726ff076a85218064160dee5

Blob: 178fa6db7bdad7306591fe610769b381a49052bb

Size: 6701 bytes

[Immutable source](https://git.cafe/versecafe/strata/blob/7a7a1544c70f936a726ff076a85218064160dee5/proposal/01-design-principles.md?format=markdown)

```
# 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](decisions.md).

## 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](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](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](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](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](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](open-problems.md) or the [roadmap](11-roadmap.md), 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.

```