Repository navigation
ruff_charon: no '?' dispatch targets; record witnessed effects with exact assert kind - #135
Merged
Merged
Conversation
…ed dispatch targets Behaviour-preserving extraction (missing names still render as '?'), plus a test that fails on it: a dispatch whose trait or method has no name must get no target, since a shared '?' placeholder merges distinct calls. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX
…7 producer side) A dispatch whose trait or method has no name is recorded as a CALLEE_NOT_NAMED residual (the existing convention for an unnamed callee) instead of a MAY_DISPATCH row to '?::?'. One harvested call is still one row or one residual, so the receipt stays conserved. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX
The committed cg_lib LLBC has an overflow check in util::double (x * 2) that no output records; util::unit has none. Expect <crate>.effects.tsv with one row per witnessed effect and its exact kind. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX
…cer side) Each import now writes <crate>.effects.tsv (version 1: subject, effect, kind, file, start, end), one row per occurrence: - ASSERT with Charon's BuiltinAssertKind tag (Overflow:<BinOp>, BoundsCheck, DivisionByZero, ...; User for a source assert!); - DEREF_WRITE Arg / Local. The counters printed by calls_text are unchanged. It is an observation list: a function with no row is not proven pure (Charon passes may fold checks into fallible operations, callees' effects and unstructured bodies are not recorded). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX
…run: 3 x Overflow:Add) The first occurrence test could not fail when same-kind effects were collapsed (no cg_lib function repeats a kind). It now uses cg_app::run; the reference-count check is kept as its own test. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars.
 |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a36cdb9703
ℹ️ 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".
…ixture derefw.rs writes twice through argument-rooted derefs, once through a local reference, and has a function that assigns only locals. The new test pins the emitted kinds and counts, so dropping the rows or swapping Arg/Local fails. Codex P1 on #135. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX
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
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.
Summary
These are producer-side fixes from the Semantic Grammar Recovery map (operator decisions S1/S2, items B7 and B1).
No placeholder dispatch targets (B7).
MAY_DISPATCHwhose trait or method has no name was emitted as?::?. Every unresolved target shared that one symbol, and the IMPLEMENTS join merged distinct calls through it.CALLEE_NOT_NAMEDresidual. That is the existing convention for an unnamed callee.?path segment at intake (defence in depth,claude/sgr-coverage-gates).Witnessed effects (B1). Every import writes
<crate>.effects.tsv(version 1:subject, effect, kind, file, start, end), one row per occurrence:ASSERT, with Charon'sBuiltinAssertKindtag:Overflow:<BinOp>,BoundsCheck,DivisionByZero, and so on, orUserfor a sourceassert!;DEREF_WRITEArg/Local.Subjects equal the
DEFINESsubjects, so effects join to the relation rows. The file is an observation list. A function with no row is not proven pure:The
calls_textcounters are unchanged.Test plan
Each test was committed red first, then the fix.
may_dispatch_objectunit tests: unnamed trait/method → no target; the twin is a named target.tests/effects.rs(5 tests), on the committed LLBC:double/triple→Overflow:Mul;Square::area→[DivisionByZero, Overflow:Mul];unithas no row (silence twin);cg_app::runhas 3 ×Overflow:Add(one row per occurrence);cg_lib.llbc_calls.txt.--all-targets -D warningsis clean; fmt is clean.Disable runs, each red:
?fallback restoredThe first version of the occurrence test stayed green under the collapse disable, because no
cg_libfunction repeats an assert kind. It was rewritten oncg_app::run.Remaining
effects.tsvyet. Promoting effects into a shared evidence grade is deferred (S3).Not to be merged automatically.
Generated by Claude Code