Phase7/shared hash vector ci#3
Merged
Merged
Conversation
Replace mojibake logical operators with proper UTF-8, move imports before module docstrings for Lean 4, trim PCS.lean to existing modules, and fix ReleaseChain theorem destructuring.
Emit concrete_trace_safe_prop and concrete_allowed_events_allowed from codegen, extend theorems_checked and LeanKernelChecked validation, and add contract_semantics_checked to PFCoreCertificate.v0.
Remove duplicate validate helpers, fix LeanCheckResult detection for PF-Core results, skip compiled ToolUseTrace in pf-core fixtures, add pf-core conformance suite, and separate PCS ProofChecked from PF-Core LeanKernelChecked in CLI disclaimers.
Document meaning, trusted use, and non-implications for theorems across PFCore Lean modules.
Add Rust and TypeScript PF-Core hash recomputation, trace hash-chain validation, claim_class checks, release-verify PF-Core steps, and expanded cross-language tests.
Tracks release gates for PF-Core kernel promotion so operators know what must pass before production use.
Explains which theorems are codegen-backed versus hand-maintained so claim boundaries stay honest.
Documents platform-specific Lean toolchain steps so CI and local Windows dev stay aligned.
Records user-visible PF-Core semantics and validation changes for release notes.
Clarifies trusted inputs and discharge assumptions after Tier 1 contract semantics land.
Aligns certificate claims with lean vs runtime layers so overclaiming is explicit.
Documents semantics_layer fields and validation rules that gate Lean-checked certificates.
Captures remaining PF-Core work and closed gaps after split validation and fixtures.
Updates non-interference story to reference contract semantics and runtime observations.
Walks through invalid fixture families introduced for semantics and kernel checks.
Adds semantics-layer and adapter verification steps before tagging PF-Core releases.
Separates Lean kernel trust from runtime observation trust at the contract boundary.
Maps new invalid traces and semantics fields onto PCS trace_certificate expectations.
Contracts declare per-field lean vs runtime layers at the source so certificates cannot overclaim Lean discharge.
Certificate schema encodes proof term references required when lean_kernel_checked is asserted.
Observation schema carries fields validated against contract semantics_layer at runtime.
Centralizes parsing and checks for per-field lean vs runtime semantics on PF-Core contracts.
Wires semantics_layer into contract hashing and validation so lean/runtime fields stay consistent.
Splits validate.py by moving artifact detection into validate_detect for clearer Tier boundaries.
Moves PCS envelope validation into validate_pcs_core to isolate PF-Core work.
Concentrates PF-Core trace, certificate, and observation checks in validate_pf_core.
Isolates semantics_layer and kernel-checked certificate rules in validate_semantics.
Keeps public validate API stable while delegating to split modules.
Records the mechanical split used to maintain validate module boundaries.
Applies semantics_layer checks when validating PF-Core runtime observations.
Trace references a contract hash that is not bundled with the artifact set.
Invalid trace where an allowed event violates tenant isolation expectations.
Observation sequence omits a denied runtime event required for audit.
Certificate asserts kernel checked while build was skipped.
Kernel-checked claim without accompanying contract bundle.
Trace asserts lean discharge without proof_ref metadata.
Certificate missing proof_term_ref while claiming lean_kernel_checked.
PF-Core trace breaks hash chain via mismatched previous_event_hash.
Updates contract.json to reflect semantics_layer fields used by Tier 1 validation.
Adds observation fields required by updated PFCoreRuntimeObservation schema.
Aligns unknown capability negative test with runtime observation schema.
Aligns unknown effect negative test with runtime observation schema.
Valid contract includes semantics_layer for lean vs runtime discharge.
Trace aligns with semantics-aware contract hashing and claim_class rules.
Observation carries schema fields validated against contract semantics.
Observation carries schema fields validated against contract semantics.
Observation carries schema fields validated against contract semantics.
Observation carries schema fields validated against contract semantics.
CertifyEdge emits certificates that respect semantics_layer and kernel proof refs.
CLI surfaces Tier 1-3 validation and adapter hooks for PF-Core artifacts.
Local script mirrors CI adapter verification for PF-Core bundles.
Orchestrates adapter checks in CI-compatible environments.
Generates deferred-tier invalid fixtures kept out of default example set.
Workflow runs semantics tests, hash vectors, and adapter scripts on PF-Core changes.
Covers semantics_layer validation rules across contracts and certificates.
Exercises deferred invalid fixtures without bloating default CI time.
Asserts Python, Rust, and TypeScript agree on new semantics fixtures.
Stage1 harness aligns with split validate modules and schema fields.
Stage2 checks kernel-checked and observation semantics end to end.
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.
No description provided.