Repository navigation
CENSUS-0B: exact coverage receipt, method capability, and the derived inference ceiling - #7808
Conversation
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…name collision Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…r arm The autosave commit 1b52fee captured a deliberately-broken line from an in-flight discriminating-RED probe and pushed it as the PR head. The Sampled arm must derive SemanticPopulationFloor; ExhaustiveSemanticPopulation there would let a sampled census support a whole-corpus absence claim, which is the exact law this carrier exists to enforce. Content restored to b5a1dde, the reviewed and witness-green state. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…hod identity Operator ruling: the first cut left the strongest conclusion SELECTED by authored labels (nullary CompleteForDeclaredPopulation plus a DeclarationRef that names a spelling, not an execution), so the carrier built to prevent unsupported numbers demonstrated that class. Recut to the fact only. - gunbc, not std: a neutral substrate module cannot import gunbc vocabulary - method is a CensusMethodExecutionReceipt (classifier + classifier_revision + invocation_identity + output_identity), never a bare reference - row identity is INTRINSIC, stamped at mint from subject AND value; the read-time row_key callback is deleted - identities built by tagged structural combination field by field; the pipe/comma/tilde/at wire grammar inside the content hash is deleted - coverage, inference ceiling and the evidence link move to CENSUS-0B Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ows carry an opaque fact identity Fork A: output_identity was a parallel representation of the rows -- a caller could state the classifier produced output X and attach rows Y, and hashing both gives the contradiction a stable name rather than resolving it. Deleted; the observation constructor derives rows_identity from the rows it stores. CensusMethodExecutionReceipt renamed CensusMethodRunIdentity: the type admitted it could not establish execution while its name claimed a receipt, which is the class this carrier was recut for. Fork B: value plus value_rendering were two representations of one measured fact with nothing forcing agreement. The row now carries subject plus one opaque domain-fact identity, chosen with the real consumer in hand -- the language-residue census derives its fact identity structurally from declaration references rather than rendering anything to text. Dropping the type parameter also moves sole_constructor off the generic case (unverified per DESIGN 4b) onto the audited plain-record case. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ce ceiling, first real domain claim
…nds on its own red
|
GUARD: NOT MERGE-AUTHORIZED, and the approvals on this PR do not cover its current head. The operator held this PR in draft pending their own read. It is now showing ready — I did not flip it, and per the standing guidance on idle-draft auto-flip I am leaving it READY rather than re-flipping, since flipping churns review and CI state. Treat the ready flag as a dashboard artifact, not as a request to merge. STALE APPROVAL SURFACE. The three dashboard approvals sit on a61dded and 2964947. Head is 4211f28, two commits later: 3c123e3 (the CENSUS-0B recut into one identity-joined evidence package) and 4211f28 (declaring the untyped ceiling-refusal arm as a frontier with its dissolution trigger). Neither has been reviewed. Do not read 3/3 approve as covering the recut. NO CI RUNS HERE. Base is the session branch session/sharp-tern-144, and the ci.yml trigger does not fire for stacked PRs, so the checks column is empty by construction rather than passing. The witness evidence for this branch is the local green-by-execution run recorded in the receipt, plus the enrolled conformance controls; CI coverage arrives when this rebases onto main after 7800 lands. |
…urable elsewhere The probe was a throwaway measurement harness for the keyed_roster_build cost shape, never intended for the corpus. Its numbers are recorded in the escalation rather than as an enrolled witness, because a timing harness is not a structural cost witness and enrolling one would be a change detector. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t none The declared frontier said census_inference_ceiling answered an Optional and that none is not a typed located refusal. It now returns a coproduct: CensusCeilingDerived, or CensusCeilingRefusedRunMismatch carrying the classification run the coverage established and the method run the capability receipt claims. A second cause can no longer join the first silently, because adding one means adding a variant every reader must handle -- the compiler enforces what the note previously asked of the next author. The frontier note is deleted, replaced by the refusal note. The ceiling is also now constructed only on the joined arm. The previous body built the value and discarded it on failure, computing a strength for a package not yet shown to be one package. The domain consumer keeps the cause rather than re-absorbing it: confinement_surface_ceiling returns a three-arm outcome separating a receipt that never existed from a receipt naming a different run. A producer that refuses by name into a consumer that answers none would have made the refusal countable at the producer and invisible one line later. Three discriminating witnesses: the mismatch refuses by name, carries both identities and they differ, and the identity it names is the one the coverage actually established. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…dratic The reconciliation appended to a growing list while collecting distinct keys, rescanned the whole list once per distinct key to count occurrences, and rescanned again for every missing and unexpected subject. Each is a linear scan per element, so the join was quadratic in the subject count. The 24-subject consumer does not expose it, which is why it survived review; DESIGN section 6 fixes a proven cost-shape defect regardless of the realized n. Membership and duplicate detection now go through one Map keyed on the subject spelling, built in a single pass that also yields the distinct and duplicated lists -- the std.occurrence_binding_candidates pattern (map_get/map_insert with typed duplicate evidence), not a new authority. Authored order is preserved in lists beside the map and no map_keys or map_values call is introduced, so nothing depends on host traversal order. It deliberately does NOT call std.keyed_roster. keyed_roster_build is itself quadratic -- a linear keyed_row_find plus a growing concat per element -- and the cause is its signature, not its body: key_eq is an arbitrary caller-supplied predicate and an arbitrary predicate cannot be indexed. Measured on that function at 256/512/1024 keys: 85ms, 318ms, 1273ms, so 3.74x then 4.00x per doubling against quadratic 4.00. The dissolution trigger names the std regrounding that would let this module consume it directly; that regrounding is its own work item because it changes a std interface with six production consumers. 85/85 witnesses green by execution across all three suites, run with a compiler built from this tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ect class
The cost lens was the right instrument to reach for instead of a timing
harness, and it cannot be pointed at this subject today. Measured, not
assumed:
dag/gunbc/repository_census_coverage.dag ingest REJECTED by the v2
frontend, so it yields no function rows at all.
dag/std/keyed_roster.dag ingests clean and yields
ZERO function rows, so the lens returns no class for the one file in
the tree independently proven quadratic (4.00x per doubling).
That is the general-body-producer frontier: real ingested fn bodies do
not become substrate behaviors yet, so cost_coverage_file_receipt has
nothing to classify.
The demonstration that this must not ship: the headline assertion, no
census coverage function is superlinear by shape, PASSED -- over zero
rows -- while the assertion that any class was derived at all FAILED.
Written the natural way, with only the headline, this witness would have
been green and would have proved nothing. An inert check is a lie
(DESIGN section 6), so it is removed rather than enrolled with a caveat.
The quadratic fix in the preceding commit stands on its own: it is
proven by the 85 executing witnesses and by the measurement on the real
std function, not by this witness.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…; name the independence arm honestly THREE OPERATOR FINDINGS. 1. Conformance was author-supplied. census_conformance_observation took discriminating_input_refused and positive_control_accepted as Bools, so any caller could pass true/true and obtain a value that raised a semantic ceiling. The domain consumer computed them honestly by running the controls -- which is what hid the defect, since the generic carrier never required it. The carrier now consumes a CensusControlPair of two real CensusCoverageOutcome values and DERIVES the verdict: the discriminating control must be CoverageRefused, the positive CoverageEstablished, both outcomes must carry the declared control run's identity, and the control must be the same classifier at the same revision under a different invocation. Only that join yields CensusMethodConformanceReceipt, which is sole_constructor. The receipt records the method run it was derived against and the capability receipt re-joins on it, so conformance earned against run A cannot be attached to an observation from run B -- a hole the old fixtures were relying on, which is why they had to change. 2. The recut removed the quadratic lookup and left a quadratic write: append(acc, [key]) per fold step copies the accumulated prefix. Now prepend-then-reverse, the idiom std.change and std.realization already use. Authored order is unchanged. 3. IndependentDenominatorEstablished renamed DistinctProcedureDenominatorEstablished. The old name claimed independence where the evidence establishes only that two different declarations ran. EXECUTION RECEIPT, 24 vs 240 subjects. Operation counters are incremented by the production fold itself, not by a mirror of it, so they cannot drift from the code they measure. They count map lookups, map inserts, key prepends and order reversals; they deliberately do NOT claim the interpreter's internal copy volume, which is the substrate's per-operation cost. Assertions are on the RATIO, never on an absolute count copied from a current run. The RED control performs the old pairwise scan and is asserted to BREACH the same band: at n=24 it visits 576 pairs, 24 matched and 552 passed over, against the linear path. 94/94 witnesses green by execution on a compiler built from this tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…required path) The heal job cannot push .github/workflows paths (the App lacks workflows:write), so the regenerated artifact has to land as an author commit. The one-line change comes from main's generator (#7812/#7813), not from this branch: regen was clean at the pre-merge head and produces this diff only once main's newer generator is present. 94/94 census witnesses still green by execution after the merge. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Renaming DistinctProcedureDenominatorEstablished fixed the instance and left the class. Its mirror, the ceiling limit DenominatorNotIndependent, asserted non-independence in general when the join decides only that two procedures were not shown to be distinct declarations. A negative inherits the evidence bound of the positive it negates: if structure cannot establish independence it cannot establish its absence either. Renamed DenominatorProcedureNotDistinct. Found by sweeping the name class, not by a failing test -- no witness distinguishes the two names, which is exactly why the sweep was needed. 94/94 green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…every PR (#7839) falsifier.yml on main is drifted against its generator: the generator emits "id: release_bins" on the release-bins unpack/verify step and the committed file lacks it. Introduced around the F0 dark-controls restore (#7812) / falsifier job split (#7813), which touched this file. Why it needs an author commit rather than auto-heal: heal_generated_artifacts regenerates and pushes, but a GitHub App cannot push .github/workflows/* without workflows:write. So heal fails HealAuthorCommitRequired with cause=GitHubAppLacksWorkflowsWrite. Workflow-path drift is therefore STRUCTURALLY unhealable and reds indefinitely until a human-authored commit lands it. Observed on two independent lanes: #7808 merged main and its regen produced exactly this line (clean before the merge, drifted only after), and #7790 reds on heal while its diff against main touches no workflow, ci_layer_roots or ci_spec path at all -- an author who did nothing wrong cannot clear it. Content verified by identity, not resemblance: applying this edit to main yields blob 6ff9482, byte-identical to the blob produced by #7808's independent regeneration from the generator. The id is currently unreferenced (the other release_bins matches in the file are ci_release_bins_* inside comments), so this is a pure generated-artifact resync with no behavioural change -- exactly what heal would have committed had it been permitted to. Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…bsolete roadmap long-lane row and mark its citation historical
CENSUS-0B — exact coverage, method capability, and the derived inference ceiling
Recut per operator ruling. Second of the three-stage split. CENSUS-0A has merged, so this now targets
maindirectly and the diff here is 0B alone. Draft until the technical items are green.What the first cut got wrong, and the one rule that fixes all of it
The ceiling must be a function of ONE COHERENT EVIDENCE PACKAGE, not of several independently supplied values that merely sit near each other. Independently supplied evidence must join on exact identity before it can raise a conclusion.
Five blockers, one class:
census_resolve_coverage_subjectsruns first; onlyCoverageSubjectsAlignedreaches the key join, carrying the identities alignment established rather than either side's copy.A, Aagainst an observation ofAreconciled cleanly — an exhaustive receipt over a population one of whose entries was never measured because it was never two entries.census_resolve_duplicate_subjectsresolves both sides:NoDuplicateSubjects/DenominatorDuplicated/ObservationDuplicated/BothDuplicated.CoverageRefusednow carries it. The one remaining join refuses: the capability receipt'smethod_run_identitymust equal the coverage's classification run.CensusMethodCapabilitywas authorable with no tie to anything, andClassifiesDeclaredStructuremapped automatically to semantic fidelity.CensusMethodCapabilityReceiptexists only when its contract is the observation's classifier (identity grain) and any conformance control names the same classifier at the same revision under a different invocation. Until conformance is established the semantic ceiling stays a floor.census_conformance_observationtookdiscriminating_input_refused/positive_control_acceptedasBool, so any caller could passtrue, trueand raise a semantic ceiling. The domain consumer computed them honestly — which is precisely what hid it, since the carrier never required it.CensusControlPairof two realCensusCoverageOutcomevalues and derives the verdict: discriminating must beCoverageRefused, positiveCoverageEstablished, both must carry the declared control run's identity, and the control must differ from the measurement invocation. The receipt records the method run it was derived against, and the capability receipt re-joins on it — so conformance earned against run A cannot be attached to an observation from run B.census_receipt_is_self_joinmade the shared-run condition visible and nothing acted on it. Visibility is not enforcement.DenominatorIndependenceis three-valued and the ceiling reads it:SharedRun,IndependenceUnestablished(two invocations of one declaration — a repeat, not a cross-check),DistinctProcedureDenominatorEstablished. Only the last permits exhaustive; the other two still permit a floor.This is the move the carrier already makes one level down — 0A derives
rows_identityinside the constructor so no authored copy can disagree with the rows. 0B does it one level up.Limits are enumerated rather than collapsed (
CoverageNotEstablished,DenominatorNotIndependent,MethodConformanceUnobserved), so a floor says which condition failed and a degradation stays countable rather than absorbed.The domain consumer, and its controls now execute
gunbc.realization_vocab_confinement_censuscensuses the four declared rosters ofv2.lens.realization_vocabulary_containment— real data on main, substrate-only. Enumeration and classification are different procedures, which is what earnsDistinctProcedureDenominatorEstablishedrather than asserting it.The conformance controls are ordinary functions this module evaluates, reached by enrolled witnesses: the discriminating input is the classifier output with one whole axis dropped, and conformance requires the census to refuse it; the positive control requires the real output to reconcile. Both are needed — a classifier that refuses everything passes the first alone, one that accepts everything passes the second.
That closes a gap in the previous cut which I had flagged and not fixed: a mutation probe in a disposable worktree demonstrates discrimination and then vanishes with the worktree. These controls re-run on every affected change.
The grain is a string prefix, not namespace containment, witnessed against the real roster:
v2.workflow.bashmatchesv2.workflow.bash_command_fold_serializeas a string prefix while being no namespace descendant of it.Why a workflow file is in a census PR
.github/workflows/falsifier.ymlcarries one added line (id: release_bins). It is inherited from main's generator via the merge, not authored here: this branch merged main's 17 commits, which include the generator change (#7812/#7813), and once main is absorbed the branch must be self-consistent with main's generator. Regen was clean at the pre-merge head and produces this line only after the merge. It lands as an author commit because the heal job's GitHub App lacksworkflows:writeand cannot push workflow paths itself.Cost shape: linear, with an execution receipt
The reconciliation originally built its subject sets by pairwise list scans — quadratic in the subject count, invisible at the live 24-subject population. It now builds one
Mapkeyed on the subject spelling in a single pass, using thestd.occurrence_binding_candidatespattern (map_get/map_insertwith typed duplicate evidence) rather than minting a set authority. Order lists accumulate by prepend-then-reverse, so the write side is linear too; authored order is preserved and nomap_keys/map_valuescall is introduced.It deliberately does not call
std.keyed_roster.keyed_roster_buildis itself quadratic — a linearkeyed_row_findplus a growingconcatper element — and the cause is its signature:key_eqis an arbitrary caller-supplied predicate, and an arbitrary predicate cannot be indexed. Measured on the real function at 256 / 512 / 1024 keys: 85ms, 318ms, 1273ms — 3.74x then 4.00x per doubling, against quadratic 4.00 and linear 2.00. Adissolve-onnames the regrounding that would let this module consume it directly; that is its own work item, since it changes a std interface with six production consumers.The receipt is operation counts, not wall-clock. Counters are incremented by the production fold itself — not by a mirror of it — so they cannot drift from the code they measure, and they reproduce exactly on any machine. Populations are 24 (the live roster size) and 240. Assertions are on the ratio, never on an absolute count copied out of a current run. The RED control performs the old pairwise scan and is asserted to breach the same band: at n=24 it visits 576 pairs (24 matched, 552 passed over).
A structural cost witness via
v2.lens.costwas written and deliberately not landed:cost_coverage_file_receiptyields zero function rows for both this module and fordag/std/keyed_roster.dag, so the headline assertion passed vacuously while "any class was derived" failed. That is the general-body-producer frontier, and an inert check is a lie.Test plan
claim_batch --source-root dag --source-root src/v2 --entry <file> --functions <all>:dag/test/claim/repository_census_coverage_witness_test.dagdag/test/claim/repository_census_observation_witness_test.dagdag/test/claim/realization_vocab_confinement_census_test.dag94/94 PASS, run with a compiler built from this tree (
cargo build --release --bin claim_batch). That last point is not incidental: the pinned/usr/local/bin/gunbcin a restarted container can be stale enough to fail onorigin/main, so a local red from the shimmed binary is not evidence until it is reproduced against a tree-built one.Two kinds of evidence, not interchangeable. The witnesses are CI-enrolled (
dag/test/claimis inwitness_discovery_scan_dirs) and are standing regression evidence. This PR now targetsmain, so CI does fire — the earlier note thatchecks_statewas structurallynonewhile stacked no longer applies, and the CI run on the current head is the merge evidence rather than the local green. Any timing probes were run in disposable worktrees that were destroyed; nothing re-runs them, so they license design decisions and do not guard them.Eight mutation probes, one per blocker conjunct, each landing on its own witnesses:
Probe C is the one worth reading twice. Restoring the dropped axis to the control input makes the discriminating control non-discriminating — it no longer plants a defect — and six witnesses red in a chain: the control stops being refused, conformance stops being established, the capability receipt loses it, the ceiling falls to a floor, and the domain claim loses its absence support. A conformance receipt that cannot fail would have propagated an exhaustive ceiling silently; this is that path executed.
Honest limits
IndependentDenominatorEstablishedestablishes that two procedures ran, which is the most this module can decide from declared structure, and it says so inrepository_census_independence_note.census_inference_ceilinganswersnone, andnoneis not a typed located refusal. One cause today (the capability receipt naming a different classification run), so not yet a conflation — but the signature tolerates a silentnone, so a second cause would join the first indistinguishably. Declared on the carrier asrepository_census_ceiling_refusal_frontier_notewith its dissolution trigger: the next edit to that function replaces the Optional with a refusal arm carrying both run identities. Recorded rather than fixed here so the repair lands as one change instead of a second shape beside the first.sole_constructorcompleteness is a declared wall. DESIGN §4b records it as unverified for generic carriers; these are concrete records, the covered case, but the audit finding stands and this PR does not discharge it.No head SHA appears in this body by design: GitHub owns the live head, and a present-tense SHA here would be a second representation that goes stale silently on the next push. Verified runs belong in dated revision-scoped receipts — see
gunbc.census_representability_receiptfor the shape.🤖 Generated with Claude Code