Lifecycle — CVE 7-symbol taxonomy

Every Verum cog declares its Shape.lifecycle — the artefact's position in the CVE seven-symbol taxonomy. The declaration is read by the audit machinery, by the linter, by the compiler's anti-pattern catalog, and by the dual-audience surface that renders both developer-facing and auditor-facing views.

This page is the operational reference. For the conceptual story behind the seven symbols, read CVE — Constructive / Verifiable / Executable; for the canonical glyph table, read CVE — seven canonical symbols. This page assumes both.

1. The Lifecycle variant

public type ConfidenceLevel is
    | Low | Medium | High;

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

Nine variants — seven of them are the canonical CVE glyphs; two (Plan and Obsolete) are ATS-V legacy variants retained for backward compatibility.

Variant	CVE glyph	Rank	Mature-corpus admissible?
Theorem(since)	[T]	6	yes
Definition	[D]	5	yes
Conditional(conditions)	[C]	5	yes
Postulate(citation)	[P]	4	yes
Plan(target_completion)	(legacy)	3	discouraged
Hypothesis(confidence)	[H]	2	only with @plan(...)
Interpretation(reason)	[I]	1	no — flagged in strict
Retracted(reason, repl)	[✗]	0	no — citing produces error
Obsolete(reason, repl)	(legacy)	0	no — replace before remove

2. Declaration sites

A cog declares Lifecycle exactly once, in the @arch_module(...) attribute on its module …; statement:

@arch_module(
    foundation: Foundation.ZfcTwoInacc,
    stratum:    MsfsStratum.LFnd,
    lifecycle:  Lifecycle.Theorem("v1.0"),
)
module my_app.checkout;

Two corollaries:

1. One Lifecycle per cog. Lifecycle is not a per-function attribute. Function-level granularity is expressed via @verify(strategy) (the verification ladder) and via @plan(...) / @retracted(...) macros that wrap declarations inside an otherwise-mature cog.
2. Lifecycle is mandatory in strict: true cogs. A cog that sets strict: true must declare a Lifecycle. The default (when strict is omitted or false) treats a missing Lifecycle as Lifecycle.Plan("unspecified") — a permissive default suitable for available development.

3. Lifecycle ordering and citation discipline

The poset on Lifecycle is load-bearing in the type system. The AP-009 LifecycleRegression anti-pattern enforces a single rule:

A cog with Lifecycle of rank R may only cite cogs with Lifecycle of rank ≥ R.

In other words: a [T] Theorem cog may cite [T], [D], [C], [P] cogs — but not [H], [I], [✗] cogs. The discipline ensures that "mature artefacts depend on mature artefacts"; a [T] cog that cites a [H] Hypothesis is in fact only as strong as a [H], but the developer is asserting it is [T] — the type checker rejects the inconsistency.

A common pitfall: transitive lifecycle regression. A [T] cog imports a [D] Definition cog which itself imports a [H] Hypothesis cog. The direct relationship is OK ([T] → [D], both rank ≥ 5), but the transitive chain reveals the [T] is ultimately resting on a [H]. The AP-024 TransitiveLifecycleRegression anti-pattern walks the import graph and flags the chain.

4. Variant-by-variant operational guide

Each variant has a recommended discipline for when to use it, what additional attributes to add, and how to mature it.

4.1 Theorem(since: Text) — [T]

When: the cog is fully proved, every public function carries @verify(certified) (or stronger), and the proof corpus has been re-checked through the trusted kernel.

Companion attributes: @verify(certified) on each public function; optionally @framework(...) markers for cited axioms. In strict mode, the cog MUST also declare:

• declarations.purpose: Some(Purpose { ... }) — declared thresholds bounding the audit (AP-037 BoundlessAudit).
• declarations.substrate: Some(CognitiveSubstrate.AnalyticDecompositional) — cognitive substrate disclosure (AP-038 ImplicitSubstrate).
• declarations.anchoring: Some(FormalAnchoring.CurryHowardLawvere) — required only when Foundation is outside the CHL domain {ZfcTwoInacc, Cic, Mltt, Hott, Cubical, Eff} (AP-039 AnchoringOverextension).

The E axis sense. A [T] Theorem requires E in the StructuralReadiness sense, per cve-architecture spec §2.3.0. "Currently running in production" and "ran in the past" are co-located but distinct concepts; conflating them is a register collision.

Maturation path: none — [T] is the terminal status. To retract a [T], transition to Retracted("reason", Some(replacement)).

Example:

@arch_module(
    lifecycle: Lifecycle.Theorem("v2.1"),
    strict: true,
    declarations: ShapeDeclarations {
        purpose: Some(Purpose {
            role: "AEAD primitive: integrity + confidentiality for the payment cog graph",
            k_min: CveThresholdK.FullWitness,
            v_min: CveThresholdV.FullFormalProof,
            e_min: CveThresholdE.StructurallyReady,
        }),
        substrate: Some(CognitiveSubstrate.AnalyticDecompositional),
        anchoring: Some(FormalAnchoring.CurryHowardLawvere),
        e_sense: Some(ExecutabilitySense.StructuralReadiness),
    },
)
module my_app.crypto.poly1305;

@verify(certified)
public fn mac(key: Key32, msg: &Bytes) -> Tag16
    where ensures (verify_mac(key, msg, result) == true)
{ … }

4.2 Definition — [D]

When: the cog establishes a boundary — types, capability ontology entries, configuration constants. There is no theorem to prove; the definitions ARE the content.

Companion attributes: @derive(...) for trait derivations, @repr(C) for FFI-relevant records.

Maturation path: none — Definition is terminal. If the boundary needs proving (e.g., refinement satisfiability), the cog graduates to Theorem once the proofs are added.

Example:

@arch_module(lifecycle: Lifecycle.Definition)
module my_app.config.types;

public type DatabaseUrl is Text { self.starts_with("postgres://") };
public type Port        is Int { 1 <= self && self <= 65535 };
public type MaxRetries  is Int { 0 <= self && self <= 100 };

4.3 Conditional(conditions: List<Text>) — [C]

When: the cog is fully proved under listed assumptions. Outside the assumptions, the cog is undefined. Useful when the proof relies on external invariants (OS guarantees, hardware behaviours, cryptographic standards).

Companion attributes: @verify(formal) is typical; @condition(...) markers can pin individual conditions to call sites.

Maturation path: discharge the conditions (move to [T]) or demote to [H] if conditions cannot be satisfied.

Example:

@arch_module(
    lifecycle: Lifecycle.Conditional([
        "host platform is POSIX-compliant",
        "fs.realpath returns a canonical path",
        "process has CWD permissions on the target tree",
    ]),
)
module my_app.fs.canonical;

4.4 Postulate(citation: Text) — [P]

When: the cog is accepted without internal proof, on the strength of an external citation: a peer-reviewed paper, a published proof corpus, or a kernel discharge axiom.

Companion attributes: @framework(name, "citation") or @kernel_discharge are mandatory; the audit gate enumerates them.

Maturation path: typically terminal. To "internalise" a postulate (replace external trust with internal proof), graduate to [C] or [T] and remove the framework citation.

Example:

@arch_module(
    lifecycle: Lifecycle.Postulate(
        "Joux 2009 · 'Algorithmic Cryptanalysis' · Theorem 4.2"
    ),
)
@framework(joux_2009, "Theorem 4.2 — generic group lower bound")
module my_app.crypto.security_arguments;

4.5 Plan(target_completion: Text) — (legacy)

When: committed work, not yet implemented. Distinct from [P] Postulate (which carries a citation backing).

Why retained. Cogs in the existing corpus already cite Plan(...) lifecycle entries; removing the variant would break those citations. Retained as a legacy form pending a future RFC that folds Plan into Hypothesis(...) plus the @plan(...) attribute.

Replacement guidance. New code SHOULD prefer Hypothesis(ConfidenceLevel.X) plus @plan(target: "...", milestones: [...]) — the same intent ("committed but not implemented") expressed via the canonical maturation pair.

Audit treatment. Lint warning, not error. The audit gate flags Plan(...) declarations as "legacy" in the audit-bundle output but does not block release. A per-cog @suppress("legacy_lifecycle") opt-out exists for cogs that have a documented migration plan.

Companion attributes: @plan(target: "...", milestones: [...]).

4.6 Hypothesis(confidence: ConfidenceLevel) — [H]

When: speculation. The cog is in active design, no implementation, no proof, no tests. MUST carry a maturation plan; a hypothesis without a @plan(...) attribute is AP-034 HypothesisWithoutMaturationPlan.

Companion attributes: @plan(target: ..., milestones: [...]).

Maturation path: as the cog matures, transition to:

• Conditional(...) once the proof exists under hypotheses, or
• Theorem(...) once the proof exists unconditionally, or
• Retracted(...) if the bet does not pan out.

Example:

@arch_module(lifecycle: Lifecycle.Hypothesis(ConfidenceLevel.Medium))
@plan(
    target:     "v0.5",
    milestones: ["spec drafted", "POC built", "verified", "shipped"],
)
module my_app.experimental.zk_proof;

4.7 Interpretation(reason: Text) — [I]

When: the cog has been written down but neither realised, nor checked, nor extracted. Transitional only. A mature corpus contains zero [I] entries — every Interpretation must either mature into a higher status or be removed before the corpus ships.

In strict: true mode, an Interpretation annotation is AP-035 InterpretationInMatureCorpus.

Maturation path: transition out as soon as the artefact gains C, V, or E content.

Why it exists at all: during exploration, some artefacts are written down before any of C/V/E is realised. Naming the status [I] rather than "todo" or "draft" forces explicit transition rather than silent decay.

4.8 Retracted(reason: Text, replacement: Maybe<Text>) — [✗]

When: the artefact has been deliberately withdrawn — refuted, deprecated, scope-removed. The record is preserved as a negative example in the audit chronicle.

Citing a [✗] cog produces a compile-time error (AP-033 RetractedCitationUse).

Companion attributes: @retracted_as_of(date: "YYYY-MM-DD") optionally pins the retraction date for audit chronology.

Example:

@arch_module(
    lifecycle: Lifecycle.Retracted(
        "weak primitive — deprecated by NIST SP 800-131A",
        Some("my_app.crypto.aes256_gcm"),
    ),
)
@retracted_as_of(date: "2024-03-15")
module my_app.crypto.des_legacy;

4.9 Obsolete(reason: Text, replacement: Maybe<Text>) — (legacy)

When: scheduled for removal. Less strict than [✗] Retracted: the artefact still functions but is expected to be replaced.

Why retained. A staged-removal lifecycle stage is genuinely useful — Retracted is "do not cite", Obsolete is "still callable, but cite the replacement going forward". Existing cogs use Obsolete for graceful migration paths where breaking callers in one release would be impractical. Retained pending a future RFC that folds Obsolete into Retracted with a @migration_window(release: "...") annotation.

Replacement guidance. New code SHOULD prefer Retracted(reason, Some(replacement)) for explicit withdrawals. For migration paths where the artefact must remain callable for one or more release cycles before final removal, document the window explicitly in the reason field and use Retracted(...) with the replacement pointer — most consumers will read the reason and migrate.

Audit treatment. Lint warning, not error. Cogs declaring Obsolete(...) are listed in the audit-bundle's legacy_status section; the audit gate emits a warning but does not block release. Citing an Obsolete(...) cog is allowed at compile time (unlike Retracted which produces AP-033).

5. Compile-time checks summary

The Verum compiler enforces the following Lifecycle-related checks:

Check	Anti-pattern	When it fires
Citing cog has lower rank than cited	AP-009 LifecycleRegression	direct citation
Citing chain exposes a low-rank link	AP-024 TransitiveLifecycleRegression	transitive walk
Citing a [✗] cog	AP-033 RetractedCitationUse	direct citation
[H] Hypothesis without @plan	AP-034 HypothesisWithoutMaturationPlan	declaration site
[I] Interpretation in strict: true	AP-035 InterpretationInMatureCorpus	declaration site
Lifecycle missing from strict: true cog	ATS-V-LIFECYCLE-MISSING (declaration error)	declaration site
Lifecycle.Theorem cog whose body lacks @verify(...)	ATS-V-LIFECYCLE-UNDERSPECIFIED	declaration site

All of these emit at compile time. There is no runtime cost.

6. Audit-time enumeration

verum audit --arch-corpus enumerates every annotated cog with its CVE glyph, its rank, and its citation graph. The output is suitable for archival in audit chronicles:

$ verum audit --arch-corpus

corpus: 267 annotated cogs
  [T] Theorem        : 89   (33%)
  [D] Definition     : 121  (45%)
  [C] Conditional    : 31   (11%)
  [P] Postulate      : 17   (6%)
  Plan (legacy)      : 4    (1%)
  [H] Hypothesis     : 4    (1%)
  [I] Interpretation : 0    (0%)  ✓ mature corpus
  [✗] Retracted      : 1    (0%)
  Obsolete (legacy)  : 0    (0%)

regression edges: 0   (✓ Lifecycle poset honoured)
retracted citations: 0   (✓ no [✗] cited)

audit duration: 1.4s

The "mature corpus" badge appears when [I] count is zero. A non-zero [I] count in strict mode is a build failure; in permissive mode it is a hint.

7. Programmatic access

The Lifecycle variant exposes two methods used by the audit pipeline and by tooling:

• lifecycle.tag() — returns a stable single-token string ("theorem", "definition", "conditional", "postulate", "plan", "hypothesis", "interpretation", "retracted", "obsolete").
• lifecycle.cve_glyph() — returns the canonical glyph as a string ("T", "D", "C", "P", "Plan", "H", "I", "✗", "O").
• lifecycle.rank() — returns the integer rank used by LifecycleRegression.

Tooling that consumes audit output should prefer these accessors over re-deriving the values from the variant tag.

8. Cross-references

• CVE overview — the universal correctness frame.
• CVE — seven canonical symbols — the glyph reference.
• CVE — seven layers — where Lifecycle sits in the layered application of CVE.
• Shape — the aggregate carrier of which Lifecycle is one field.
• Anti-pattern AP-009 LifecycleRegression
• Anti-pattern AP-033 RetractedCitationUse
• Anti-pattern AP-034 HypothesisWithoutMaturationPlan
• Anti-pattern AP-035 InterpretationInMatureCorpus
• Anti-pattern AP-024 TransitiveLifecycleRegression