Skip to content

Commit 997934c

Browse files
TorstenStueberTorstenStueber
committed
coinage-layer task #87: composite find_subset_sum_up_to_4 + SubsetSumCover
Practical multi-coin selector. Tries 1-, 2-, 3-, 4-coin exact covers in order and returns the first hit as a tagged enum (SubsetSumCover). The None branch carries the CONJOINED sharp postconditions from all four primitives — for any subset of size <=4 in the purse, no such subset sums to amount. The Vec-of-coins API rejected in favor of a tagged enum keeps the size-specific postcondition shape clean per variant. This closes the practically-relevant slice of #87. The remaining open piece — N-coin subset-sum for arbitrary N via bitmask enumeration — would extend coverage to larger subsets at the cost of new spec scaffolding (sum_by_mask, witness extraction). Size 1-4 covers essentially every realistic transfer in a real wallet. 259 verified, 0 errors.
1 parent 08d76a9 commit 997934c

1 file changed

Lines changed: 160 additions & 0 deletions

File tree

  • rust/crates/coinage-layer/src

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

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -438,6 +438,17 @@ pub enum CoinSelection {
438438
Split { coin: (PurseId, u64) },
439439
}
440440

441+
/// Result of a bounded subset-sum search over `Available` coins:
442+
/// either a single coin, a pair, a triple, or a quadruple of distinct
443+
/// coin keys whose values sum exactly to the requested amount. Returned
444+
/// by [`State::find_subset_sum_up_to_4`].
445+
pub enum SubsetSumCover {
446+
One((PurseId, u64)),
447+
Two((PurseId, u64), (PurseId, u64)),
448+
Three((PurseId, u64), (PurseId, u64), (PurseId, u64)),
449+
Four((PurseId, u64), (PurseId, u64), (PurseId, u64), (PurseId, u64)),
450+
}
451+
441452
/// Snapshot returned by `query_purse` (design §8.1 `PurseInfo`).
442453
/// Pilot scope: `spendable`, `spendable_strict`, `pending` are always 0
443454
/// (no coins/entries in state yet).
@@ -9674,6 +9685,155 @@ impl State {
96749685
None
96759686
}
96769687

9688+
/// Composite multi-coin subset-sum search: tries 1-, 2-, 3-, 4-coin
9689+
/// exact covers in order and returns the first hit. The `None`
9690+
/// branch carries the *conjoined* sharp postconditions from all
9691+
/// four primitives — i.e. no subset of size 1, 2, 3, or 4 in the
9692+
/// purse sums to `amount`.
9693+
///
9694+
/// Practical multi-coin selector for task #87. Full N-coin powerset
9695+
/// (any size) remains open; this covers the realistic small-K case
9696+
/// that almost all transfers actually hit.
9697+
pub fn find_subset_sum_up_to_4(&self, p: PurseId, amount: u64)
9698+
-> (res: Option<SubsetSumCover>)
9699+
requires
9700+
self.invariant(),
9701+
ensures
9702+
match res {
9703+
Some(SubsetSumCover::One(k1)) =>
9704+
self.coins().dom().contains(k1)
9705+
&& k1.0 == p
9706+
&& self.coins()[k1].state == CoinState::Available
9707+
&& coin_value(self.coins()[k1].exponent) == amount as nat,
9708+
Some(SubsetSumCover::Two(k1, k2)) =>
9709+
self.coins().dom().contains(k1)
9710+
&& self.coins().dom().contains(k2)
9711+
&& k1 != k2
9712+
&& k1.0 == p && k2.0 == p
9713+
&& self.coins()[k1].state == CoinState::Available
9714+
&& self.coins()[k2].state == CoinState::Available
9715+
&& coin_value(self.coins()[k1].exponent)
9716+
+ coin_value(self.coins()[k2].exponent)
9717+
== amount as nat,
9718+
Some(SubsetSumCover::Three(k1, k2, k3)) =>
9719+
self.coins().dom().contains(k1)
9720+
&& self.coins().dom().contains(k2)
9721+
&& self.coins().dom().contains(k3)
9722+
&& k1 != k2 && k1 != k3 && k2 != k3
9723+
&& k1.0 == p && k2.0 == p && k3.0 == p
9724+
&& self.coins()[k1].state == CoinState::Available
9725+
&& self.coins()[k2].state == CoinState::Available
9726+
&& self.coins()[k3].state == CoinState::Available
9727+
&& coin_value(self.coins()[k1].exponent)
9728+
+ coin_value(self.coins()[k2].exponent)
9729+
+ coin_value(self.coins()[k3].exponent)
9730+
== amount as nat,
9731+
Some(SubsetSumCover::Four(k1, k2, k3, k4)) =>
9732+
self.coins().dom().contains(k1)
9733+
&& self.coins().dom().contains(k2)
9734+
&& self.coins().dom().contains(k3)
9735+
&& self.coins().dom().contains(k4)
9736+
&& k1 != k2 && k1 != k3 && k1 != k4
9737+
&& k2 != k3 && k2 != k4 && k3 != k4
9738+
&& k1.0 == p && k2.0 == p && k3.0 == p && k4.0 == p
9739+
&& self.coins()[k1].state == CoinState::Available
9740+
&& self.coins()[k2].state == CoinState::Available
9741+
&& self.coins()[k3].state == CoinState::Available
9742+
&& self.coins()[k4].state == CoinState::Available
9743+
&& coin_value(self.coins()[k1].exponent)
9744+
+ coin_value(self.coins()[k2].exponent)
9745+
+ coin_value(self.coins()[k3].exponent)
9746+
+ coin_value(self.coins()[k4].exponent)
9747+
== amount as nat,
9748+
None => {
9749+
// Conjoined sharp Nones from the four primitives.
9750+
&&& forall|k: (PurseId, u64)|
9751+
#[trigger] self.coins().dom().contains(k)
9752+
&& k.0 == p
9753+
&& self.coins()[k].state == CoinState::Available
9754+
==> coin_value(self.coins()[k].exponent) != amount as nat
9755+
&&& forall|i1: int, i2: int|
9756+
0 <= i1 < self.coins@.len()
9757+
&& 0 <= i2 < self.coins@.len()
9758+
&& i1 != i2
9759+
==> {
9760+
let c1 = #[trigger] self.coins@[i1];
9761+
let c2 = #[trigger] self.coins@[i2];
9762+
c1.purse != p
9763+
|| c1.state != CoinState::Available
9764+
|| c2.purse != p
9765+
|| c2.state != CoinState::Available
9766+
|| (coin_value(c1.exponent) + coin_value(c2.exponent)
9767+
!= amount as nat)
9768+
}
9769+
&&& forall|i1: int, i2: int, i3: int|
9770+
0 <= i1 < self.coins@.len()
9771+
&& 0 <= i2 < self.coins@.len()
9772+
&& 0 <= i3 < self.coins@.len()
9773+
&& i1 != i2 && i1 != i3 && i2 != i3
9774+
==> {
9775+
let c1 = #[trigger] self.coins@[i1];
9776+
let c2 = #[trigger] self.coins@[i2];
9777+
let c3 = #[trigger] self.coins@[i3];
9778+
c1.purse != p
9779+
|| c1.state != CoinState::Available
9780+
|| c2.purse != p
9781+
|| c2.state != CoinState::Available
9782+
|| c3.purse != p
9783+
|| c3.state != CoinState::Available
9784+
|| (coin_value(c1.exponent)
9785+
+ coin_value(c2.exponent)
9786+
+ coin_value(c3.exponent)
9787+
!= amount as nat)
9788+
}
9789+
&&& forall|i1: int, i2: int, i3: int, i4: int|
9790+
0 <= i1 < self.coins@.len()
9791+
&& 0 <= i2 < self.coins@.len()
9792+
&& 0 <= i3 < self.coins@.len()
9793+
&& 0 <= i4 < self.coins@.len()
9794+
&& i1 != i2 && i1 != i3 && i1 != i4
9795+
&& i2 != i3 && i2 != i4 && i3 != i4
9796+
==> {
9797+
let c1 = #[trigger] self.coins@[i1];
9798+
let c2 = #[trigger] self.coins@[i2];
9799+
let c3 = #[trigger] self.coins@[i3];
9800+
let c4 = #[trigger] self.coins@[i4];
9801+
c1.purse != p
9802+
|| c1.state != CoinState::Available
9803+
|| c2.purse != p
9804+
|| c2.state != CoinState::Available
9805+
|| c3.purse != p
9806+
|| c3.state != CoinState::Available
9807+
|| c4.purse != p
9808+
|| c4.state != CoinState::Available
9809+
|| (coin_value(c1.exponent)
9810+
+ coin_value(c2.exponent)
9811+
+ coin_value(c3.exponent)
9812+
+ coin_value(c4.exponent)
9813+
!= amount as nat)
9814+
}
9815+
},
9816+
},
9817+
{
9818+
match self.find_exact_single_coin(p, amount) {
9819+
Some(k1) => return Some(SubsetSumCover::One(k1)),
9820+
None => {}
9821+
}
9822+
match self.find_two_coin_exact_cover(p, amount) {
9823+
Some((k1, k2)) => return Some(SubsetSumCover::Two(k1, k2)),
9824+
None => {}
9825+
}
9826+
match self.find_three_coin_exact_cover(p, amount) {
9827+
Some((k1, k2, k3)) => return Some(SubsetSumCover::Three(k1, k2, k3)),
9828+
None => {}
9829+
}
9830+
match self.find_four_coin_exact_cover(p, amount) {
9831+
Some((k1, k2, k3, k4)) =>
9832+
Some(SubsetSumCover::Four(k1, k2, k3, k4)),
9833+
None => None,
9834+
}
9835+
}
9836+
96779837
/// Tier-2 (split cover, §6.3): find any `Available` coin in purse `p`
96789838
/// whose `coin_value(exp)` strictly exceeds `amount`. Such a coin can
96799839
/// be split into two coins of strictly smaller exponent (one of which

0 commit comments

Comments
 (0)