1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
//! Obligation analysis: static leak checking, graded types, marking, and contracts.
//!
//! This module provides four complementary approaches to obligation safety:
//!
//! 1. **Static leak checking** (`leak_check`): Abstract interpretation over
//! a structured IR to detect code paths where obligations may leak.
//!
//! 2. **Graded types** ([`graded`]): A type-level encoding where obligations
//! carry resource annotations, making leaks into compile warnings or
//! runtime panics via `#[must_use]` and `Drop`.
//!
//! 3. **VASS marking analysis** ([`marking`]): Projects trace events into a
//! vector-addition system for coverability-style analyses on bounded models.
//!
//! 4. **Dialectica contracts** ([`dialectica`]): Formalizes the two-phase
//! effects as Dialectica morphisms (forward value + backward obligation)
//! and encodes five contracts that the obligation system must satisfy.
//!
//! 5. **Lyapunov governor** ([`lyapunov`]): A potential-function-based
//! scheduling governor that drives cancellation drain toward quiescence.
//!
//! 6. **Guarded recursion lens** ([`guarded`]): Maps the "later" modality
//! (▸A) onto actors, leases, regions, and budgets — formalizing how
//! time-indexed invariants are preserved across unfolding steps.
//!
//! # Static Leak Checker
//!
//! The checker operates on a simple structured IR ([`Body`]) rather than Rust
//! source code directly. This allows testing the analysis logic independently
//! from the Rust parser/type system.
//!
//! ```
//! use asupersync::obligation::{Body, Instruction, LeakChecker, ObligationVar};
//! use asupersync::record::ObligationKind;
//!
//! let body = Body::new("send_message", vec![
//! Instruction::Reserve { var: ObligationVar(0), kind: ObligationKind::SendPermit },
//! // Oops: no commit or abort before scope exit
//! ]);
//!
//! let mut checker = LeakChecker::new();
//! let result = checker.check(&body);
//! assert!(!result.is_clean());
//! assert_eq!(result.leaks().len(), 1);
//! ```
//!
//! # Graded Types
//!
//! The graded surface makes obligation leaks a type-level concern:
//!
//! ```
//! use asupersync::obligation::graded::{GradedObligation, Resolution};
//! use asupersync::record::ObligationKind;
//!
//! let ob = GradedObligation::reserve(ObligationKind::SendPermit, "test");
//! ob.resolve(Resolution::Commit); // Must resolve before scope exit
//! ```
pub use ;