Phase 0-7: correctness, protocol hardening, and release-quality gates - #6
Merged
Conversation
Keep local provision and packaging outputs out of the tree so release work stays reproducible.
Reject traversal, absolute, and control-character paths before filesystem access so validators fail closed on unsafe artifact references.
Switch from foldr to foldl so oldest-first JSON event arrays match Trace.events, with round-trip theorems for the trusted Lean bridge.
Tighten protocol surfaces for integrity digests and format-assertion probes used by Phase 1 hardening.
Define PCS/PF-Core projection and kernel/bundle manifests so extracted proof fields bind to digests instead of placeholders.
Give release bundles a typed place to record live or absent external attestation without inventing digests.
Align common format assertions and certificate/obligation/release schemas with fail-closed protocol checks.
Capture invalid duration, email, hostname, UUID, date-time, and URI cases so format enforcement stays testable.
Make Python hashing match the Phase 1 canonicalization contract so cross-language digests stay aligned.
Keep the Rust validator digest path consistent with Python so shared hash vectors remain authoritative.
Preserve cross-language digest parity for artifact hashing in the TS package.
Check key ordering, unicode, integer boundaries, and escape handling so all language ports share one golden set.
Regenerate digests so conformance suites exercise the tightened canonical JSON rules.
Fail closed on missing dataset/environment/run digests, duplicate result hashes, and undeclared result digests for CertificateChecked releases.
Generate harness fixtures that cover declared-hash and result-set mismatch failures.
Provide concrete negative examples so release-chain tests can assert the new witness checks.
Keep existing examples aligned with the stricter ComputationWitness digest rules.
Report which validator, Lean, and CertifyEdge capabilities are actually available instead of assuming a full verifier install.
Lock external tool and workflow pins so CI and provision scripts resolve reproducible artifacts.
Clarify reporting, trusted boundaries, and ownership expectations for release-grade PF-Core work.
Improve review routing and automated dependency/security scanning for the release branch.
Lock in format assertions, path containment, and related schema checks introduced for Phase 1.
Reject missing or placeholder proof identifiers instead of inventing digests during Lean codegen.
Require digest-backed projection entries so PCS envelopes cannot emit unknown certificate or release IDs.
Hash Lean-relevant fields independently of the full trace envelope for concrete term emission.
Drive artifact, commit, and handoff checks from shared specs so domain validators can converge on one fail-closed path.
Verify fail-closed extraction and release-profile engine behavior against malformed envelopes.
Support digest typing and effect classification used by deny-closed and observed-effect modules.
Separate declared action effects from runtime observations so attestation assumptions stay explicit.
Constrain declared deny records against mutating effects and tool invocations without changing base EventSafe.
Document instrumentation assumptions and lock deny-closed/observed-effect behavior in Python tests.
Cover compositional, contract, effect-frame, handoff, and TraceSafe failure modes used by GeneratedLeanProof evidence.
Record live CertifyEdge checks or explicit absence notices without fabricating attestation digests.
Make local and CI installs resolve pinned elan/CertifyEdge artifacts before release gates run.
Support reproducible wheel builds and distribution docs for the verifier install profile.
Wire Phase 2/6 gates, provenance attestations, and pinned actions into the main verification pipelines.
Keep Windows and Unix local runners aligned with the expanded CI checklist.
Emit catalog metadata that distinguishes proved, scaffolding, and deferred claims for Phase 4.
Propagate obligation-extraction errors and projection digests so GeneratedLeanProof evidence cannot invent identifiers.
Bundle validation, CertifyEdge checks, and runtime helpers consume the Phase 3-6 surfaces.
Register projection, integrity, and attestation schemas so detection and conformance stay in sync.
Keep LabTrust, computation, and tool-use wrappers compatible while sharing declarative bindings.
Surface capabilities, projection, and attestation helpers from the package API.
Assert GeneratedLeanProof and catalog status fields reject placeholder identifiers.
Keep Python/Rust/TS parity checks aligned with projection and observed-effect changes.
Adjust expectations for TenantProjectionIsolation wording and certificate-mode fixtures.
Lock Hypothesis coverage, Pyright, and dependency pins for Phase 7 verification quality.
Record Phase 7 quality-gate criteria beyond unit tests alone.
Keep the Rust validator aligned with Python projection, catalog status, and schema registry changes.
Provide a starting point for Phase 7 fuzz coverage without claiming a production fuzzer yet.
Mirror schema registry and catalog status fields so TS examples stay cross-language consistent.
Refresh GeneratedLeanProof artifacts after fail-closed codegen and digest binding changes.
Reflect instrumentation, attestation, and fail-closed extraction boundaries introduced in Phases 3-6.
Separate proved TenantProjectionIsolation from research paired-execution scaffolding.
Record Phase 0-7 checklist progress and pin-driven CI expectations for the release branch.
Point contributors at new schemas, projection docs, security policy, and quality-gate material.
Keep domain and cross-domain benchmark digests consistent with regenerated release artifacts.
|
You are seeing this message because GitHub Code Scanning has recently been set up for this repository, or this pull request contains the workflow file for the Code Scanning tool. What Enabling Code Scanning Means:
For more information about GitHub Code Scanning, check out the documentation. |
6 tasks
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
2 participants
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
This branch lands the Phase 0–7 correctness and release-readiness work for PCS / PF-Core: shared hashing and path safety through protocol hardening, distribution honesty, envelope binding, TCB clarity, runtime semantics, external attestation, and quality gates.
canonical_json_v1vectors; aligned Rust/TypeScript hashing; declared computation witness hashes with fail-closed invalid fixtures; containment-checked path resolution for untrusted refs; Trace event order fix.Stable release caveat: A production-stable release still needs a real CertifyEdge pin and org signing keys. Until those are in place, the honest ship mode is the technical preview path documented in this branch.
~61 commits ahead of
main(~298 files).Test plan