diff --git a/dag/std/realization_reconcile.dag b/dag/std/realization_reconcile.dag index d60fef6cfbb..6585070161d 100644 --- a/dag/std/realization_reconcile.dag +++ b/dag/std/realization_reconcile.dag @@ -2,6 +2,13 @@ module std.realization_reconcile import std.types { String, Bool } import std.disposition { Disposition, Terminal } +import std.state_durability { + StateDurabilityQualification, + StateDurabilityRefusal, + StateDurabilityQualified, + StateDurabilityRefused, + StateDurabilityVerdict, +} type ShowEffectiveRead = ReadObserved { value: R } @@ -11,6 +18,21 @@ type Grounding = Grounds { evidence: E } | DoesNotGround { reason: String } +type DurabilityGroundingRefusal + = EffectiveStateDoesNotGround { reason: String } + | DeclaredLifetimeDoesNotGround { + cause: StateDurabilityRefusal, + } + +type DurabilityQualifiedGrounding + = DurabilityGrounds { + effective_state_evidence: E, + durability_evidence: StateDurabilityQualification, + } + | DurabilityDoesNotGround { + cause: DurabilityGroundingRefusal, + } + type Reconciliation = Converged { evidence: E, applied: A } | NotConverged { reason: String, applied: A } @@ -40,3 +62,27 @@ fn reconciliation_converged(r: Reconciliation) -> Bool { NotConverged { reason: _, applied: _ } => false } } + +fn grounding_qualified_by_durability( + grounding: Grounding, + durability: StateDurabilityVerdict, +) -> DurabilityQualifiedGrounding { + match grounding { + DoesNotGround { reason: reason } => + DurabilityDoesNotGround { + cause: EffectiveStateDoesNotGround { reason: reason }, + } + Grounds { evidence: evidence } => + match durability { + StateDurabilityQualified { qualification: qualification } => + DurabilityGrounds { + effective_state_evidence: evidence, + durability_evidence: qualification, + } + StateDurabilityRefused { cause: cause } => + DurabilityDoesNotGround { + cause: DeclaredLifetimeDoesNotGround { cause: cause }, + } + } + } +} diff --git a/dag/std/state_durability.dag b/dag/std/state_durability.dag new file mode 100644 index 00000000000..239d201ce6f --- /dev/null +++ b/dag/std/state_durability.dag @@ -0,0 +1,634 @@ +module std.state_durability + +import extdeps.crypto.hash { Digest } +import std.disposition { Disposition, Terminal } +import std.types { Bool, ContentHash, Int, List, NonEmptyStr, String } + +data state_durability_boundary_contract: Disposition = Terminal { + reason: "Desired world-state lifetime is explicit before realization: RuntimeLifetimeOnly or DurableAcross named lifecycle boundaries. The closed boundary coproduct prevents a generic Persistent label from standing in for service restart, control-plane restart, host restart, power loss, software replacement, or factory reset." +} + +data state_durability_separation_note: String = "State durability is neither extdeps.storage.types.PersistenceKind nor std.materialization_ladder. PersistenceKind describes a storage device/medium; the materialization ladder decides where redundant computation is retained. This module asks a different reconciliation question: across WHICH lifecycle boundary must desired world state remain effective, can the selected realizer provide that lifetime with a commit barrier, and has that exact target + desired state + realization + capability generation been qualified by a perturbation and independent readback? Keeping the facts separate prevents a writable filesystem, an extant file, current runtime effectiveness, or a stale receipt from being misclassified as durable convergence." + +type LifecycleRestartMode + = LifecycleGracefulRestart + | LifecycleForcedRestart + +type PowerLossScope + = ControlPlanePowerLoss + | HostPowerLoss + | SitePowerLoss + +type SoftwareReplacementScope + = ControlPlaneFirmwareReplacement + | HostOsReplacement + | ApplicationReplacement + +type StateDurabilityBoundary + = ServiceRestartBoundary + | ControlPlaneRestartBoundary { mode: LifecycleRestartMode } + | HostRestartBoundary { mode: LifecycleRestartMode } + | PowerLossBoundary { scope: PowerLossScope } + | SoftwareReplacementBoundary { scope: SoftwareReplacementScope } + | FactoryResetBoundary + +type StateDurabilityIntent + = DurabilityUnspecified + | RuntimeLifetimeOnly + | DurableAcross { boundaries: List } + +type DurabilityCommitBarrier + = NoDurabilityCommitBarrier + | SynchronizedCommit + +type StateRealizationIdentity { + realization_id: NonEmptyStr + content_hash: ContentHash +} + +type StateDurabilityCapabilityVersion { + version: NonEmptyStr + definition_hash: ContentHash +} + +type StatePerturbationGeneration = + Int where range(min: 1), brand("StatePerturbationGeneration") + +type StateDurabilityAdmission { + target: Target + desired_state_digest: Digest + realization: StateRealizationIdentity + capability_version: StateDurabilityCapabilityVersion + perturbation_generation: StatePerturbationGeneration + readback_subject: ReadbackSubject +} + +type StateDurabilityCapability { + realization: StateRealizationIdentity + capability_version: StateDurabilityCapabilityVersion + supported_boundaries: List + commit_barrier: DurabilityCommitBarrier +} + +type StatePerturbationReceipt { + receipt_id: NonEmptyStr + target: Target + boundary: StateDurabilityBoundary + generation: StatePerturbationGeneration + started_at: NonEmptyStr + completed_at: NonEmptyStr +} + +type StateReadbackReceipt { + target: Target + subject: ReadbackSubject + state_digest: Digest + observed_at: NonEmptyStr +} + +type StateActivationEvidence + = ActivationVerified + | ActivationUnverified { reason: String } + +type StatePreservationOutcome + = StatePreserved { + before: StateReadbackReceipt, + after: StateReadbackReceipt, + activation: StateActivationEvidence, + } + | StateLost { + before: StateReadbackReceipt, + after: StateReadbackReceipt, + reason: String, + } + | StatePreservationObservationRefused { reason: String } + +type StateDurabilityEvidence { + admission: StateDurabilityAdmission + perturbation: StatePerturbationReceipt + outcome: StatePreservationOutcome +} + +type StateReadbackPosition + = BeforeBoundaryReadback + | AfterBoundaryReadback + +type StateDurabilityRefusal + = DurabilityIntentUnspecified + | DurabilityRequirementEmpty + | DurabilityRequirementDuplicate { + boundary: StateDurabilityBoundary, + count: Int, + } + | DurabilityCapabilityMissing + | DurabilityCapabilityAdmissionMismatch { + expected_realization: StateRealizationIdentity, + observed_realization: StateRealizationIdentity, + expected_capability_version: StateDurabilityCapabilityVersion, + observed_capability_version: StateDurabilityCapabilityVersion, + } + | DurabilityCommitBarrierMissing { + realization: StateRealizationIdentity, + } + | DurabilityBoundaryUnsupported { + realization: StateRealizationIdentity, + boundary: StateDurabilityBoundary, + } + | DurabilityEvidenceMissing { + admission: StateDurabilityAdmission, + boundary: StateDurabilityBoundary, + } + | DurabilityEvidenceAmbiguous { + admission: StateDurabilityAdmission, + boundary: StateDurabilityBoundary, + count: Int, + } + | DurabilityPerturbationTargetMismatch { + expected: Target, + observed: Target, + } + | DurabilityPerturbationBoundaryMismatch { + expected: StateDurabilityBoundary, + observed: StateDurabilityBoundary, + } + | DurabilityPerturbationGenerationMismatch { + expected: StatePerturbationGeneration, + observed: StatePerturbationGeneration, + } + | DurabilityReadbackTargetMismatch { + position: StateReadbackPosition, + expected: Target, + observed: Target, + } + | DurabilityReadbackSubjectMismatch { + position: StateReadbackPosition, + expected: ReadbackSubject, + observed: ReadbackSubject, + } + | DurabilityDesiredStateMismatch { + desired: Digest, + before: Digest, + after: Digest, + } + | DurabilityActivationUnverified { reason: String } + | DurabilityStateLost { + before: StateReadbackReceipt, + after: StateReadbackReceipt, + reason: String, + } + | DurabilityObservationRefused { reason: String } + +type StateDurabilityQualification + = RuntimeLifetimeQualification { + admission: StateDurabilityAdmission, + } + | DurableLifetimeQualification { + admission: StateDurabilityAdmission, + capability: StateDurabilityCapability, + boundaries: List, + evidence: List>, + } + +type StateDurabilityVerdict + = StateDurabilityQualified { + qualification: StateDurabilityQualification, + } + | StateDurabilityRefused { + cause: StateDurabilityRefusal, + } + +type StateDurabilityEvidenceCardinality + = NoMatchingDurabilityEvidence + | OneMatchingDurabilityEvidence { + evidence: StateDurabilityEvidence, + } + | MultipleMatchingDurabilityEvidence { count: Int } + +fn durability_commit_barrier_is_synchronized( + barrier: DurabilityCommitBarrier, +) -> Bool { + match barrier { + NoDurabilityCommitBarrier => false + SynchronizedCommit => true + } +} + +fn state_durability_boundary_eq( + a: StateDurabilityBoundary, + b: StateDurabilityBoundary, +) -> Bool { + a == b +} + +fn state_durability_boundary_present( + boundaries: List, + wanted: StateDurabilityBoundary, +) -> Bool { + boundaries |> any(boundary => + state_durability_boundary_eq(a: boundary, b: wanted) + ) +} + +fn state_durability_boundary_count( + boundaries: List, + wanted: StateDurabilityBoundary, +) -> Int { + fold( + boundaries, + init: 0, + f: (count, boundary) => + if state_durability_boundary_eq(a: boundary, b: wanted) { + count + 1 + } else { + count + }, + ) +} + +fn state_durability_admission_eq( + a: StateDurabilityAdmission, + b: StateDurabilityAdmission, +) -> Bool { + a.target == b.target + && a.desired_state_digest == b.desired_state_digest + && a.realization == b.realization + && a.capability_version == b.capability_version + && a.perturbation_generation == b.perturbation_generation + && a.readback_subject == b.readback_subject +} + +fn state_durability_capability_matches_admission( + capability: StateDurabilityCapability, + admission: StateDurabilityAdmission, +) -> Bool { + capability.realization == admission.realization + && capability.capability_version == admission.capability_version +} + +fn state_durability_evidence_cardinality( + evidence: List>, + admission: StateDurabilityAdmission, + boundary: StateDurabilityBoundary, +) -> StateDurabilityEvidenceCardinality { + fold( + evidence, + init: NoMatchingDurabilityEvidence, + f: (cardinality, candidate) => + if state_durability_admission_eq( + a: candidate.admission, + b: admission, + ) && state_durability_boundary_eq( + a: candidate.perturbation.boundary, + b: boundary, + ) { + match cardinality { + NoMatchingDurabilityEvidence => + OneMatchingDurabilityEvidence { evidence: candidate } + OneMatchingDurabilityEvidence { evidence: _ } => + MultipleMatchingDurabilityEvidence { count: 2 } + MultipleMatchingDurabilityEvidence { count: count } => + MultipleMatchingDurabilityEvidence { count: count + 1 } + } + } else { + cardinality + }, + ) +} + +fn state_durability_evidence_refusal( + admission: StateDurabilityAdmission, + boundary: StateDurabilityBoundary, + evidence: StateDurabilityEvidence, +) -> StateDurabilityRefusal? { + if evidence.perturbation.target != admission.target { + Present { + value: DurabilityPerturbationTargetMismatch { + expected: admission.target, + observed: evidence.perturbation.target, + }, + } + } else if !state_durability_boundary_eq( + a: evidence.perturbation.boundary, + b: boundary, + ) { + Present { + value: DurabilityPerturbationBoundaryMismatch { + expected: boundary, + observed: evidence.perturbation.boundary, + }, + } + } else if evidence.perturbation.generation != admission.perturbation_generation { + Present { + value: DurabilityPerturbationGenerationMismatch { + expected: admission.perturbation_generation, + observed: evidence.perturbation.generation, + }, + } + } else { + match evidence.outcome { + StatePreservationObservationRefused { reason: reason } => + Present { + value: DurabilityObservationRefused { reason: reason }, + } + StateLost { + before: before, + after: after, + reason: reason, + } => + Present { + value: DurabilityStateLost { + before: before, + after: after, + reason: reason, + }, + } + StatePreserved { + before: before, + after: after, + activation: activation, + } => + if before.target != admission.target { + Present { + value: DurabilityReadbackTargetMismatch { + position: BeforeBoundaryReadback, + expected: admission.target, + observed: before.target, + }, + } + } else if after.target != admission.target { + Present { + value: DurabilityReadbackTargetMismatch { + position: AfterBoundaryReadback, + expected: admission.target, + observed: after.target, + }, + } + } else if before.subject != admission.readback_subject { + Present { + value: DurabilityReadbackSubjectMismatch { + position: BeforeBoundaryReadback, + expected: admission.readback_subject, + observed: before.subject, + }, + } + } else if after.subject != admission.readback_subject { + Present { + value: DurabilityReadbackSubjectMismatch { + position: AfterBoundaryReadback, + expected: admission.readback_subject, + observed: after.subject, + }, + } + } else if before.state_digest != admission.desired_state_digest + || after.state_digest != admission.desired_state_digest { + Present { + value: DurabilityDesiredStateMismatch { + desired: admission.desired_state_digest, + before: before.state_digest, + after: after.state_digest, + }, + } + } else { + match activation { + ActivationUnverified { reason: reason } => + Present { + value: DurabilityActivationUnverified { reason: reason }, + } + ActivationVerified => none + } + } + } + } +} + +fn state_durability_boundaries_verdict( + remaining: List, + required: List, + admission: StateDurabilityAdmission, + capability: StateDurabilityCapability, + evidence: List>, + qualified: List>, +) -> StateDurabilityVerdict { + match remaining.first() { + Absent => + StateDurabilityQualified { + qualification: DurableLifetimeQualification { + admission: admission, + capability: capability, + boundaries: required, + evidence: qualified, + }, + } + Present { value: boundary } => + let requirement_count = state_durability_boundary_count( + boundaries: required, + wanted: boundary, + ) + if requirement_count > 1 { + StateDurabilityRefused { + cause: DurabilityRequirementDuplicate { + boundary: boundary, + count: requirement_count, + }, + } + } else if !state_durability_boundary_present( + boundaries: capability.supported_boundaries, + wanted: boundary, + ) { + StateDurabilityRefused { + cause: DurabilityBoundaryUnsupported { + realization: capability.realization, + boundary: boundary, + }, + } + } else { + match state_durability_evidence_cardinality( + evidence: evidence, + admission: admission, + boundary: boundary, + ) { + NoMatchingDurabilityEvidence => + StateDurabilityRefused { + cause: DurabilityEvidenceMissing { + admission: admission, + boundary: boundary, + }, + } + MultipleMatchingDurabilityEvidence { count: count } => + StateDurabilityRefused { + cause: DurabilityEvidenceAmbiguous { + admission: admission, + boundary: boundary, + count: count, + }, + } + OneMatchingDurabilityEvidence { evidence: receipt } => + match state_durability_evidence_refusal( + admission: admission, + boundary: boundary, + evidence: receipt, + ) { + Present { value: cause } => + StateDurabilityRefused { cause: cause } + Absent => + state_durability_boundaries_verdict( + remaining: remaining.skip(n: 1), + required: required, + admission: admission, + capability: capability, + evidence: evidence, + qualified: append(qualified, items: [receipt]), + ) + } + } + } + } +} + +fn state_durability_verdict( + intent: StateDurabilityIntent, + admission: StateDurabilityAdmission, + capability: StateDurabilityCapability?, + evidence: List>, +) -> StateDurabilityVerdict { + match intent { + DurabilityUnspecified => + StateDurabilityRefused { cause: DurabilityIntentUnspecified } + RuntimeLifetimeOnly => + StateDurabilityQualified { + qualification: RuntimeLifetimeQualification { + admission: admission, + }, + } + DurableAcross { boundaries: boundaries } => + if boundaries.length() == 0 { + StateDurabilityRefused { cause: DurabilityRequirementEmpty } + } else { + match capability { + Absent => + StateDurabilityRefused { cause: DurabilityCapabilityMissing } + Present { value: realizer } => + if !state_durability_capability_matches_admission( + capability: realizer, + admission: admission, + ) { + StateDurabilityRefused { + cause: DurabilityCapabilityAdmissionMismatch { + expected_realization: admission.realization, + observed_realization: realizer.realization, + expected_capability_version: admission.capability_version, + observed_capability_version: realizer.capability_version, + }, + } + } else if !durability_commit_barrier_is_synchronized( + barrier: realizer.commit_barrier, + ) { + StateDurabilityRefused { + cause: DurabilityCommitBarrierMissing { + realization: realizer.realization, + }, + } + } else { + state_durability_boundaries_verdict( + remaining: boundaries, + required: boundaries, + admission: admission, + capability: realizer, + evidence: evidence, + qualified: [], + ) + } + } + } + } +} + +fn state_durability_satisfied( + verdict: StateDurabilityVerdict, +) -> Bool { + match verdict { + StateDurabilityQualified { qualification: _ } => true + StateDurabilityRefused { cause: _ } => false + } +} + +fn state_durability_refusal_reason( + refusal: StateDurabilityRefusal, +) -> String { + match refusal { + DurabilityIntentUnspecified => + "desired state does not declare its required lifetime" + DurabilityRequirementEmpty => + "durable desired state declares no lifecycle boundary" + DurabilityRequirementDuplicate { boundary: _, count: _ } => + "durable desired state repeats a lifecycle boundary" + DurabilityCapabilityMissing => + "selected realization does not declare a durability capability" + DurabilityCapabilityAdmissionMismatch { + expected_realization: _, + observed_realization: _, + expected_capability_version: _, + observed_capability_version: _, + } => + "durability capability identity does not match the admitted realization and capability version" + DurabilityCommitBarrierMissing { realization: realization } => + concat( + "selected realization lacks a synchronized durability commit barrier: ", + realization.realization_id as String, + ) + DurabilityBoundaryUnsupported { realization: realization, boundary: _ } => + concat( + "selected realization does not support a required lifecycle boundary: ", + realization.realization_id as String, + ) + DurabilityEvidenceMissing { admission: admission, boundary: _ } => + concat( + "selected realization has no exact evidence for target, desired state, realization, capability version, perturbation generation, readback subject, and boundary: ", + admission.realization.realization_id as String, + ) + DurabilityEvidenceAmbiguous { admission: admission, boundary: _, count: _ } => + concat( + "selected realization has duplicate or conflicting exact durability evidence: ", + admission.realization.realization_id as String, + ) + DurabilityPerturbationTargetMismatch { expected: _, observed: _ } => + "durability perturbation receipt targets a different state owner" + DurabilityPerturbationBoundaryMismatch { expected: _, observed: _ } => + "durability perturbation receipt names a different lifecycle boundary" + DurabilityPerturbationGenerationMismatch { expected: _, observed: _ } => + "durability perturbation receipt belongs to a different generation" + DurabilityReadbackTargetMismatch { position: _, expected: _, observed: _ } => + "durability readback targets a different state owner" + DurabilityReadbackSubjectMismatch { position: _, expected: _, observed: _ } => + "durability readback observes a different subject" + DurabilityDesiredStateMismatch { desired: _, before: _, after: _ } => + "before and after readback must both equal the admitted desired-state digest" + DurabilityActivationUnverified { reason: reason } => + concat("post-boundary activation was not verified: ", reason) + DurabilityStateLost { before: _, after: _, reason: reason } => + concat("state was lost across the lifecycle boundary: ", reason) + DurabilityObservationRefused { reason: reason } => + concat("durability observation was refused: ", reason) + } +} + +fn state_durability_verdict_reason( + verdict: StateDurabilityVerdict, +) -> String { + match verdict { + StateDurabilityQualified { qualification: qualification } => + match qualification { + RuntimeLifetimeQualification { admission: _ } => + "runtime-only lifetime explicitly satisfied" + DurableLifetimeQualification { + admission: _, + capability: _, + boundaries: _, + evidence: _, + } => + "required durability boundaries satisfied by exact perturbation and readback evidence" + } + StateDurabilityRefused { cause: cause } => + state_durability_refusal_reason(refusal: cause) + } +} diff --git a/dag/test/claim/state_durability_witness_test.dag b/dag/test/claim/state_durability_witness_test.dag new file mode 100644 index 00000000000..fb63fd875c1 --- /dev/null +++ b/dag/test/claim/state_durability_witness_test.dag @@ -0,0 +1,698 @@ +module test.claim.state_durability_witness + +import extdeps.crypto.hash { Digest, sha256_digest } +import std.realization_reconcile { + DeclaredLifetimeDoesNotGround, + DurabilityDoesNotGround, + DurabilityGrounds, + DurabilityQualifiedGrounding, + Grounding, + Grounds, + grounding_qualified_by_durability, +} +import std.state_durability { + ActivationUnverified, + ActivationVerified, + ControlPlaneFirmwareReplacement, + ControlPlaneRestartBoundary, + DurableAcross, + DurableLifetimeQualification, + DurabilityActivationUnverified, + DurabilityBoundaryUnsupported, + DurabilityCapabilityAdmissionMismatch, + DurabilityCapabilityMissing, + DurabilityCommitBarrier, + DurabilityCommitBarrierMissing, + DurabilityDesiredStateMismatch, + DurabilityEvidenceAmbiguous, + DurabilityEvidenceMissing, + DurabilityIntentUnspecified, + DurabilityReadbackSubjectMismatch, + DurabilityRequirementDuplicate, + DurabilityRequirementEmpty, + DurabilityUnspecified, + LifecycleGracefulRestart, + NoDurabilityCommitBarrier, + RuntimeLifetimeOnly, + SoftwareReplacementBoundary, + StateActivationEvidence, + StateDurabilityAdmission, + StateDurabilityBoundary, + StateDurabilityCapability, + StateDurabilityCapabilityVersion, + StateDurabilityEvidence, + StateDurabilityIntent, + StateDurabilityQualified, + StateDurabilityRefused, + StateDurabilityVerdict, + StateLost, + StatePerturbationGeneration, + StatePerturbationReceipt, + StatePreserved, + StateReadbackReceipt, + StateRealizationIdentity, + SynchronizedCommit, + state_durability_satisfied, + state_durability_verdict, +} +import std.types { Bool, ContentHash, List, NonEmptyStr, String } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +type FixtureTarget = NonEmptyStr where brand("FixtureTarget") + +type FixtureReadbackSubject { + path: NonEmptyStr +} + +data fixture_target: FixtureTarget = "fixture-host" as FixtureTarget +data fixture_other_target: FixtureTarget = "other-host" as FixtureTarget + +data fixture_subject: FixtureReadbackSubject = FixtureReadbackSubject { + path: "/etc/fixture-policy", +} + +data fixture_other_subject: FixtureReadbackSubject = FixtureReadbackSubject { + path: "/etc/unrelated-policy", +} + +data fixture_graceful_control_plane_restart: StateDurabilityBoundary = ControlPlaneRestartBoundary { + mode: LifecycleGracefulRestart, +} + +data fixture_control_plane_firmware_replacement: StateDurabilityBoundary = SoftwareReplacementBoundary { + scope: ControlPlaneFirmwareReplacement, +} + +data fixture_digest_a: Digest = sha256_digest( + hex: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", +) + +data fixture_digest_b: Digest = sha256_digest( + hex: "bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb", +) + +data fixture_realization: StateRealizationIdentity = StateRealizationIdentity { + realization_id: "fixture-realizer", + content_hash: "fixture-realizer-content-v1" as ContentHash, +} + +data fixture_stale_realization: StateRealizationIdentity = StateRealizationIdentity { + realization_id: "fixture-realizer", + content_hash: "fixture-realizer-content-v0" as ContentHash, +} + +data fixture_capability_version: StateDurabilityCapabilityVersion = StateDurabilityCapabilityVersion { + version: "fixture-capability-v1", + definition_hash: "fixture-capability-definition-v1" as ContentHash, +} + +data fixture_stale_capability_version: StateDurabilityCapabilityVersion = StateDurabilityCapabilityVersion { + version: "fixture-capability-v0", + definition_hash: "fixture-capability-definition-v0" as ContentHash, +} + +fn fixture_admission( + target: FixtureTarget, + desired: Digest, + realization: StateRealizationIdentity, + capability_version: StateDurabilityCapabilityVersion, + generation: StatePerturbationGeneration, + subject: FixtureReadbackSubject, +) -> StateDurabilityAdmission { + StateDurabilityAdmission { + target: target, + desired_state_digest: desired, + realization: realization, + capability_version: capability_version, + perturbation_generation: generation, + readback_subject: subject, + } +} + +fn current_admission() -> StateDurabilityAdmission { + fixture_admission( + target: fixture_target, + desired: fixture_digest_a, + realization: fixture_realization, + capability_version: fixture_capability_version, + generation: 7, + subject: fixture_subject, + ) +} + +fn fixture_capability( + realization: StateRealizationIdentity, + capability_version: StateDurabilityCapabilityVersion, + boundaries: List, + barrier: DurabilityCommitBarrier, +) -> StateDurabilityCapability { + StateDurabilityCapability { + realization: realization, + capability_version: capability_version, + supported_boundaries: boundaries, + commit_barrier: barrier, + } +} + +fn synchronized_restart_capability() -> StateDurabilityCapability { + fixture_capability( + realization: fixture_realization, + capability_version: fixture_capability_version, + boundaries: [fixture_graceful_control_plane_restart], + barrier: SynchronizedCommit, + ) +} + +fn fixture_readback( + target: FixtureTarget, + subject: FixtureReadbackSubject, + digest: Digest, + observed_at: NonEmptyStr, +) -> StateReadbackReceipt { + StateReadbackReceipt { + target: target, + subject: subject, + state_digest: digest, + observed_at: observed_at, + } +} + +fn fixture_preserved_evidence( + admission: StateDurabilityAdmission, + perturbation_target: FixtureTarget, + perturbation_generation: StatePerturbationGeneration, + before_target: FixtureTarget, + before_subject: FixtureReadbackSubject, + before: Digest, + after_target: FixtureTarget, + after_subject: FixtureReadbackSubject, + after: Digest, + activation: StateActivationEvidence, +) -> StateDurabilityEvidence { + StateDurabilityEvidence { + admission: admission, + perturbation: StatePerturbationReceipt { + receipt_id: "fixture-restart-receipt", + target: perturbation_target, + boundary: fixture_graceful_control_plane_restart, + generation: perturbation_generation, + started_at: "2026-07-27T23:09:42Z", + completed_at: "2026-07-27T23:14:45Z", + }, + outcome: StatePreserved { + before: fixture_readback( + target: before_target, + subject: before_subject, + digest: before, + observed_at: "2026-07-27T23:09:42Z", + ), + after: fixture_readback( + target: after_target, + subject: after_subject, + digest: after, + observed_at: "2026-07-27T23:14:45Z", + ), + activation: activation, + }, + } +} + +fn matching_preserved_evidence() -> StateDurabilityEvidence { + fixture_preserved_evidence( + admission: current_admission(), + perturbation_target: fixture_target, + perturbation_generation: 7, + before_target: fixture_target, + before_subject: fixture_subject, + before: fixture_digest_a, + after_target: fixture_target, + after_subject: fixture_subject, + after: fixture_digest_a, + activation: ActivationVerified, + ) +} + +fn matching_lost_evidence() -> StateDurabilityEvidence { + StateDurabilityEvidence { + admission: current_admission(), + perturbation: StatePerturbationReceipt { + receipt_id: "fixture-restart-lost-receipt", + target: fixture_target, + boundary: fixture_graceful_control_plane_restart, + generation: 7, + started_at: "2026-07-27T23:09:42Z", + completed_at: "2026-07-27T23:14:45Z", + }, + outcome: StateLost { + before: fixture_readback( + target: fixture_target, + subject: fixture_subject, + digest: fixture_digest_a, + observed_at: "2026-07-27T23:09:42Z", + ), + after: fixture_readback( + target: fixture_target, + subject: fixture_subject, + digest: fixture_digest_b, + observed_at: "2026-07-27T23:14:45Z", + ), + reason: "fixture state was lost", + }, + } +} + +fn durable_restart_intent() -> StateDurabilityIntent { + DurableAcross { boundaries: [fixture_graceful_control_plane_restart] } +} + +fn durable_restart_verdict( + evidence: List>, +) -> StateDurabilityVerdict { + state_durability_verdict( + intent: durable_restart_intent(), + admission: current_admission(), + capability: Present { value: synchronized_restart_capability() }, + evidence: evidence, + ) +} + +fn qualify_string_grounding( + verdict: StateDurabilityVerdict, +) -> DurabilityQualifiedGrounding { + grounding_qualified_by_durability( + grounding: Grounds { evidence: "currently effective" }, + durability: verdict, + ) +} + +test fn unspecified_lifetime_refuses_before_reconciliation() -> Bool { + match state_durability_verdict( + intent: DurabilityUnspecified, + admission: current_admission(), + capability: none, + evidence: [], + ) { + StateDurabilityRefused { cause: DurabilityIntentUnspecified } => true + _ => false + } +} + +test fn runtime_only_lifetime_is_explicitly_satisfiable_without_durable_storage() -> Bool { + state_durability_satisfied(verdict: state_durability_verdict( + intent: RuntimeLifetimeOnly, + admission: current_admission(), + capability: none, + evidence: [], + )) +} + +test fn durable_lifetime_requires_at_least_one_named_boundary() -> Bool { + match state_durability_verdict( + intent: DurableAcross { boundaries: [] }, + admission: current_admission(), + capability: Present { value: synchronized_restart_capability() }, + evidence: [], + ) { + StateDurabilityRefused { cause: DurabilityRequirementEmpty } => true + _ => false + } +} + +test fn duplicate_required_boundaries_refuse_instead_of_reusing_one_receipt() -> Bool { + match state_durability_verdict( + intent: DurableAcross { + boundaries: [ + fixture_graceful_control_plane_restart, + fixture_graceful_control_plane_restart, + ], + }, + admission: current_admission(), + capability: Present { value: synchronized_restart_capability() }, + evidence: [matching_preserved_evidence()], + ) { + StateDurabilityRefused { + cause: DurabilityRequirementDuplicate { boundary: _, count: 2 }, + } => true + _ => false + } +} + +test fn durable_lifetime_requires_a_selected_capability() -> Bool { + match state_durability_verdict( + intent: durable_restart_intent(), + admission: current_admission(), + capability: none, + evidence: [], + ) { + StateDurabilityRefused { cause: DurabilityCapabilityMissing } => true + _ => false + } +} + +test fn capability_identity_must_match_the_admission() -> Bool { + match state_durability_verdict( + intent: durable_restart_intent(), + admission: current_admission(), + capability: Present { + value: fixture_capability( + realization: fixture_stale_realization, + capability_version: fixture_stale_capability_version, + boundaries: [fixture_graceful_control_plane_restart], + barrier: SynchronizedCommit, + ), + }, + evidence: [], + ) { + StateDurabilityRefused { + cause: DurabilityCapabilityAdmissionMismatch { + expected_realization: _, + observed_realization: _, + expected_capability_version: _, + observed_capability_version: _, + }, + } => true + _ => false + } +} + +test fn writable_without_a_commit_barrier_is_not_durable_capability() -> Bool { + match state_durability_verdict( + intent: durable_restart_intent(), + admission: current_admission(), + capability: Present { + value: fixture_capability( + realization: fixture_realization, + capability_version: fixture_capability_version, + boundaries: [fixture_graceful_control_plane_restart], + barrier: NoDurabilityCommitBarrier, + ), + }, + evidence: [], + ) { + StateDurabilityRefused { + cause: DurabilityCommitBarrierMissing { realization: realization }, + } => realization == fixture_realization + _ => false + } +} + +test fn capability_for_a_different_boundary_cannot_satisfy_the_intent() -> Bool { + match state_durability_verdict( + intent: durable_restart_intent(), + admission: current_admission(), + capability: Present { + value: fixture_capability( + realization: fixture_realization, + capability_version: fixture_capability_version, + boundaries: [fixture_control_plane_firmware_replacement], + barrier: SynchronizedCommit, + ), + }, + evidence: [], + ) { + StateDurabilityRefused { + cause: DurabilityBoundaryUnsupported { realization: realization, boundary: _ }, + } => realization == fixture_realization + _ => false + } +} + +test fn declared_capability_without_exact_evidence_refuses() -> Bool { + match durable_restart_verdict(evidence: []) { + StateDurabilityRefused { + cause: DurabilityEvidenceMissing { admission: _, boundary: _ }, + } => true + _ => false + } +} + +test fn matching_perturbation_and_readback_qualify_the_exact_admission() -> Bool { + match durable_restart_verdict(evidence: [matching_preserved_evidence()]) { + StateDurabilityQualified { qualification: qualification } => + match qualification { + DurableLifetimeQualification { + admission: admission, + capability: capability, + boundaries: boundaries, + evidence: evidence, + } => + admission == current_admission() + && capability == synchronized_restart_capability() + && boundaries == [fixture_graceful_control_plane_restart] + && evidence == [matching_preserved_evidence()] + _ => false + } + _ => false + } +} + +test fn an_old_receipt_for_the_same_string_id_cannot_qualify_new_realization_content() -> Bool { + let stale_admission = fixture_admission( + target: fixture_target, + desired: fixture_digest_a, + realization: fixture_stale_realization, + capability_version: fixture_capability_version, + generation: 7, + subject: fixture_subject, + ) + let stale = fixture_preserved_evidence( + admission: stale_admission, + perturbation_target: fixture_target, + perturbation_generation: 7, + before_target: fixture_target, + before_subject: fixture_subject, + before: fixture_digest_a, + after_target: fixture_target, + after_subject: fixture_subject, + after: fixture_digest_a, + activation: ActivationVerified, + ) + match durable_restart_verdict(evidence: [stale]) { + StateDurabilityRefused { + cause: DurabilityEvidenceMissing { admission: _, boundary: _ }, + } => true + _ => false + } +} + +test fn evidence_for_an_old_desired_digest_cannot_qualify_changed_intent() -> Bool { + let stale_admission = fixture_admission( + target: fixture_target, + desired: fixture_digest_b, + realization: fixture_realization, + capability_version: fixture_capability_version, + generation: 7, + subject: fixture_subject, + ) + let stale = fixture_preserved_evidence( + admission: stale_admission, + perturbation_target: fixture_target, + perturbation_generation: 7, + before_target: fixture_target, + before_subject: fixture_subject, + before: fixture_digest_b, + after_target: fixture_target, + after_subject: fixture_subject, + after: fixture_digest_b, + activation: ActivationVerified, + ) + match durable_restart_verdict(evidence: [stale]) { + StateDurabilityRefused { + cause: DurabilityEvidenceMissing { admission: _, boundary: _ }, + } => true + _ => false + } +} + +test fn evidence_for_an_old_capability_version_cannot_qualify() -> Bool { + let stale_admission = fixture_admission( + target: fixture_target, + desired: fixture_digest_a, + realization: fixture_realization, + capability_version: fixture_stale_capability_version, + generation: 7, + subject: fixture_subject, + ) + let stale = fixture_preserved_evidence( + admission: stale_admission, + perturbation_target: fixture_target, + perturbation_generation: 7, + before_target: fixture_target, + before_subject: fixture_subject, + before: fixture_digest_a, + after_target: fixture_target, + after_subject: fixture_subject, + after: fixture_digest_a, + activation: ActivationVerified, + ) + match durable_restart_verdict(evidence: [stale]) { + StateDurabilityRefused { + cause: DurabilityEvidenceMissing { admission: _, boundary: _ }, + } => true + _ => false + } +} + +test fn evidence_for_an_old_perturbation_generation_cannot_qualify() -> Bool { + let stale_admission = fixture_admission( + target: fixture_target, + desired: fixture_digest_a, + realization: fixture_realization, + capability_version: fixture_capability_version, + generation: 6, + subject: fixture_subject, + ) + let stale = fixture_preserved_evidence( + admission: stale_admission, + perturbation_target: fixture_target, + perturbation_generation: 6, + before_target: fixture_target, + before_subject: fixture_subject, + before: fixture_digest_a, + after_target: fixture_target, + after_subject: fixture_subject, + after: fixture_digest_a, + activation: ActivationVerified, + ) + match durable_restart_verdict(evidence: [stale]) { + StateDurabilityRefused { + cause: DurabilityEvidenceMissing { admission: _, boundary: _ }, + } => true + _ => false + } +} + +test fn equal_before_and_after_bytes_do_not_qualify_when_not_desired() -> Bool { + let wrong = fixture_preserved_evidence( + admission: current_admission(), + perturbation_target: fixture_target, + perturbation_generation: 7, + before_target: fixture_target, + before_subject: fixture_subject, + before: fixture_digest_b, + after_target: fixture_target, + after_subject: fixture_subject, + after: fixture_digest_b, + activation: ActivationVerified, + ) + match durable_restart_verdict(evidence: [wrong]) { + StateDurabilityRefused { + cause: DurabilityDesiredStateMismatch { + desired: desired, + before: before, + after: after, + }, + } => + desired == fixture_digest_a + && before == fixture_digest_b + && after == fixture_digest_b + _ => false + } +} + +test fn a_different_readback_subject_refuses_with_typed_cause() -> Bool { + let wrong = fixture_preserved_evidence( + admission: current_admission(), + perturbation_target: fixture_target, + perturbation_generation: 7, + before_target: fixture_target, + before_subject: fixture_other_subject, + before: fixture_digest_a, + after_target: fixture_target, + after_subject: fixture_subject, + after: fixture_digest_a, + activation: ActivationVerified, + ) + match durable_restart_verdict(evidence: [wrong]) { + StateDurabilityRefused { + cause: DurabilityReadbackSubjectMismatch { + position: _, + expected: expected, + observed: observed, + }, + } => + expected == fixture_subject && observed == fixture_other_subject + _ => false + } +} + +test fn unverified_post_boundary_activation_refuses_with_typed_cause() -> Bool { + let unverified = fixture_preserved_evidence( + admission: current_admission(), + perturbation_target: fixture_target, + perturbation_generation: 7, + before_target: fixture_target, + before_subject: fixture_subject, + before: fixture_digest_a, + after_target: fixture_target, + after_subject: fixture_subject, + after: fixture_digest_a, + activation: ActivationUnverified { + reason: "service activation was not read back", + }, + ) + match durable_restart_verdict(evidence: [unverified]) { + StateDurabilityRefused { + cause: DurabilityActivationUnverified { reason: reason }, + } => reason == "service activation was not read back" + _ => false + } +} + +test fn duplicate_preserved_and_lost_receipts_refuse_independent_of_list_order() -> Bool { + let preserved_first = durable_restart_verdict( + evidence: [matching_preserved_evidence(), matching_lost_evidence()], + ) + let lost_first = durable_restart_verdict( + evidence: [matching_lost_evidence(), matching_preserved_evidence()], + ) + match preserved_first { + StateDurabilityRefused { + cause: DurabilityEvidenceAmbiguous { admission: _, boundary: _, count: 2 }, + } => + match lost_first { + StateDurabilityRefused { + cause: DurabilityEvidenceAmbiguous { admission: _, boundary: _, count: 2 }, + } => true + _ => false + } + _ => false + } +} + +test fn current_effectiveness_preserves_typed_durability_refusal() -> Bool { + match qualify_string_grounding(verdict: durable_restart_verdict(evidence: [])) { + DurabilityDoesNotGround { + cause: DeclaredLifetimeDoesNotGround { + cause: DurabilityEvidenceMissing { admission: _, boundary: _ }, + }, + } => true + _ => false + } +} + +test fn qualified_grounding_carries_effective_and_durability_evidence() -> Bool { + match qualify_string_grounding( + verdict: durable_restart_verdict(evidence: [matching_preserved_evidence()]), + ) { + DurabilityGrounds { + effective_state_evidence: effective, + durability_evidence: durability, + } => + effective == "currently effective" + && match durability { + DurableLifetimeQualification { + admission: admission, + capability: _, + boundaries: _, + evidence: evidence, + } => + admission == current_admission() + && evidence == [matching_preserved_evidence()] + _ => false + } + _ => false + } +}