PF-Core release evidence hardening and PCS completion gates - #23
Merged
Conversation
Introduce an explicit A0 status table so experimental certificate modes cannot silently claim release-ready evidence. Schemas and unit tests pin the policy surface for downstream binding.
Extend LeanCheckResult and trust/catalog plumbing so release workflows can gate on structured check outcomes instead of opaque exit codes alone.
Require handoff manifests to declare delegated capabilities against resolved evidence so CertifyEdge bridges cannot inherit undeclared authority.
Centralize resolved evidence manifests so handoff and certificate paths share a single, schema-validated view of what evidence was selected and why.
Make contract checks emit a stable semantics_layer projection so certificate modes can cite contract outcomes without re-deriving them ad hoc.
Give EffectFrameCertificate a first-class frame artifact and negative fixtures so extra observed effects fail closed instead of being ignored.
Pin frame-preserved traces to explicit stepState transitions and reject cross-tenant noop cases that would otherwise look vacuously safe.
Introduce PFCoreTheoremManifest so Lean theorem identity is explicit in proof binding, keeping presentation claims aligned with machine-checked obligations.
Expand bundle packaging and verification so consumers get a schema-backed BundleVerificationResult instead of ad-hoc success booleans.
Keep cross-language PF-Core validation on a shared TraceSafe surface so language adapters cannot diverge on fail-closed acceptance.
Make mandatory PCS projection generation and Lean binding fail closed so release catalogs cannot ship without a checked projection witness.
Reject missing, modified, symlink, and traversal payloads with dedicated invalid fixtures so release chains cannot accept hash-only claims.
Resolve pinned distribution assets through a single resolver and add wheel/OCI smoke scripts so consumers can verify packaged verifier artifacts reproducibly.
Move profile requirements into explicit specs evaluated by the engine so operators can reason about gate composition without reading imperative glue.
Keep legacy digests for compatibility while release hashing rejects unsafe floats and out-of-range integers, backed by expanded cross-language vectors.
Pin CertifyEdge provenance and trusted keys so attestation verification fails closed when pins or signatures drift from the registry.
Wire provenance subjects through a ReleaseProvenanceBinding schema so attestation finalize/verify steps share one subject digest contract.
Isolate PF-Core, distribution, and gate jobs so failures surface the owning surface instead of a monolithic workflow collapse.
Extend DenyClosed, PairedExecution, and ResourcePattern surfaces so Workstream C regression suites exercise compositional certificate modes fail-closed.
Encode release checklist gates as executable checks so operators can fail closed before publishing without relying on manual doc walkthroughs alone.
Expose detect/validate paths for effect frames, theorem manifests, and release gates so operators can invoke the new surfaces without bespoke scripts.
Regenerate proof obligations and registry examples so release-chain reports match the tightened payload and projection contracts.
Document claim boundaries, runtime semantics, and remaining gaps so release operators can map new gates to the trust model without reading code diffs.
Keep adapter CI, CertifyEdge dry-runs, and protocol materializers aligned with the hardened release verification entrypoints.
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
1 participant
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
Test plan