Skip to main content

CVE — three axes (C / V / E)

Document CVE self-application​

ShapeDeclarations {
    purpose: Some(Purpose {
        role: "axis-by-axis specification of C, V, E with independence demonstration",
        k_min: CveThresholdK.FullWitness,
        v_min: CveThresholdV.NamedCertification,
        e_min: CveThresholdE.StructurallyReady,
    }),
    substrate: Some(CognitiveSubstrate.AnalyticDecompositional),
    anchoring: Some(FormalAnchoring.CurryHowardLawvere),
    e_sense:   Some(ExecutabilitySense.StructuralReadiness),
    self_reference: None,
}

Lifecycle: [D] Definition (defines the three axes; not a theorem to be proved). Independence demonstration in §4 is [T] Theorem (a witness exists for every cell of the truth-table).

The Constructive / Verifiable / Executable frame stands or falls on the independence of its three axes. If any one axis were derivable from another, the framework would collapse to a two-dimensional grid; the seven canonical statuses would correspondingly collapse to four. The independence is therefore not aesthetic — it is the structural property that makes the framework load-bearing.

This page documents each axis precisely, gives examples across the full present/partial/absent range, and demonstrates the independence by exhibiting artefacts at every meaningful combination.

1. Axis 1 — Constructive (C)​

A claim is constructive when there is a procedure that produces a witness — a value, a proof term, a computational object — the language can manipulate as a first-class entity.

1.1 Range of constructiveness​

ModeMeaningVerum surface
PresentConstructor realised; witness computable.fn id<T>(x: T) -> T { x } — the polymorphic identity is a constructor.
PartialConstructor formulated; witness type exists but no inhabitant exhibited.type Halts(p: Program); (no constructor)
AbsentNo constructor, even partial; the claim is purely descriptive."This problem is hard."

1.2 Why constructiveness matters​

A theorem proved by classical reductio without exhibiting a witness is true but not constructive. In a verification context, the distinction has real consequences:

  • A constructive proof of ∃ x. P(x) lets the program use the witness — extract it, ship it, run it.
  • A non-constructive proof tells the program the witness exists but offers no way to obtain it.

Verum's verum extract + program-extraction pipeline relies on constructiveness. A [T] Theorem with classical-only proof content extracts to the meta-theory but not to runnable code.

1.3 Constructiveness vs proof relevance​

Constructiveness is not the same as the propositions-as-types discipline of proof-relevance. A propositionally-relevant proof may still be classical (using LEM internally); a constructive proof may be propositionally-irrelevant (built in Prop rather than Set/Type).

Verum carries both distinctions independently:

  • Constructiveness lives on the C axis.
  • Proof relevance lives in the universe-level discipline (Type vs Prop).

The two axes interact at extraction time: constructive + relevant proofs extract cleanly; non-constructive + irrelevant proofs do not extract at all. Refer to verification → program extraction for the full extraction matrix.

2. Axis 2 — Verifiable (V)​

A claim is verifiable when there is an effective procedure — a type checker, a kernel, an SMT replay, a decision procedure — that, given a candidate witness, decides whether it satisfies the claim.

2.1 Range of verifiability​

ModeMeaningVerum surface
PresentAlgorithmic check, bounded time.Int { self > 0 } — the SMT layer decides instances.
ConditionalEffective only under stated assumptions."Halting on terminating inputs" — conditional check.
ExternalCheck delegated to a trusted external base.[P] Postulate citing a published theorem.
AbsentNo check, even partial.A claim asserted without procedure.

2.2 Verifiability is the audit substrate​

Verifiability matters because the audit of a claim depends on re-running the verifier. A claim that is constructive but not verifiable is useful (the witness exists) but unauditable — no third party can confirm it without re-deriving the witness.

This is why Verum's [T] Theorem status requires both C and V: the theorem must be constructively provable and the proof must be re-checkable by a procedure — typically the trusted kernel following an SMT cert replay.

2.3 The verifier hierarchy​

Verum's verification ladder (nine semantic strategies, see verification → gradual-verification) is precisely a hierarchy of V:

  • runtime — verifiability is "the assertion runs at runtime"; weakest V.
  • static — dataflow-level checks; type-level only.
  • fast — bounded SMT.
  • formal — portfolio SMT; the typical V for shipped code.
  • proof — kernel-checked tactic proof.
  • thorough / reliable / certified / synthesize — progressively stronger V.

A claim's strongest V is the strongest strategy that admits it. Verum aggressively reports the strongest V for each artefact — a claim that admits formal is recorded as such, not silently demoted to runtime.

3. Axis 3 — Executable (E)​

A claim is executable when the constructor reduces to runnable machine code — bytecode, native, GPU kernel — without losing the property the claim asserts.

3.0 The three senses of executability​

The term "executable" in everyday usage carries several operationally distinct senses. Conflating them is a typical source of unclear judgements that mask the real state of an artefact. The CVE-E axis rests on one of these senses and must distinguish it from its neighbours. Verum's ExecutabilitySense enum (core/architecture/types.vr:532, mirrored in crates/verum_kernel/src/arch.rs:877) exposes all three; the soundness pin executability_sense_canonical_unique (core/architecture/types.vr:1364, cross-side asserted at crates/verum_kernel/tests/k_arch_v_alignment.rs:515) enforces that exactly one of them (StructuralReadiness) anchors CVE-E.

SenseOperational meaningCanonical for CVE-E?
StructuralReadinessThe artefact admits a working representation deployable in any environment of the declared class. Readiness as a property of the artefact, not the fact of present execution.✓ — THIS IS the content of the E axis.
CurrentExecutionThe artefact is, at this moment, running in production: the program executes in production, the law applies in court, the model serves requests.Stronger; characterises full L0 maturity ([T] Theorem in the seven-symbols sense), but is NOT the E axis.
PostFactumChronicleAccumulated history of past execution: execution logs, the artefact's historical track.Material for the antifragility chronicle (see overview §1.2 erosions and chronicle of architectural revisions), NOT the E axis.

Typical conflations. "The artefact is executable because it once executed" (the third sense usurps the first); "the artefact is executable because right now it is running" (the second usurps the first, even though current operation may not imply structural readiness for fresh deployment); "the artefact is executable because in principle it could execute" — without confirmation of structural readiness — is rhetoric without content.

The CVE-audit of axis E always checks the first sense: by the description of the artefact it is possible to construct or deploy a working representation in a suitable environment without recourse to external unverifiable resources. That is "working representation" in the canonical formulation.

The canonicality is load-bearing: a [T] Theorem requires structural readiness, not "currently running" or "ran in the past". Citing past execution as evidence of E is the typical entry-point for the AP-037 BoundlessAudit register collision — an audit that reads "executable" while the artefact is not redeployable.

The kernel exposes an is_canonical_e accessor on ExecutabilitySense. Among its three constructors only StructuralReadiness is canonical-E:

Constructoris_canonical_e()
StructuralReadinesstrue
CurrentExecutionfalse
PostFactumChroniclefalse
// Verum side — declare the sense explicitly when it matters
@arch_module(
    lifecycle: Lifecycle.Theorem("v1.0"),
    declarations: ShapeDeclarations {
        e_sense: Some(ExecutabilitySense.StructuralReadiness),
        ..ShapeDeclarations::empty()
    },
)
module my_app.cog;

3.1 Range of executability​

ModeMeaningVerum surface
PresentConstructor extracts to a binary running at native (or near-native) speed.A @verify(formal) function with @extract(rust).
TrivialExecutability is not at issue; the claim is a definition or boundary.type X is …; declaration.
AbsentConstructor exists in the meta-theory but does not reduce to runnable code.Many classical-mathematics theorems whose proofs use AC.

3.2 Executability lands verification​

Executability is what makes verification land in production. A proof certificate that does not reduce to executable code lives forever in the proof corpus but never affects the running program. Verum aggressively prefers C-and-V-and-E-positive proofs because those are the ones that ship.

This is also why Verum's program-extraction pipeline is a first-class subsystem rather than a side feature: the extraction is the E axis made operational.

3.3 Executability vs efficiency​

Executability is binary (does the program run? yes/no). Efficiency is orthogonal — a slow program is still E-positive. Verum tracks performance as a separate concern via the verification → performance gates.

4. Demonstrating the independence​

The three axes' independence is demonstrable by exhibiting artefacts at every interesting combination.

CVEGlyphReal-world example
✓✓✓[T] TheoremA @verify(certified) function with extraction.
✓trivial✓[D] Definitiontype DatabaseUrl is Text { … };.
cond.cond.cond.[C] ConditionalA kernel result that holds only on POSIX hosts.
✓external✓[P] PostulateJoux 2009 lower bound, cited but not internalised.
partialabsentabsent[H] HypothesisAn unproven design idea with a @plan(...) attribute.
absentabsentabsent[I] InterpretationPure prose stub awaiting realisation.
✓✓absent(rare)Pencil-and-paper proof exposed in the corpus without extraction.
absent✓✓(rare)A computable check with no witness — e.g., a runtime assertion.
✓absent✓(rare)Code that runs but has no spec — typical "TODO: prove later".

The "rare" rows are real but uncommon. The seven canonical glyphs cover the common productive combinations; rare combinations exist in the wild but typically migrate to one of the canonical seven within the project's lifetime.

The simple test of independence: exhibit two artefacts that agree on two axes and disagree on the third. All three axes admit this, so all three are independent.

5. Cross-references​

Each cross-reference carries an italicised relation marker: frame (the canonical statement this page specialises), specialisation (a more specific case of this page's content), refinement (adds detail without changing scope), instantiation (concrete application of this page's content), operationalisation (mechanises this page's content), or pin (cross-side invariant test).