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;
28#[expect(
29    unused_imports,
30    reason = "ChainOperation is used by ghost specifications erased by rustc"
31)]
32use crate::primitives::audit_sink::ChainOperation;
33use crate::primitives::budget::Budget;
34use crate::primitives::propagation_pass::PropagationPass;
35#[expect(
36    unused_imports,
37    reason = "Round appears in ghost specifications erased by rustc"
38)]
39use crate::primitives::propagation_pass::Round;
40use crate::primitives::resource_registry::ResourceRegistry;
41
42verus! {
43
44#[derive(Clone, Copy, PartialEq, Eq, Debug)]
45/// Concrete phase of the bounded governed-commit assembly.
46pub enum CommitPhase {
47    /// Request has not yet been admitted.
48    Pending,
49    /// Capacity and registry admission have committed.
50    Admitted,
51    /// Propagation has prepared the request for its external effect.
52    Ready,
53    /// A pre-effect failure permits another bounded attempt.
54    Retryable,
55    /// An applied effect is waiting for durable recovery evidence.
56    RecoveryPending,
57    /// Effect and durable evidence have both committed.
58    Committed,
59    /// The request cannot make another admitted attempt.
60    Rejected,
61}
62
63/// Frozen abstract phases for the direct source-level refinement proof.  These
64/// are the same five observations used by `GovernedCommitAbstract.tla`.
65#[derive(Clone, Copy, PartialEq, Eq, Debug)]
66pub enum AbstractPhase {
67    /// No abstract work is active.
68    Pending,
69    /// Admission, preparation, or retry is active.
70    Active,
71    /// An applied effect is being recovered.
72    Recovering,
73    /// Effect and evidence are committed.
74    Committed,
75    /// The abstract request has failed.
76    Failed,
77}
78
79/// One bounded integrated request.  The component fields are the actual
80/// executable carriers; the remaining fields expose the external effect,
81/// persistence, failure, and recovery boundary absent from the individual rows.
82pub struct GovernedCommit {
83    /// Registry owner for the admitted request.
84    pub registry: ResourceRegistry<u64, u64>,
85    /// Resource-capacity owner.
86    pub budget: Budget,
87    /// Preparation owner.
88    pub propagation: PropagationPass,
89    /// External-effect lifecycle owner.
90    pub actuation: ActuationPass,
91    /// Durable evidence owner.
92    pub audit: AuditSink,
93    /// Execution-order owner.
94    pub sequential: Sequential,
95    /// Current concrete assembly phase.
96    pub phase: CommitPhase,
97    /// Owner of bounded retry attempts.
98    pub attempt_budget: Budget,
99    /// Whether the external effect has been applied.
100    pub effect_applied: bool,
101    /// Whether durable evidence for the effect has been retained.
102    pub evidence_persisted: bool,
103    /// Whether durable recovery intent has been retained.
104    pub recovery_intent: bool,
105    /// Whether the modeled process is currently crashed.
106    pub crashed: bool,
107}
108
109impl GovernedCommit {
110    /// Project the retained component states to the abstract commit phase.
111    pub open spec fn abstract_phase(&self) -> AbstractPhase {
112        if self.phase == CommitPhase::Pending {
113            AbstractPhase::Pending
114        } else if self.phase == CommitPhase::Admitted
115            || self.phase == CommitPhase::Ready
116            || self.phase == CommitPhase::Retryable
117        {
118            AbstractPhase::Active
119        } else if self.phase == CommitPhase::RecoveryPending {
120            AbstractPhase::Recovering
121        } else if self.phase == CommitPhase::Committed {
122            AbstractPhase::Committed
123        } else {
124            AbstractPhase::Failed
125        }
126    }
127
128    /// Project committed resource use from the retained budget owners.
129    pub open spec fn abstract_used(&self) -> int {
130        self.budget.allocated as int + self.budget.reserved as int
131    }
132
133    /// The frozen abstract initial predicate, evaluated through the executable
134    /// abstraction map above.
135    pub open spec fn abstract_init(&self) -> bool {
136        &&& self.abstract_phase() == AbstractPhase::Pending
137        &&& self.abstract_used() == 0
138        &&& !self.effect_applied
139        &&& !self.evidence_persisted
140        &&& !self.recovery_intent
141    }
142
143    /// Direct Verus counterpart of `AbstractSystemStep`.
144    pub open spec fn abstract_system_step(
145        pre: &GovernedCommit,
146        post: &GovernedCommit,
147    ) -> bool {
148        &&& post.budget.capacity == pre.budget.capacity
149        &&& post.effect_applied == pre.effect_applied
150        &&& post.evidence_persisted == pre.evidence_persisted
151        &&& post.recovery_intent == pre.recovery_intent
152        &&& ((pre.abstract_phase() == AbstractPhase::Pending
153                && post.abstract_phase() == AbstractPhase::Active
154                && post.abstract_used() == 1)
155            || (pre.abstract_phase() == AbstractPhase::Active
156                && post.abstract_phase() == AbstractPhase::Active
157                && post.abstract_used() == pre.abstract_used()))
158    }
159
160    /// Direct Verus counterpart of `AbstractFailureStep`.  Rejection, retry,
161    /// partial failure, and crash are exhaustive named arms.
162    pub open spec fn abstract_failure_step(
163        pre: &GovernedCommit,
164        post: &GovernedCommit,
165    ) -> bool {
166        &&& post.budget.capacity == pre.budget.capacity
167        &&& ((post.abstract_phase() == AbstractPhase::Failed
168                && post.abstract_used() == pre.abstract_used()
169                && post.effect_applied == pre.effect_applied
170                && post.evidence_persisted == pre.evidence_persisted
171                && post.recovery_intent == pre.recovery_intent)
172            || (pre.abstract_phase() == AbstractPhase::Active
173                && post.abstract_phase() == AbstractPhase::Active
174                && post.abstract_used() == pre.abstract_used()
175                && post.effect_applied == pre.effect_applied
176                && post.evidence_persisted == pre.evidence_persisted
177                && post.recovery_intent == pre.recovery_intent)
178            || (pre.abstract_phase() == AbstractPhase::Active
179                && post.abstract_phase() == AbstractPhase::Recovering
180                && post.abstract_used() == pre.abstract_used()
181                && post.effect_applied
182                && !post.evidence_persisted
183                && post.recovery_intent)
184            || (post.abstract_phase() == pre.abstract_phase()
185                && post.abstract_used() == pre.abstract_used()
186                && post.effect_applied == pre.effect_applied
187                && post.evidence_persisted == pre.evidence_persisted
188                && post.recovery_intent == pre.recovery_intent))
189    }
190
191    /// Direct Verus counterpart of `AbstractCommitStep`.
192    pub open spec fn abstract_commit_step(
193        pre: &GovernedCommit,
194        post: &GovernedCommit,
195    ) -> bool {
196        &&& (pre.abstract_phase() == AbstractPhase::Active
197            || pre.abstract_phase() == AbstractPhase::Recovering)
198        &&& post.abstract_phase() == AbstractPhase::Committed
199        &&& post.budget.capacity == pre.budget.capacity
200        &&& post.abstract_used() == 1
201        &&& post.effect_applied
202        &&& post.evidence_persisted
203        &&& !post.recovery_intent
204    }
205
206    /// Direct Verus counterpart of the registered restart stutter.
207    pub open spec fn abstract_stutter_step(
208        pre: &GovernedCommit,
209        post: &GovernedCommit,
210    ) -> bool {
211        &&& post.abstract_phase() == pre.abstract_phase()
212        &&& post.budget.capacity == pre.budget.capacity
213        &&& post.abstract_used() == pre.abstract_used()
214        &&& post.effect_applied == pre.effect_applied
215        &&& post.evidence_persisted == pre.evidence_persisted
216        &&& post.recovery_intent == pre.recovery_intent
217    }
218
219    /// Concrete and abstract external observations agree by the frozen phase
220    /// projection; effect and audit fields are identity-mapped.
221    pub open spec fn abstract_observation_agrees(&self) -> bool {
222        &&& ((self.phase == CommitPhase::Committed)
223            == (self.abstract_phase() == AbstractPhase::Committed))
224        &&& ((self.phase == CommitPhase::Rejected
225                || self.phase == CommitPhase::RecoveryPending)
226            == (self.abstract_phase() == AbstractPhase::Failed
227                || self.abstract_phase() == AbstractPhase::Recovering))
228    }
229
230    /// Prove that executable observations agree with their abstract projections.
231    pub proof fn prove_observation_agreement(&self)
232        ensures self.abstract_observation_agrees(),
233    {
234    }
235
236    /// Whether each reused structure satisfies its local invariant.
237    pub open spec fn component_invariants(&self) -> bool {
238        &&& self.registry.unique_mapping()
239        &&& self.budget.safety_invariant()
240        &&& self.attempt_budget.safety_invariant()
241        &&& self.propagation.inv()
242        &&& self.actuation.invariant()
243        &&& self.audit.inv()
244        &&& self.sequential.inv()
245    }
246
247    /// Whether the retained structures agree on the shared commit lifecycle.
248    pub open spec fn integrated_coupling(&self) -> bool {
249        &&& self.attempt_budget.capacity > 0
250        &&& self.attempt_budget.reserved == 0
251        &&& self.attempt_budget.pending_eviction == 0
252        &&& self.propagation.num_nodes == 1
253        &&& self.propagation.max_iterations == 1
254        &&& self.propagation.max_value == 0
255        &&& self.propagation.edges@.len() == 0
256        &&& self.registry.contains_key(0)
257        &&& self.actuation.num_seats == 1
258        &&& self.actuation.allocation@.len() == 1
259        &&& self.actuation.allocation@[0] is Some
260        &&& self.actuation.effects@.len() == 1
261        &&& self.audit.max_log_len == 1
262        &&& self.sequential.steps == 3
263        &&& self.sequential.value_domain_size == 4
264        &&& !self.sequential.active
265        &&& (self.effect_applied == (self.actuation.effects@[0] is Some))
266        &&& (self.evidence_persisted == (self.audit.log@.len() == 1))
267        &&& (self.phase == CommitPhase::Pending ==> self.sequential.pc == 0)
268        &&& (self.phase == CommitPhase::Pending
269                ==> self.budget.allocated == 0
270                    && self.budget.reserved == 0
271                    && !self.effect_applied
272                    && !self.evidence_persisted
273                    && !self.recovery_intent)
274        &&& (self.phase == CommitPhase::Admitted ==> self.sequential.pc == 1)
275        &&& (self.phase == CommitPhase::Ready
276             || self.phase == CommitPhase::Retryable
277             || self.phase == CommitPhase::RecoveryPending
278                ==> self.sequential.pc == 2)
279        &&& (self.phase == CommitPhase::Committed ==> self.sequential.pc == 3)
280        &&& (self.phase == CommitPhase::Admitted
281             || self.phase == CommitPhase::Ready
282             || self.phase == CommitPhase::Retryable
283             || self.phase == CommitPhase::RecoveryPending
284                ==> self.budget.reserved == 1)
285        &&& (self.phase == CommitPhase::Admitted
286             || self.phase == CommitPhase::Ready
287             || self.phase == CommitPhase::Retryable
288                ==> self.budget.allocated == 0
289                    && !self.effect_applied
290                    && !self.evidence_persisted
291                    && !self.recovery_intent)
292        &&& (self.phase == CommitPhase::Rejected
293                ==> !self.effect_applied && !self.evidence_persisted && !self.recovery_intent)
294        &&& (self.phase == CommitPhase::RecoveryPending
295                ==> self.budget.allocated == 0
296                    && self.effect_applied
297                    && self.recovery_intent
298                    && !self.evidence_persisted)
299        &&& (self.phase == CommitPhase::Committed
300                ==> self.effect_applied
301                    && self.evidence_persisted
302                    && !self.recovery_intent
303                    && self.budget.allocated == 1
304                    && self.budget.reserved == 0)
305    }
306
307    /// Whether all component and integration obligations hold.
308    pub open spec fn inv(&self) -> bool {
309        self.component_invariants() && self.integrated_coupling()
310    }
311
312    /// The exact bounded guarantee transferred by the semantic bridge.
313    pub open spec fn transferred_guarantee(&self) -> bool {
314        &&& self.budget.used() <= self.budget.capacity as int
315        &&& (self.phase == CommitPhase::Committed ==> self.evidence_persisted)
316    }
317
318    /// Construct one pending bounded request.
319    pub fn new(resource: u64, capacity: u64, max_attempts: u64) -> (s: GovernedCommit)
320        requires capacity <= 1, 0 < max_attempts <= 2,
321        ensures
322            s.inv(),
323            s.transferred_guarantee(),
324            s.abstract_init(),
325            s.abstract_observation_agrees(),
326            s.phase == CommitPhase::Pending,
327            s.attempt_budget.allocated == 0,
328            !s.effect_applied,
329            !s.evidence_persisted,
330            !s.recovery_intent,
331            !s.crashed,
332            s.budget.capacity == capacity,
333            s.attempt_budget.capacity == max_attempts,
334            s.registry.entries@ == seq![(0u64, resource)],
335            s.registry.maps_to(0, resource),
336            s.budget.allocated == 0,
337            s.budget.reserved == 0,
338            s.budget.pending_eviction == 0,
339            s.attempt_budget.allocated == 0,
340            s.attempt_budget.reserved == 0,
341            s.attempt_budget.pending_eviction == 0,
342            s.propagation.iteration == 0,
343            s.propagation.round == Round::Idle,
344            s.propagation.changed,
345            s.actuation.allocation@ == seq![Some(resource)],
346            s.actuation.effects@ == seq![None],
347            !s.actuation.complete,
348            s.audit.log@.len() == 0,
349            s.audit.last_hash == 0,
350            s.sequential.pc == 0,
351            !s.sequential.active,
352            s.sequential.history@.len() == 0,
353    {
354        let mut registry = ResourceRegistry::new();
355        registry.register(0, resource);
356
357        let budget = Budget::new(capacity);
358        let attempt_budget = Budget::new(max_attempts);
359
360        let edges: Vec<(usize, usize)> = Vec::new();
361        let mut values: Vec<u64> = Vec::new();
362        values.push(0);
363        let propagation = PropagationPass::new(1, 1, 0, edges, values);
364
365        let mut allocation: Vec<Option<u64>> = Vec::new();
366        allocation.push(Some(resource));
367        let actuation = ActuationPass::new(allocation, 1);
368
369        let audit = AuditSink::new(1);
370        let sequential = Sequential::new(3, 4, 0);
371
372        GovernedCommit {
373            registry,
374            budget,
375            propagation,
376            actuation,
377            audit,
378            sequential,
379            phase: CommitPhase::Pending,
380            attempt_budget,
381            effect_applied: false,
382            evidence_persisted: false,
383            recovery_intent: false,
384            crashed: false,
385        }
386    }
387
388    fn advance(sequential: &mut Sequential, next_value: u64)
389        requires
390            old(sequential).inv(),
391            old(sequential).pc < old(sequential).steps,
392            !old(sequential).active,
393            next_value < old(sequential).value_domain_size,
394        ensures
395            final(sequential).inv(),
396            final(sequential).steps == old(sequential).steps,
397            final(sequential).value_domain_size == old(sequential).value_domain_size,
398            final(sequential).pc == old(sequential).pc + 1,
399            !final(sequential).active,
400            final(sequential).value == next_value,
401            final(sequential).history@ == old(sequential).history@.push(next_value),
402    {
403        let began = sequential.begin_step();
404        let _ = began;
405        assert(began);
406        let completed = sequential.complete_step(next_value);
407        let _ = completed;
408        assert(completed);
409    }
410
411    /// Budget admission.  Capacity rejection is an explicit terminal API result
412    /// and leaves every claim-bearing carrier other than the phase unchanged.
413    pub fn admit(&mut self) -> (accepted: bool)
414        requires
415            old(self).inv(),
416            !old(self).crashed,
417            old(self).phase == CommitPhase::Pending,
418            old(self).sequential.pc == 0,
419        ensures
420            final(self).component_invariants(),
421            final(self).integrated_coupling(),
422            final(self).transferred_guarantee(),
423            accepted ==> Self::abstract_system_step(old(self), final(self)),
424            !accepted ==> Self::abstract_failure_step(old(self), final(self)),
425            accepted == (old(self).budget.used() + 1 <= old(self).budget.capacity as int),
426            accepted ==> final(self).phase == CommitPhase::Admitted,
427            !accepted ==> final(self).phase == CommitPhase::Rejected,
428            final(self).registry == old(self).registry,
429            final(self).budget.capacity == old(self).budget.capacity,
430            final(self).budget.allocated == old(self).budget.allocated,
431            final(self).budget.pending_eviction == old(self).budget.pending_eviction,
432            final(self).budget.reserved == if accepted {
433                (old(self).budget.reserved + 1) as u64
434            } else {
435                old(self).budget.reserved
436            },
437            final(self).propagation == old(self).propagation,
438            final(self).actuation == old(self).actuation,
439            final(self).audit == old(self).audit,
440            final(self).attempt_budget == old(self).attempt_budget,
441            accepted ==> {
442                &&& final(self).sequential.steps == old(self).sequential.steps
443                &&& final(self).sequential.value_domain_size
444                    == old(self).sequential.value_domain_size
445                &&& final(self).sequential.pc == old(self).sequential.pc + 1
446                &&& !final(self).sequential.active
447                &&& final(self).sequential.value == 1
448                &&& final(self).sequential.history@
449                    == old(self).sequential.history@.push(1)
450            },
451            !accepted ==> final(self).sequential == old(self).sequential,
452            final(self).effect_applied == old(self).effect_applied,
453            final(self).evidence_persisted == old(self).evidence_persisted,
454            final(self).recovery_intent == old(self).recovery_intent,
455            final(self).crashed == old(self).crashed,
456    {
457        let accepted = self.budget.reserve(1);
458        if accepted {
459            Self::advance(&mut self.sequential, 1);
460            self.phase = CommitPhase::Admitted;
461        } else {
462            self.phase = CommitPhase::Rejected;
463        }
464        accepted
465    }
466
467    /// Run the one-node propagation witness and advance the Sequential carrier.
468    /// This is the bounded readiness stage between admission and effect commit.
469    pub fn propagate(&mut self)
470        requires
471            old(self).inv(),
472            !old(self).crashed,
473            old(self).phase == CommitPhase::Admitted,
474            old(self).sequential.pc == 1,
475            old(self).propagation.round == Round::Idle,
476            old(self).propagation.changed,
477            old(self).propagation.iteration == 0,
478        ensures
479            final(self).inv(),
480            final(self).transferred_guarantee(),
481            Self::abstract_system_step(old(self), final(self)),
482            final(self).phase == CommitPhase::Ready,
483            final(self).sequential.pc == 2,
484            final(self).propagation.iteration == 1,
485            final(self).propagation.round == Round::Idle,
486            !final(self).propagation.changed,
487            final(self).registry == old(self).registry,
488            final(self).budget == old(self).budget,
489            final(self).attempt_budget == old(self).attempt_budget,
490            final(self).actuation == old(self).actuation,
491            final(self).audit == old(self).audit,
492            final(self).propagation.num_nodes == old(self).propagation.num_nodes,
493            final(self).propagation.max_iterations
494                == old(self).propagation.max_iterations,
495            final(self).propagation.max_value == old(self).propagation.max_value,
496            final(self).propagation.edges@ == old(self).propagation.edges@,
497            final(self).propagation.values@ == old(self).propagation.values@,
498            final(self).propagation.snapshot@ == old(self).propagation.values@,
499            forall|index: int| 0 <= index < final(self).propagation.updated@.len() ==>
500                #[trigger] final(self).propagation.updated@[index],
501            final(self).sequential.steps == old(self).sequential.steps,
502            final(self).sequential.value_domain_size
503                == old(self).sequential.value_domain_size,
504            final(self).sequential.value == 2,
505            !final(self).sequential.active,
506            final(self).sequential.history@ == old(self).sequential.history@.push(2),
507            final(self).effect_applied == old(self).effect_applied,
508            final(self).evidence_persisted == old(self).evidence_persisted,
509            final(self).recovery_intent == old(self).recovery_intent,
510            final(self).crashed == old(self).crashed,
511    {
512        self.propagation.start_round();
513        self.propagation.update_node(0);
514        assert(self.propagation.all_updated());
515        assert(self.propagation.values@ == self.propagation.snapshot@);
516        self.propagation.end_round();
517        Self::advance(&mut self.sequential, 2);
518        self.phase = CommitPhase::Ready;
519    }
520
521    /// Record a failed external-service attempt before any effect occurred.
522    /// Calling this action again from `Retryable` is the explicit bounded retry
523    /// path; the last permitted failure is a terminal rejection.
524    pub fn fail_before_effect(&mut self) -> (terminal: bool)
525        requires
526            old(self).inv(),
527            !old(self).crashed,
528            old(self).phase == CommitPhase::Ready
529                || old(self).phase == CommitPhase::Retryable,
530            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
531            old(self).sequential.pc == 2,
532            !old(self).effect_applied,
533            !old(self).evidence_persisted,
534        ensures
535            final(self).inv(),
536            final(self).transferred_guarantee(),
537            Self::abstract_failure_step(old(self), final(self)),
538            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
539            final(self).registry == old(self).registry,
540            final(self).budget == old(self).budget,
541            final(self).propagation == old(self).propagation,
542            final(self).actuation == old(self).actuation,
543            final(self).audit == old(self).audit,
544            final(self).sequential == old(self).sequential,
545            final(self).attempt_budget.capacity == old(self).attempt_budget.capacity,
546            final(self).attempt_budget.reserved == old(self).attempt_budget.reserved,
547            final(self).attempt_budget.pending_eviction
548                == old(self).attempt_budget.pending_eviction,
549            final(self).effect_applied == old(self).effect_applied,
550            final(self).evidence_persisted == old(self).evidence_persisted,
551            final(self).recovery_intent == old(self).recovery_intent,
552            final(self).crashed == old(self).crashed,
553            final(self).attempt_budget.allocated < final(self).attempt_budget.capacity ==>
554                !terminal && final(self).phase == CommitPhase::Retryable,
555            final(self).attempt_budget.allocated == final(self).attempt_budget.capacity ==>
556                terminal && final(self).phase == CommitPhase::Rejected,
557    {
558        let recorded = self.attempt_budget.try_allocate(1);
559        let _ = recorded;
560        assert(recorded);
561        if self.attempt_budget.allocated == self.attempt_budget.capacity {
562            self.phase = CommitPhase::Rejected;
563            true
564        } else {
565            self.phase = CommitPhase::Retryable;
566            false
567        }
568    }
569
570    /// Record the external effect together with a durable recovery intent, then
571    /// expose the modeled failure before the audit evidence commit. The effect must not
572    /// be retried; only `recover` may complete this state.
573    pub fn fail_after_effect(&mut self)
574        requires
575            old(self).inv(),
576            !old(self).crashed,
577            old(self).phase == CommitPhase::Ready
578                || old(self).phase == CommitPhase::Retryable,
579            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
580            old(self).sequential.pc == 2,
581            !old(self).effect_applied,
582            !old(self).evidence_persisted,
583            old(self).audit.log@.len() == 0,
584            old(self).actuation.effects@[0] is None,
585        ensures
586            final(self).inv(),
587            final(self).transferred_guarantee(),
588            Self::abstract_failure_step(old(self), final(self)),
589            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
590            final(self).phase == CommitPhase::RecoveryPending,
591            final(self).effect_applied,
592            !final(self).evidence_persisted,
593            final(self).recovery_intent,
594            final(self).registry == old(self).registry,
595            final(self).budget == old(self).budget,
596            final(self).propagation == old(self).propagation,
597            final(self).audit == old(self).audit,
598            final(self).sequential == old(self).sequential,
599            final(self).attempt_budget.capacity == old(self).attempt_budget.capacity,
600            final(self).attempt_budget.reserved == old(self).attempt_budget.reserved,
601            final(self).attempt_budget.pending_eviction
602                == old(self).attempt_budget.pending_eviction,
603            final(self).actuation.num_seats == old(self).actuation.num_seats,
604            final(self).actuation.allocation@ == old(self).actuation.allocation@,
605            final(self).actuation.effects@
606                == old(self).actuation.effects@.update(
607                    0,
608                    old(self).actuation.allocation@[0],
609                ),
610            final(self).actuation.complete == old(self).actuation.complete,
611            final(self).crashed == old(self).crashed,
612    {
613        let recorded = self.attempt_budget.try_allocate(1);
614        let _ = recorded;
615        assert(recorded);
616        // The durable intent precedes the effect receipt at this API boundary.
617        self.recovery_intent = true;
618        self.actuation.actuate(0);
619        self.effect_applied = true;
620        self.phase = CommitPhase::RecoveryPending;
621    }
622
623    /// Atomic success boundary for the bounded persistence adapter: effect
624    /// receipt, unit-budget commit, audit append, and sequential closure become
625    /// visible together at method return.
626    pub fn commit_success(&mut self)
627        requires
628            old(self).inv(),
629            !old(self).crashed,
630            old(self).phase == CommitPhase::Ready
631                || old(self).phase == CommitPhase::Retryable,
632            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
633            old(self).sequential.pc == 2,
634            !old(self).effect_applied,
635            !old(self).evidence_persisted,
636            old(self).audit.log@.len() == 0,
637            old(self).actuation.effects@[0] is None,
638        ensures
639            final(self).inv(),
640            final(self).transferred_guarantee(),
641            Self::abstract_commit_step(old(self), final(self)),
642            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
643            final(self).phase == CommitPhase::Committed,
644            final(self).effect_applied,
645            final(self).evidence_persisted,
646            !final(self).recovery_intent,
647            final(self).sequential.pc == 3,
648            final(self).registry == old(self).registry,
649            final(self).propagation == old(self).propagation,
650            final(self).attempt_budget.capacity == old(self).attempt_budget.capacity,
651            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
652            final(self).attempt_budget.reserved == old(self).attempt_budget.reserved,
653            final(self).attempt_budget.pending_eviction
654                == old(self).attempt_budget.pending_eviction,
655            final(self).budget.capacity == old(self).budget.capacity,
656            final(self).budget.allocated == old(self).budget.allocated + 1,
657            final(self).budget.reserved == old(self).budget.reserved - 1,
658            final(self).budget.pending_eviction == old(self).budget.pending_eviction,
659            final(self).actuation.num_seats == old(self).actuation.num_seats,
660            final(self).actuation.allocation@ == old(self).actuation.allocation@,
661            final(self).actuation.effects@
662                == old(self).actuation.effects@.update(
663                    0,
664                    old(self).actuation.allocation@[0],
665                ),
666            final(self).actuation.complete == old(self).actuation.complete,
667            final(self).audit.operator == old(self).audit.operator,
668            final(self).audit.max_log_len == old(self).audit.max_log_len,
669            final(self).audit.log@.len() == old(self).audit.log@.len() + 1,
670            final(self).audit.last_hash
671                == old(self).audit.operator.combine_spec(old(self).audit.last_hash, 0),
672            final(self).audit.log@[old(self).audit.log@.len() as int].operation == 0,
673            final(self).audit.log@[old(self).audit.log@.len() as int].prev_hash
674                == old(self).audit.last_hash,
675            forall|index: int| 0 <= index < old(self).audit.log@.len() ==>
676                #[trigger] final(self).audit.log@[index] == old(self).audit.log@[index],
677            final(self).sequential.steps == old(self).sequential.steps,
678            final(self).sequential.value_domain_size
679                == old(self).sequential.value_domain_size,
680            final(self).sequential.value == 3,
681            !final(self).sequential.active,
682            final(self).sequential.history@ == old(self).sequential.history@.push(3),
683            final(self).crashed == old(self).crashed,
684    {
685        let recorded = self.attempt_budget.try_allocate(1);
686        let _ = recorded;
687        assert(recorded);
688        self.actuation.actuate(0);
689        self.effect_applied = true;
690        self.budget.commit_reservation(1);
691        let recorded = self.audit.record(0);
692        let _ = recorded;
693        assert(recorded);
694        self.evidence_persisted = true;
695        self.recovery_intent = false;
696        Self::advance(&mut self.sequential, 3);
697        self.phase = CommitPhase::Committed;
698    }
699
700    /// Finish a partial failure without reissuing the already applied effect.
701    pub fn recover(&mut self)
702        requires
703            old(self).inv(),
704            !old(self).crashed,
705            old(self).phase == CommitPhase::RecoveryPending,
706            old(self).sequential.pc == 2,
707            old(self).audit.log@.len() == 0,
708        ensures
709            final(self).inv(),
710            final(self).transferred_guarantee(),
711            Self::abstract_commit_step(old(self), final(self)),
712            final(self).phase == CommitPhase::Committed,
713            final(self).effect_applied,
714            final(self).evidence_persisted,
715            !final(self).recovery_intent,
716            final(self).sequential.pc == 3,
717            final(self).registry == old(self).registry,
718            final(self).propagation == old(self).propagation,
719            final(self).attempt_budget == old(self).attempt_budget,
720            final(self).budget.capacity == old(self).budget.capacity,
721            final(self).budget.allocated == old(self).budget.allocated + 1,
722            final(self).budget.reserved == old(self).budget.reserved - 1,
723            final(self).budget.pending_eviction == old(self).budget.pending_eviction,
724            final(self).actuation == old(self).actuation,
725            final(self).audit.operator == old(self).audit.operator,
726            final(self).audit.max_log_len == old(self).audit.max_log_len,
727            final(self).audit.log@.len() == old(self).audit.log@.len() + 1,
728            final(self).audit.last_hash
729                == old(self).audit.operator.combine_spec(old(self).audit.last_hash, 0),
730            final(self).audit.log@[old(self).audit.log@.len() as int].operation == 0,
731            final(self).audit.log@[old(self).audit.log@.len() as int].prev_hash
732                == old(self).audit.last_hash,
733            forall|index: int| 0 <= index < old(self).audit.log@.len() ==>
734                #[trigger] final(self).audit.log@[index] == old(self).audit.log@[index],
735            final(self).sequential.steps == old(self).sequential.steps,
736            final(self).sequential.value_domain_size
737                == old(self).sequential.value_domain_size,
738            final(self).sequential.value == 3,
739            !final(self).sequential.active,
740            final(self).sequential.history@ == old(self).sequential.history@.push(3),
741            final(self).crashed == old(self).crashed,
742    {
743        self.budget.commit_reservation(1);
744        let recorded = self.audit.record(0);
745        let _ = recorded;
746        assert(recorded);
747        self.evidence_persisted = true;
748        self.recovery_intent = false;
749        Self::advance(&mut self.sequential, 3);
750        self.phase = CommitPhase::Committed;
751    }
752
753    /// Crash only the volatile process boundary.  All fields named by the
754    /// persistence abstraction remain unchanged and therefore survive restart.
755    pub fn crash(&mut self)
756        requires old(self).inv(),
757        ensures
758            final(self).inv(),
759            final(self).transferred_guarantee(),
760            Self::abstract_failure_step(old(self), final(self)),
761            final(self).crashed,
762            final(self).phase == old(self).phase,
763            final(self).effect_applied == old(self).effect_applied,
764            final(self).evidence_persisted == old(self).evidence_persisted,
765            final(self).recovery_intent == old(self).recovery_intent,
766            final(self).registry == old(self).registry,
767            final(self).budget == old(self).budget,
768            final(self).propagation == old(self).propagation,
769            final(self).actuation == old(self).actuation,
770            final(self).audit == old(self).audit,
771            final(self).sequential == old(self).sequential,
772            final(self).attempt_budget == old(self).attempt_budget,
773    {
774        self.crashed = true;
775    }
776
777    /// Restart the volatile process state without changing durable owners.
778    pub fn restart(&mut self)
779        requires old(self).inv(), old(self).crashed,
780        ensures
781            final(self).inv(),
782            final(self).transferred_guarantee(),
783            Self::abstract_stutter_step(old(self), final(self)),
784            !final(self).crashed,
785            final(self).phase == old(self).phase,
786            final(self).effect_applied == old(self).effect_applied,
787            final(self).evidence_persisted == old(self).evidence_persisted,
788            final(self).recovery_intent == old(self).recovery_intent,
789            final(self).registry == old(self).registry,
790            final(self).budget == old(self).budget,
791            final(self).propagation == old(self).propagation,
792            final(self).actuation == old(self).actuation,
793            final(self).audit == old(self).audit,
794            final(self).sequential == old(self).sequential,
795            final(self).attempt_budget == old(self).attempt_budget,
796    {
797        self.crashed = false;
798    }
799}
800
801}
automation_structures/integration/governed_commit.rs

automation_structures/integration/
governed_commit.rs
