X2: DT64 execution-admission policy probe (LAB)

.claude/board/entries/2026-10-31-x2-dt64-admission-policy.md

@@ -0,0 +1,55 @@
+# X2-DT64-ADMISSION: a typed execution-admission policy after `BindStore::admit`
+
+**Date 2026-10-31 · Plan `d-dynbag-holographic-bags-v1` §18.4 (X2, as briefed) · Status LAB · Crate `crates/dt64-admission-probe` (excluded, own workspace) · Prior [D-SAG-6-2-LAB](2026-10-31-d-sag-6-2-lab-projection.md), [D-SAG-6-2-JOIN-IDENT](2026-10-31-d-sag-6-2-span-join-identity.md)**
+
+**Decision (operator):** `BindStore::admit` stays as it is. It authenticates method identity, signature revision and guard witness. Admission for execution is a separate typed policy, layered after it.
+
+## Shape
+
+`ExecutionPolicy::decide(store, ref, evidence, request)` first runs `admit`; a refusal there passes through as `Binding(..)`. It then classifies the method's D-SAG-6 rows:
+
+| # | Evidence | Result |
+|---|---|---|
+| 1 | proven pure | `Admitted::Pure { assumed }` |
+| 2 | WITNESSED effect, every effect row covered by a `DoGrant` for this exact `MethodRef` | `Admitted::UnderDoGrant` |
+| 3 | any POSSIBLE row | `ExecRefusal::Possible` |
+| 4 | any UNKNOWN fact | `ExecRefusal::Unknown { causes }` |
+| 5 | WITNESSED effect, no covering grant | `RequiresDoGate` / `GrantDoesNotCover` / `GrantForOtherMethod` |
+
+Precedence: UNKNOWN, then POSSIBLE, then a witnessed effect. A grant lifts only witnessed effects.
+
+What the types add:
+- `Attachment` keys evidence to `(class, MethodId, SigRev)`, never to `MethodBinding::name`.
+- `DoGrant` names one `MethodRef` and the `(relation, subject)` effect rows it accepts.
+- `UnknownCause` has six arms: `NotAttached`, `NoDefinition`, `Unjoined`, `UnnamedCallee`, `UnauditedCallee`, `Mislabelled`.
+
+Evidence types:
+- `Relation` and `Evidence` mirror `project_rows.py`'s strings, crate-local only.
+- No global evidence enum was added and `set_rules::Truth` is not reused.
+- No DT64 type was needed: no change to `lance-graph-dt64/src`, no new classid. The lab classids of DT64's own tests are reused.
+
+## Measured (fixture `sag_fixture`)
+
+`cargo test`: **25 pass, 0 fail.**
+
+| Method | Result |
+|---|---|
+| `count_below` | `Pure`, `assumed` = 3 callees |
+| `count_with_tally` | `RequiresDoGate`: 1 × `WRITES_CALLER_MEMORY` |
+| `count_div` | `RequiresDoGate`: 1 × `MAY_PANIC` |
+| `count_generic` / `count_dyn` | `Possible`, also when a grant names the row |
+| `mask_below` | `Possible` |
+| `Below::test` | `Unknown` (`Unjoined`) under the path join, `Pure` under the span join |
+| a method bound under the name `count_below` with no attachment | `Unknown` (`NotAttached`) |
+
+All 8 bound methods pass `admit`; 2 execute as pure. Binding is not authorization.
+
+**Disable runs: 14 guards, 14 red.** Each run was committed first, then the patch was asserted to have applied, then restored with `git checkout`. The table is in the crate README. The `admit` pass-through was not disabled (no smaller patch than deleting it); it is pinned by a test.
+
+## Open
+
+1. **The rows are reconstructed, not measured.** No `project_rows.py` output is committed. `src/fixture.rs` rebuilds the rows bearing on these functions from the two entries' stated facts, citing each group. The `CALLS` objects are illustrative `core::` spellings. The 8 `MAY_PANIC` rows (profile-dependent) are not all listed. Next step: run Charon → `llbc_calls.py` → `span_join.py` → `project_rows.py` on the fixture and commit the TSV as the fixture.
+2. **The trust list is policy, not evidence.** A pure verdict on `count_below` relies on `core::slice::` / `core::iter::` being pure; the verdict returns them in `assumed`. Without the list the answer is UNKNOWN. Who owns the list is undecided.
+3. **Scope is by subject prefix.** Closures are found through `subject::`. A closure passed into a *non-local* callee is not in scope unless it is nested under the subject; the span join's closure spelling makes it nested on this fixture. Not tested on closures defined elsewhere and passed in.
+4. **`DoGrant` has no issuer.** Who may mint one (RBAC, an operator approval) is not modelled. The policy only checks a grant.
+5. **§18.4 was not found in the plan.** The plan file on `origin/main` (d3c2a29) ends at §16. The citation is as given in the brief.

.claude/board/entries/README.md

@@ -25,10 +25,11 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately
 opposite directions; the stranding this convention prevents shows up in
 exactly one of them, never both.
 
-525 entries, 2026-08-06 .. 2026-10-31.
+526 entries, 2026-08-06 .. 2026-10-31.
 
 | date | entry id | finding | file |
 |---|---|---|---|
+| 2026-10-31 | `x2-dt64-admission-policy` |  | [2026-10-31-x2-dt64-admission-policy.md](2026-10-31-x2-dt64-admission-policy.md) |
 | 2026-10-31 | `D-XLOG-NATIVE-6` |  | [2026-10-31-d-xlog-native-6-ndarray-simd-execution.md](2026-10-31-d-xlog-native-6-ndarray-simd-execution.md) |
 | 2026-10-31 | `D-XLOG-NATIVE-5` |  | [2026-10-31-d-xlog-native-5-bindstore-epi5.md](2026-10-31-d-xlog-native-5-bindstore-epi5.md) |
 | 2026-10-31 | `D-SAG-6-2-JOIN-IDENT` |  | [2026-10-31-d-sag-6-2-span-join-identity.md](2026-10-31-d-sag-6-2-span-join-identity.md) |

Cargo.toml

@@ -214,6 +214,10 @@ exclude = [
     # Plan: .claude/plans/weather-soa-bake-v1.md.
     "crates/weather-poc",
     "crates/d-diamond-1-probe",
+    # X2 DT64 execution-admission policy (LAB). Own workspace root; path-deps
+    # lance-graph-dt64 and the contract only. Verify via
+    # `cargo test --manifest-path crates/dt64-admission-probe/Cargo.toml`.
+    "crates/dt64-admission-probe",
 ]
 resolver = "2"
 

crates/dt64-admission-probe/Cargo.toml

@@ -0,0 +1,19 @@
+# X2 (plan d-dynbag-holographic-bags-v1 §18.4): a DT64-owned LAB probe for a
+# typed execution-admission policy layered AFTER `BindStore::admit`. NOT a
+# workspace member, nothing depends on it. Verify with
+#   cargo test --manifest-path crates/dt64-admission-probe/Cargo.toml
+[package]
+name = "dt64-admission-probe"
+version = "0.0.0"
+edition = "2021"
+publish = false
+license = "MIT OR Apache-2.0"
+description = "Decides whether an admitted DT64 method may execute, from D-SAG-6 evidence rows: proven pure, witnessed effect under an explicit DO grant, POSSIBLE, or UNKNOWN. BindStore::admit authenticates; this policy authorizes."
+
+# Own workspace root, like the other lab probes.
+[workspace]
+
+[dependencies]
+# Consumed read-only through their public APIs; neither crate is changed.
+lance-graph-dt64 = { path = "../lance-graph-dt64" }
+lance-graph-contract = { path = "../lance-graph-contract" }

crates/dt64-admission-probe/README.md

@@ -0,0 +1,94 @@
+# dt64-admission-probe (LAB)
+
+`BindStore::admit` authenticates a router's method reference: method
+identity, signature revision, guard witness. It is unchanged here. This probe
+adds a typed **execution-admission policy** after it:
+`ExecutionPolicy::decide(store, ref, evidence, request)` runs `admit`, then
+reads the method's D-SAG-6 evidence rows and decides whether the method may
+execute.
+
+Standalone: own `[workspace]`, excluded from the lance-graph workspace,
+nothing depends on it. Depends only on `lance-graph-dt64` and
+`lance-graph-contract`, by path, read-only.
+
+```
+CARGO_PROFILE_DEV_DEBUG=0 CARGO_INCREMENTAL=0 \
+  cargo test --manifest-path crates/dt64-admission-probe/Cargo.toml
+```
+
+## The outcomes
+
+| Evidence of the method's source | Result |
+|---|---|
+| 1. proven pure | `Ok(Admitted::Pure { binding, assumed })` |
+| 2. WITNESSED effect, DO grant covers every effect row | `Ok(Admitted::UnderDoGrant { binding, effects })` |
+| 3. any POSSIBLE row | `Err(ExecRefusal::Possible { rows })` |
+| 4. any UNKNOWN fact | `Err(ExecRefusal::Unknown { causes })` |
+| 5. WITNESSED effect, no covering grant | `Err(ExecRefusal::RequiresDoGate { effects })`, `GrantDoesNotCover`, `GrantForOtherMethod` |
+| `admit` refused | `Err(ExecRefusal::Binding(refusal))`, unchanged |
+
+UNKNOWN dominates POSSIBLE, which dominates a witnessed effect. A DO grant
+authorizes witnessed effects only; it never lifts POSSIBLE or UNKNOWN.
+
+Rules the tests pin:
+- **Absence of rows is not purity.** Pure requires an attachment and a
+  `DEFINES` row for the subject.
+- **Evidence attaches to `(class, MethodId, SigRev)`**, never to the method's
+  name. Evidence for another signature revision does not attach.
+- **Scope** = the subject, nested subjects (`subject::…`, which covers the
+  closures), and local callees (a `CALLS` target that has a `DEFINES` row).
+- **A non-local callee is UNKNOWN** unless the policy trusts its prefix. A
+  pure verdict returns the trusted callees it relied on (`assumed`).
+
+The evidence vocabulary is `project_rows.py`'s (`WITNESSED` / `POSSIBLE` /
+`UNKNOWN`), mirrored as a crate-local enum. It is not a global evidence type,
+and `set_rules::Truth` (row logic) is not used as one.
+
+## Fixture outcomes (D-SAG-6 `sag_fixture`)
+
+| Method | Result |
+|---|---|
+| `count_below` | `Pure`, assuming 3 `core::slice::` / `core::iter::` callees; `Unknown` (3 × `UnauditedCallee`) with no trusted prefixes |
+| `count_with_tally` | `RequiresDoGate` (1 × `WRITES_CALLER_MEMORY`); `UnderDoGrant` with a covering grant |
+| `count_div` | `RequiresDoGate` (1 × `MAY_PANIC`); `UnderDoGrant` with a grant naming the panic |
+| `count_generic`, `count_dyn` | `Possible` (`trait:Clause`, `dynamic`), also when a grant names the row |
+| `mask_below` | `Possible` (`WRITES_THROUGH_LOCAL_REF`) |
+| `Below::test` | `Unknown` under the path join (`UNJOINED`); `Pure` under the span join |
+| a method named `count_below`, no attachment | `Unknown` (`NotAttached`) |
+
+All eight methods pass `admit`; only two execute as pure.
+
+The rows in `src/fixture.rs` are reconstructed from the facts in the D-SAG-6
+board entries. Row lists are not committed anywhere; the entries record
+counts and per-function findings. The provenance is cited per row group in
+that file. They were not measured by a Charon run.
+
+## Disable table
+
+Method: commit, apply one patch (the anchor must occur exactly once, and the
+script checks that the replacement applied), run the integration tests,
+restore with `git checkout`, and check that the anchor is back. The runs were
+against commit `b7cfe93`.
+
+| Guard | Patch | Red tests |
+|---|---|---|
+| G1 `DEFINES` required | drop the `NoDefinition` push | `absence_of_rows_is_not_purity` |
+| G2 UNKNOWN kept | UNKNOWN row → ignored | `below_test_is_unknown_under_the_path_join_…`, `unknown_dominates_possible_dominates_effect` |
+| G3 POSSIBLE kept apart | POSSIBLE row → effect | `generic_and_dyn_…`, `a_grant_naming_the_dispatch_row_…`, `a_local_buffer_write_…`, `unknown_dominates_…` |
+| G4 pure request refuses effects | `Request::Pure` → `Admitted::Pure` | `witnessed_effects_are_refused_…`, `every_fixture_method_admits_but_only_two_…` |
+| G5 grant names this method | method check → `false` | `an_empty_grant_or_one_for_another_method_…` |
+| G6 grant covers every row | coverage → `true` | `an_empty_grant_…`, `count_div_executes_only_under_a_grant_…` |
+| G7 attachment keyed by `SigRev` | drop the `sig_rev` match | `evidence_for_another_signature_revision_…` |
+| G8 local callees followed | no recursion | `an_effect_in_a_local_callee_is_found` |
+| G9 nesting needs `::` | prefix without `::` | `a_nested_subject_is_in_scope_but_a_name_sharing_a_prefix_is_not` |
+| G10 untrusted callee is UNKNOWN | trust every callee | `count_below_without_trust_is_unknown_not_pure` |
+| G11 unnamed impl callee is UNKNOWN | `known impl` check → `false` | `an_unnamed_trait_impl_call_is_unknown` |
+| G12 mislabelled hand-built row | ignore it | `a_hand_built_mislabelled_row_is_never_pure` |
+| G13 parser checks relation/evidence | check → `false` | `a_possible_relation_labelled_witnessed_is_rejected` |
+| G14 nested subjects in scope | exact subject only | 9 tests, among them `count_with_tally_executes_only_…`, `witnessed_effects_are_refused_…`, `generic_and_dyn_…` |
+| G15 an in-scope closure callee is not unaudited (Codex P2, #1891) | treat it as any other callee | 8 tests, among them `a_call_into_an_in_scope_closure_…`, `count_below_is_admitted_pure_…`, `count_with_tally_executes_only_…` |
+| G16 in scope needs the `::` boundary | prefix match without `::` | `a_call_into_another_functions_closure_stays_unaudited` |
+
+Not disabled: the `admit` pass-through. `decide` needs the binding `admit`
+returns, so there is no smaller patch than removing the call. Its refusals are
+pinned by `an_admit_refusal_passes_through_even_with_perfect_evidence`.

crates/dt64-admission-probe/src/evidence.rs

@@ -0,0 +1,167 @@
+//! D-SAG-6 evidence rows, typed.
+//!
+//! The row format and its vocabulary are the ones
+//! `crates/sag-ra-probe/tools/project_rows.py` prints:
+//!
+//! ```text
+//! relation  subject  object  witness  evidence
+//! ```
+//!
+//! with evidence one of `WITNESSED`, `POSSIBLE`, `UNKNOWN` (that tool spells
+//! the UNKNOWN class through its `UNJOINED` relation). The enums below are a
+//! typed mirror of those strings for this lab crate only; they are not a
+//! global evidence ontology and nothing outside this crate uses them.
+//!
+//! Parsing is strict: an unknown relation or evidence string, a wrong column
+//! count, or a relation carried at an evidence class `project_rows.py` never
+//! assigns it (a `MAY_DISPATCH` row labelled `WITNESSED`, say) is a
+//! [`RowError`], never a silently accepted row.
+
+/// The `relation` column of a D-SAG-6 row.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum Relation {
+    Defines,
+    HasImpls,
+    Calls,
+    MayDispatch,
+    MayPanic,
+    WritesCallerMemory,
+    WritesThroughLocalRef,
+    Unjoined,
+}
+
+impl Relation {
+    pub fn parse(s: &str) -> Option<Relation> {
+        Some(match s {
+            "DEFINES" => Relation::Defines,
+            "HAS_IMPLS" => Relation::HasImpls,
+            "CALLS" => Relation::Calls,
+            "MAY_DISPATCH" => Relation::MayDispatch,
+            "MAY_PANIC" => Relation::MayPanic,
+            "WRITES_CALLER_MEMORY" => Relation::WritesCallerMemory,
+            "WRITES_THROUGH_LOCAL_REF" => Relation::WritesThroughLocalRef,
+            "UNJOINED" => Relation::Unjoined,
+            _ => return None,
+        })
+    }
+
+    /// The only evidence class `project_rows.py` emits this relation at.
+    pub fn evidence(self) -> Evidence {
+        match self {
+            Relation::Defines
+            | Relation::HasImpls
+            | Relation::Calls
+            | Relation::MayPanic
+            | Relation::WritesCallerMemory => Evidence::Witnessed,
+            Relation::MayDispatch | Relation::WritesThroughLocalRef => Evidence::Possible,
+            Relation::Unjoined => Evidence::Unknown,
+        }
+    }
+}
+
+/// The `evidence` column of a D-SAG-6 row.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum Evidence {
+    /// A compiler frontend reports it.
+    Witnessed,
+    /// Dispatch or a write whose target the frontend does not fix.
+    Possible,
+    /// A fact one frontend has and the other cannot be joined to.
+    Unknown,
+}
+
+impl Evidence {
+    pub fn parse(s: &str) -> Option<Evidence> {
+        Some(match s {
+            "WITNESSED" => Evidence::Witnessed,
+            "POSSIBLE" => Evidence::Possible,
+            "UNKNOWN" => Evidence::Unknown,
+            _ => return None,
+        })
+    }
+}
+
+/// One row.
+#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub struct Row {
+    pub relation: Relation,
+    pub subject: String,
+    pub object: String,
+    pub witness: String,
+    pub evidence: Evidence,
+}
+
+/// Why a row was rejected.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum RowError {
+    /// The header line is not `relation subject object witness evidence`.
+    BadHeader(String),
+    /// A data line without exactly five tab-separated columns.
+    Columns {
+        line: usize,
+        got: usize,
+    },
+    UnknownRelation {
+        line: usize,
+        relation: String,
+    },
+    UnknownEvidence {
+        line: usize,
+        evidence: String,
+    },
+    /// The relation at an evidence class it is never emitted at.
+    EvidenceMismatch {
+        line: usize,
+        relation: Relation,
+        evidence: Evidence,
+    },
+}
+
+pub const HEADER: &str = "relation\tsubject\tobject\twitness\tevidence";
+
+/// Parse `project_rows.py` output.
+pub fn parse_rows(tsv: &str) -> Result<Vec<Row>, RowError> {
+    let mut lines = tsv
+        .lines()
+        .enumerate()
+        .filter(|(_, l)| !l.trim().is_empty());
+    match lines.next() {
+        Some((_, h)) if h == HEADER => {}
+        Some((_, h)) => return Err(RowError::BadHeader(h.to_string())),
+        None => return Err(RowError::BadHeader(String::new())),
+    }
+    let mut rows = Vec::new();
+    for (i, l) in lines {
+        let line = i + 1;
+        let cols: Vec<&str> = l.split('\t').collect();
+        if cols.len() != 5 {
+            return Err(RowError::Columns {
+                line,
+                got: cols.len(),
+            });
+        }
+        let relation = Relation::parse(cols[0]).ok_or_else(|| RowError::UnknownRelation {
+            line,
+            relation: cols[0].to_string(),
+        })?;
+        let evidence = Evidence::parse(cols[4]).ok_or_else(|| RowError::UnknownEvidence {
+            line,
+            evidence: cols[4].to_string(),
+        })?;
+        if relation.evidence() != evidence {
+            return Err(RowError::EvidenceMismatch {
+                line,
+                relation,
+                evidence,
+            });
+        }
+        rows.push(Row {
+            relation,
+            subject: cols[1].to_string(),
+            object: cols[2].to_string(),
+            witness: cols[3].to_string(),
+            evidence,
+        });
+    }
+    Ok(rows)
+}