diff --git a/.claude/board/entries/2026-10-31-x2-dt64-admission-policy.md b/.claude/board/entries/2026-10-31-x2-dt64-admission-policy.md new file mode 100644 index 000000000..7a2068a9e --- /dev/null +++ b/.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. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index afde3629c..c49146404 100644 --- a/.claude/board/entries/README.md +++ b/.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) | diff --git a/Cargo.toml b/Cargo.toml index c153b3c3e..b206638fb 100644 --- a/Cargo.toml +++ b/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" diff --git a/crates/dt64-admission-probe/Cargo.toml b/crates/dt64-admission-probe/Cargo.toml new file mode 100644 index 000000000..85c1d3891 --- /dev/null +++ b/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" } diff --git a/crates/dt64-admission-probe/README.md b/crates/dt64-admission-probe/README.md new file mode 100644 index 000000000..74a3810f8 --- /dev/null +++ b/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`. diff --git a/crates/dt64-admission-probe/src/evidence.rs b/crates/dt64-admission-probe/src/evidence.rs new file mode 100644 index 000000000..292e44932 --- /dev/null +++ b/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 { + 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 { + 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, 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) +} diff --git a/crates/dt64-admission-probe/src/fixture.rs b/crates/dt64-admission-probe/src/fixture.rs new file mode 100644 index 000000000..fdc2aace4 --- /dev/null +++ b/crates/dt64-admission-probe/src/fixture.rs @@ -0,0 +1,231 @@ +//! The D-SAG-6 fixture (`crates/sag-ra-probe/fixtures/sag_fixture`) as +//! committed evidence, plus a DT64 store binding its functions. +//! +//! # Provenance of the rows +//! +//! No row-level output of `project_rows.py` is committed anywhere in the +//! repository: the board entries record counts and per-function findings, not +//! row lists. The rows below are therefore RECONSTRUCTED in that tool's +//! format from facts the entries state, one citation per row group: +//! +//! - E1 = `.claude/board/entries/2026-10-31-d-sag-6-2-lab-projection.md` +//! §3 (relation table) and §4 (binding table); +//! - E2 = `.claude/board/entries/2026-10-31-d-sag-6-2-span-join-identity.md` +//! §1 (span join: subjects are rust-analyzer monikers, closures are +//! `::{closure@L}::`, and the path join leaves 17 rows +//! `UNJOINED` on this fixture). +//! +//! What is NOT reproduced: the full 38 `CALLS`, 8 `MAY_PANIC` and 23 +//! `DEFINES` rows of E1 §3. Only the rows bearing on the functions below are +//! here. The `CALLS` objects (`core::slice::...`, `core::iter::...`) are +//! illustrative spellings of the standard-library callees each body makes; +//! the policy reads them only by prefix against its trusted list. Closure +//! line numbers are the closures' lines in the fixture source. Profile- +//! dependent overflow asserts (E1 F03) are not listed; adding them would +//! not change any outcome below, since every function they would touch is +//! already refused or is pure arithmetic outside this set. +//! +//! Each closure also carries the producer's shim call: Charon's +//! `call_once` calls the closure body `call_mut`, and the span join names +//! both by the enclosing function's moniker (`project_rows.py` +//! `subject_of`, `ENCLOSED`). Neither name gets a `DEFINES` row. +//! +//! Re-running Charon and the two tools on the fixture would replace these +//! rows with measured ones; that is not done here (no `/tmp` input, no +//! Charon run at test time). + +use lance_graph_contract::class_view::WideFieldMask; +use lance_graph_contract::set_algebra::{Cmp, Logic, SetExpr}; +use lance_graph_contract::set_rules::{Population, Truth}; +use lance_graph_dt64::{ + AlgebraRef, Arg, BindStore, ClassSchema, Effect, Extent, Guard, MethodBinding, MethodId, + MethodRef, SchemaRev, SigRev, ValueDemand, +}; + +use crate::evidence::{parse_rows, Row}; +use crate::{Attachment, EvidenceSet}; + +/// The span-joined rows (E2 §1: `sag_fixture` joins 29 of 29 bodies). +pub const SPAN_JOINED_ROWS: &str = "\ +relation\tsubject\tobject\twitness\tevidence +DEFINES\tsag_fixture::count_below\tFunction\trust-analyzer\tWITNESSED +CALLS\tsag_fixture::count_below\tcore::slice::::iter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_below\tcore::iter::traits::iterator::Iterator::filter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_below\tcore::iter::traits::iterator::Iterator::count\tcharon\tWITNESSED +CALLS\tsag_fixture::count_below::{closure@L26}::call_once\tsag_fixture::count_below::{closure@L26}::call_mut\tcharon\tWITNESSED +DEFINES\tsag_fixture::count_with_tally\tFunction\trust-analyzer\tWITNESSED +CALLS\tsag_fixture::count_with_tally\tcore::slice::::iter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_with_tally\tcore::iter::traits::iterator::Iterator::filter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_with_tally\tcore::iter::traits::iterator::Iterator::count\tcharon\tWITNESSED +CALLS\tsag_fixture::count_with_tally::{closure@L42}::call_once\tsag_fixture::count_with_tally::{closure@L42}::call_mut\tcharon\tWITNESSED +WRITES_CALLER_MEMORY\tsag_fixture::count_with_tally::{closure@L42}::call_mut\t1\tcharon\tWITNESSED +DEFINES\tsag_fixture::count_div\tFunction\trust-analyzer\tWITNESSED +CALLS\tsag_fixture::count_div\tcore::slice::::iter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_div\tcore::iter::traits::iterator::Iterator::filter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_div\tcore::iter::traits::iterator::Iterator::count\tcharon\tWITNESSED +CALLS\tsag_fixture::count_div::{closure@L51}::call_once\tsag_fixture::count_div::{closure@L51}::call_mut\tcharon\tWITNESSED +MAY_PANIC\tsag_fixture::count_div::{closure@L51}::call_mut\t1 assert\tcharon\tWITNESSED +DEFINES\tsag_fixture::count_generic\tFunction\trust-analyzer\tWITNESSED +CALLS\tsag_fixture::count_generic\tcore::slice::::iter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_generic\tcore::iter::traits::iterator::Iterator::filter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_generic\tcore::iter::traits::iterator::Iterator::count\tcharon\tWITNESSED +MAY_DISPATCH\tsag_fixture::count_generic::{closure@L31}::call_mut\ttrait:Clause\tcharon\tPOSSIBLE +DEFINES\tsag_fixture::count_dyn\tFunction\trust-analyzer\tWITNESSED +CALLS\tsag_fixture::count_dyn\tcore::slice::::iter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_dyn\tcore::iter::traits::iterator::Iterator::filter\tcharon\tWITNESSED +CALLS\tsag_fixture::count_dyn\tcore::iter::traits::iterator::Iterator::count\tcharon\tWITNESSED +MAY_DISPATCH\tsag_fixture::count_dyn::{closure@L36}::call_mut\tdynamic\tcharon\tPOSSIBLE +DEFINES\tsag_fixture::mask_below\tFunction\trust-analyzer\tWITNESSED +CALLS\tsag_fixture::mask_below\tcore::slice::::iter\tcharon\tWITNESSED +CALLS\tsag_fixture::mask_below\tcore::iter::traits::iterator::Iterator::enumerate\tcharon\tWITNESSED +WRITES_THROUGH_LOCAL_REF\tsag_fixture::mask_below\t1\tcharon\tPOSSIBLE +DEFINES\tsag_fixture::impl::Below::Pred::test\tFunction\trust-analyzer\tWITNESSED +"; + +/// The path-joined rows for `Below::test` (E1 §3: impls and closures do not +/// join by path, so Charon's `sag_fixture::Impl::test` is `UNJOINED`; E2 §1: +/// the two `Impl::test` methods share that one Charon path). +pub const PATH_JOINED_ROWS: &str = "\ +relation\tsubject\tobject\twitness\tevidence +DEFINES\tsag_fixture::impl::Below::Pred::test\tFunction\trust-analyzer\tWITNESSED +UNJOINED\tsag_fixture::Impl::test\tno rust-analyzer moniker with this path\tjoin\tUNKNOWN +"; + +/// The bound class. This is the lab classid `lance-graph-dt64`'s own tests +/// bind (`tests/bind_store.rs`, `ORDER`); reused, not minted. +pub const CLASS: u32 = 0x0A1E_0001; +/// The polyfill lens; `lance-graph-dt64`'s test lens (`POLYFILL`), reused. +pub const LENS: u32 = 0x7F0A_0001; +/// Word 0 of the lens: a one-operand popcount over a mask field (E1 §4: the +/// count is written "through mask-risc's popcount word"). +pub const POPCOUNT: AlgebraRef = AlgebraRef { + lens: LENS, + word: 0, +}; + +/// Field 0: the element `x`; field 1: the count. +pub const FIELD_X: u8 = 0; +pub const FIELD_COUNT: u8 = 1; + +pub const COUNT_BELOW: MethodId = MethodId(1); +pub const COUNT_WITH_TALLY: MethodId = MethodId(2); +pub const COUNT_DIV: MethodId = MethodId(3); +pub const COUNT_GENERIC: MethodId = MethodId(4); +pub const COUNT_DYN: MethodId = MethodId(5); +pub const MASK_BELOW: MethodId = MethodId(6); +pub const BELOW_TEST: MethodId = MethodId(7); +/// Bound, but no evidence attachment. +pub const UNATTACHED: MethodId = MethodId(8); + +/// The functions and the subjects their evidence is attached to. +pub const SUBJECTS: [(MethodId, &str); 7] = [ + (COUNT_BELOW, "sag_fixture::count_below"), + (COUNT_WITH_TALLY, "sag_fixture::count_with_tally"), + (COUNT_DIV, "sag_fixture::count_div"), + (COUNT_GENERIC, "sag_fixture::count_generic"), + (COUNT_DYN, "sag_fixture::count_dyn"), + (MASK_BELOW, "sag_fixture::mask_below"), + (BELOW_TEST, "sag_fixture::impl::Below::Pred::test"), +]; + +/// One binding: ON `x`, reads `x`, one effect writing the count through the +/// popcount word. `count_below` alone carries its WHEN (`x < 6`, two-valued); +/// the others are unguarded. +pub fn binding(id: MethodId, name: &str) -> MethodBinding { + let when = (id == COUNT_BELOW).then(|| { + Guard::new( + SetExpr::i32(u16::from(FIELD_X), Cmp::Lt, 6), + Logic::TwoValued, + ) + }); + MethodBinding { + id, + sig_rev: SigRev(1), + name: name.to_string(), + on: WideFieldMask::from_positions(&[FIELD_X]), + when, + reads: WideFieldMask::from_positions(&[FIELD_X]), + effects: vec![Effect { + target: FIELD_COUNT, + algebra: POPCOUNT, + args: vec![Arg::Field(FIELD_X)], + }], + population: Population::Distinct, + truth: Truth::TwoValued, + demand: ValueDemand::Values, + } +} + +/// Every function bound in one class. All of them admit: binding is +/// authentication, not authorization. +pub fn store() -> BindStore { + let mut s = BindStore::new(); + s.declare_algebra(LENS, SchemaRev(1), Extent::DR64_CUBE, vec![1]) + .expect("lens"); + let mut methods: Vec = SUBJECTS + .iter() + .map(|(id, subj)| binding(*id, subj.rsplit("::").next().unwrap_or(subj))) + .collect(); + methods.push(binding(UNATTACHED, "count_below")); + s.register( + CLASS, + ClassSchema { + schema_rev: SchemaRev(1), + field_count: 2, + extent: Extent::DR64_CUBE, + }, + methods, + ) + .expect("register"); + s +} + +/// The faithful reference to a bound method. +pub fn method_ref(store: &BindStore, id: MethodId) -> MethodRef { + let b = store + .admit(&MethodRef { + class: CLASS, + method: id, + sig_rev: SigRev(1), + guard: (id == COUNT_BELOW).then(|| binding(id, "").when.unwrap().witness()), + }) + .expect("bound"); + MethodRef::of(CLASS, b) +} + +fn attachments() -> Vec { + SUBJECTS + .iter() + .map(|(id, subj)| Attachment { + class: CLASS, + method: *id, + sig_rev: SigRev(1), + subject: subj.to_string(), + }) + .collect() +} + +pub fn rows(tsv: &str) -> Vec { + parse_rows(tsv).expect("committed rows parse") +} + +/// The span-joined evidence set. +pub fn span_joined() -> EvidenceSet { + EvidenceSet { + rows: rows(SPAN_JOINED_ROWS), + attachments: attachments(), + } +} + +/// The path-joined evidence set: `Below::test` attaches to Charon's path. +pub fn path_joined() -> EvidenceSet { + EvidenceSet { + rows: rows(PATH_JOINED_ROWS), + attachments: vec![Attachment { + class: CLASS, + method: BELOW_TEST, + sig_rev: SigRev(1), + subject: "sag_fixture::Impl::test".to_string(), + }], + } +} diff --git a/crates/dt64-admission-probe/src/lib.rs b/crates/dt64-admission-probe/src/lib.rs new file mode 100644 index 000000000..baad39ec3 --- /dev/null +++ b/crates/dt64-admission-probe/src/lib.rs @@ -0,0 +1,315 @@ +//! X2: a typed execution-admission policy for DT64 methods (LAB). +//! +//! [`BindStore::admit`] authenticates a router's [`MethodRef`]: the method +//! exists, at the referenced signature revision, with exactly the guard the +//! reference witnesses. It says nothing about what the method's source does +//! when it runs. A binding that admits is bound, not authorized. +//! +//! [`ExecutionPolicy::decide`] runs `admit` unchanged and then reads the +//! method's D-SAG-6 evidence rows ([`evidence`]) to decide whether it may +//! execute. The answer is one of: +//! +//! | Evidence of the method's source | Answer | +//! |---|---| +//! | 1. proven pure | [`Admitted::Pure`] | +//! | 2. a WITNESSED effect, under a DO grant that covers every effect row | [`Admitted::UnderDoGrant`] | +//! | 3. any POSSIBLE row | [`ExecRefusal::Possible`] | +//! | 4. any UNKNOWN fact | [`ExecRefusal::Unknown`] | +//! | 5. a WITNESSED effect and no covering DO grant | [`ExecRefusal::RequiresDoGate`] (or [`ExecRefusal::GrantDoesNotCover`] / [`ExecRefusal::GrantForOtherMethod`]) | +//! +//! UNKNOWN dominates POSSIBLE, which dominates a witnessed effect. A DO +//! grant authorizes witnessed effects only: it never lifts a POSSIBLE row or +//! an UNKNOWN fact. Every refusal is a named variant, never an empty answer. +//! +//! # What "proven pure" means here +//! +//! The method is attached ([`Attachment`]) to a subject the frontend defined +//! (a `DEFINES` row), and the subject, every nested subject (closures, by the +//! `subject::` prefix) and every local callee (a `CALLS` target with its own +//! `DEFINES` row) carry no effect, POSSIBLE or UNKNOWN row. A call to a +//! non-local callee is UNKNOWN unless the policy names it as trusted +//! ([`ExecutionPolicy::trusted_external`]); the trusted callees a pure +//! verdict relies on are returned with it ([`Admitted::Pure::assumed`]), so +//! the assumption is visible rather than silent. +//! +//! Absence of rows is not purity. A method with no attachment, or attached to +//! a subject with no `DEFINES` row, is UNKNOWN. +//! +//! # Identity +//! +//! Evidence attaches to `(class, MethodId, SigRev)`, never to +//! [`MethodBinding::name`], which DT64 carries and never uses as identity. +//! Evidence recorded for another signature revision does not attach. +//! +//! [`MethodBinding::name`]: lance_graph_dt64::MethodBinding::name + +#![forbid(unsafe_code)] + +pub mod evidence; +pub mod fixture; + +use std::collections::BTreeSet; + +use evidence::{Evidence, Relation, Row}; +use lance_graph_dt64::{BindStore, MethodBinding, MethodId, MethodRef, Refusal, SigRev}; + +/// Which evidence subject a method's source is, recorded per +/// `(class, method, signature revision)`. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Attachment { + pub class: u32, + pub method: MethodId, + pub sig_rev: SigRev, + /// A subject spelling in the rows (a rust-analyzer moniker after the + /// span join, a Charon path under the path join). + pub subject: String, +} + +/// One evidence set: the rows of one projection run and the attachments of +/// methods to its subjects. +#[derive(Debug, Clone, Default)] +pub struct EvidenceSet { + pub rows: Vec, + pub attachments: Vec, +} + +/// An explicit DO authorization for one method reference: which witnessed +/// effect rows its holder accepts. Issued outside this crate; the policy +/// only checks it. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct DoGrant { + pub method: MethodRef, + /// `(relation, subject)` of every effect row the grant accepts. + pub effects: Vec<(Relation, String)>, +} + +/// What the caller asks for. +#[derive(Debug, Clone, Copy)] +pub enum Request<'g> { + /// Execute (or fuse) as pure. + Pure, + /// Execute under a DO grant. + Do(&'g DoGrant), +} + +/// An execution the policy admits. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Admitted<'s> { + /// Class 1: no effect, POSSIBLE or UNKNOWN row in the method's scope. + Pure { + binding: &'s MethodBinding, + /// The trusted non-local callees this verdict relies on. + assumed: Vec, + }, + /// Class 2: witnessed effects, every one covered by the grant. + UnderDoGrant { + binding: &'s MethodBinding, + effects: Vec, + }, +} + +/// Why a fact is UNKNOWN. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum UnknownCause { + /// No attachment for this `(class, method, sig_rev)`. + NotAttached { + class: u32, + method: MethodId, + sig_rev: SigRev, + }, + /// The attached subject has no `DEFINES` row: the frontend never saw it. + NoDefinition { subject: String }, + /// An `UNJOINED` row in scope. + Unjoined(Row), + /// A resolved call whose callee the row does not name (`known impl`). + UnnamedCallee(Row), + /// A non-local callee the policy does not trust. + UnauditedCallee(Row), + /// A row at an evidence class its relation is never emitted at. + Mislabelled(Row), +} + +/// Why the policy refused. `admit`'s own refusal passes through unchanged. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ExecRefusal { + /// `BindStore::admit` refused: not even bound. + Binding(Refusal), + /// Class 3: POSSIBLE rows. No grant lifts these. + Possible { rows: Vec }, + /// Class 4: UNKNOWN facts. No grant lifts these. + Unknown { causes: Vec }, + /// Class 5: witnessed effects and pure execution was asked. + RequiresDoGate { effects: Vec }, + /// Class 5: the grant does not cover these effect rows. + GrantDoesNotCover { uncovered: Vec }, + /// Class 5: the grant names another method reference. + GrantForOtherMethod { + granted: MethodRef, + asked: MethodRef, + }, +} + +/// The evidence class of one method's source, before any DO gate. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum EvidenceClass { + ProvenPure { assumed: Vec }, + WitnessedEffect { effects: Vec }, + Possible { rows: Vec }, + Unknown { causes: Vec }, +} + +/// The execution-admission policy. +#[derive(Debug, Clone, Default)] +pub struct ExecutionPolicy { + /// Path prefixes of non-local callees treated as pure (for example + /// `core::iter::`). Empty means no non-local call is trusted. + pub trusted_external: Vec, +} + +/// The CALLS object `project_rows.py` writes for a resolved trait impl it +/// does not name. +pub const UNNAMED_IMPL: &str = "known impl"; + +impl ExecutionPolicy { + /// Authenticate with `admit`, then decide from `evidence`. + pub fn decide<'s>( + &self, + store: &'s BindStore, + r: &MethodRef, + evidence: &EvidenceSet, + request: Request<'_>, + ) -> Result, ExecRefusal> { + let binding = store.admit(r).map_err(ExecRefusal::Binding)?; + match self.classify(r, evidence) { + EvidenceClass::Unknown { causes } => Err(ExecRefusal::Unknown { causes }), + EvidenceClass::Possible { rows } => Err(ExecRefusal::Possible { rows }), + EvidenceClass::ProvenPure { assumed } => Ok(Admitted::Pure { binding, assumed }), + EvidenceClass::WitnessedEffect { effects } => match request { + Request::Pure => Err(ExecRefusal::RequiresDoGate { effects }), + Request::Do(grant) => { + if grant.method != *r { + return Err(ExecRefusal::GrantForOtherMethod { + granted: grant.method.clone(), + asked: r.clone(), + }); + } + let uncovered: Vec = effects + .iter() + .filter(|e| { + !grant + .effects + .iter() + .any(|(rel, subj)| *rel == e.relation && *subj == e.subject) + }) + .cloned() + .collect(); + if uncovered.is_empty() { + Ok(Admitted::UnderDoGrant { binding, effects }) + } else { + Err(ExecRefusal::GrantDoesNotCover { uncovered }) + } + } + }, + } + } + + /// The evidence class of the method `r` names. Does not authenticate. + pub fn classify(&self, r: &MethodRef, evidence: &EvidenceSet) -> EvidenceClass { + let Some(att) = evidence + .attachments + .iter() + .find(|a| a.class == r.class && a.method == r.method && a.sig_rev == r.sig_rev) + else { + return EvidenceClass::Unknown { + causes: vec![UnknownCause::NotAttached { + class: r.class, + method: r.method, + sig_rev: r.sig_rev, + }], + }; + }; + + let defined = |s: &str| { + evidence + .rows + .iter() + .any(|row| row.relation == Relation::Defines && row.subject == s) + }; + + let mut unknown = Vec::new(); + let mut possible = Vec::new(); + let mut effects = Vec::new(); + let mut assumed = BTreeSet::new(); + + let mut visited = BTreeSet::new(); + let mut todo = vec![att.subject.clone()]; + while let Some(subject) = todo.pop() { + if !visited.insert(subject.clone()) { + continue; + } + // Undefined is UNKNOWN; its rows are still read, so an UNJOINED + // row under the same subject is reported too. + if !defined(&subject) { + unknown.push(UnknownCause::NoDefinition { + subject: subject.clone(), + }); + } + let nested = format!("{subject}::"); + for row in evidence + .rows + .iter() + .filter(|row| row.subject == subject || row.subject.starts_with(&nested)) + { + match (row.relation, row.evidence) { + (_, Evidence::Unknown) => unknown.push(UnknownCause::Unjoined(row.clone())), + (_, Evidence::Possible) => possible.push(row.clone()), + (Relation::MayPanic | Relation::WritesCallerMemory, Evidence::Witnessed) => { + effects.push(row.clone()) + } + (Relation::Calls, Evidence::Witnessed) => { + // A callee nested under a subject already in scope + // (a closure body the span join named after its + // enclosing function, with no `DEFINES` row of its + // own) has its rows read through that subject's + // prefix. It is in scope, not an external callee. + let in_scope = visited + .iter() + .any(|v| row.object.starts_with(&format!("{v}::"))); + if in_scope { + } else if row.object == UNNAMED_IMPL { + unknown.push(UnknownCause::UnnamedCallee(row.clone())); + } else if defined(&row.object) { + todo.push(row.object.clone()); + } else if self + .trusted_external + .iter() + .any(|p| row.object.starts_with(p.as_str())) + { + assumed.insert(row.object.clone()); + } else { + unknown.push(UnknownCause::UnauditedCallee(row.clone())); + } + } + (Relation::Defines | Relation::HasImpls, Evidence::Witnessed) => {} + // A relation at an evidence class `parse_rows` rejects. + // Rows built by hand may still carry one: never pure. + (_, Evidence::Witnessed) => { + unknown.push(UnknownCause::Mislabelled(row.clone())); + } + } + } + } + + if !unknown.is_empty() { + EvidenceClass::Unknown { causes: unknown } + } else if !possible.is_empty() { + EvidenceClass::Possible { rows: possible } + } else if !effects.is_empty() { + EvidenceClass::WitnessedEffect { effects } + } else { + EvidenceClass::ProvenPure { + assumed: assumed.into_iter().collect(), + } + } + } +} diff --git a/crates/dt64-admission-probe/tests/integration/admission.rs b/crates/dt64-admission-probe/tests/integration/admission.rs new file mode 100644 index 000000000..c519ad6f8 --- /dev/null +++ b/crates/dt64-admission-probe/tests/integration/admission.rs @@ -0,0 +1,290 @@ +//! The five outcomes on the D-SAG-6 fixture's functions. Each class has a +//! case that fires and a non-trivial case where it must stay silent. + +use dt64_admission_probe::evidence::Relation; +use dt64_admission_probe::fixture::{self, *}; +use dt64_admission_probe::{ + Admitted, DoGrant, ExecRefusal, ExecutionPolicy, Request, UnknownCause, +}; +use lance_graph_dt64::{MethodRef, Refusal, SigRev}; + +fn policy() -> ExecutionPolicy { + ExecutionPolicy { + trusted_external: vec!["core::slice::".into(), "core::iter::".into()], + } +} + +fn decide<'s>( + store: &'s lance_graph_dt64::BindStore, + id: lance_graph_dt64::MethodId, + request: Request<'_>, +) -> Result, ExecRefusal> { + let r = method_ref(store, id); + policy().decide(store, &r, &fixture::span_joined(), request) +} + +// ---- binding is not authorization ------------------------------------- + +#[test] +fn every_fixture_method_admits_but_only_two_execute_pure() { + let s = store(); + let all = [ + COUNT_BELOW, + COUNT_WITH_TALLY, + COUNT_DIV, + COUNT_GENERIC, + COUNT_DYN, + MASK_BELOW, + BELOW_TEST, + UNATTACHED, + ]; + let mut pure = Vec::new(); + for id in all { + let r = method_ref(&s, id); + assert!(s.admit(&r).is_ok(), "{id:?} must authenticate"); + if matches!(decide(&s, id, Request::Pure), Ok(Admitted::Pure { .. })) { + pure.push(id); + } + } + assert_eq!(pure, vec![COUNT_BELOW, BELOW_TEST]); +} + +#[test] +fn an_admit_refusal_passes_through_even_with_perfect_evidence() { + let s = store(); + let mut r = method_ref(&s, COUNT_BELOW); + r.sig_rev = SigRev(2); + let got = policy().decide(&s, &r, &fixture::span_joined(), Request::Pure); + assert!(matches!( + got, + Err(ExecRefusal::Binding( + Refusal::SignatureRevisionMismatch { .. } + )) + )); + let mut r = method_ref(&s, COUNT_BELOW); + r.guard = None; + let got = policy().decide(&s, &r, &fixture::span_joined(), Request::Pure); + assert!(matches!( + got, + Err(ExecRefusal::Binding(Refusal::GuardDropped { .. })) + )); +} + +// ---- 1. proven pure --------------------------------------------------- + +#[test] +fn count_below_is_admitted_pure_and_names_its_assumptions() { + let s = store(); + match decide(&s, COUNT_BELOW, Request::Pure) { + Ok(Admitted::Pure { binding, assumed }) => { + assert_eq!(binding.id, COUNT_BELOW); + assert_eq!(assumed.len(), 3, "{assumed:?}"); + assert!(assumed.iter().all(|c| c.starts_with("core::"))); + } + other => panic!("{other:?}"), + } +} + +#[test] +fn count_below_without_trust_is_unknown_not_pure() { + let s = store(); + let r = method_ref(&s, COUNT_BELOW); + let got = ExecutionPolicy::default().decide(&s, &r, &fixture::span_joined(), Request::Pure); + match got { + Err(ExecRefusal::Unknown { causes }) => { + assert_eq!(causes.len(), 3); + assert!(causes + .iter() + .all(|c| matches!(c, UnknownCause::UnauditedCallee(_)))); + } + other => panic!("{other:?}"), + } +} + +// ---- 2. witnessed effect, under an explicit DO grant ------------------ + +fn grant_for(r: &MethodRef, effects: &[(Relation, &str)]) -> DoGrant { + DoGrant { + method: r.clone(), + effects: effects + .iter() + .map(|(rel, s)| (*rel, s.to_string())) + .collect(), + } +} + +const TALLY_CLOSURE: &str = "sag_fixture::count_with_tally::{closure@L42}::call_mut"; +const DIV_CLOSURE: &str = "sag_fixture::count_div::{closure@L51}::call_mut"; + +#[test] +fn count_with_tally_executes_only_under_a_covering_grant() { + let s = store(); + let r = method_ref(&s, COUNT_WITH_TALLY); + let g = grant_for(&r, &[(Relation::WritesCallerMemory, TALLY_CLOSURE)]); + match decide(&s, COUNT_WITH_TALLY, Request::Do(&g)) { + Ok(Admitted::UnderDoGrant { binding, effects }) => { + assert_eq!(binding.id, COUNT_WITH_TALLY); + assert_eq!(effects.len(), 1); + assert_eq!(effects[0].relation, Relation::WritesCallerMemory); + } + other => panic!("{other:?}"), + } +} + +#[test] +fn count_div_executes_only_under_a_grant_naming_the_panic() { + let s = store(); + let r = method_ref(&s, COUNT_DIV); + let g = grant_for(&r, &[(Relation::MayPanic, DIV_CLOSURE)]); + assert!(matches!( + decide(&s, COUNT_DIV, Request::Do(&g)), + Ok(Admitted::UnderDoGrant { .. }) + )); + // The same subject under another relation does not cover it. + let wrong = grant_for(&r, &[(Relation::WritesCallerMemory, DIV_CLOSURE)]); + assert!(matches!( + decide(&s, COUNT_DIV, Request::Do(&wrong)), + Err(ExecRefusal::GrantDoesNotCover { uncovered }) if uncovered.len() == 1 + )); +} + +// ---- 5. the DO gate refuses ------------------------------------------- + +#[test] +fn witnessed_effects_are_refused_for_pure_execution() { + let s = store(); + for (id, rel) in [ + (COUNT_WITH_TALLY, Relation::WritesCallerMemory), + (COUNT_DIV, Relation::MayPanic), + ] { + match decide(&s, id, Request::Pure) { + Err(ExecRefusal::RequiresDoGate { effects }) => { + assert_eq!(effects.len(), 1); + assert_eq!(effects[0].relation, rel); + } + other => panic!("{id:?}: {other:?}"), + } + } +} + +#[test] +fn an_empty_grant_or_one_for_another_method_does_not_open_the_gate() { + let s = store(); + let r = method_ref(&s, COUNT_WITH_TALLY); + let empty = grant_for(&r, &[]); + assert!(matches!( + decide(&s, COUNT_WITH_TALLY, Request::Do(&empty)), + Err(ExecRefusal::GrantDoesNotCover { uncovered }) if uncovered.len() == 1 + )); + let other = method_ref(&s, COUNT_DIV); + let misdirected = grant_for(&other, &[(Relation::WritesCallerMemory, TALLY_CLOSURE)]); + assert!(matches!( + decide(&s, COUNT_WITH_TALLY, Request::Do(&misdirected)), + Err(ExecRefusal::GrantForOtherMethod { .. }) + )); +} + +// ---- 3. POSSIBLE ------------------------------------------------------ + +#[test] +fn generic_and_dyn_dispatch_are_possible_never_pure() { + let s = store(); + for (id, object) in [(COUNT_GENERIC, "trait:Clause"), (COUNT_DYN, "dynamic")] { + match decide(&s, id, Request::Pure) { + Err(ExecRefusal::Possible { rows }) => { + assert_eq!(rows.len(), 1); + assert_eq!(rows[0].relation, Relation::MayDispatch); + assert_eq!(rows[0].object, object); + } + other => panic!("{id:?}: {other:?}"), + } + } +} + +#[test] +fn a_grant_naming_the_dispatch_row_does_not_lift_possible() { + let s = store(); + let r = method_ref(&s, COUNT_DYN); + let g = grant_for( + &r, + &[( + Relation::MayDispatch, + "sag_fixture::count_dyn::{closure@L36}::call_mut", + )], + ); + assert!(matches!( + decide(&s, COUNT_DYN, Request::Do(&g)), + Err(ExecRefusal::Possible { .. }) + )); +} + +#[test] +fn a_local_buffer_write_is_possible_not_an_authorizable_effect() { + let s = store(); + match decide(&s, MASK_BELOW, Request::Pure) { + Err(ExecRefusal::Possible { rows }) => { + assert_eq!(rows.len(), 1); + assert_eq!(rows[0].relation, Relation::WritesThroughLocalRef); + } + other => panic!("{other:?}"), + } +} + +// ---- 4. UNKNOWN ------------------------------------------------------- + +#[test] +fn below_test_is_unknown_under_the_path_join_and_pure_under_the_span_join() { + let s = store(); + let r = method_ref(&s, BELOW_TEST); + let path = policy().decide(&s, &r, &fixture::path_joined(), Request::Pure); + match path { + Err(ExecRefusal::Unknown { causes }) => { + assert!(causes.iter().any( + |c| matches!(c, UnknownCause::Unjoined(row) if row.relation == Relation::Unjoined) + )); + } + other => panic!("{other:?}"), + } + let span = policy().decide(&s, &r, &fixture::span_joined(), Request::Pure); + assert!(matches!(span, Ok(Admitted::Pure { .. })), "{span:?}"); +} + +#[test] +fn a_method_named_like_a_pure_one_but_unattached_is_unknown() { + let s = store(); + // UNATTACHED is bound under the name "count_below"; the name is never + // identity, so count_below's evidence must not attach to it. + let r = method_ref(&s, UNATTACHED); + assert_eq!(s.admit(&r).unwrap().name, "count_below"); + match policy().decide(&s, &r, &fixture::span_joined(), Request::Pure) { + Err(ExecRefusal::Unknown { causes }) => { + assert!(matches!(causes[..], [UnknownCause::NotAttached { .. }])) + } + other => panic!("{other:?}"), + } +} + +#[test] +fn evidence_for_another_signature_revision_does_not_attach() { + let s = store(); + let r = method_ref(&s, COUNT_BELOW); + let mut ev = fixture::span_joined(); + for a in &mut ev.attachments { + a.sig_rev = SigRev(0); + } + assert!(matches!( + policy().decide(&s, &r, &ev, Request::Pure), + Err(ExecRefusal::Unknown { .. }) + )); +} + +#[test] +fn a_grant_does_not_lift_unknown() { + let s = store(); + let r = method_ref(&s, BELOW_TEST); + let g = grant_for(&r, &[(Relation::Unjoined, "sag_fixture::Impl::test")]); + assert!(matches!( + policy().decide(&s, &r, &fixture::path_joined(), Request::Do(&g)), + Err(ExecRefusal::Unknown { .. }) + )); +} diff --git a/crates/dt64-admission-probe/tests/integration/evidence_rows.rs b/crates/dt64-admission-probe/tests/integration/evidence_rows.rs new file mode 100644 index 000000000..bc197c20c --- /dev/null +++ b/crates/dt64-admission-probe/tests/integration/evidence_rows.rs @@ -0,0 +1,70 @@ +//! The committed rows parse, and the parser rejects rows outside the +//! D-SAG-6 vocabulary. + +use dt64_admission_probe::evidence::{parse_rows, Evidence, Relation, RowError, HEADER}; +use dt64_admission_probe::fixture::{PATH_JOINED_ROWS, SPAN_JOINED_ROWS}; + +fn count(rows: &[dt64_admission_probe::evidence::Row], rel: Relation) -> usize { + rows.iter().filter(|r| r.relation == rel).count() +} + +#[test] +fn committed_rows_parse_with_exact_counts() { + let rows = parse_rows(SPAN_JOINED_ROWS).unwrap(); + // 29 reconstructed rows + 3 closure shim calls (call_once -> call_mut). + assert_eq!(rows.len(), 32); + assert_eq!(count(&rows, Relation::Defines), 7); + assert_eq!(count(&rows, Relation::Calls), 20); + assert_eq!(count(&rows, Relation::MayDispatch), 2); + assert_eq!(count(&rows, Relation::MayPanic), 1); + assert_eq!(count(&rows, Relation::WritesCallerMemory), 1); + assert_eq!(count(&rows, Relation::WritesThroughLocalRef), 1); + assert_eq!(count(&rows, Relation::Unjoined), 0); + let path = parse_rows(PATH_JOINED_ROWS).unwrap(); + assert_eq!(path.len(), 2); + assert_eq!(count(&path, Relation::Unjoined), 1); + assert_eq!(path[1].evidence, Evidence::Unknown); +} + +fn one(line: &str) -> Result, RowError> { + parse_rows(&format!("{HEADER}\n{line}\n")) +} + +#[test] +fn a_possible_relation_labelled_witnessed_is_rejected() { + assert!(matches!( + one("MAY_DISPATCH\tx::f\tdynamic\tcharon\tWITNESSED"), + Err(RowError::EvidenceMismatch { + relation: Relation::MayDispatch, + evidence: Evidence::Witnessed, + .. + }) + )); + assert!(matches!( + one("UNJOINED\tx::f\twhy\tjoin\tWITNESSED"), + Err(RowError::EvidenceMismatch { .. }) + )); + // Silence: the same relations at their own class parse. + assert!(one("MAY_DISPATCH\tx::f\tdynamic\tcharon\tPOSSIBLE").is_ok()); + assert!(one("UNJOINED\tx::f\twhy\tjoin\tUNKNOWN").is_ok()); +} + +#[test] +fn unknown_vocabulary_and_bad_shape_are_rejected() { + assert!(matches!( + one("MAY_EXPLODE\tx::f\t-\tcharon\tWITNESSED"), + Err(RowError::UnknownRelation { .. }) + )); + assert!(matches!( + one("CALLS\tx::f\tx::g\tcharon\tPROBABLY"), + Err(RowError::UnknownEvidence { .. }) + )); + assert!(matches!( + one("CALLS\tx::f\tx::g\tcharon"), + Err(RowError::Columns { got: 4, .. }) + )); + assert!(matches!( + parse_rows("subject\trelation\nCALLS\ta\tb\tc\tWITNESSED"), + Err(RowError::BadHeader(_)) + )); +} diff --git a/crates/dt64-admission-probe/tests/integration/main.rs b/crates/dt64-admission-probe/tests/integration/main.rs new file mode 100644 index 000000000..c7b54ee84 --- /dev/null +++ b/crates/dt64-admission-probe/tests/integration/main.rs @@ -0,0 +1,5 @@ +//! X2 execution-admission policy, against the D-SAG-6 fixture. + +pub mod admission; +pub mod evidence_rows; +pub mod structure; diff --git a/crates/dt64-admission-probe/tests/integration/structure.rs b/crates/dt64-admission-probe/tests/integration/structure.rs new file mode 100644 index 000000000..0f16b5b57 --- /dev/null +++ b/crates/dt64-admission-probe/tests/integration/structure.rs @@ -0,0 +1,185 @@ +//! Structural guards on synthetic rows (labelled synthetic: these subjects +//! are not in the D-SAG-6 fixture). They pin what the fixture alone cannot: +//! that effects are found through local callees, that UNKNOWN dominates +//! POSSIBLE dominates a witnessed effect, and that absence of rows is not +//! purity. + +use dt64_admission_probe::evidence::{parse_rows, Evidence, Relation, Row, HEADER}; +use dt64_admission_probe::fixture::{method_ref, store, CLASS, COUNT_BELOW}; +use dt64_admission_probe::{Attachment, EvidenceClass, EvidenceSet, ExecutionPolicy, UnknownCause}; +use lance_graph_dt64::SigRev; + +fn evidence(body: &str, subject: &str) -> EvidenceSet { + EvidenceSet { + rows: parse_rows(&format!("{HEADER}\n{body}")).unwrap(), + attachments: vec![Attachment { + class: CLASS, + method: COUNT_BELOW, + sig_rev: SigRev(1), + subject: subject.to_string(), + }], + } +} + +fn classify(ev: &EvidenceSet) -> EvidenceClass { + let s = store(); + let r = method_ref(&s, COUNT_BELOW); + ExecutionPolicy::default().classify(&r, ev) +} + +const DEF_F: &str = "DEFINES\tx::f\tFunction\trust-analyzer\tWITNESSED\n"; +const DEF_G: &str = "DEFINES\tx::g\tFunction\trust-analyzer\tWITNESSED\n"; +const F_CALLS_G: &str = "CALLS\tx::f\tx::g\tcharon\tWITNESSED\n"; + +#[test] +fn an_effect_in_a_local_callee_is_found() { + let ev = evidence( + &format!("{DEF_F}{DEF_G}{F_CALLS_G}MAY_PANIC\tx::g\t1 assert\tcharon\tWITNESSED\n"), + "x::f", + ); + match classify(&ev) { + EvidenceClass::WitnessedEffect { effects } => { + assert_eq!(effects.len(), 1); + assert_eq!(effects[0].subject, "x::g"); + } + other => panic!("{other:?}"), + } + // Silence: a pure local callee keeps the caller pure, with no assumption. + let pure = evidence(&format!("{DEF_F}{DEF_G}{F_CALLS_G}"), "x::f"); + assert_eq!( + classify(&pure), + EvidenceClass::ProvenPure { assumed: vec![] } + ); +} + +#[test] +fn a_recursive_cycle_terminates() { + let ev = evidence( + &format!("{DEF_F}{DEF_G}{F_CALLS_G}CALLS\tx::g\tx::f\tcharon\tWITNESSED\n"), + "x::f", + ); + assert_eq!(classify(&ev), EvidenceClass::ProvenPure { assumed: vec![] }); +} + +#[test] +fn unknown_dominates_possible_dominates_effect() { + let effect = "MAY_PANIC\tx::f\t1 assert\tcharon\tWITNESSED\n"; + let possible = "MAY_DISPATCH\tx::f\tdynamic\tcharon\tPOSSIBLE\n"; + let unknown = "UNJOINED\tx::f::{closure@L3}::call_mut\tno symbol\tjoin\tUNKNOWN\n"; + assert!(matches!( + classify(&evidence( + &format!("{DEF_F}{effect}{possible}{unknown}"), + "x::f" + )), + EvidenceClass::Unknown { .. } + )); + assert!(matches!( + classify(&evidence(&format!("{DEF_F}{effect}{possible}"), "x::f")), + EvidenceClass::Possible { .. } + )); + assert!(matches!( + classify(&evidence(&format!("{DEF_F}{effect}"), "x::f")), + EvidenceClass::WitnessedEffect { .. } + )); +} + +#[test] +fn absence_of_rows_is_not_purity() { + // An attachment to a subject the frontend never defined. + let ev = evidence(DEF_G, "x::f"); + match classify(&ev) { + EvidenceClass::Unknown { causes } => { + assert_eq!( + causes, + vec![UnknownCause::NoDefinition { + subject: "x::f".into() + }] + ) + } + other => panic!("{other:?}"), + } + // Silence: the defined neighbour is pure. + assert!(matches!( + classify(&evidence(DEF_G, "x::g")), + EvidenceClass::ProvenPure { .. } + )); +} + +#[test] +fn an_unnamed_trait_impl_call_is_unknown() { + let ev = evidence( + &format!("{DEF_F}CALLS\tx::f\tknown impl\tcharon\tWITNESSED\n"), + "x::f", + ); + assert!(matches!( + classify(&ev), + EvidenceClass::Unknown { causes } if matches!(causes[..], [UnknownCause::UnnamedCallee(_)]) + )); +} + +#[test] +fn a_nested_subject_is_in_scope_but_a_name_sharing_a_prefix_is_not() { + let closure_effect = + "WRITES_CALLER_MEMORY\tx::f::{closure@L9}::call_mut\t1\tcharon\tWITNESSED\n"; + assert!(matches!( + classify(&evidence(&format!("{DEF_F}{closure_effect}"), "x::f")), + EvidenceClass::WitnessedEffect { .. } + )); + let sibling = "WRITES_CALLER_MEMORY\tx::f_other\t1\tcharon\tWITNESSED\n"; + assert!(matches!( + classify(&evidence(&format!("{DEF_F}{sibling}"), "x::f")), + EvidenceClass::ProvenPure { .. } + )); +} + +#[test] +fn a_hand_built_mislabelled_row_is_never_pure() { + // `parse_rows` rejects this row; a caller that builds rows directly can + // still hand one over. + let mut ev = evidence(DEF_F, "x::f"); + ev.rows.push(Row { + relation: Relation::MayDispatch, + subject: "x::f".into(), + object: "dynamic".into(), + witness: "charon".into(), + evidence: Evidence::Witnessed, + }); + assert!(matches!( + classify(&ev), + EvidenceClass::Unknown { causes } if matches!(causes[..], [UnknownCause::Mislabelled(_)]) + )); +} + +/// A call from a closure shim into the closure body names a subject that has +/// no `DEFINES` row (the span join generates closure subjects) but lies +/// inside the analyzed scope, whose rows are already read through its +/// prefix. It is not an unaudited external callee. +#[test] +fn a_call_into_an_in_scope_closure_is_not_an_unaudited_callee() { + let shim = + "CALLS\tx::f::{closure@L9}::call_once\tx::f::{closure@L9}::call_mut\tcharon\tWITNESSED\n"; + let ev = evidence(&format!("{DEF_F}{shim}"), "x::f"); + assert_eq!(classify(&ev), EvidenceClass::ProvenPure { assumed: vec![] }); +} + +/// The silent twin: a name that only shares a prefix with the scope, without +/// the `::` boundary, or a closure of another function, is still unaudited. +#[test] +fn a_call_into_another_functions_closure_stays_unaudited() { + for callee in [ + "x::fg::{closure@L1}::call_mut", + "x::h::{closure@L2}::call_mut", + ] { + let call = format!("CALLS\tx::f\t{callee}\tcharon\tWITNESSED\n"); + let ev = evidence(&format!("{DEF_F}{call}"), "x::f"); + match classify(&ev) { + EvidenceClass::Unknown { causes } => assert!( + causes + .iter() + .all(|c| matches!(c, UnknownCause::UnauditedCallee(_))), + "{callee}: {causes:?}" + ), + other => panic!("{callee}: {other:?}"), + } + } +}