Repository navigation
feat(map): the intent layer: the specifications' intent against the map, and the conformance it found - #1055
Merged
Merged
Conversation
…the map
The map establishes what the code does. It never decides what the code ought
to do. The intent manifest (specs/requirements/INTENT_MANIFEST.tsv, the
owner-authorized home) says that, one row per requirement, symbol and build.
ci/intent_comparator.py maps each row's intent and the map's reading to an
outcome through one table, and the outcome to an action. The owner's policy
says which outcomes fail.
- MUST_REACH is satisfied by REACHED and REACHED_VIA_DISPATCH alike: dispatch
is evidence provenance, not a correctness level (owner ruling). The
spec-only MUST_REACH_DIRECT accepts a direct path alone, and a
dispatch-only reading is DIRECT_PATH_GAP.
- The outcomes:
- SATISFIED and CORRECT;
- WIRING_GAP, ARTIFACT_GAP, UNDECIDED, DIRECT_PATH_GAP and ROOT_MISMATCH;
- UNEXPECTED_LIVE_PATH and PRODUCTION_LEAK;
- REMOVAL_CANDIDATE and DELETE;
- MISSING_SYMBOL, and AMBIGUOUS_SYMBOL for a path several definitions
share (two `From` impls on one type);
- UNSPECIFIED, every production definition no row names.
A gap fails unless its requirement is Partial, Missing or Violated in
CONFORMANCE §8, where it is reported as the known hole. REMOVAL_CANDIDATE,
DELETE and UNSPECIFIED are only reported.
- A manifest that cannot be read is refused, never guessed at. It is refused
for:
- an unknown value;
- a requirement MASTER does not define;
- a missing exception for an exclusion, a deprecation or a row with no
requirement;
- a row with no requirement that demands reach;
- test-only code that is not MUST_NOT_REACH;
- a missing citation;
- a duplicate row;
- a root that is not an entry point.
- `root` is the map's fact, never the comparator's. `requirement_map index`
and `fixture` answer `--root-queries` (is this symbol reached from this one
entry point?) with the same reach, direct-path and classify rules, and
write root-queries.tsv. Asking nothing is `None`, never an empty answer.
- The requirements come from MASTER and CONFORMANCE §8 through
ci/conformance_evidence.py, still the only Markdown parser. It now exposes
canonical_ids, status_rows and requirement_statuses, which its own checks
use.
Tests and gates:
- The fixture gains an intent manifest with a row for every outcome, and the
outcome each must produce (intent.tsv, requirements.tsv,
intent-expected.tsv), run by `make requirement-map-fixture`. It also gains
two `From` impls on one type.
- Seven `manifest` mutation cases each change one thing in a copy of the
manifest. The comparator must refuse the row, or move exactly the outcomes
named, with every other row held to its expected outcome.
- rules.tsv gains the `outcome` kind. src/rules.rs reads OUTCOMES from Python
(as it reads CHECK_RULES) and checks that each outcome's positive fixture
row has it and its negative does not.
- `make requirement-map` asks the manifest's root questions. `make
requirement-map-intent` runs the comparator, and CI runs it with both
builds required. intent.tsv, unspecified.tsv and root-queries.tsv are kept.
The manifest holds its header only. Its rows are the next chunk.
From the gate:
- The root answers come back in the order asked, whatever the builds' order.
- A root is checked to be an entry point in each build this host indexed.
- The harness checks every table's header and cell count, and tells a
comparator crash (stderr) from a failing row. It writes the changed
manifest and the report to separate places.
…tations traced (§6.39) The manifest's first rows declare the specifications' intent for the code §8 cites. - **What is covered.** Every canonical code reference of a Met or Partial row (Violated rows cite violating code, not code that must run) becomes a MUST_REACH row. - **Build.** A row goes in the build that reaches its code, preferring its requirement's family (storage to node, the rest to Android). It goes in the family's build only when nothing reaches the code, since storage-spec obligations the client carries run in the Android build. - **Evidence and source.** Each row names the §8 row's tests as its evidence and cites the §8 row. - **Node pins.** MR-SOFI-0070 and MR-STOR-0042 add node MUST_NOT_REACH rows for Route::of and Route::leader: a storage node never computes a cell's route or its leader, and the map shows the node's build reaches neither. Before landing, the comparator read those citations against the canonical Linux map (CI's map of main at 20f63cb). Sixteen Met rows, over fourteen requirements, cited code that no shipped build reaches. Each was traced again from the requirement's text (owner ruling): - 12 stay Met, citing the production code: - a leader comes from position_seed or storage_seed, through RoutedCell::new, Route::of (permute) and Route::leader; - SoFi signatures: verify_precommit and verify_fulfillment; - a setup's identity: setup_ref and verify_setup; - the conjunction: validate's Verdict; - waiting on an unread leader: evaluate; - determinism: dsm_domain_hasher. The dead helpers cited before (position_leader, first_member, verify_signed_object, SignedSofiBody::object_id, Validation::and/all, CanonicalEncode) are named in each note. - MR-STOR-0156 is now Partial. No shipped build checks a completion proof: production builds one and keeps its digest, and nothing reads a kept proof back or checks it. - MR-DSM-0100 is now Partial. The uniform CanonicalEncode is never called, and only per-type canonical encodings exist. CONFORMANCE §6.39 records all of it. Also recorded there: 101 references that name no definition the map holds (module paths, method shorthand, deleted code), which are Stage 3's to canonicalize and are not rows yet. The §7 totals are regenerated: Met 325, Partial 236. Against the canonical map the manifest reads 539 SATISFIED, 4 CORRECT, and 6 WIRING_GAPs that are Partial requirements' known holes: 0 failing rows. On a host that cannot index the node, its 76 rows read not-built (UNDECIDED), and CI requires both builds. ci/conformance_evidence.py passes. Also: ci/intent_comparator.py loses an unused `import csv` (it reads its tables with its own strict reader).
… test-only fates
The manifest gains the owner's remaining first scope. Entry points are bound
to what they serve, and production symbols no build reaches get the
conservative class fates. The map's uncertainty never becomes intent.
Root queries follow the process, not one call.
- A path must start at the named entry point. A dispatch on it may rest on
a value any entry point made, since the process holds it: the app router
is built at startup (JNI_OnLoad, SDK start) and every later request
dispatches to it through dispatchIngress.
- `reach::reached_with` starts from known type evidence and returns what it
gathered. A build's reach starts from none; a root query starts from the
whole build's.
- `reached` had no production caller left and is gone.
- New unit test: a_root_query_dispatches_on_a_value_another_entry_point_made.
- New fixture shape: a router JNI_OnLoad installs in a global and
`Probe.query()` calls through a trait object (installed.rs). Its manifest
row is SATISFIED from `query`. It reads UNDECIDED if the query starts from
no evidence (mutation-checked).
Entry points (owner ruling: bind each root to the requirements it serves).
- A read-only trace of all 71, confirmed by the map:
- dispatchIngress reaches the code of 208 of the 213 Android symbols the
manifest names; the other 5 are known holes that no entry point reaches.
- Those rows, 468 of them, take dispatchIngress as their root.
- The node's 72 requirement rows take dsm_storage_node::main, its only
entry point.
- 67 more entry points get rows saying why each exists:
- 36 offline BLE, 6 NFC recovery and 7 dBTC (the six undeclared bitcoin*
exports and the builtins guard), as MAY_REACH with the scope exception;
- 18 infrastructure (library load, SDK start, UI state and status), as
MAY_REACH with its reason.
- removeContact and dsm_init_runtime stay unspecified, with no stated
purpose, for the owner.
Unreached production symbols (owner ruling: conservative class rules).
- Dead code in out-of-scope subsystems is MAY_REACH with the scope exception
and stays active, never deprecated. That covers dBTC (§8.3 Deferred),
emissions, recovery, the hardware anchor crates and the offline BLE
transport.
- The testing tags module, which declares itself never used by production
protocol paths, is test-only MUST_NOT_REACH.
- Everything else stays UNSPECIFIED. The comparator's report now gives the
action by reading:
- dead: a removal candidate pending review;
- indeterminate: undecided;
- reached: declare its intent.
It is reported only. 83 paths that name several definitions in a build
stay unspecified rather than become ambiguous rows.
CONFORMANCE §6.39 records the rest of what the trace found:
- the two ingress points, and removeContact and dsm_init_runtime;
- the parked dBTC policy's load-time assert, which can abort the Android
library's load;
- a committed C header whose nine declarations have no Rust definition;
- three §8 rows stale the other way: MR-SOFI-0255's sofi_routes.rs exists,
and spool payloads are sealed (MR-DSM-0272, MR-STOR-0146). They are left
until traced.
Found while verifying:
- The comparator counted a definition the build does not compile (another
profile's host-only twin of the same path, which reads not-in-artifact)
as a candidate. On macOS that made three anchor rows AMBIGUOUS_SYMBOL.
- Only compiled definitions are candidates now. With none compiled, a row
reads not-in-artifact: ARTIFACT_GAP under MUST_REACH, CORRECT under
MUST_NOT_REACH.
Against CI's Linux map of main, all 1,062 rows read 0 failing:
- Android: 468 SATISFIED, 376 CORRECT, 5 known holes;
- node: 71 SATISFIED, 141 CORRECT, 1 known hole.
Locally the Android rows read the same, and the node's 92 read not-built,
which CI's --built android,node evaluates.
From the gate: the fixture's Probe.query() expects its installed router (JNI_OnLoad
installs it first) instead of turning a missing one into 0.
…als reach the terminal Owner ruling (2026-09-29): a finding the investigation established stays in §6 even when its remediation is outside the change that found it, marked deferred. Unfinished implementations of active requirements are never deleted as dead code, and what awaits the owner is recorded as open, not settled. §6.39's Open list now says which each item is: - *confirmed, remediation deferred*: MR-STOR-0156, whose check_completion_proof and completion_proofs::get are kept to be wired; MR-DSM-0100, whose CanonicalEncode is kept; the stale C header; the 101 unresolved references (Stage 3); - *owner decision*: removeContact and dsm_init_runtime (keep, wire or delete), and whether the parked dBTC policy's mismatch should stop the library loading; - *unconfirmed*: the three Missing rows whose code exists, until traced; - *recorded, not a defect*: the entry points, which the manifest binds. ci/intent_comparator.py prints a refusal to stderr. `make` redirects `root-queries`' stdout into a file, and a malformed manifest's refusal disappeared into it while make aborted. ci/requirement_map_mutations.py reads an expected refusal from stderr, and fails a case on any other stderr.
CI's first run of #1055 (the first to index the node with the manifest's root questions) refused: `a root query's entry point dsm_storage_node::main names 2 definitions the node build compiles`. The node's index also holds its build script's `main`, which shares the binary's path and is not in the build. That is the class #1054 fixed for sentinel and fixture lookups. A root query now looks paths up only among definitions in the build's own crates. - The fixture gains the question: MR-FIX-0008 asks whether probe::main, a path the fixture's build script shares, is reached from the entry point. Before the fix the fixture refused with CI's exact error; it now reads SATISFIED. - ci/conformance_evidence.py requirement_statuses refuses a canonical ID §8 gives no row, where it used to map the ID to None. The comparator reports that refusal on stderr. A macOS host cannot index the node, which is why the local run missed this. The Android root answers are byte-identical before and after. The map check is clean, 40/40 mutation cases pass, and the fixture reads 90/90 with 0 unexpected intent outcomes.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The intent layer: what the specifications say the code must do, against what it does
The map establishes what the code does, and never decides what it ought to do.
specs/requirements/INTENT_MANIFEST.tsv, your authorized home for it, now says that.ci/intent_comparator.pycompares the two through one outcome table and derives an action. The adversarial layer can challenge rows, but never write them.1 · The comparator (
d2e3484c0)Outcomes and policy.
SATISFIED/CORRECT;WIRING_GAP,ARTIFACT_GAP,UNDECIDED,DIRECT_PATH_GAPandROOT_MISMATCH;UNEXPECTED_LIVE_PATHandPRODUCTION_LEAK;REMOVAL_CANDIDATEandDELETE;MISSING_SYMBOLandAMBIGUOUS_SYMBOL;UNSPECIFIED.REMOVAL_CANDIDATE,DELETEandUNSPECIFIED.Reachability intents (your ruling).
MUST_REACHis satisfied byREACHEDandREACHED_VIA_DISPATCHalike.MUST_REACH_DIRECTrejects a dispatch-only path, asDIRECT_PATH_GAP.Malformed rows are refused, never guessed at. The comparator refuses:
MUST_NOT_REACH;rootis the map's fact.requirement_map --root-queriesanswers "is this symbol reached from this entry point?" with the same rules the map uses. A path must start at the root. A dispatch on it may rest on a value any entry point made, because the process holds it: the app router is built at startup, and every request dispatches to it.Tests.
outcomekind inrules.tsv, checked by its test.2 · The conformance it found (
7e99c7a3e, CONFORMANCE §6.39)Read against CI's Linux map, 16 Met rows over 14 requirements cited code no shipped build reaches. Each was traced again from its requirement's text:
position_seed/storage_seed→RoutedCell::new→Route::of→Route::leader;verify_precommit/verify_fulfillment;setup_ref;validate'sVerdict;evaluate;dsm_domain_hasher.CanonicalEncodeis never called; only per-type encodings exist.§7 totals: Met 327 → 325, Partial 234 → 236.
3 · The manifest (
7e99c7a3e,330525c67): 1,062 rowsMUST_REACHrows from §8's canonical code references.dispatchIngress, which reaches the code of 208 of the 213 Android symbols the manifest names; the other 5 are known holes. The node's 72 are bound tomain.MUST_NOT_REACHrows pin "a storage node never computes a route or its leader" (MR-SOFI-0070, MR-STOR-0042).MAY_REACHwith the scope exception, and stay active, never deprecated: dBTC, emissions, recovery, hardware anchors and offline BLE.test-only.UNSPECIFIED, with its reading's action reported: removal candidate, undecided, or declare intent. No intent is inferred from reachability.Result. Against CI's Linux map (
mainat 20f63cb), with the root column cleared (that map holds no root answers):SATISFIED, 376CORRECT, 5 known holes;SATISFIED, 141CORRECT, 1 known hole;This PR's own CI runs the full comparison, the node's root answers included.
For your review (§6.39 Open)
removeContactanddsm_init_runtimehave no stated purpose. Both are left unspecified for you to decide on._dsm_builtins_guardcan abort the Android library's load if the parked dBTC policy's bytes and commit ever disagree.dsm_sdk/include/dsm_sdk.his stale: it declares nine functions, none of which exists in Rust.sofi_routes.rsexists.process_online_transfer_logic). Stage 3 canonicalizes them.Verification (local, macOS; the node is indexed only on Linux)
requirement_mapunit tests: 97/97 (--release). Clippy-D warnings, fmt, the real-code guard andci/conformance_evidence.pyall pass.make requirement-map-fixture: the fixture builds and its test passes, 90/90 readings, and all 21 intent rows give their expected outcome.make requirement-map+-check: 0 contradictions; 25 sentinels, 70 entry points and the counts unchanged.make requirement-map-intent(local): Android rows 468SATISFIED, 494CORRECT, 5 known holes. The node's 92 rows read not-built, and CI evaluates them.make requirement-map-mutations: 40/40.MUST_REACH;