Conversation
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
Security findingsAdvisory findings (1)ℹ️ 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. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #3719 +/- ##
=======================================
Coverage 92.64% 92.64%
=======================================
Files 20 20
Lines 6429 6429
=======================================
Hits 5956 5956
Misses 473 473 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
![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: 76b033373e
ℹ️ 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".
| Why a fact is trusted does not change this core semantics. Anneal may record that | ||
| provenance for diagnostics, auditing, or policy, but an unfinished proof, an | ||
| external semantic assumption, and another unchecked premise are all trusted | ||
| premises at this level. |
There was a problem hiding this comment.
When an analysis leaves a UB obligation unfinished, these lines permit treating the missing proof exactly like an external TCB assumption; together with lines 36–39, a downstream design could therefore report ordinary verification success merely by logging the unproved obligation. That conflicts with PRINCIPLES.md's requirement that unsupported code fail closed and that development-only UB bypasses produce explicitly tainted results. Require unfinished proofs, skipped checks, and tool failures to emit an error or a clearly non-successful/tainted result rather than accepting them as ordinary trusted premises.
AGENTS.md reference: anneal/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
| By default, values passed to an unsafe API are also assumed to satisfy their | ||
| ordinary type invariants. Some unsafe APIs may need to accept values that violate | ||
| invariants normally associated with their types. Whether Anneal permits an unsafe | ||
| API contract to relax such an invariant, and how that permission is expressed, | ||
| remains unresolved. |
There was a problem hiding this comment.
When “ordinary type invariants” includes language validity invariants—as the preceding &str/UTF-8 example indicates—permitting an unsafe API to relax them cannot be a policy choice: producing or passing a value invalid for its Rust type is already undefined behavior, and an unsafe declaration does not suspend that rule. Choosing the permissive branch left open here could therefore certify a call that violates the baseline guarantee before the implementation begins. Require Rust validity invariants for every API, and reserve any opt-out mechanism for library or abstraction invariants that Rust permits an unsafe contract to suspend.
AGENTS.md reference: anneal/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
|
|
||
| At a high level, an Anneal claim has: | ||
|
|
||
| - a **subject** whose behavior is being verified; |
There was a problem hiding this comment.
For cached or CI results, and for crates built under multiple feature, target, or profile configurations, merely saying that a claim has a “subject” does not require the result to identify the exact source/generated artifacts and configuration domain it covers. A proof for one revision or build could therefore be reused as an apparently successful result for different code while still satisfying this schema. Require every successful result to bind an immutable artifact identity and the exact covered configuration and execution domain.
AGENTS.md reference: anneal/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
|
@codex review |
🛡️ Codex Security Review · Automatically triggeredSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a4c6dd1629
ℹ️ 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".
| - **API or library invariants** may be stronger than Rust language validity. | ||
| Rust's conventions may permit an API implementation to rely on such an | ||
| invariant even though violating the invariant is not itself immediate undefined | ||
| behavior. Valid UTF-8 for `str` is an example. |
There was a problem hiding this comment.
The revised split still places valid UTF-8 for str on the relaxable API/library side, but Rust defines a non-UTF-8 str as an invalid value; producing or passing an invalid &str is already undefined behavior, not merely an invariant violation that an unsafe API can opt out of. If the unresolved relaxation in lines 199–203 is applied to this stated example, Anneal could certify a call whose argument is invalid before the implementation begins, contradicting its baseline well-definedness guarantee. Move this example to the language-validity category and use a genuinely library-only invariant here.
AGENTS.md reference: anneal/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
| Every fact Anneal itself needs to justify a reported claim must either be | ||
| established by checked evidence or represented explicitly in the TCB. |
There was a problem hiding this comment.
These lines require unchecked facts to be represented in the TCB, but the revision removes the prior requirements that the trusted code and assumptions be identified in the result and remain visible. A lower-level result format could therefore expose only an assurance-policy name while keeping the actual admissions internal and still satisfy this contract, even though PRINCIPLES.md promises users a TCB audit log whose code and assumptions they can inspect to interpret the conditional guarantee. Require each successful result to expose or immutably reference its complete, concretely identified TCB.
AGENTS.md reference: anneal/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c40555425d
ℹ️ 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".
| TCB. Development workflows may deliberately accept weaker assurance, but their | ||
| results must remain distinguishable from ordinary successful verification. |
There was a problem hiding this comment.
When a development workflow bypasses a required UB obligation, requiring its result to be merely “distinguishable” still permits it to be presented as a weaker successful result without labeling either the result or TCB as tainted or irreparably untrustworthy. That weakens PRINCIPLES.md's explicit rule for UB-bypass modes and could let downstream tooling or users treat an unverified program as a valid success category. Fresh evidence is the newly added development-workflow exception here, which specifies only distinguishability rather than the required taint semantics.
AGENTS.md reference: anneal/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
| The result must identify the assurance policy under which it reports success, so | ||
| that its actual TCB can be interpreted against that policy. |
There was a problem hiding this comment.
When a cached or archived result identifies a policy through a mutable name such as default, these lines allow later policy edits to change whether the recorded TCB qualifies as successful; unlike the TCB references above, the policy is not required to have an immutable identity or version. The same stored result can therefore be reinterpreted under a weaker policy than the one actually evaluated, undermining its auditability. Require the result to embed or immutably reference the exact assurance policy used.
AGENTS.md reference: anneal/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
🛡️ Codex Security Review · Automatically triggeredSecurity review completed. No security issues were found in this pull request. Reviewed commit: Only the user who started this review can view the report in Codex. ℹ️ About Codex security reviews in GitHubThis is an experimental Codex feature. Security reviews are triggered when:
Once complete, Codex will leave suggestions, or a comment if no findings are found. |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c64bcf8e1d
ℹ️ 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".
| For a closed program, Anneal's well-definedness guarantee applies to complete | ||
| executions covered by the claim. |
There was a problem hiding this comment.
For a closed program, this permits the claim's scope to include only executions that are already well-defined—or to give the baseline clause an equivalent requirement—so an unsafe program could receive an ordinary successful result because every excluded execution is simply “not covered.” Precision alone does not prevent this circular scope, undermining the principles that UB-freedom is always on and unsupported code fails closed; require the baseline to cover all executions enabled by the artifact and independently justified environment domain, without assuming the well-definedness it is meant to establish.
AGENTS.md reference: anneal/AGENTS.md:L11-L13
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
🛡️ Codex Security Review · Automatically triggered
Here are some automated security review suggestions for this pull request.
Reviewed commit: c64bcf8e1d
ℹ️ About Codex security reviews in GitHub
This is an experimental Codex feature. Security reviews are triggered when:
- You comment "@codex security review"
- A regular code review gets triggered (for example, "@codex review" or when a PR is opened), and you’re opted in so security review runs alongside code review
Once complete, Codex will leave suggestions, or a comment if no findings are found.
| assume that a `str` contains valid UTF-8 even though constructing a non-UTF-8 | ||
| `str` is not itself immediate undefined behavior. |
There was a problem hiding this comment.
🛡️ Codex Security Review · Automatically triggered
If this contract guides unsafe-API verification, classifying UTF-8 for str as a relaxable API/library invariant can let a contract admit a non-UTF-8 str and still claim baseline well-definedness. Rustc rejects from_utf8_unchecked(&[0xff]) as undefined behavior: a str with invalid UTF-8 is an invalid Rust value, so unsafe cannot make it admissible. Lines 228–235 only block this when correctly classified and then leave library-invariant relaxation open. Fresh evidence versus the earlier review is the newly added assertion that constructing such a str is not immediate UB. Move UTF-8 validity to the language-level category and use a truly library-only invariant here.
Useful? React with 👍 / 👎.
This branch has not been deployed
2 participants
Refine Anneal's shared design contract around a smaller semantic core and clearer dependency order.
This change:
str;One question remains explicitly unresolved: whether and how an unsafe API may relax API or library invariants that are stronger than Rust's language-level requirements for well-defined execution.
Authored by an AI agent acting on Josh Liebow-Feeser's behalf.