automation_structures/integration/
governed_commit.rs

1// Bounded executable slice used by the governed-commit semantic bridge.
2//
3// The slice owns the mapped ResourceRegistry, Budget, PropagationPass,
4// ActuationPass, AuditSink, and Sequential carriers. It fixes one
5// registry key, one seat, one work item, and a unit resource charge.  Those bounds
6// make the cross-tool transition relation finite without changing the transferred
7// claim: capacity safety and `Committed => durable audit evidence`.
8//
9// Runtime boundaries that Rust does not supply are explicit in the API:
10//
11// - `CommitOutcome` is the external-effect adapter result.  `FailureAfterEffect`
12//   records a durable recovery intent before exposing the applied effect, so a
13//   retry cannot duplicate the effect.
14// - `crash` clears only the volatile process flag.  The six carrier states,
15//   effect receipt, audit record, and recovery intent are the modeled durable
16//   store and require the registered linearizable persistence provider.
17// - scheduler fairness and eventual external-service success remain deployment
18//   relies.  Safety and recovery-step correspondence do not assume either.
19// - retry attempts are owned by a second Budget. Its unit admission is stated
20//   with mathematical-integer specifications and executed with overflow-safe
21//   u64 code.
22
23use vstd::prelude::*;
24
25use crate::modalities::sequential::Sequential;
26use crate::primitives::actuation_pass::ActuationPass;
27use crate::primitives::audit_sink::AuditSink;
28use crate::primitives::budget::Budget;
29use crate::primitives::propagation_pass::PropagationPass;
30#[expect(
31    unused_imports,
32    reason = "Round appears in ghost specifications erased by rustc"
33)]
34use crate::primitives::propagation_pass::Round;
35use crate::primitives::resource_registry::ResourceRegistry;
36
37verus! {
38
39#[derive(Clone, Copy, PartialEq, Eq, Debug)]
40/// Concrete phase of the bounded governed-commit assembly.
41pub enum CommitPhase {
42    /// Request has not yet been admitted.
43    Pending,
44    /// Capacity and registry admission have committed.
45    Admitted,
46    /// Propagation has prepared the request for its external effect.
47    Ready,
48    /// A pre-effect failure permits another bounded attempt.
49    Retryable,
50    /// An applied effect is waiting for durable recovery evidence.
51    RecoveryPending,
52    /// Effect and durable evidence have both committed.
53    Committed,
54    /// The request cannot make another admitted attempt.
55    Rejected,
56}
57
58/// Frozen abstract phases for the direct source-level refinement proof.  These
59/// are the same five observations used by `GovernedCommitAbstract.tla`.
60#[derive(Clone, Copy, PartialEq, Eq, Debug)]
61pub enum AbstractPhase {
62    /// No abstract work is active.
63    Pending,
64    /// Admission, preparation, or retry is active.
65    Active,
66    /// An applied effect is being recovered.
67    Recovering,
68    /// Effect and evidence are committed.
69    Committed,
70    /// The abstract request has failed.
71    Failed,
72}
73
74/// One bounded integrated request.  The component fields are the actual
75/// executable carriers; the remaining fields expose the external effect,
76/// persistence, failure, and recovery boundary absent from the individual rows.
77pub struct GovernedCommit {
78    /// Registry owner for the admitted request.
79    pub registry: ResourceRegistry<u64, u64>,
80    /// Resource-capacity owner.
81    pub budget: Budget,
82    /// Preparation owner.
83    pub propagation: PropagationPass,
84    /// External-effect lifecycle owner.
85    pub actuation: ActuationPass,
86    /// Durable evidence owner.
87    pub audit: AuditSink,
88    /// Execution-order owner.
89    pub sequential: Sequential,
90    /// Current concrete assembly phase.
91    pub phase: CommitPhase,
92    /// Owner of bounded retry attempts.
93    pub attempt_budget: Budget,
94    /// Whether the external effect has been applied.
95    pub effect_applied: bool,
96    /// Whether durable evidence for the effect has been retained.
97    pub evidence_persisted: bool,
98    /// Whether durable recovery intent has been retained.
99    pub recovery_intent: bool,
100    /// Whether the modeled process is currently crashed.
101    pub crashed: bool,
102}
103
104impl GovernedCommit {
105    /// Project the retained component states to the abstract commit phase.
106    pub open spec fn abstract_phase(&self) -> AbstractPhase {
107        if self.phase == CommitPhase::Pending {
108            AbstractPhase::Pending
109        } else if self.phase == CommitPhase::Admitted
110            || self.phase == CommitPhase::Ready
111            || self.phase == CommitPhase::Retryable
112        {
113            AbstractPhase::Active
114        } else if self.phase == CommitPhase::RecoveryPending {
115            AbstractPhase::Recovering
116        } else if self.phase == CommitPhase::Committed {
117            AbstractPhase::Committed
118        } else {
119            AbstractPhase::Failed
120        }
121    }
122
123    /// Project committed resource use from the retained budget owners.
124    pub open spec fn abstract_used(&self) -> int {
125        self.budget.allocated as int + self.budget.reserved as int
126    }
127
128    /// The frozen abstract initial predicate, evaluated through the executable
129    /// abstraction map above.
130    pub open spec fn abstract_init(&self) -> bool {
131        &&& self.abstract_phase() == AbstractPhase::Pending
132        &&& self.abstract_used() == 0
133        &&& !self.effect_applied
134        &&& !self.evidence_persisted
135        &&& !self.recovery_intent
136    }
137
138    /// Direct Verus counterpart of `AbstractSystemStep`.
139    pub open spec fn abstract_system_step(
140        pre: &GovernedCommit,
141        post: &GovernedCommit,
142    ) -> bool {
143        &&& post.budget.capacity == pre.budget.capacity
144        &&& post.effect_applied == pre.effect_applied
145        &&& post.evidence_persisted == pre.evidence_persisted
146        &&& post.recovery_intent == pre.recovery_intent
147        &&& ((pre.abstract_phase() == AbstractPhase::Pending
148                && post.abstract_phase() == AbstractPhase::Active
149                && post.abstract_used() == 1)
150            || (pre.abstract_phase() == AbstractPhase::Active
151                && post.abstract_phase() == AbstractPhase::Active
152                && post.abstract_used() == pre.abstract_used()))
153    }
154
155    /// Direct Verus counterpart of `AbstractFailureStep`.  Rejection, retry,
156    /// partial failure, and crash are exhaustive named arms.
157    pub open spec fn abstract_failure_step(
158        pre: &GovernedCommit,
159        post: &GovernedCommit,
160    ) -> bool {
161        &&& post.budget.capacity == pre.budget.capacity
162        &&& ((post.abstract_phase() == AbstractPhase::Failed
163                && post.abstract_used() == pre.abstract_used()
164                && post.effect_applied == pre.effect_applied
165                && post.evidence_persisted == pre.evidence_persisted
166                && post.recovery_intent == pre.recovery_intent)
167            || (pre.abstract_phase() == AbstractPhase::Active
168                && post.abstract_phase() == AbstractPhase::Active
169                && post.abstract_used() == pre.abstract_used()
170                && post.effect_applied == pre.effect_applied
171                && post.evidence_persisted == pre.evidence_persisted
172                && post.recovery_intent == pre.recovery_intent)
173            || (pre.abstract_phase() == AbstractPhase::Active
174                && post.abstract_phase() == AbstractPhase::Recovering
175                && post.abstract_used() == pre.abstract_used()
176                && post.effect_applied
177                && !post.evidence_persisted
178                && post.recovery_intent)
179            || (post.abstract_phase() == pre.abstract_phase()
180                && post.abstract_used() == pre.abstract_used()
181                && post.effect_applied == pre.effect_applied
182                && post.evidence_persisted == pre.evidence_persisted
183                && post.recovery_intent == pre.recovery_intent))
184    }
185
186    /// Direct Verus counterpart of `AbstractCommitStep`.
187    pub open spec fn abstract_commit_step(
188        pre: &GovernedCommit,
189        post: &GovernedCommit,
190    ) -> bool {
191        &&& (pre.abstract_phase() == AbstractPhase::Active
192            || pre.abstract_phase() == AbstractPhase::Recovering)
193        &&& post.abstract_phase() == AbstractPhase::Committed
194        &&& post.budget.capacity == pre.budget.capacity
195        &&& post.abstract_used() == 1
196        &&& post.effect_applied
197        &&& post.evidence_persisted
198        &&& !post.recovery_intent
199    }
200
201    /// Direct Verus counterpart of the registered restart stutter.
202    pub open spec fn abstract_stutter_step(
203        pre: &GovernedCommit,
204        post: &GovernedCommit,
205    ) -> bool {
206        &&& post.abstract_phase() == pre.abstract_phase()
207        &&& post.budget.capacity == pre.budget.capacity
208        &&& post.abstract_used() == pre.abstract_used()
209        &&& post.effect_applied == pre.effect_applied
210        &&& post.evidence_persisted == pre.evidence_persisted
211        &&& post.recovery_intent == pre.recovery_intent
212    }
213
214    /// Concrete and abstract external observations agree by the frozen phase
215    /// projection; effect and audit fields are identity-mapped.
216    pub open spec fn abstract_observation_agrees(&self) -> bool {
217        &&& ((self.phase == CommitPhase::Committed)
218            == (self.abstract_phase() == AbstractPhase::Committed))
219        &&& ((self.phase == CommitPhase::Rejected
220                || self.phase == CommitPhase::RecoveryPending)
221            == (self.abstract_phase() == AbstractPhase::Failed
222                || self.abstract_phase() == AbstractPhase::Recovering))
223    }
224
225    /// Prove that executable observations agree with their abstract projections.
226    pub proof fn prove_observation_agreement(&self)
227        ensures self.abstract_observation_agrees(),
228    {
229    }
230
231    /// Whether each reused structure satisfies its local invariant.
232    pub open spec fn component_invariants(&self) -> bool {
233        &&& self.registry.unique_mapping()
234        &&& self.budget.safety_invariant()
235        &&& self.attempt_budget.safety_invariant()
236        &&& self.propagation.inv()
237        &&& self.actuation.invariant()
238        &&& self.audit.inv()
239        &&& self.sequential.inv()
240    }
241
242    /// Whether the retained structures agree on the shared commit lifecycle.
243    pub open spec fn integrated_coupling(&self) -> bool {
244        &&& self.attempt_budget.capacity > 0
245        &&& self.attempt_budget.reserved == 0
246        &&& self.attempt_budget.pending_eviction == 0
247        &&& self.propagation.num_nodes == 1
248        &&& self.propagation.max_iterations == 1
249        &&& self.propagation.max_value == 0
250        &&& self.propagation.edges@.len() == 0
251        &&& self.registry.contains_key(0)
252        &&& self.actuation.num_seats == 1
253        &&& self.actuation.allocation@.len() == 1
254        &&& self.actuation.allocation@[0] is Some
255        &&& self.actuation.effects@.len() == 1
256        &&& self.audit.max_log_len == 1
257        &&& self.sequential.steps == 3
258        &&& self.sequential.value_domain_size == 4
259        &&& !self.sequential.active
260        &&& (self.effect_applied == (self.actuation.effects@[0] is Some))
261        &&& (self.evidence_persisted == (self.audit.log@.len() == 1))
262        &&& (self.phase == CommitPhase::Pending ==> self.sequential.pc == 0)
263        &&& (self.phase == CommitPhase::Pending
264                ==> self.budget.allocated == 0
265                    && self.budget.reserved == 0
266                    && !self.effect_applied
267                    && !self.evidence_persisted
268                    && !self.recovery_intent)
269        &&& (self.phase == CommitPhase::Admitted ==> self.sequential.pc == 1)
270        &&& (self.phase == CommitPhase::Ready
271             || self.phase == CommitPhase::Retryable
272             || self.phase == CommitPhase::RecoveryPending
273                ==> self.sequential.pc == 2)
274        &&& (self.phase == CommitPhase::Committed ==> self.sequential.pc == 3)
275        &&& (self.phase == CommitPhase::Admitted
276             || self.phase == CommitPhase::Ready
277             || self.phase == CommitPhase::Retryable
278             || self.phase == CommitPhase::RecoveryPending
279                ==> self.budget.reserved == 1)
280        &&& (self.phase == CommitPhase::Admitted
281             || self.phase == CommitPhase::Ready
282             || self.phase == CommitPhase::Retryable
283                ==> self.budget.allocated == 0
284                    && !self.effect_applied
285                    && !self.evidence_persisted
286                    && !self.recovery_intent)
287        &&& (self.phase == CommitPhase::Rejected
288                ==> !self.effect_applied && !self.evidence_persisted && !self.recovery_intent)
289        &&& (self.phase == CommitPhase::RecoveryPending
290                ==> self.budget.allocated == 0
291                    && self.effect_applied
292                    && self.recovery_intent
293                    && !self.evidence_persisted)
294        &&& (self.phase == CommitPhase::Committed
295                ==> self.effect_applied
296                    && self.evidence_persisted
297                    && !self.recovery_intent
298                    && self.budget.allocated == 1
299                    && self.budget.reserved == 0)
300    }
301
302    /// Whether all component and integration obligations hold.
303    pub open spec fn inv(&self) -> bool {
304        self.component_invariants() && self.integrated_coupling()
305    }
306
307    /// The exact bounded guarantee transferred by the semantic bridge.
308    pub open spec fn transferred_guarantee(&self) -> bool {
309        &&& self.budget.used() <= self.budget.capacity as int
310        &&& (self.phase == CommitPhase::Committed ==> self.evidence_persisted)
311    }
312
313    /// Construct one pending bounded request.
314    pub fn new(resource: u64, capacity: u64, max_attempts: u64) -> (s: GovernedCommit)
315        requires capacity <= 1, 0 < max_attempts <= 2,
316        ensures
317            s.inv(),
318            s.transferred_guarantee(),
319            s.abstract_init(),
320            s.abstract_observation_agrees(),
321            s.phase == CommitPhase::Pending,
322            s.attempt_budget.allocated == 0,
323            !s.effect_applied,
324            !s.evidence_persisted,
325            !s.recovery_intent,
326            !s.crashed,
327            s.budget.capacity == capacity,
328            s.attempt_budget.capacity == max_attempts,
329    {
330        let mut registry = ResourceRegistry::new();
331        registry.register(0, resource);
332
333        let budget = Budget::new(capacity);
334        let attempt_budget = Budget::new(max_attempts);
335
336        let edges: Vec<(usize, usize)> = Vec::new();
337        let mut values: Vec<u64> = Vec::new();
338        values.push(0);
339        let propagation = PropagationPass::new(1, 1, 0, edges, values);
340
341        let mut allocation: Vec<Option<u64>> = Vec::new();
342        allocation.push(Some(resource));
343        let actuation = ActuationPass::new(allocation, 1);
344
345        let audit = AuditSink::new(1);
346        let sequential = Sequential::new(3, 4, 0);
347
348        GovernedCommit {
349            registry,
350            budget,
351            propagation,
352            actuation,
353            audit,
354            sequential,
355            phase: CommitPhase::Pending,
356            attempt_budget,
357            effect_applied: false,
358            evidence_persisted: false,
359            recovery_intent: false,
360            crashed: false,
361        }
362    }
363
364    fn advance(sequential: &mut Sequential, next_value: u64)
365        requires
366            old(sequential).inv(),
367            old(sequential).pc < old(sequential).steps,
368            !old(sequential).active,
369            next_value < old(sequential).value_domain_size,
370        ensures
371            final(sequential).inv(),
372            final(sequential).steps == old(sequential).steps,
373            final(sequential).value_domain_size == old(sequential).value_domain_size,
374            final(sequential).pc == old(sequential).pc + 1,
375            !final(sequential).active,
376            final(sequential).value == next_value,
377    {
378        let began = sequential.begin_step();
379        let _ = began;
380        assert(began);
381        let completed = sequential.complete_step(next_value);
382        let _ = completed;
383        assert(completed);
384    }
385
386    /// Budget admission.  Capacity rejection is an explicit terminal API result
387    /// and leaves every claim-bearing carrier other than the phase unchanged.
388    pub fn admit(&mut self) -> (accepted: bool)
389        requires
390            old(self).inv(),
391            !old(self).crashed,
392            old(self).phase == CommitPhase::Pending,
393            old(self).sequential.pc == 0,
394        ensures
395            final(self).component_invariants(),
396            final(self).integrated_coupling(),
397            final(self).transferred_guarantee(),
398            accepted ==> Self::abstract_system_step(old(self), final(self)),
399            !accepted ==> Self::abstract_failure_step(old(self), final(self)),
400            accepted == (old(self).budget.used() + 1 <= old(self).budget.capacity as int),
401            accepted ==> final(self).phase == CommitPhase::Admitted,
402            !accepted ==> final(self).phase == CommitPhase::Rejected,
403            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated,
404            final(self).effect_applied == old(self).effect_applied,
405            final(self).evidence_persisted == old(self).evidence_persisted,
406    {
407        let accepted = self.budget.reserve(1);
408        if accepted {
409            Self::advance(&mut self.sequential, 1);
410            self.phase = CommitPhase::Admitted;
411        } else {
412            self.phase = CommitPhase::Rejected;
413        }
414        accepted
415    }
416
417    /// Run the one-node propagation witness and advance the Sequential carrier.
418    /// This is the bounded readiness stage between admission and effect commit.
419    pub fn propagate(&mut self)
420        requires
421            old(self).inv(),
422            !old(self).crashed,
423            old(self).phase == CommitPhase::Admitted,
424            old(self).sequential.pc == 1,
425            old(self).propagation.round == Round::Idle,
426            old(self).propagation.changed,
427            old(self).propagation.iteration == 0,
428        ensures
429            final(self).inv(),
430            final(self).transferred_guarantee(),
431            Self::abstract_system_step(old(self), final(self)),
432            final(self).phase == CommitPhase::Ready,
433            final(self).sequential.pc == 2,
434            final(self).propagation.iteration == 1,
435            final(self).propagation.round == Round::Idle,
436            !final(self).propagation.changed,
437    {
438        self.propagation.start_round();
439        self.propagation.update_node(0);
440        assert(self.propagation.all_updated());
441        assert(self.propagation.values@ == self.propagation.snapshot@);
442        self.propagation.end_round();
443        Self::advance(&mut self.sequential, 2);
444        self.phase = CommitPhase::Ready;
445    }
446
447    /// Record a failed external-service attempt before any effect occurred.
448    /// Calling this action again from `Retryable` is the explicit bounded retry
449    /// path; the last permitted failure is a terminal rejection.
450    pub fn fail_before_effect(&mut self) -> (terminal: bool)
451        requires
452            old(self).inv(),
453            !old(self).crashed,
454            old(self).phase == CommitPhase::Ready
455                || old(self).phase == CommitPhase::Retryable,
456            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
457            old(self).sequential.pc == 2,
458            !old(self).effect_applied,
459            !old(self).evidence_persisted,
460        ensures
461            final(self).inv(),
462            final(self).transferred_guarantee(),
463            Self::abstract_failure_step(old(self), final(self)),
464            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
465            final(self).effect_applied == old(self).effect_applied,
466            final(self).evidence_persisted == old(self).evidence_persisted,
467            final(self).recovery_intent == old(self).recovery_intent,
468            final(self).attempt_budget.allocated < final(self).attempt_budget.capacity ==>
469                !terminal && final(self).phase == CommitPhase::Retryable,
470            final(self).attempt_budget.allocated == final(self).attempt_budget.capacity ==>
471                terminal && final(self).phase == CommitPhase::Rejected,
472    {
473        let recorded = self.attempt_budget.try_allocate(1);
474        let _ = recorded;
475        assert(recorded);
476        if self.attempt_budget.allocated == self.attempt_budget.capacity {
477            self.phase = CommitPhase::Rejected;
478            true
479        } else {
480            self.phase = CommitPhase::Retryable;
481            false
482        }
483    }
484
485    /// Record the external effect together with a durable recovery intent, then
486    /// expose the modeled failure before the audit evidence commit. The effect must not
487    /// be retried; only `recover` may complete this state.
488    pub fn fail_after_effect(&mut self)
489        requires
490            old(self).inv(),
491            !old(self).crashed,
492            old(self).phase == CommitPhase::Ready
493                || old(self).phase == CommitPhase::Retryable,
494            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
495            old(self).sequential.pc == 2,
496            !old(self).effect_applied,
497            !old(self).evidence_persisted,
498            old(self).audit.log@.len() == 0,
499            old(self).actuation.effects@[0] is None,
500        ensures
501            final(self).inv(),
502            final(self).transferred_guarantee(),
503            Self::abstract_failure_step(old(self), final(self)),
504            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
505            final(self).phase == CommitPhase::RecoveryPending,
506            final(self).effect_applied,
507            !final(self).evidence_persisted,
508            final(self).recovery_intent,
509    {
510        let recorded = self.attempt_budget.try_allocate(1);
511        let _ = recorded;
512        assert(recorded);
513        // The durable intent precedes the effect receipt at this API boundary.
514        self.recovery_intent = true;
515        self.actuation.actuate(0);
516        self.effect_applied = true;
517        self.phase = CommitPhase::RecoveryPending;
518    }
519
520    /// Atomic success boundary for the bounded persistence adapter: effect
521    /// receipt, unit-budget commit, audit append, and sequential closure become
522    /// visible together at method return.
523    pub fn commit_success(&mut self)
524        requires
525            old(self).inv(),
526            !old(self).crashed,
527            old(self).phase == CommitPhase::Ready
528                || old(self).phase == CommitPhase::Retryable,
529            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
530            old(self).sequential.pc == 2,
531            !old(self).effect_applied,
532            !old(self).evidence_persisted,
533            old(self).audit.log@.len() == 0,
534            old(self).actuation.effects@[0] is None,
535        ensures
536            final(self).inv(),
537            final(self).transferred_guarantee(),
538            Self::abstract_commit_step(old(self), final(self)),
539            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
540            final(self).phase == CommitPhase::Committed,
541            final(self).effect_applied,
542            final(self).evidence_persisted,
543            !final(self).recovery_intent,
544            final(self).sequential.pc == 3,
545    {
546        let recorded = self.attempt_budget.try_allocate(1);
547        let _ = recorded;
548        assert(recorded);
549        self.actuation.actuate(0);
550        self.effect_applied = true;
551        self.budget.commit_reservation(1);
552        let recorded = self.audit.record(0);
553        let _ = recorded;
554        assert(recorded);
555        self.evidence_persisted = true;
556        self.recovery_intent = false;
557        Self::advance(&mut self.sequential, 3);
558        self.phase = CommitPhase::Committed;
559    }
560
561    /// Finish a partial failure without reissuing the already applied effect.
562    pub fn recover(&mut self)
563        requires
564            old(self).inv(),
565            !old(self).crashed,
566            old(self).phase == CommitPhase::RecoveryPending,
567            old(self).sequential.pc == 2,
568            old(self).audit.log@.len() == 0,
569        ensures
570            final(self).inv(),
571            final(self).transferred_guarantee(),
572            Self::abstract_commit_step(old(self), final(self)),
573            final(self).phase == CommitPhase::Committed,
574            final(self).effect_applied,
575            final(self).evidence_persisted,
576            !final(self).recovery_intent,
577            final(self).sequential.pc == 3,
578    {
579        self.budget.commit_reservation(1);
580        let recorded = self.audit.record(0);
581        let _ = recorded;
582        assert(recorded);
583        self.evidence_persisted = true;
584        self.recovery_intent = false;
585        Self::advance(&mut self.sequential, 3);
586        self.phase = CommitPhase::Committed;
587    }
588
589    /// Crash only the volatile process boundary.  All fields named by the
590    /// persistence abstraction remain unchanged and therefore survive restart.
591    pub fn crash(&mut self)
592        requires old(self).inv(),
593        ensures
594            final(self).inv(),
595            final(self).transferred_guarantee(),
596            Self::abstract_failure_step(old(self), final(self)),
597            final(self).crashed,
598            final(self).phase == old(self).phase,
599            final(self).effect_applied == old(self).effect_applied,
600            final(self).evidence_persisted == old(self).evidence_persisted,
601            final(self).recovery_intent == old(self).recovery_intent,
602    {
603        self.crashed = true;
604    }
605
606    /// Restart the volatile process state without changing durable owners.
607    pub fn restart(&mut self)
608        requires old(self).inv(), old(self).crashed,
609        ensures
610            final(self).inv(),
611            final(self).transferred_guarantee(),
612            Self::abstract_stutter_step(old(self), final(self)),
613            !final(self).crashed,
614            final(self).phase == old(self).phase,
615            final(self).effect_applied == old(self).effect_applied,
616            final(self).evidence_persisted == old(self).evidence_persisted,
617            final(self).recovery_intent == old(self).recovery_intent,
618    {
619        self.crashed = false;
620    }
621}
622
623}
automation_structures/integration/governed_commit.rs

automation_structures/integration/
governed_commit.rs
