V45 Gate 16: Proof Families And Generated Artifacts#219
Conversation
Adds deterministic source-safe V45 proof-family generation, draft V45 PROVEN output, generated spec-family and canonical-input reports, package test coverage, workflow bindings, and a gate checker for generated proof closure.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![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: 086fd27c27
ℹ️ 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".
| const witnessFailures = witnessArtifactInventory.flatMap((entry) => { | ||
| if (!entry.present) return [`missing witness artifact ${entry.relativePath}`]; | ||
| if (!entry.parseable) return [`unparseable witness artifact ${entry.relativePath}`]; | ||
| if (!entry.sourceSafe) return [`source-unsafe witness artifact ${entry.relativePath}`]; | ||
| return []; |
There was a problem hiding this comment.
When a required witness JSON is present, parseable, and contains no forbidden marker but reports a failed verdict such as passed: false or status: "repair-required", this branch returns no failure, so the V45 artifact can still emit status: "pass" and the aggregate proof can pass after regeneration. That contradicts the fail-closed contract for stale or contradictory witness evidence; use the parsed witness verdict/status/source-safety fields to reject non-passing witness artifacts.
Useful? React with 👍 / 👎.
| const failures = [ | ||
| ...sourceEvidenceFailures, | ||
| ...witnessFailures, | ||
| ...(forbiddenMarkerDetected ? [`${input.definition.title} artifact contains a secret-shaped marker`] : []), | ||
| ]; |
There was a problem hiding this comment.
If any path listed in generatedArtifactAndTestBindings is deleted or renamed, this artifact still passes because the failure list is built only from source evidence, witness artifacts, and secret-marker checks, while the bindings are only counted later. Since these bindings are the declared tests/workflows for the proof family and the repair text says missing tests must fail closed, missing binding files should be checked here before allowing failures.length === 0.
Useful? React with 👍 / 👎.
1 participant
Summary
Validation