PF-Core production kernel: claim classes, Lean research, CI fixes#5
Merged
Conversation
Add KnownCapability and KnownCapabilityEffect to the Lean kernel so file_write_capability_aligns_write_footprint is sound via catalog effect labels rather than an incorrect projection from CapabilityMatchesEffects.
Export elan PATH in CI lean job, run verify-proof-binding after lean-check, and separate runtime smoke from full LeanKernelChecked release verification.
CI rust job runs cargo fmt --check; format paths added in PF-Core vectors.
Normalize labtrust-release fixture digests to LF byte hashes, refresh RELEASE_FIXTURE_MANIFEST and related pins, and enforce eol=lf via gitattributes.
Align release manifests and benchmark goldens with canonical hashing, restore ToolUseCertificate detection, and enforce LF for examples/benchmarks so Linux CI matches local validation.
… wording. Refresh RELEASE_FIXTURE_MANIFEST hashes after LF normalization and rephrase tool-use workflow limitations to satisfy PF-Core claim audit.
Fix PFCore Capability Lean proof with match-based case split and align RELEASE_FIXTURE_MANIFEST with Linux file digests.
Use tauto for catalog membership iff and re-materialize benchmark goldens after Linux-aligned manifest digests.
Prove knownCapabilityEffectD_sound by case-splitting on Effect and capability patterns, and fix file-write corollary contradictions so PFCore builds on CI again.
Emit schema-valid PCS LeanCheckResult documents, refresh gallery manifest digests during benchmark materialization, use pcs-envelope in lean-trust CLI tests, and tighten deferred registry/conformance helpers.
Refresh release-chain fixtures, benchmark reports/runs, shared hash vectors, and gallery manifest digests using canonical LF-normalized Python hashing to match Linux CI.
Replace match-based KnownCapabilityEffect with a finite catalog list so soundness follows decide_eq_true_iff, matching Capability.lean and fixing Lean 4.14 build failures.
Re-materialize tool-use/computation releases and protocol valid examples so release_manifest pins match release_chain_validation_result bytes on Linux CI.
Refresh RELEASE_FIXTURE_MANIFEST scientific_memory_import_report digest and stop materialize_tool_use from reintroducing audit-flagged limitations_notice phrasing.
Correct contract refinement post direction, tenant isolation extraction, and operational frame preservation proofs so PFCore builds past Action.lean.
Regenerate WorkflowProfile.v0 digest after limitations_notice wording change for audit-claims compliance.
Close insertResource membership cases and use Option.some.injEq for stepState injections.
Normalize manifest digests to LF content and write JSON with newline=LF so Linux CI matches Windows materialization.
Convert fixture JSON to LF line endings and refresh manifest, benchmark, and shared hash digests for Linux CI parity.
Update lean check and release manifest hashes after LF-normalized materialization.
Fix insertResource and stepState proofs; normalize protocol fixture writes and validation digest paths for LF/Linux CI parity.
Finish stepState frame proof with explicit post-state substitution; expand file_read_allowed principal capabilities and refresh trace hashes.
Repair insertResource membership and stepState equality extraction; import check_pf_core_invalid_fixtures in validate_semantics.
Resolve ruff lint/format gate, finish insertResource and stepState proofs, and drop unused test variable.
Pins trace-hash mismatch failure so LabTrust QC release cannot bypass PF-Core chain checks.
Updates legacy handoff negative case to match current PCS-to-PF-Core handoff validation.
Ensures missing QC result cases remain blocked at the LabTrust release trust boundary.
Rejects placeholder commit pins in LabTrust QC release negative benchmarks.
Updates import-failure negative benchmark for LabTrust QC release-grade checks.
Pins stale-trace-after-certificate failure at the PF-Core certificate boundary.
Updates trace-hash tamper negative case for shared hash-vector CI alignment.
Ensures unauthorized LabTrust release attempts fail under current CertifyEdge gates.
Updates positive LabTrust QC release benchmark pins after release-chain Lean integration.
Aligns tool-use rejected-certificate negative benchmark with PF-Core certificate semantics.
Updates trace-hash negative benchmark for cross-language PF-Core hash parity.
Pins unauthorized tool-call failure at the tool-use safety trust boundary.
Updates positive tool-use release-chain benchmark after direct-trace validation changes.
Clarifies which claims certificates may assert so consumers do not over-trust beyond the PF-Core kernel.
Records how observational and direct-trace parity fit the broader compositional trust plan.
Tracks remaining gaps now that release-chain Lean and hash-vector CI cover more of the boundary.
Explains observational equivalence obligations that guard against hidden channels at the trust boundary.
Walks reviewers through Lean release-chain and hash-vector checks during demos.
Adds direct-trace and release-grade Lean items required before calling the kernel production-ready.
Lists release-grade Lean and cross-language hash steps gating PF-Core releases.
States which artifacts and formal checks define the PF-Core trusted computing base.
Describes how CI CertifyEdge gates enforce the PF-Core trust boundary on every change.
Summarizes evidence required before merging phase-seven trust-boundary work.
Outlines formalization path for PCS envelopes atop pinned PF-Core release bundles.
Reorder decidable NI helpers, fix trace induction binders, and align Python/Rust lint with workflow checks.
Use ev after head substitution in Observational.lean and simplify capability object access for CI clippy.
Rewrite the lowEventD decider clash proof after head substitution so Lean 4 accepts the cases split.
Close the false decider branch with simp-normalized bool cases instead of rewriting an equality.
Let simp discharge the false decider branch without an extra cases tactic.
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
python -m pytestPF-Core stage and tier suites locallycargo testinrust/crates/pcs-corefor PF-Core validationlake buildfor PCS and PFCore Lean libraries (where Lean toolchain available)examples/pf-core-*