From 93d3fc78f1863cfd8f1be675f6b4cdbf7c2ef1fd Mon Sep 17 00:00:00 2001 From: Mayckon Giovani Date: Wed, 16 Sep 2026 18:17:58 -0300 Subject: [PATCH] formal: add replay boundary kernel --- docs/formal_certificates.md | 2 +- formal/lean/Noetheris.lean | 1 + formal/lean/Noetheris/ReplayBoundary.lean | 71 ++++++++++++++++++ formal/lean/README.md | 3 + formal/tla/README.md | 3 +- formal/tla/external_candidate_replay.tla | 88 +++++++++++++++++++++++ 6 files changed, 166 insertions(+), 2 deletions(-) create mode 100644 formal/lean/Noetheris/ReplayBoundary.lean create mode 100644 formal/tla/external_candidate_replay.tla diff --git a/docs/formal_certificates.md b/docs/formal_certificates.md index 391e312..d42254c 100644 --- a/docs/formal_certificates.md +++ b/docs/formal_certificates.md @@ -42,4 +42,4 @@ When a certificate includes `external_replay_artifact`, `external_replay`, `exte ## Formal Surface -Lean models a simplified certificate-validity predicate and small true lemmas. The executable Python/Rust validators are the release enforcement path; Lean artifacts define reviewable kernels rather than whole-repository proofs. +Lean models a simplified certificate-validity predicate, a replay-boundary acceptance predicate, and small true lemmas. The replay kernel states that an accepted candidate preserves reported/recomputed energy equality and hash identity under a declared context. The executable Python/Rust validators are the release enforcement path; Lean artifacts define reviewable kernels rather than whole-repository proofs. diff --git a/formal/lean/Noetheris.lean b/formal/lean/Noetheris.lean index 622ce75..a18460e 100644 --- a/formal/lean/Noetheris.lean +++ b/formal/lean/Noetheris.lean @@ -6,3 +6,4 @@ import Noetheris.StructuralIR import Noetheris.QuboEnergy import Noetheris.MigrationPolicy import Noetheris.CircuitOracle +import Noetheris.ReplayBoundary diff --git a/formal/lean/Noetheris/ReplayBoundary.lean b/formal/lean/Noetheris/ReplayBoundary.lean new file mode 100644 index 0000000..2dfb107 --- /dev/null +++ b/formal/lean/Noetheris/ReplayBoundary.lean @@ -0,0 +1,71 @@ +import Noetheris.Basic + +namespace Noetheris + +structure ReplayContext where + expectedProblemHash : String + expectedCompiledModelHash : String +deriving Repr, DecidableEq + +structure ReplayCandidate where + submittedProblemHash : String + submittedCompiledModelHash : String + reportedEnergy : Energy + recomputedEnergy : Energy + assignmentComplete : Bool + metadataWellFormed : Bool +deriving Repr, DecidableEq + +def HashIdentityHolds (context : ReplayContext) (candidate : ReplayCandidate) : Prop := + candidate.submittedProblemHash = context.expectedProblemHash ∧ + candidate.submittedCompiledModelHash = context.expectedCompiledModelHash + +def EnergyAgreementHolds (candidate : ReplayCandidate) : Prop := + candidate.reportedEnergy = candidate.recomputedEnergy + +def ReplayAccepted (context : ReplayContext) (candidate : ReplayCandidate) : Prop := + HashIdentityHolds context candidate ∧ + EnergyAgreementHolds candidate ∧ + candidate.assignmentComplete = true ∧ + candidate.metadataWellFormed = true + +theorem accepted_candidate_preserves_energy_agreement + (context : ReplayContext) + (candidate : ReplayCandidate) + (hAccepted : ReplayAccepted context candidate) : + candidate.reportedEnergy = candidate.recomputedEnergy := by + exact hAccepted.right.left + +theorem accepted_candidate_matches_problem_hash + (context : ReplayContext) + (candidate : ReplayCandidate) + (hAccepted : ReplayAccepted context candidate) : + candidate.submittedProblemHash = context.expectedProblemHash := by + exact hAccepted.left.left + +theorem accepted_candidate_has_complete_assignment + (context : ReplayContext) + (candidate : ReplayCandidate) + (hAccepted : ReplayAccepted context candidate) : + candidate.assignmentComplete = true := by + exact hAccepted.right.right.left + +def replayContextExample : ReplayContext := + { + expectedProblemHash := "sha256:problem", + expectedCompiledModelHash := "sha256:compiled" + } + +def acceptedReplayCandidateExample : ReplayCandidate := + { + submittedProblemHash := "sha256:problem", + submittedCompiledModelHash := "sha256:compiled", + reportedEnergy := 10, + recomputedEnergy := 10, + assignmentComplete := true, + metadataWellFormed := true + } + +#eval acceptedReplayCandidateExample.reportedEnergy + +end Noetheris diff --git a/formal/lean/README.md b/formal/lean/README.md index 3b26369..f4a5c3f 100644 --- a/formal/lean/README.md +++ b/formal/lean/README.md @@ -12,6 +12,9 @@ Included modules: - `QuboEnergy.lean`: binary assignments and QUBO energy evaluation. - `MigrationPolicy.lean`: simple policy predicates for asset migration choices. - `CircuitOracle.lean`: finite truth-table semantics for Boolean oracle evaluation. +- `ReplayBoundary.lean`: simplified replay acceptance over hashes, assignment completeness, metadata well-formedness, and reported/recomputed energy equality. + +`ReplayBoundary.lean` is a small formal kernel for the external-candidate replay boundary. It proves local lemmas about the simplified predicate only; it is not an end-to-end proof of the Python or Rust implementation. Build with: diff --git a/formal/tla/README.md b/formal/tla/README.md index 509ee13..956e5c0 100644 --- a/formal/tla/README.md +++ b/formal/tla/README.md @@ -6,5 +6,6 @@ The TLA+ files model small safety surfaces used by Noetheris examples. - `threshold_policy.tla` models authorization threshold, whitelist, and time-window safety. - `pq_migration_policy.tla` models migration dependency ordering. - `saga_failure_semantics.tla` models terminal consistency for a small compensating-transaction flow. +- `external_candidate_replay.tla` models the submitted, verified, and rejected states for a single external solver candidate under hash, energy, assignment-domain, and metadata checks. -They are compact specifications intended for review and later bounded model-checking harnesses. +They are compact specifications intended for review and bounded model-checking harnesses. The replay specification is scoped to a single candidate and does not assert correctness of the full executable implementation. diff --git a/formal/tla/external_candidate_replay.tla b/formal/tla/external_candidate_replay.tla new file mode 100644 index 0000000..57e9e9a --- /dev/null +++ b/formal/tla/external_candidate_replay.tla @@ -0,0 +1,88 @@ +---- MODULE external_candidate_replay ---- +EXTENDS FiniteSets + +CONSTANTS + ExpectedProblemHash, + ExpectedCompiledModelHash, + SubmittedProblemHash, + SubmittedCompiledModelHash, + ReportedEnergy, + RecomputedEnergy, + AssignmentComplete, + MetadataWellFormed + +VARIABLES state, reasons + +Init == + /\ state = "submitted" + /\ reasons = {} + +HashIdentityHolds == + /\ SubmittedProblemHash = ExpectedProblemHash + /\ SubmittedCompiledModelHash = ExpectedCompiledModelHash + +EnergyAgreementHolds == + ReportedEnergy = RecomputedEnergy + +CandidateWellFormed == + /\ AssignmentComplete + /\ MetadataWellFormed + +Verify == + /\ state = "submitted" + /\ HashIdentityHolds + /\ EnergyAgreementHolds + /\ CandidateWellFormed + /\ state' = "verified" + /\ reasons' = {} + +RejectHash == + /\ state = "submitted" + /\ ~HashIdentityHolds + /\ state' = "rejected" + /\ reasons' = reasons \cup {"hash_mismatch"} + +RejectEnergy == + /\ state = "submitted" + /\ HashIdentityHolds + /\ ~EnergyAgreementHolds + /\ state' = "rejected" + /\ reasons' = reasons \cup {"energy_mismatch"} + +RejectDomain == + /\ state = "submitted" + /\ HashIdentityHolds + /\ EnergyAgreementHolds + /\ ~AssignmentComplete + /\ state' = "rejected" + /\ reasons' = reasons \cup {"assignment_incomplete"} + +RejectMetadata == + /\ state = "submitted" + /\ HashIdentityHolds + /\ EnergyAgreementHolds + /\ AssignmentComplete + /\ ~MetadataWellFormed + /\ state' = "rejected" + /\ reasons' = reasons \cup {"metadata_malformed"} + +Next == + \/ Verify + \/ RejectHash + \/ RejectEnergy + \/ RejectDomain + \/ RejectMetadata + +StatusDomain == + state \in {"submitted", "verified", "rejected"} + +VerifiedImpliesEnergyAgreement == + state = "verified" => EnergyAgreementHolds + +VerifiedImpliesHashIdentity == + state = "verified" => HashIdentityHolds + +Spec == + Init /\ [][Next]_<> + +====