Skip to content

X2: DT64 execution-admission policy probe (LAB) - #1891

Merged
AdaWorldAPI merged 5 commits into
mainfrom
ccr-85acaff0-oszq40-x2
Oct 31, 2026
Merged

AdaWorldAPI merged 5 commits into
mainfrom
ccr-85acaff0-oszq40-x2

Conversation

@AdaWorldAPI

Copy link
Copy Markdown
Owner

A lab probe (crates/dt64-admission-probe, its own workspace, excluded from the root) for the execution-admission policy that sits after BindStore::admit.

admit is unchanged. It still authenticates method id, signature revision and guard witness. ExecutionPolicy::decide calls it and then classifies the method's D-SAG-6 evidence rows:

evidence outcome
proven pure (needs a DEFINES row; absence of rows is not purity) Admitted::Pure { binding, assumed }
WITNESSED effect covered by a DoGrant for this exact MethodRef Admitted::UnderDoGrant
WITNESSED effect, no covering grant RequiresDoGate / GrantDoesNotCover / GrantForOtherMethod
any POSSIBLE row Possible (a grant never lifts it)
any UNKNOWN fact Unknown { causes } (never read as false)

Precedence: UNKNOWN, then POSSIBLE, then witnessed effect. Evidence attaches to (class, MethodId, SigRev), never to the method's name.

Fixture outcomes:

  • count_below runs as pure, but only under a trusted-callee list; without the list it is UNKNOWN.
  • count_with_tally and count_div run only under a covering grant.
  • The generic and dyn variants are POSSIBLE.
  • A method that is unattached but carries a pure-looking name is UNKNOWN.

All 8 fixture methods pass admit, and only 2 of them run as pure.

What changed

  • New lab crate crates/dt64-admission-probe, plus its entry in the root exclude list.
  • No change to lance-graph-dt64 or lance-graph-contract.
  • No new classid and no global evidence enum.

Validation

  • cargo test --manifest-path crates/dt64-admission-probe/Cargo.toml: 25 passed, reproduced independently. Clippy -D warnings and fmt are clean.
  • 14 disable runs, all red; the table is in the crate README.

Caveats

  • The evidence rows are reconstructed from the D-SAG-6 board entries (src/fixture.rs cites each group). They are not project_rows.py output, because none is committed. Running Charon on the fixture and committing the real TSV would replace them.
  • Open:
    • who owns the trusted-callee list;
    • who issues a DoGrant;
    • how scope is resolved for closures passed in from elsewhere.

Plan: D-DYNBAG §18.4 X2 (on #1890, not yet on main). Board entry: .claude/board/entries/2026-10-31-x2-dt64-admission-policy.md.


Generated by Claude Code

A typed policy layered after BindStore::admit: admit authenticates, the
policy decides from D-SAG-6 evidence rows whether an admitted method may
execute (pure, under an explicit DO grant, or refused as POSSIBLE /
UNKNOWN / requiring the DO gate).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
14 guards disabled one at a time against b7cfe93, each red. Board entry
records the measured fixture outcomes and the open points (rows are
reconstructed, trust list ownership, DoGrant issuer).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
@coderabbitai

coderabbitai Bot commented Oct 31, 2026 •

Copy link
Copy Markdown

Important

  • Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

Run configuration
  • Source mode: Auto
  • Repository: Unavailable
  • Branch: Unavailable
  • File: No configuration file from this repository applied
  • Commit: Unavailable
  • Layers: Organization UI
  • Review profile: CHILL
  • Plan: Advanced
  • Run ID: ad116b2e-6a0e-4c54-aecb-ed2016fa138e
  • Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

@AdaWorldAPI
AdaWorldAPI marked this pull request as ready for review October 31, 2026 15:48
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Oct 31, 2026 •

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-10-31T15:49:59.429997Z ed5c536 Draft marked ready
ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ed5c536eab

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread crates/dt64-admission-probe/src/lib.rs Resolved
The span join names closure bodies after their enclosing function
(fn::{closure@Lnn}::call_mut) and gives them no DEFINES row, so the
producer's call_once -> call_mut shim call was refused as an unaudited
external callee and every closure-bearing method read UNKNOWN. A callee
nested under a subject already in scope is now treated as in scope; its
rows were already read through the prefix. The fixture gains the shim
rows the producer emits, and two structure tests pin both directions (a
look-alike prefix without the :: boundary, or another function's
closure, stays unaudited).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF
# Conflicts:
#	.claude/board/entries/README.md
@AdaWorldAPI
AdaWorldAPI merged commit c34803d into main Oct 31, 2026
12 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants