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 while retaining the bridge contract:
7// capacity safety and `Committed => modeled 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 adapter-reported effect is waiting for modeled durable recovery evidence.
56    RecoveryPending,
57    /// The effect receipt and modeled 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 adapter-reported effect,
81/// modeled 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    /// Modeled evidence-chain owner; durability depends on the registered persistence provider.
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 adapter reports that the effect was applied.
100    pub effect_applied: bool,
101    /// Whether the persistence adapter acknowledges retaining evidence for the effect.
102    pub evidence_persisted: bool,
103    /// Whether the persistence adapter acknowledges retaining recovery intent.
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 contract clauses hold.
308    pub open spec fn inv(&self) -> bool {
309        self.component_invariants() && self.integrated_coupling()
310    }
311
312    /// The exact bounded contract consequence established by the semantic bridge.
313    pub open spec fn bridge_contract(&self) -> bool {
314        &&& self.budget.used() <= self.budget.capacity as int
315        &&& (self.phase == CommitPhase::Committed ==> self.evidence_persisted)
316    }
317
318    /// Compatibility alias for [`Self::bridge_contract`].
319    ///
320    /// The bridge proves this state predicate. A deployment guarantee still belongs to the
321    /// principal that owns the framed persistence and effect obligation.
322    pub open spec fn transferred_guarantee(&self) -> bool {
323        self.bridge_contract()
324    }
325
326    /// Construct one pending bounded request.
327    pub fn new(resource: u64, capacity: u64, max_attempts: u64) -> (s: GovernedCommit)
328        requires capacity <= 1, 0 < max_attempts <= 2,
329        ensures
330            s.inv(),
331            s.bridge_contract(),
332            s.abstract_init(),
333            s.abstract_observation_agrees(),
334            s.phase == CommitPhase::Pending,
335            s.attempt_budget.allocated == 0,
336            !s.effect_applied,
337            !s.evidence_persisted,
338            !s.recovery_intent,
339            !s.crashed,
340            s.budget.capacity == capacity,
341            s.attempt_budget.capacity == max_attempts,
342            s.registry.entries@ == seq![(0u64, resource)],
343            s.registry.maps_to(0, resource),
344            s.budget.allocated == 0,
345            s.budget.reserved == 0,
346            s.budget.pending_eviction == 0,
347            s.attempt_budget.allocated == 0,
348            s.attempt_budget.reserved == 0,
349            s.attempt_budget.pending_eviction == 0,
350            s.propagation.iteration == 0,
351            s.propagation.round == Round::Idle,
352            s.propagation.changed,
353            s.actuation.allocation@ == seq![Some(resource)],
354            s.actuation.effects@ == seq![None],
355            !s.actuation.complete,
356            s.audit.log@.len() == 0,
357            s.audit.last_hash == 0,
358            s.sequential.pc == 0,
359            !s.sequential.active,
360            s.sequential.history@.len() == 0,
361    {
362        let mut registry = ResourceRegistry::new();
363        registry.register(0, resource);
364
365        let budget = Budget::new(capacity);
366        let attempt_budget = Budget::new(max_attempts);
367
368        let edges: Vec<(usize, usize)> = Vec::new();
369        let mut values: Vec<u64> = Vec::new();
370        values.push(0);
371        let propagation = PropagationPass::new(1, 1, 0, edges, values);
372
373        let mut allocation: Vec<Option<u64>> = Vec::new();
374        allocation.push(Some(resource));
375        let actuation = ActuationPass::new(allocation, 1);
376
377        let audit = AuditSink::new(1);
378        let sequential = Sequential::new(3, 4, 0);
379
380        GovernedCommit {
381            registry,
382            budget,
383            propagation,
384            actuation,
385            audit,
386            sequential,
387            phase: CommitPhase::Pending,
388            attempt_budget,
389            effect_applied: false,
390            evidence_persisted: false,
391            recovery_intent: false,
392            crashed: false,
393        }
394    }
395
396    fn advance(sequential: &mut Sequential, next_value: u64)
397        requires
398            old(sequential).inv(),
399            old(sequential).pc < old(sequential).steps,
400            !old(sequential).active,
401            next_value < old(sequential).value_domain_size,
402        ensures
403            final(sequential).inv(),
404            final(sequential).steps == old(sequential).steps,
405            final(sequential).value_domain_size == old(sequential).value_domain_size,
406            final(sequential).pc == old(sequential).pc + 1,
407            !final(sequential).active,
408            final(sequential).value == next_value,
409            final(sequential).history@ == old(sequential).history@.push(next_value),
410    {
411        let began = sequential.begin_step();
412        let _ = began;
413        assert(began);
414        let completed = sequential.complete_step(next_value);
415        let _ = completed;
416        assert(completed);
417    }
418
419    /// Budget admission.  Capacity rejection is an explicit terminal API result
420    /// and leaves every state-bearing carrier other than the phase unchanged.
421    pub fn admit(&mut self) -> (accepted: bool)
422        requires
423            old(self).inv(),
424            !old(self).crashed,
425            old(self).phase == CommitPhase::Pending,
426            old(self).sequential.pc == 0,
427        ensures
428            final(self).component_invariants(),
429            final(self).integrated_coupling(),
430            final(self).bridge_contract(),
431            accepted ==> Self::abstract_system_step(old(self), final(self)),
432            !accepted ==> Self::abstract_failure_step(old(self), final(self)),
433            accepted == (old(self).budget.used() + 1 <= old(self).budget.capacity as int),
434            accepted ==> final(self).phase == CommitPhase::Admitted,
435            !accepted ==> final(self).phase == CommitPhase::Rejected,
436            final(self).registry == old(self).registry,
437            final(self).budget.capacity == old(self).budget.capacity,
438            final(self).budget.allocated == old(self).budget.allocated,
439            final(self).budget.pending_eviction == old(self).budget.pending_eviction,
440            final(self).budget.reserved == if accepted {
441                (old(self).budget.reserved + 1) as u64
442            } else {
443                old(self).budget.reserved
444            },
445            final(self).propagation == old(self).propagation,
446            final(self).actuation == old(self).actuation,
447            final(self).audit == old(self).audit,
448            final(self).attempt_budget == old(self).attempt_budget,
449            accepted ==> {
450                &&& final(self).sequential.steps == old(self).sequential.steps
451                &&& final(self).sequential.value_domain_size
452                    == old(self).sequential.value_domain_size
453                &&& final(self).sequential.pc == old(self).sequential.pc + 1
454                &&& !final(self).sequential.active
455                &&& final(self).sequential.value == 1
456                &&& final(self).sequential.history@
457                    == old(self).sequential.history@.push(1)
458            },
459            !accepted ==> final(self).sequential == old(self).sequential,
460            final(self).effect_applied == old(self).effect_applied,
461            final(self).evidence_persisted == old(self).evidence_persisted,
462            final(self).recovery_intent == old(self).recovery_intent,
463            final(self).crashed == old(self).crashed,
464    {
465        let accepted = self.budget.reserve(1);
466        if accepted {
467            Self::advance(&mut self.sequential, 1);
468            self.phase = CommitPhase::Admitted;
469        } else {
470            self.phase = CommitPhase::Rejected;
471        }
472        accepted
473    }
474
475    /// Run the one-node propagation witness and advance the Sequential carrier.
476    /// This is the bounded readiness stage between admission and effect commit.
477    pub fn propagate(&mut self)
478        requires
479            old(self).inv(),
480            !old(self).crashed,
481            old(self).phase == CommitPhase::Admitted,
482            old(self).sequential.pc == 1,
483            old(self).propagation.round == Round::Idle,
484            old(self).propagation.changed,
485            old(self).propagation.iteration == 0,
486        ensures
487            final(self).inv(),
488            final(self).bridge_contract(),
489            Self::abstract_system_step(old(self), final(self)),
490            final(self).phase == CommitPhase::Ready,
491            final(self).sequential.pc == 2,
492            final(self).propagation.iteration == 1,
493            final(self).propagation.round == Round::Idle,
494            !final(self).propagation.changed,
495            final(self).registry == old(self).registry,
496            final(self).budget == old(self).budget,
497            final(self).attempt_budget == old(self).attempt_budget,
498            final(self).actuation == old(self).actuation,
499            final(self).audit == old(self).audit,
500            final(self).propagation.num_nodes == old(self).propagation.num_nodes,
501            final(self).propagation.max_iterations
502                == old(self).propagation.max_iterations,
503            final(self).propagation.max_value == old(self).propagation.max_value,
504            final(self).propagation.edges@ == old(self).propagation.edges@,
505            final(self).propagation.values@ == old(self).propagation.values@,
506            final(self).propagation.snapshot@ == old(self).propagation.values@,
507            forall|index: int| 0 <= index < final(self).propagation.updated@.len() ==>
508                #[trigger] final(self).propagation.updated@[index],
509            final(self).sequential.steps == old(self).sequential.steps,
510            final(self).sequential.value_domain_size
511                == old(self).sequential.value_domain_size,
512            final(self).sequential.value == 2,
513            !final(self).sequential.active,
514            final(self).sequential.history@ == old(self).sequential.history@.push(2),
515            final(self).effect_applied == old(self).effect_applied,
516            final(self).evidence_persisted == old(self).evidence_persisted,
517            final(self).recovery_intent == old(self).recovery_intent,
518            final(self).crashed == old(self).crashed,
519    {
520        self.propagation.start_round();
521        self.propagation.update_node(0);
522        assert(self.propagation.all_updated());
523        assert(self.propagation.values@ == self.propagation.snapshot@);
524        self.propagation.end_round();
525        Self::advance(&mut self.sequential, 2);
526        self.phase = CommitPhase::Ready;
527    }
528
529    /// Record a failed external-service attempt before any effect occurred.
530    /// Calling this action again from `Retryable` is the explicit bounded retry
531    /// path; the last permitted failure is a terminal rejection.
532    pub fn fail_before_effect(&mut self) -> (terminal: bool)
533        requires
534            old(self).inv(),
535            !old(self).crashed,
536            old(self).phase == CommitPhase::Ready
537                || old(self).phase == CommitPhase::Retryable,
538            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
539            old(self).sequential.pc == 2,
540            !old(self).effect_applied,
541            !old(self).evidence_persisted,
542        ensures
543            final(self).inv(),
544            final(self).bridge_contract(),
545            Self::abstract_failure_step(old(self), final(self)),
546            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
547            final(self).registry == old(self).registry,
548            final(self).budget == old(self).budget,
549            final(self).propagation == old(self).propagation,
550            final(self).actuation == old(self).actuation,
551            final(self).audit == old(self).audit,
552            final(self).sequential == old(self).sequential,
553            final(self).attempt_budget.capacity == old(self).attempt_budget.capacity,
554            final(self).attempt_budget.reserved == old(self).attempt_budget.reserved,
555            final(self).attempt_budget.pending_eviction
556                == old(self).attempt_budget.pending_eviction,
557            final(self).effect_applied == old(self).effect_applied,
558            final(self).evidence_persisted == old(self).evidence_persisted,
559            final(self).recovery_intent == old(self).recovery_intent,
560            final(self).crashed == old(self).crashed,
561            final(self).attempt_budget.allocated < final(self).attempt_budget.capacity ==>
562                !terminal && final(self).phase == CommitPhase::Retryable,
563            final(self).attempt_budget.allocated == final(self).attempt_budget.capacity ==>
564                terminal && final(self).phase == CommitPhase::Rejected,
565    {
566        let recorded = self.attempt_budget.try_allocate(1);
567        let _ = recorded;
568        assert(recorded);
569        if self.attempt_budget.allocated == self.attempt_budget.capacity {
570            self.phase = CommitPhase::Rejected;
571            true
572        } else {
573            self.phase = CommitPhase::Retryable;
574            false
575        }
576    }
577
578    /// Record the external effect together with a durable recovery intent, then
579    /// expose the modeled failure before the audit evidence commit. The effect must not
580    /// be retried; only `recover` may complete this state.
581    pub fn fail_after_effect(&mut self)
582        requires
583            old(self).inv(),
584            !old(self).crashed,
585            old(self).phase == CommitPhase::Ready
586                || old(self).phase == CommitPhase::Retryable,
587            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
588            old(self).sequential.pc == 2,
589            !old(self).effect_applied,
590            !old(self).evidence_persisted,
591            old(self).audit.log@.len() == 0,
592            old(self).actuation.effects@[0] is None,
593        ensures
594            final(self).inv(),
595            final(self).bridge_contract(),
596            Self::abstract_failure_step(old(self), final(self)),
597            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
598            final(self).phase == CommitPhase::RecoveryPending,
599            final(self).effect_applied,
600            !final(self).evidence_persisted,
601            final(self).recovery_intent,
602            final(self).registry == old(self).registry,
603            final(self).budget == old(self).budget,
604            final(self).propagation == old(self).propagation,
605            final(self).audit == old(self).audit,
606            final(self).sequential == old(self).sequential,
607            final(self).attempt_budget.capacity == old(self).attempt_budget.capacity,
608            final(self).attempt_budget.reserved == old(self).attempt_budget.reserved,
609            final(self).attempt_budget.pending_eviction
610                == old(self).attempt_budget.pending_eviction,
611            final(self).actuation.num_seats == old(self).actuation.num_seats,
612            final(self).actuation.allocation@ == old(self).actuation.allocation@,
613            final(self).actuation.effects@
614                == old(self).actuation.effects@.update(
615                    0,
616                    old(self).actuation.allocation@[0],
617                ),
618            final(self).actuation.complete == old(self).actuation.complete,
619            final(self).crashed == old(self).crashed,
620    {
621        let recorded = self.attempt_budget.try_allocate(1);
622        let _ = recorded;
623        assert(recorded);
624        // The durable intent precedes the effect receipt at this API boundary.
625        self.recovery_intent = true;
626        self.actuation.actuate(0);
627        self.effect_applied = true;
628        self.phase = CommitPhase::RecoveryPending;
629    }
630
631    /// Atomic success boundary for the bounded persistence adapter: effect
632    /// receipt, unit-budget commit, audit append, and sequential closure become
633    /// visible together at method return.
634    pub fn commit_success(&mut self)
635        requires
636            old(self).inv(),
637            !old(self).crashed,
638            old(self).phase == CommitPhase::Ready
639                || old(self).phase == CommitPhase::Retryable,
640            old(self).attempt_budget.allocated < old(self).attempt_budget.capacity,
641            old(self).sequential.pc == 2,
642            !old(self).effect_applied,
643            !old(self).evidence_persisted,
644            old(self).audit.log@.len() == 0,
645            old(self).actuation.effects@[0] is None,
646        ensures
647            final(self).inv(),
648            final(self).bridge_contract(),
649            Self::abstract_commit_step(old(self), final(self)),
650            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
651            final(self).phase == CommitPhase::Committed,
652            final(self).effect_applied,
653            final(self).evidence_persisted,
654            !final(self).recovery_intent,
655            final(self).sequential.pc == 3,
656            final(self).registry == old(self).registry,
657            final(self).propagation == old(self).propagation,
658            final(self).attempt_budget.capacity == old(self).attempt_budget.capacity,
659            final(self).attempt_budget.allocated == old(self).attempt_budget.allocated + 1,
660            final(self).attempt_budget.reserved == old(self).attempt_budget.reserved,
661            final(self).attempt_budget.pending_eviction
662                == old(self).attempt_budget.pending_eviction,
663            final(self).budget.capacity == old(self).budget.capacity,
664            final(self).budget.allocated == old(self).budget.allocated + 1,
665            final(self).budget.reserved == old(self).budget.reserved - 1,
666            final(self).budget.pending_eviction == old(self).budget.pending_eviction,
667            final(self).actuation.num_seats == old(self).actuation.num_seats,
668            final(self).actuation.allocation@ == old(self).actuation.allocation@,
669            final(self).actuation.effects@
670                == old(self).actuation.effects@.update(
671                    0,
672                    old(self).actuation.allocation@[0],
673                ),
674            final(self).actuation.complete == old(self).actuation.complete,
675            final(self).audit.operator == old(self).audit.operator,
676            final(self).audit.max_log_len == old(self).audit.max_log_len,
677            final(self).audit.log@.len() == old(self).audit.log@.len() + 1,
678            final(self).audit.last_hash
679                == old(self).audit.operator.combine_spec(old(self).audit.last_hash, 0),
680            final(self).audit.log@[old(self).audit.log@.len() as int].operation == 0,
681            final(self).audit.log@[old(self).audit.log@.len() as int].prev_hash
682                == old(self).audit.last_hash,
683            forall|index: int| 0 <= index < old(self).audit.log@.len() ==>
684                #[trigger] final(self).audit.log@[index] == old(self).audit.log@[index],
685            final(self).sequential.steps == old(self).sequential.steps,
686            final(self).sequential.value_domain_size
687                == old(self).sequential.value_domain_size,
688            final(self).sequential.value == 3,
689            !final(self).sequential.active,
690            final(self).sequential.history@ == old(self).sequential.history@.push(3),
691            final(self).crashed == old(self).crashed,
692    {
693        let recorded = self.attempt_budget.try_allocate(1);
694        let _ = recorded;
695        assert(recorded);
696        self.actuation.actuate(0);
697        self.effect_applied = true;
698        self.budget.commit_reservation(1);
699        let recorded = self.audit.record(0);
700        let _ = recorded;
701        assert(recorded);
702        self.evidence_persisted = true;
703        self.recovery_intent = false;
704        Self::advance(&mut self.sequential, 3);
705        self.phase = CommitPhase::Committed;
706    }
707
708    /// Finish a partial failure without reissuing the already applied effect.
709    pub fn recover(&mut self)
710        requires
711            old(self).inv(),
712            !old(self).crashed,
713            old(self).phase == CommitPhase::RecoveryPending,
714            old(self).sequential.pc == 2,
715            old(self).audit.log@.len() == 0,
716        ensures
717            final(self).inv(),
718            final(self).bridge_contract(),
719            Self::abstract_commit_step(old(self), final(self)),
720            final(self).phase == CommitPhase::Committed,
721            final(self).effect_applied,
722            final(self).evidence_persisted,
723            !final(self).recovery_intent,
724            final(self).sequential.pc == 3,
725            final(self).registry == old(self).registry,
726            final(self).propagation == old(self).propagation,
727            final(self).attempt_budget == old(self).attempt_budget,
728            final(self).budget.capacity == old(self).budget.capacity,
729            final(self).budget.allocated == old(self).budget.allocated + 1,
730            final(self).budget.reserved == old(self).budget.reserved - 1,
731            final(self).budget.pending_eviction == old(self).budget.pending_eviction,
732            final(self).actuation == old(self).actuation,
733            final(self).audit.operator == old(self).audit.operator,
734            final(self).audit.max_log_len == old(self).audit.max_log_len,
735            final(self).audit.log@.len() == old(self).audit.log@.len() + 1,
736            final(self).audit.last_hash
737                == old(self).audit.operator.combine_spec(old(self).audit.last_hash, 0),
738            final(self).audit.log@[old(self).audit.log@.len() as int].operation == 0,
739            final(self).audit.log@[old(self).audit.log@.len() as int].prev_hash
740                == old(self).audit.last_hash,
741            forall|index: int| 0 <= index < old(self).audit.log@.len() ==>
742                #[trigger] final(self).audit.log@[index] == old(self).audit.log@[index],
743            final(self).sequential.steps == old(self).sequential.steps,
744            final(self).sequential.value_domain_size
745                == old(self).sequential.value_domain_size,
746            final(self).sequential.value == 3,
747            !final(self).sequential.active,
748            final(self).sequential.history@ == old(self).sequential.history@.push(3),
749            final(self).crashed == old(self).crashed,
750    {
751        self.budget.commit_reservation(1);
752        let recorded = self.audit.record(0);
753        let _ = recorded;
754        assert(recorded);
755        self.evidence_persisted = true;
756        self.recovery_intent = false;
757        Self::advance(&mut self.sequential, 3);
758        self.phase = CommitPhase::Committed;
759    }
760
761    /// Crash only the volatile process boundary.  All fields named by the
762    /// persistence abstraction remain unchanged and therefore survive restart.
763    pub fn crash(&mut self)
764        requires old(self).inv(),
765        ensures
766            final(self).inv(),
767            final(self).bridge_contract(),
768            Self::abstract_failure_step(old(self), final(self)),
769            final(self).crashed,
770            final(self).phase == old(self).phase,
771            final(self).effect_applied == old(self).effect_applied,
772            final(self).evidence_persisted == old(self).evidence_persisted,
773            final(self).recovery_intent == old(self).recovery_intent,
774            final(self).registry == old(self).registry,
775            final(self).budget == old(self).budget,
776            final(self).propagation == old(self).propagation,
777            final(self).actuation == old(self).actuation,
778            final(self).audit == old(self).audit,
779            final(self).sequential == old(self).sequential,
780            final(self).attempt_budget == old(self).attempt_budget,
781    {
782        self.crashed = true;
783    }
784
785    /// Restart the volatile process state without changing durable owners.
786    pub fn restart(&mut self)
787        requires old(self).inv(), old(self).crashed,
788        ensures
789            final(self).inv(),
790            final(self).bridge_contract(),
791            Self::abstract_stutter_step(old(self), final(self)),
792            !final(self).crashed,
793            final(self).phase == old(self).phase,
794            final(self).effect_applied == old(self).effect_applied,
795            final(self).evidence_persisted == old(self).evidence_persisted,
796            final(self).recovery_intent == old(self).recovery_intent,
797            final(self).registry == old(self).registry,
798            final(self).budget == old(self).budget,
799            final(self).propagation == old(self).propagation,
800            final(self).actuation == old(self).actuation,
801            final(self).audit == old(self).audit,
802            final(self).sequential == old(self).sequential,
803            final(self).attempt_budget == old(self).attempt_budget,
804    {
805        self.crashed = false;
806    }
807}
808
809}
automation_structures/integration/governed_commit.rs

automation_structures/integration/
governed_commit.rs
