formal: add replay boundary kernel

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.

formal/lean/Noetheris.lean

@@ -6,3 +6,4 @@ import Noetheris.StructuralIR
 import Noetheris.QuboEnergy
 import Noetheris.MigrationPolicy
 import Noetheris.CircuitOracle
+import Noetheris.ReplayBoundary

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

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:
 

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.

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]_<<state, reasons>>
+
+====