core.architecture — ATS-V Architectural Type System

regression-only

Upstream defects block public API paths. Regression controls record the failing shapes and any working subset.

core.architecture is the Verum-native side of the Architectural Type System v6.5 (ATS-V). It mirrors the kernel-side primitives in crates/verum_kernel::arch* via the cross-side pin test in crates/verum_kernel/tests/k_arch_v_alignment.rs, which fails CI on any drift.

Reuse-over-invention discipline

The ATS-V extension is intentionally NOT a separate type system. It reuses the existing language surface:

1. ONE typed attribute — @arch_module(...) — recognised by compiler-internal dispatch. Follows the V8.1 META1 architectural principle and the generic identifier(args) form in grammar/verum.ebnf.
2. THIS library — Verum-native type X is variant_list declarations that mirror the kernel-side primitives.
3. Per-module kernel-discharge bridges declared as @kernel_discharge(<intrinsic>) axioms — one per architectural sub-system. Same pattern as core.verify.separation_soundness and core.verify.codegen_soundness.

Zero new keywords; zero new compiler phases; everything reuses the existing attribute + axiom + cross-side pin machinery.

Coverage is universal, and enforced

@arch_module(...) is not advisory and not opt-in: every cog under core/ carries one, currently 2 252 of them. The invariant is held by a pin — pin_universal_arch_module_coverage_in_core in verum_kernel — which walks the whole tree and fails with the name of any file that lacks an attestation.

This is what makes the roster below meaningful. An architectural type system that most modules declared and a few quietly skipped would let the unattested ones drift outside every capability, boundary and lifecycle check the system performs — and the gap would be invisible, because nothing downstream distinguishes "attested as unconstrained" from "never attested". A single missing attestation is therefore a hole in the guarantee, not a rounding error, which is why the pin names the offending file rather than reporting a percentage.

Adding a module to core/ means adding its attestation in the same change. The values are not free-form: foundation, stratum and lifecycle all draw from the canonical primitives in types.vr below, so a new module inherits the vocabulary its siblings already use.

Module roster (12 files, 4 703 lines)

File	Lines	What's in it
types.vr	1767	Canonical primitives — Capability / Boundary / Composition / Lifecycle / Foundation / Tier / MsfsStratum / CveClosure / Shape / CapabilitySchema
anti_patterns.vr	691	32-pattern roster — AntiPatternCode / AntiPatternViolation / Severity / DiagnosticContext + 12 kernel-discharge bridges
mtac.vr	458	Modal-Temporal Architectural Calculus — modal/temporal/adjunction witnesses + canonical observer roster
adjunction.vr	294	Adjunction analyzer for refactoring — CanonicalAdjunction / Refactoring / AdjunctionAnalysis / RefactoringChain
counterfactual.vr	283	Non-destructive counterfactual reasoning — ArchMetric / MetricValue / InvariantStatus / CounterfactualReport
yoneda.vr	244	Yoneda-equivalence checker — ShapeObservation / AgreementStatus / YonedaVerdict
phase.vr	183	ATS-V phase 6.5 orchestrator — ModuleArchResult / ArchPhaseReport / CompositionStep / CompositionVerificationReport
corpus.vr	143	Cross-cog invariants — CorpusInvariant / CorpusViolation / CorpusReport + 4 baseline checks
composition.vr	128	A ⊗ B typed operation — CompositionResult + associativity pin
parse.vr	117	@arch_module(...) parser error type — ArchParseError (5 variants) + canonical-field roster pin
capability_ontology.vr	112	Registered Custom capability names
mod.vr	283	Re-exports + module header

Canonical primitives (types.vr)

Every variant below is read off core/architecture/types.vr. A capability specifies the operations a cog may perform on a tagged resource.

public type Capability is
    | Read(ResourceTag)
    | Write(ResourceTag)
    | Exec(ExecTarget)
    | Escalate(PrivilegeRealm)
    | Spawn(TaskLifetime)
    | TimeBound(ExpirationPolicy)
    | Persist(PersistenceMedium)
    | Network(NetProtocol, NetDirection)
    | CustomCapability(Text);   // registered in capability_ontology.vr

public type Foundation is
    | ZfcTwoInacc               // the default in @arch_module
    | Hott
    | Cubical
    | Cic
    | Mltt
    | Eff
    | CustomFoundation(Text, Text);

public type MsfsStratum is
    | LFnd                      // foundational — most modules live here
    | LCls
    | LClsTop
    | LAbs;

// Nine lifecycle stages, and most carry a justification Text. There is
// no `Sketch`, `Lemma` or `Deprecated`.
public type Lifecycle is
    | Hypothesis(ConfidenceLevel)
    | Plan(Text)
    | Postulate(Text)
    | Definition
    | Conditional(List<Text>)
    | Theorem(Text)
    | Interpretation(Text)
    | Retracted(Text, Maybe<Text>)
    | Obsolete(Text, Maybe<Text>);

The @arch_module(...) attribute on a module declares its canonical position in this space:

@arch_module(
    foundation: Foundation.ZfcTwoInacc,
    stratum: MsfsStratum.LFnd,
    lifecycle: Lifecycle.Theorem("v0.1")
)
module core.architecture.mod;

Anti-pattern roster (anti_patterns.vr)

32 canonical anti-patterns each with a stable AntiPatternCode (e.g. AP001_GodModule, AP017_FoundationDowngrade, AP032_CorpusObservationGap). Each violation surfaces with a DiagnosticContext (module / span / severity / kernel-discharge witness) that flows through the standard diagnostic pipeline — no side-channel reporting.

Severity bands: Hint | Info | Warning | Error | KernelBlock. The top band (KernelBlock) hard-fails the verification phase; the others surface as diagnostics without halting.

Modal-Temporal Architectural Calculus (mtac.vr)

MTAC formalises temporal evolution of architectural shapes:

public type ModalKind is Necessity | Possibility | Strict | Weak;
public type TemporalKind is Always | Eventually | Until | Since;

public fn modal_is_temporal(m: &ModalKind) -> Bool;
public fn modal_is_modal(m: &ModalKind) -> Bool;
public fn time_point_precedes(a: &TimePoint, b: &TimePoint) -> Bool;
public fn observer_full_canonical_roster() -> List<Observer>;
public fn adjunction_witness_is_adjoint_of(
    w: &AdjunctionWitness, f: &Functor, g: &Functor
) -> Bool;

Counterfactual reasoning (counterfactual.vr)

Non-destructive "what if" analysis on architectural metrics: "would this refactor preserve invariant X if I applied it?". The engine never mutates the source-of-truth registries — every counterfactual is computed against a temporary overlay and discarded.

// Ten metrics, each a COUNT or an ordinal over one dimension — not the
// five aggregate names this page used to list.
public type ArchMetric is
    | ExposedCapabilityCount
    | RequiredCapabilityCount
    | ReadCapabilityCount
    | WriteCapabilityCount
    | NetworkCapabilityCount
    | BoundaryInvariantCount
    | CompositionDegree
    | LinearResourceCount
    | StratumOrdinal
    | CveCompleteness;

// The report names the two DECISIONS it compares and carries per-metric
// and per-invariant results; there is no baseline/counterfactual map
// pair and no `is_safe`.
public type CounterfactualReport is {
    schema_version:          Int,
    pair_name:               Text,
    base_decision:           Text,
    alt_decision:            Text,
    metric_comparisons:      List<MetricComparison>,
    invariant_evaluations:   List<InvariantEvaluation>,
    overall_stable:          Bool,
    diverging_metric_count:  Int,
};

Adjunction analyzer (adjunction.vr)

Identifies canonical adjunctions in the codebase and proposes refactoring chains that preserve them. The pattern "F ⊣ G" is detected structurally (Hom-set isomorphism witnessed at the call- boundary); refactorings that disrupt the adjunction surface as diagnostics.

Yoneda-equivalence checker (yoneda.vr)

YonedaVerdict is a RECORD, not a sum:

public type YonedaVerdict is {
    schema_version:     Int,
    agreements:         List<ObserverAgreement>,
    equivalent:         Bool,
    disagreement_count: Int,
};

Two architectural shapes are Yoneda-equivalent iff they agree on all observers, which is what equivalent reports; the checker enumerates the canonical observer roster and records EVERY observer's agreement in agreements, with disagreement_count as the summary. Read the disagreeing observers out of agreements — the verdict does not carry a single counter-example.

The verdict and observation types are declared in core/architecture/yoneda.vr.

Composition (composition.vr)

A ⊗ B operation with an associativity pin: (A ⊗ B) ⊗ C ≡ A ⊗ (B ⊗ C) must hold for every composable triple. The pin test fails CI on any drift in CompositionResult semantics.

Corpus invariants (corpus.vr)

Cross-cog invariants that hold across the entire dependency graph — not per-module but at the corpus level. Four baseline checks: foundation-monotonicity, lifecycle-monotonicity, stratum-respect, cve-closure-conservation. Each violation carries the two cogs involved + the witness.

Phase orchestrator (phase.vr)

The entry point for ATS-V phase 6.5. Per-module compilation flows through phase::run_module(...); cross-module composition flows through phase::compose(...). Both return structured reports with full diagnostic payloads.

Status

File	Status
mod.vr / types.vr	undocumented — canonical primitives + re-exports — no conformance suite yet
anti_patterns.vr	unverified — full 32-pattern roster — core-tests/architecture/anti_patterns
mtac.vr	unverified — full MTAC primitives + helpers — core-tests/architecture/mtac
counterfactual.vr	unverified — full report surface — core-tests/architecture/counterfactual
adjunction.vr	unverified — analyzer + refactoring chain — core-tests/architecture/adjunction
yoneda.vr	unverified — checker + observer roster — core-tests/architecture/yoneda
composition.vr	regression-only — ⊗ + associativity pin — core-tests/architecture/composition
corpus.vr	regression-only — 4 baseline invariants — core-tests/architecture/corpus
phase.vr	regression-only — orchestrator surface — core-tests/architecture/phase
parse.vr	regression-only — parser error + roster pin — core-tests/architecture/parse
capability_ontology.vr	unverified — Custom-capability registry — core-tests/architecture/capability_ontology

Cross-side alignment

The kernel-side primitives live in crates/verum_kernel::arch*. crates/verum_kernel/tests/k_arch_v_alignment.rs is the cross- side pin: any drift (new variant on one side, renamed field on the other, severity-band reshuffle) fails CI before merge.

This is the same alignment discipline as crates/verum_common/src/well_known_types.rs ↔ core/base/primitives.vr — single canonical source-of-truth on the kernel side, Verum-native projection on the library side, pin test failing on drift.