Phase 7 PR-2: Shared hash vector CI with PF-Core#2
Merged
Conversation
Document field-by-field correspondence between PCS release artifacts and PF-Core traces per Phase 7 checklist. Cross-reference shared hash rules and the LabTrust replay path used by normalize_release.py.
Clone provability-fabric-core at pf-core-v0.6.0 and byte-compare adapters/pcs hash vector fixtures with python/tests/hash_vectors.
Add pytest wrapper for the cross-repo vector diff script and assert TraceCertificate digest retains sha256: prefix handling.
Wire verify-pf-core-hash-vectors.sh into the Python CI job so drift against provability-fabric-core pf-core-v0.6.0 fails the build.
Keep codegen Lean modules out of version control while retaining the Generated directory placeholder for local lean-check runs.
Anchor PF-Core work to explicit scientific-trust outcomes so later schemas, proofs, and CLI gates share one north star.
Make ambient trust dependencies auditable instead of implicit in runtime checks and Lean theorems.
Bound what adversaries can do so claim classes and non-interference properties target real failure modes.
Clarify which components must be correct for certificates to mean anything to downstream consumers.
Prevent over-claiming by tying each certificate type to the artifacts and checks that may support it.
Track remaining engineering and proof debt so phase gates close deliberately rather than by omission.
Give implementers a single reading of allow/deny and scope rules used by Lean and Python validators.
Explain tenant and authority isolation claims that TraceCheck and runtime replay must uphold.
Define how PF-Core certificates attach to PCS release artifacts for cross-protocol verification.
Give operators a repeatable gate list before tagging PF-Core-capable PCS releases.
Support external review with a concise view of what PF-Core does and does not certify.
Walk reviewers through validate, lean-check, and bridge flows with predictable fixtures.
Give proof consumers a quick map from formal names to assurance statements.
Centralize enums and cross-field constraints reused by PF-Core artifact schemas.
Type principals so traces, contracts, and certificates refer to actors consistently.
Encode capability grants checked during contract evaluation and Lean decoding.
Model resources and scopes for tenant isolation and deny-by-default rules.
Describe side effects so runtime observations can be matched to policy.
Represent attempted actions linked to events in PF-Core traces.
Capture allow/deny outcomes required for soundness and replay checks.
Hash-chained events anchor trace integrity for validators and Lean codegen.
Define the canonical trace envelope consumed by Python, TypeScript, and Lean.
Serialize policy rules evaluated by contract decide and validate-contracts.
Bridge raw runtime telemetry into typed observations for replay and certification.
Constrain authority delegation between principals without scope expansion.
Isolation failure detectors should reject this trace shape.
Tampered tool-use compile missing a deny event from the trace.
Integrity break on a single event hash for validator tests.
Top-level trace digest tamper case for structural checks.
Delegation that widens capabilities beyond permitted subset.
Tool-use handoff path that expands compile authority illegally.
Observation without required principal for schema and replay gates.
Access outside declared resource scope for contract tests.
Capability not in registry should fail validation.
Unregistered effect enum rejected before replay.
Lock early PF-Core schemas and registry invariants before runtime work lands.
Regression tests for trace hashing and structural validation behavior.
Ensure contract decide and replay agree on allow/deny fixtures.
Guard trace-to-Lean codegen output used by lean-check.
Cover certificate assembly and PCS bridge artifact rules.
Extend Phase 7 parity coverage beyond the standalone adapter script.
CI can fail when claim docs drift from registered metadata.
Mock CertifyEdge path used in CI without external services.
Keep shell demo script aligned with CLI expectations.
Python, TypeScript, and Rust must agree on PF-Core artifact validity.
Wire pytest into Phase 7 pf-core tag comparison on every CI run.
Expose new artifact types to downstream TS consumers and validators.
Keep browser and Node validators aligned with Python PF-Core rules.
Prevent schema drift from breaking published TypeScript validation.
Cross-language parity for PCS core consumers embedding Rust validation.
Run stage tests, pf-core CLI audits, fixture validation, and lake build on every push.
Resolve conflicts by combining main PCS/benchmark/protocol work with PF-Core Lean, CLI, registry, and CI gates. Unified LeanCheckResult schema uses oneOf for PCS proof-obligation and PF-Core lean-check shapes; ToolUseTrace keeps handoffs and git_commit alignment from both sides.
Align tool-use limitations_notice with claim-boundary wording and refresh digests.
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
scripts/verify-pf-core-hash-vectors.shto byte-compare PCS vectors with provability-fabric-coreadapters/pcs/tests/fixtures/hash_vectors/at tagpf-core-v0.6.0python/tests/test_pf_core_hash_vector_parity.pyTest plan
pytest python/tests/test_pf_core_hash_vector_parity.py -v