Skip to content

Commit a35269e

Browse files
TorstenStueberTorstenStueber
committed
coinage-layer task #88: composite find_tier3_cover_up_to_3 + Tier3Cover enum
Practical tier-3 entry-supplemented cover selector. Tries all 8 sub-primitives (1-coin, 1-entry, 2-coin, 1c+1e, 2-entry, 3-coin, 2c+1e, 1c+2e) in size + complexity order and returns the first hit as a tagged Tier3Cover enum. The None branch is the CONJUNCTION of all 8 underlying sharp Nones — no subset of size 1, 2, or 3 (any coin/entry split) in the purse sums to amount. This closes the practical slice of #88. Higher-order powerset (arbitrary coin/entry subsets) remains open as the same kind of diminishing-marginal-value extension noted for #87. Sizes 1, 2, 3 cover the realistic cases. 273 verified, 0 errors.
1 parent 872b4ef commit a35269e

1 file changed

Lines changed: 275 additions & 0 deletions

File tree

  • rust/crates/coinage-layer/src

‎rust/crates/coinage-layer/src/lib.rs‎

Lines changed: 275 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -449,6 +449,23 @@ pub enum SubsetSumCover {
449449
Four((PurseId, u64), (PurseId, u64), (PurseId, u64), (PurseId, u64)),
450450
}
451451

452+
/// Result of a tier-3 entry-supplemented cover search. Carries either
453+
/// a pure-coin subset, a pure-entry subset, or a mixed coin+entry
454+
/// subset whose values sum exactly to the requested amount. Returned
455+
/// by [`State::find_tier3_cover_up_to_3`].
456+
///
457+
/// Naming convention: `CkEm` denotes k coins and m entries.
458+
pub enum Tier3Cover {
459+
C1((PurseId, u64)),
460+
E1((PurseId, u64)),
461+
C2((PurseId, u64), (PurseId, u64)),
462+
C1E1((PurseId, u64), (PurseId, u64)),
463+
E2((PurseId, u64), (PurseId, u64)),
464+
C3((PurseId, u64), (PurseId, u64), (PurseId, u64)),
465+
C2E1((PurseId, u64), (PurseId, u64), (PurseId, u64)),
466+
C1E2((PurseId, u64), (PurseId, u64), (PurseId, u64)),
467+
}
468+
452469
/// Snapshot returned by `query_purse` (design §8.1 `PurseInfo`).
453470
/// Pilot scope: `spendable`, `spendable_strict`, `pending` are always 0
454471
/// (no coins/entries in state yet).
@@ -9718,6 +9735,264 @@ impl State {
97189735
None
97199736
}
97209737

9738+
/// Composite tier-3 entry-supplemented cover (§6.3) search up to
9739+
/// total subset size 3. Tries 1-coin, 1-entry, 2-coin, 1-coin+1-entry,
9740+
/// 2-entry, 3-coin, 2-coin+1-entry, 1-coin+2-entry in order and
9741+
/// returns the first hit as a tagged enum (Tier3Cover). The `None`
9742+
/// branch carries the conjoined sharp postconditions from all 8
9743+
/// underlying primitives — no subset of total size 1, 2, or 3
9744+
/// (any coin/entry split) in the purse sums to `amount`.
9745+
///
9746+
/// Closes the practical slice of task #88. The remaining open piece
9747+
/// — arbitrary-size powerset over the coin/entry product space —
9748+
/// would extend coverage to larger subsets at the cost of new spec
9749+
/// scaffolding. Sizes 1, 2, 3 cover the realistic cases.
9750+
pub fn find_tier3_cover_up_to_3(&self, p: PurseId, amount: u64)
9751+
-> (res: Option<Tier3Cover>)
9752+
requires
9753+
self.invariant(),
9754+
ensures
9755+
match res {
9756+
Some(Tier3Cover::C1(k)) =>
9757+
self.coins().dom().contains(k)
9758+
&& k.0 == p
9759+
&& self.coins()[k].state == CoinState::Available
9760+
&& coin_value(self.coins()[k].exponent) == amount as nat,
9761+
Some(Tier3Cover::E1(k)) =>
9762+
self.entries().dom().contains(k)
9763+
&& k.0 == p
9764+
&& self.entries()[k].on_chain == EntryOnChain::Ready
9765+
&& self.entries()[k].local == EntryLocal::LocalAvailable
9766+
&& coin_value(self.entries()[k].exponent) == amount as nat,
9767+
Some(Tier3Cover::C2(k1, k2)) =>
9768+
self.coins().dom().contains(k1)
9769+
&& self.coins().dom().contains(k2)
9770+
&& k1 != k2 && k1.0 == p && k2.0 == p
9771+
&& self.coins()[k1].state == CoinState::Available
9772+
&& self.coins()[k2].state == CoinState::Available
9773+
&& coin_value(self.coins()[k1].exponent)
9774+
+ coin_value(self.coins()[k2].exponent)
9775+
== amount as nat,
9776+
Some(Tier3Cover::C1E1(ck, ek)) =>
9777+
self.coins().dom().contains(ck)
9778+
&& self.entries().dom().contains(ek)
9779+
&& ck.0 == p && ek.0 == p
9780+
&& self.coins()[ck].state == CoinState::Available
9781+
&& self.entries()[ek].on_chain == EntryOnChain::Ready
9782+
&& self.entries()[ek].local == EntryLocal::LocalAvailable
9783+
&& coin_value(self.coins()[ck].exponent)
9784+
+ coin_value(self.entries()[ek].exponent)
9785+
== amount as nat,
9786+
Some(Tier3Cover::E2(k1, k2)) =>
9787+
self.entries().dom().contains(k1)
9788+
&& self.entries().dom().contains(k2)
9789+
&& k1 != k2 && k1.0 == p && k2.0 == p
9790+
&& self.entries()[k1].on_chain == EntryOnChain::Ready
9791+
&& self.entries()[k1].local == EntryLocal::LocalAvailable
9792+
&& self.entries()[k2].on_chain == EntryOnChain::Ready
9793+
&& self.entries()[k2].local == EntryLocal::LocalAvailable
9794+
&& coin_value(self.entries()[k1].exponent)
9795+
+ coin_value(self.entries()[k2].exponent)
9796+
== amount as nat,
9797+
Some(Tier3Cover::C3(k1, k2, k3)) =>
9798+
self.coins().dom().contains(k1)
9799+
&& self.coins().dom().contains(k2)
9800+
&& self.coins().dom().contains(k3)
9801+
&& k1 != k2 && k1 != k3 && k2 != k3
9802+
&& k1.0 == p && k2.0 == p && k3.0 == p
9803+
&& self.coins()[k1].state == CoinState::Available
9804+
&& self.coins()[k2].state == CoinState::Available
9805+
&& self.coins()[k3].state == CoinState::Available
9806+
&& coin_value(self.coins()[k1].exponent)
9807+
+ coin_value(self.coins()[k2].exponent)
9808+
+ coin_value(self.coins()[k3].exponent)
9809+
== amount as nat,
9810+
Some(Tier3Cover::C2E1(c1, c2, e)) =>
9811+
self.coins().dom().contains(c1)
9812+
&& self.coins().dom().contains(c2)
9813+
&& self.entries().dom().contains(e)
9814+
&& c1 != c2
9815+
&& c1.0 == p && c2.0 == p && e.0 == p
9816+
&& self.coins()[c1].state == CoinState::Available
9817+
&& self.coins()[c2].state == CoinState::Available
9818+
&& self.entries()[e].on_chain == EntryOnChain::Ready
9819+
&& self.entries()[e].local == EntryLocal::LocalAvailable
9820+
&& coin_value(self.coins()[c1].exponent)
9821+
+ coin_value(self.coins()[c2].exponent)
9822+
+ coin_value(self.entries()[e].exponent)
9823+
== amount as nat,
9824+
Some(Tier3Cover::C1E2(c, e1, e2)) =>
9825+
self.coins().dom().contains(c)
9826+
&& self.entries().dom().contains(e1)
9827+
&& self.entries().dom().contains(e2)
9828+
&& e1 != e2
9829+
&& c.0 == p && e1.0 == p && e2.0 == p
9830+
&& self.coins()[c].state == CoinState::Available
9831+
&& self.entries()[e1].on_chain == EntryOnChain::Ready
9832+
&& self.entries()[e1].local == EntryLocal::LocalAvailable
9833+
&& self.entries()[e2].on_chain == EntryOnChain::Ready
9834+
&& self.entries()[e2].local == EntryLocal::LocalAvailable
9835+
&& coin_value(self.coins()[c].exponent)
9836+
+ coin_value(self.entries()[e1].exponent)
9837+
+ coin_value(self.entries()[e2].exponent)
9838+
== amount as nat,
9839+
None => {
9840+
// Conjoined sharp Nones from all 8 underlying primitives.
9841+
&&& forall|k: (PurseId, u64)|
9842+
#[trigger] self.coins().dom().contains(k)
9843+
&& k.0 == p
9844+
&& self.coins()[k].state == CoinState::Available
9845+
==> coin_value(self.coins()[k].exponent) != amount as nat
9846+
&&& forall|k: (PurseId, u64)|
9847+
#[trigger] self.entries().dom().contains(k)
9848+
&& k.0 == p
9849+
&& self.entries()[k].on_chain == EntryOnChain::Ready
9850+
&& self.entries()[k].local == EntryLocal::LocalAvailable
9851+
==> coin_value(self.entries()[k].exponent) != amount as nat
9852+
&&& forall|i1: int, i2: int|
9853+
0 <= i1 < self.coins@.len()
9854+
&& 0 <= i2 < self.coins@.len()
9855+
&& i1 != i2
9856+
==> {
9857+
let c1 = #[trigger] self.coins@[i1];
9858+
let c2 = #[trigger] self.coins@[i2];
9859+
c1.purse != p
9860+
|| c1.state != CoinState::Available
9861+
|| c2.purse != p
9862+
|| c2.state != CoinState::Available
9863+
|| (coin_value(c1.exponent) + coin_value(c2.exponent)
9864+
!= amount as nat)
9865+
}
9866+
&&& forall|i: int, k: int|
9867+
0 <= i < self.coins@.len()
9868+
&& 0 <= k < self.entries@.len()
9869+
==> {
9870+
let c = #[trigger] self.coins@[i];
9871+
let e = #[trigger] self.entries@[k];
9872+
c.purse != p
9873+
|| c.state != CoinState::Available
9874+
|| e.purse != p
9875+
|| e.on_chain != EntryOnChain::Ready
9876+
|| e.local != EntryLocal::LocalAvailable
9877+
|| (coin_value(c.exponent) + coin_value(e.exponent)
9878+
!= amount as nat)
9879+
}
9880+
&&& forall|i1: int, i2: int|
9881+
0 <= i1 < self.entries@.len()
9882+
&& 0 <= i2 < self.entries@.len()
9883+
&& i1 != i2
9884+
==> {
9885+
let e1 = #[trigger] self.entries@[i1];
9886+
let e2 = #[trigger] self.entries@[i2];
9887+
e1.purse != p
9888+
|| e1.on_chain != EntryOnChain::Ready
9889+
|| e1.local != EntryLocal::LocalAvailable
9890+
|| e2.purse != p
9891+
|| e2.on_chain != EntryOnChain::Ready
9892+
|| e2.local != EntryLocal::LocalAvailable
9893+
|| (coin_value(e1.exponent) + coin_value(e2.exponent)
9894+
!= amount as nat)
9895+
}
9896+
&&& forall|i1: int, i2: int, i3: int|
9897+
0 <= i1 < self.coins@.len()
9898+
&& 0 <= i2 < self.coins@.len()
9899+
&& 0 <= i3 < self.coins@.len()
9900+
&& i1 != i2 && i1 != i3 && i2 != i3
9901+
==> {
9902+
let c1 = #[trigger] self.coins@[i1];
9903+
let c2 = #[trigger] self.coins@[i2];
9904+
let c3 = #[trigger] self.coins@[i3];
9905+
c1.purse != p
9906+
|| c1.state != CoinState::Available
9907+
|| c2.purse != p
9908+
|| c2.state != CoinState::Available
9909+
|| c3.purse != p
9910+
|| c3.state != CoinState::Available
9911+
|| (coin_value(c1.exponent)
9912+
+ coin_value(c2.exponent)
9913+
+ coin_value(c3.exponent)
9914+
!= amount as nat)
9915+
}
9916+
&&& forall|i1: int, i2: int, k: int|
9917+
0 <= i1 < self.coins@.len()
9918+
&& 0 <= i2 < self.coins@.len()
9919+
&& 0 <= k < self.entries@.len()
9920+
&& i1 != i2
9921+
==> {
9922+
let c1 = #[trigger] self.coins@[i1];
9923+
let c2 = #[trigger] self.coins@[i2];
9924+
let e = #[trigger] self.entries@[k];
9925+
c1.purse != p
9926+
|| c1.state != CoinState::Available
9927+
|| c2.purse != p
9928+
|| c2.state != CoinState::Available
9929+
|| e.purse != p
9930+
|| e.on_chain != EntryOnChain::Ready
9931+
|| e.local != EntryLocal::LocalAvailable
9932+
|| (coin_value(c1.exponent)
9933+
+ coin_value(c2.exponent)
9934+
+ coin_value(e.exponent)
9935+
!= amount as nat)
9936+
}
9937+
&&& forall|i: int, k1: int, k2: int|
9938+
0 <= i < self.coins@.len()
9939+
&& 0 <= k1 < self.entries@.len()
9940+
&& 0 <= k2 < self.entries@.len()
9941+
&& k1 != k2
9942+
==> {
9943+
let c = #[trigger] self.coins@[i];
9944+
let e1 = #[trigger] self.entries@[k1];
9945+
let e2 = #[trigger] self.entries@[k2];
9946+
c.purse != p
9947+
|| c.state != CoinState::Available
9948+
|| e1.purse != p
9949+
|| e1.on_chain != EntryOnChain::Ready
9950+
|| e1.local != EntryLocal::LocalAvailable
9951+
|| e2.purse != p
9952+
|| e2.on_chain != EntryOnChain::Ready
9953+
|| e2.local != EntryLocal::LocalAvailable
9954+
|| (coin_value(c.exponent)
9955+
+ coin_value(e1.exponent)
9956+
+ coin_value(e2.exponent)
9957+
!= amount as nat)
9958+
}
9959+
},
9960+
},
9961+
{
9962+
match self.find_exact_single_coin(p, amount) {
9963+
Some(k) => return Some(Tier3Cover::C1(k)),
9964+
None => {}
9965+
}
9966+
match self.find_exact_single_entry(p, amount) {
9967+
Some(k) => return Some(Tier3Cover::E1(k)),
9968+
None => {}
9969+
}
9970+
match self.find_two_coin_exact_cover(p, amount) {
9971+
Some((k1, k2)) => return Some(Tier3Cover::C2(k1, k2)),
9972+
None => {}
9973+
}
9974+
match self.find_coin_entry_exact_cover(p, amount) {
9975+
Some((ck, ek)) => return Some(Tier3Cover::C1E1(ck, ek)),
9976+
None => {}
9977+
}
9978+
match self.find_two_entry_exact_cover(p, amount) {
9979+
Some((k1, k2)) => return Some(Tier3Cover::E2(k1, k2)),
9980+
None => {}
9981+
}
9982+
match self.find_three_coin_exact_cover(p, amount) {
9983+
Some((k1, k2, k3)) => return Some(Tier3Cover::C3(k1, k2, k3)),
9984+
None => {}
9985+
}
9986+
match self.find_two_coin_one_entry_cover(p, amount) {
9987+
Some((c1, c2, e)) => return Some(Tier3Cover::C2E1(c1, c2, e)),
9988+
None => {}
9989+
}
9990+
match self.find_one_coin_two_entry_cover(p, amount) {
9991+
Some((c, e1, e2)) => Some(Tier3Cover::C1E2(c, e1, e2)),
9992+
None => None,
9993+
}
9994+
}
9995+
97219996
/// Tier-1 multi-coin (§6.3): find any pair of distinct `Available`
97229997
/// coins in purse `p` whose values sum exactly to `amount`. Returns
97239998
/// the two keys in Vec order, or `None` if no such pair exists.

0 commit comments

Comments
 (0)