Enum GateExtra

Source

#[non_exhaustive]pub enum GateExtra {
Show 14 variants    DuplicateStems {
        divergent: usize,
        baselined: usize,
        unbaselined: Vec<String>,
        stale: Vec<String>,
        divergent_stems: Vec<String>,
    },
    Sigma {
        entity_types: usize,
        roles: usize,
        symbols: usize,
        contracts_checked: usize,
        violations: usize,
        formal_total: usize,
        formal_prose: usize,
    },
    Relations {
        relations_n: usize,
        contracts_with_relations: usize,
        roles_used: Vec<String>,
        cycles: Vec<String>,
        legacy_depends_on: usize,
        legacy_unresolved_depends_on: usize,
        violations: usize,
    },
    Evidence {
        contracts_checked: usize,
        contracts_with_evidence: usize,
        entity_types_checked: usize,
        entity_types: Vec<String>,
        levels_source: String,
        by_level: Vec<String>,
        census_git_sha: Option<String>,
        unresolved_git_shas: usize,
        violations: usize,
    },
    ValidUnder {
        worlds: Vec<String>,
        contracts_checked: usize,
        kernel_contracts: usize,
        contracts_with_valid_under: usize,
        contracts_without_valid_under: usize,
        baseline: Option<usize>,
        by_world: Vec<String>,
        violations: usize,
    },
    TheoremPairing {
        lean_base: String,
        book_pages: usize,
        theorem_modules: usize,
        paired: usize,
        unpaired_theorem_modules: usize,
        baseline: Option<usize>,
        unpaired: Vec<String>,
        violations: usize,
    },
    DependsOnPresent {
        contracts_checked: usize,
        kernel_contracts: usize,
        contracts_without_depends_on: usize,
        baseline: Option<usize>,
        violations: usize,
    },
    ProvedIsDerived {
        summary: Option<String>,
        summary_error: Option<String>,
        summary_green: bool,
        contracts_checked: usize,
        proved_claims: usize,
        underived_proved_claims: usize,
        baseline: Option<usize>,
        underived: Vec<String>,
        violations: usize,
    },
    ChallengeFresh {
        lean_dir: String,
        files: usize,
        stale: Vec<String>,
        unrestated: Vec<String>,
    },
    Shapes {Show 25 fields
        shapes_n: usize,
        focus_nodes_n: usize,
        pc_shape: String,
        plant_violations: usize,
        violations: usize,
        warnings: usize,
        by_shape: Vec<String>,
        triples: usize,
        armed_shapes: Vec<String>,
        not_armed_shapes: Vec<String>,
        declines: Vec<String>,
        unarmed_violations: usize,
        by_entity_type: BTreeMap<String, usize>,
        controls: Box<ShapesControls>,
        receipts: usize,
        witnesses: usize,
        hex_mismatches: usize,
        unmeasured_rows: usize,
        w3c_cases_passed: usize,
        w3c_cases_n: usize,
        counters: Box<ShapesCounters>,
        release: Option<Box<ReleaseStats>>,
        readme: MeasuredSet,
        claude_md: MeasuredSet,
        ratchets: Ratchets,
    },
    Consistency {
        checkable_n: usize,
        units: usize,
        unencoded_edges: usize,
        pc_checker: String,
        core: Vec<String>,
        violations: usize,
        witness: WitnessReport,
    },
    Refines(Box<RefinesCounters>),
    Bindings(Box<BindingsCounters>),
    Refinement(Box<RefinementCounters>),
}

Expand description

Out-of-band structured detail for gates that post-date the frozen GateDetail vocabulary.

This type did not exist in provable-contracts 0.3.1, so no 0.3.1 program names it and none can match it. That is what makes it extensible where GateDetail is not, and it is #[non_exhaustive] from birth so the next post-0.3.1 gate does not have to repeat this exercise.

Variants (Non-exhaustive)§

This enum is marked as non-exhaustive

Non-exhaustive enums could have additional variants added in future. Therefore, when matching against variants of non-exhaustive enums, an extra wildcard arm must be added to account for any future variants.

§

DuplicateStems

PV-DUP-001: contract stems claimed by several files with divergent content.

Fields

§divergent: usize

Total ambiguous stems found in the tree.

§baselined: usize

How many of those are recorded in the ratchet baseline.

§unbaselined: Vec<String>

Ambiguous stems NOT in the baseline — these fail the gate.

§stale: Vec<String>

Baseline entries that no longer diverge — these fail the gate too.

§divergent_stems: Vec<String>

Every ambiguous stem, with its variant count and paths, for the report.

§

Sigma

ONT-2b: what Σ declares and what the corpus was checked against.

Fields

§entity_types: usize

entity_types Σ declares.

§roles: usize

roles Σ declares.

§symbols: usize

symbols Σ declares.

§contracts_checked: usize

Contract files read (never counting ontology.yaml itself).

§violations: usize

Findings: undeclared entity types, undeclared roles, undeclared glyphs.

§formal_total: usize

formal: expressions read.

§formal_prose: usize

Of those, how many carry NO symbol Σ declares — the formal_prose debt, shrink-only.

§

Relations

ONT-4: the corpus’s typed relations, checked against Σ’s roles.

Fields

§relations_n: usize

Typed edges after symmetric closure.

§contracts_with_relations: usize

Contracts carrying a relations: block.

§roles_used: Vec<String>

role=count per role used.

§cycles: Vec<String>

Cycles through acyclic roles, as role: a -> b -> a.

§legacy_depends_on: usize

metadata.depends_on edges, read and counted, never rewritten (R-5).

§legacy_unresolved_depends_on: usize

Of those, how many name no contract — ratcheted shrink-only in the baseline.

§violations: usize

Findings.

§

Evidence

ONT-8: one evidence block — PROV-O names, one L-enum, every entity type.

Fields

§contracts_checked: usize

Contract files read.

§contracts_with_evidence: usize

Of those, how many carry an evidence block.

§entity_types_checked: usize

Distinct entity.type among the contracts carrying evidence — counted, never branched on (R-17).

§entity_types: Vec<String>

Those types, sorted.

§levels_source: String

enum: levels are parsed through ProofLevel, never matched against a list kept in the gate.

§by_level: Vec<String>

level=count over the evidence blocks that passed every rule.

§census_git_sha: Option<String>

The census git_sha a [V] claim binds to; None (the 2026-09-16 ruling) binds it to the repository.

§unresolved_git_shas: usize

[V] shas git could not look for — non-zero makes the verdict Unknown{ToolAbsent}, never Pass.

§violations: usize

Findings.

§

ValidUnder

ONT-7: kernel-kind contracts carry a world index (metadata.valid_under.world, a key of Σ’s worlds).

Fields

§worlds: Vec<String>

The worlds Σ declares — the index a valid_under.world must resolve into.

§contracts_checked: usize

Contract files read.

§kernel_contracts: usize

Of those, kernel-kind and not a registry — the class the row obliges.

§contracts_with_valid_under: usize

Contracts (any kind) carrying metadata.valid_under.

§contracts_without_valid_under: usize

Kernel-kind contracts carrying none — the debt, shrink-only against the baseline.

§baseline: Option<usize>

The top-level contracts_without_valid_under in lint-baseline.json; None = not recorded.

§by_world: Vec<String>

world=count over the contracts whose valid_under passed every rule.

§violations: usize

Findings.

§

TheoremPairing

PVL-001 EV-11: Lean theorem modules named by a book page — the unpaired_theorem_modules ratchet.

Fields

§lean_base: String

The Lean base the modules were read under.

§book_pages: usize

.md pages read under the book roots.

§theorem_modules: usize

.lean files under <base>/ProvableContracts/Theorems/.

§paired: usize

Of those, named in full by at least one book page.

§unpaired_theorem_modules: usize

The debt, shrink-only against the baseline.

§baseline: Option<usize>

The top-level unpaired_theorem_modules in lint-baseline.json; None = not recorded (reported only).

§unpaired: Vec<String>

The unpaired modules, dotted, in byte order.

§violations: usize

Findings.

§

DependsOnPresent

PVL-001 EV-11: kernel-kind contracts with an empty metadata.depends_on — the ratchet.

Fields

§contracts_checked: usize

Contract files parsed.

§kernel_contracts: usize

Of those, kernel-kind and not a registry.

§contracts_without_depends_on: usize

Kernel-kind contracts whose metadata.depends_on is empty — the debt, shrink-only.

§baseline: Option<usize>

The top-level contracts_without_depends_on in lint-baseline.json; None = not recorded (reported only).

§violations: usize

Findings.

§

ProvedIsDerived

PVL-001 EV-8a (#4202): status: proved claims no green discharge-summary.json derives — the ratchet.

Fields

§summary: Option<String>

The summary read (beside the Lean base); None = no Lean base.

§summary_error: Option<String>

Why it derived nothing when it could not be read; None = it was read.

§summary_green: bool

Every Lean step ran and passed. Only a green summary derives a claim.

§contracts_checked: usize

Contract files parsed.

§proved_claims: usize

proof_obligations[].lean.status: proved claims.

§underived_proved_claims: usize

Of those, not derived — the debt, shrink-only against the baseline, and it must reach 0.

§baseline: Option<usize>

The top-level underived_proved_claims in lint-baseline.json; None = not recorded (reported only).

§underived: Vec<String>

The underived claims, as contract: theorem, in contract order.

§violations: usize

Findings.

§

ChallengeFresh

PVL-001 EV-7a (#4200): <lean>/Challenge/ against its regeneration (pv challenge check).

Fields

§lean_dir: String

The Lean dir judged.

§files: usize

Challenge files the contracts render.

§stale: Vec<String>

Extra, missing or differing files, one line each.

§unrestated: Vec<String>

Bound roots whose statement could not be lifted, as contract: fqn: why.

§

Shapes

ONT-4b: the shapes gate — every shape: block over the extracted graph, with the plant.

Fields

§shapes_n: usize

shape: blocks read.

§focus_nodes_n: usize

Distinct focus nodes across the shapes (the plant excluded).

§pc_shape: String

fired — the plant drew a violation; the gate never reaches Ran otherwise.

§plant_violations: usize

How many violations the plant drew.

§violations: usize

Corpus violations (the plant excluded).

§warnings: usize

Corpus warnings.

§by_shape: Vec<String>

shape=focus-count per shape.

§triples: usize

Triples in the extracted graph.

§armed_shapes: Vec<String>

ONT-4c1 (§3.9 per-shape arming): shapes that feed the verdict, in corpus order.

§not_armed_shapes: Vec<String>

Shapes computed and reported but not armed — their violations are in unarmed_violations.

§declines: Vec<String>

#3610: shapes that graded ZERO focus nodes, named — the reach the gate did not have.

A separate list from not_armed_shapes on purpose. “Not armed by policy” and “armed and measured nothing” are different facts, and folding the second into the first would file a vacuity as a deliberate choice — which is how the defect hid in the first place.

This carries EVERY shape that graded zero, armed or unarmed, and it is the only list any of them appears in: a vacuity is in neither armed_shapes (the tool’s claim about what it MEASURED) nor not_armed_shapes (a policy choice it never made).

The two differ in what they do to the verdict, not in whether they are listed here. An ARMED vacuity drives the verdict to Unknown(NoFocus) and the run declines — unless an armed shape that DID grade something found a violation, in which case the verdict is Fail (a measured violation outranks a vacuity, #3622). An UNARMED one leaves the verdict alone, because it never fed it. Both are named, because a reader needs to know the gate looked at nothing for them either way.

An earlier draft of this comment said an armed vacuity “does not reach here at all”, which was false — nothing returns early at the verdict, and both kinds reach this field. A quorum lane caught the sentence; the code beside it had the matching bug.

§unarmed_violations: usize

Violations from unarmed shapes (named in the findings as warnings; never in the meet).

§by_entity_type: BTreeMap<String, usize>

Focus nodes each extractor produced: pv-contract, gguf, apr-model.

§controls: Box<ShapesControls>

The positive controls (pc_extract, pc_shapes) and ONT-4c5’s capability_cells, boxed and FLATTENED: the JSON keys stay top-level where the §5 probes read them, and the variant stays under clippy’s large-enum-variant bound (it sat exactly at it before ONT-4c5).

§receipts: usize

Ladder receipt files read under evidence/dogfood/models/.

§witnesses: usize

Receipt rows whose sha256 equals a rung’s.

§hex_mismatches: usize

Receipt rows whose sha256 differs from the rung’s.

§unmeasured_rows: usize

Receipt rows without a sha256 (never a witness).

§w3c_cases_passed: usize

ONT-4b2: vendored W3C SHACL-Core cases that passed this run, and how many are vendored.

§w3c_cases_n: usize

§counters: Box<ShapesCounters>

The ONT-4b2 extractor counters and ONT-4d’s inheritance, FLATTENED into this object: the JSON keys (symbols_resolved, …, inherited_shapes_applied) are unchanged. They are boxed only so the variant stays under clippy’s large_enum_variant once ONT-4d’s two fields joined it.

§release: Option<Box<ReleaseStats>>

aprender#3715: what extract:release-evidence derived — absent unless a release subject was given.

§readme: MeasuredSet

ONT-4c (v4.14): the README claim commands a merge-path workflow runs — the MEASURED set F-33 compares.

§claude_md: MeasuredSet

ONT-4c (v4.14): the same for CLAUDE.md (extract:llm-context).

§ratchets: Ratchets

ONT-4c (v4.14): whether the measured-set ratchets (F-33 and F-34) were checked this run.

§