From d8e715e25423ebaec148d8bbc65d1e8ce95c0a62 Mon Sep 17 00:00:00 2001 From: Alex Rasevych Date: Wed, 23 Sep 2026 03:28:04 -0400 Subject: [PATCH 1/9] Work In Progress - cards and hand are implemented but need evaluation --- dag/examples/blackjack/cards.dag | 51 +++++++++++++++++++++++++++++++- dag/examples/blackjack/hand.dag | 48 +++++++++++++++++++++++++++++- 2 files changed, 97 insertions(+), 2 deletions(-) diff --git a/dag/examples/blackjack/cards.dag b/dag/examples/blackjack/cards.dag index 6f9c6b4c80d..f17e2862dfa 100644 --- a/dag/examples/blackjack/cards.dag +++ b/dag/examples/blackjack/cards.dag @@ -5,4 +5,53 @@ module examples.blackjack.cards // section 4.1 (authority gunbc.plans.blackjack_onboarding) and is written by the contributor // working that brief. This anchor is the one declaration given, so the file parses on day one // and shows the shape of a closed set of alternatives. -type Suit = Clubs | Diamonds | Hearts | Spades + +type Suit + = Clubs + | Diamonds + | Hearts + | Spades + +type Rank + = Ace + | Two + | Three + | Four + | Five + | Six + | Seven + | Eight + | Nine + | Ten + | Jack + | Queen + | King + +type Card { + rank: Rank + suit: Suit + } + +fn rank_pips(r: Rank) -> Int { + match r { + Ace => 11 + Two => 2 + Three => 3 + Four => 4 + Five => 5 + Six => 6 + Seven => 7 + Eight => 8 + Nine => 9 + Ten => 10 + Jack => 10 + Queen => 10 + King => 10 + } +} + +fn is_ace(c: Card) -> Bool { + c.rank == Ace +} + +data standard_deck: List = [Ace, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten, Jack, Queen, King] |> flat_map(r => [Clubs, Diamonds, Hearts, Spades] |> map(s => Card { rank: r, suit: s})) \ No newline at end of file diff --git a/dag/examples/blackjack/hand.dag b/dag/examples/blackjack/hand.dag index bf7a000692f..f58fa7d4482 100644 --- a/dag/examples/blackjack/hand.dag +++ b/dag/examples/blackjack/hand.dag @@ -5,4 +5,50 @@ module examples.blackjack.hand // section 4.2 (authority gunbc.plans.blackjack_onboarding). The anchor is the derived value // a hand evaluates to; the raw total and the soft flag are distinct facts, which is the // first modeling lesson of that section. -type HandValue { total: Int, soft: Bool } + +import examples.blackjack.cards { Card, Rank, Ace, rank_pips, is_ace } + +type Hand { + cards: List + } + +type HandValue { + total: Int + soft: Bool + } + +fn soften(total: Int, aces: Int) -> Int { + if total > 21 && aces > 0 { + soften(total: total - 10,aces: aces - 1) + } else { + total + } +} + +fn hard_total(hand: Hand) -> Int { + fold(hand.cards, init: 0, f: (acc, c) => acc + rank_pips(r: c.rank)) +} + +fn hand_value(hand: Hand) -> HandValue { + let raw_total = hard_total(hand: hand) + let ace_count = length(hand.cards |> filter(c => is_ace(c: c))) + let total = soften(total: raw_total, aces: ace_count) + let all_aces_low_total = raw_total - ace_count * 10 + + HandValue { + total: total, + soft: ace_count > 0 && all_aces_low_total + 10 <= 21 + } +} + +fn is_bust(v: HandValue) -> Bool { + v.total > 21 +} + +fn is_blackjack(hand: Hand) -> Bool { + (length(hand.cards) == 2) && (hand_value(hand: hand).total == 21) +} + +fn add_card(hand: Hand, card: Card) -> Hand { + Hand { cards: concat(hand.cards, [card]) } +} \ No newline at end of file From 750d3f05f8ebadc24d321a301e5a60ce60519a1f Mon Sep 17 00:00:00 2001 From: Alex Rasevych Date: Fri, 25 Sep 2026 17:18:09 -0400 Subject: [PATCH 2/9] added test file for blackjack hand evaluation --- .../examples/blackjack_hand_witness_test.dag | 93 +++++++++++++++++++ 1 file changed, 93 insertions(+) create mode 100644 dag/test/claim/examples/blackjack_hand_witness_test.dag diff --git a/dag/test/claim/examples/blackjack_hand_witness_test.dag b/dag/test/claim/examples/blackjack_hand_witness_test.dag new file mode 100644 index 00000000000..84633750b08 --- /dev/null +++ b/dag/test/claim/examples/blackjack_hand_witness_test.dag @@ -0,0 +1,93 @@ +module test.claim.examples.blackjack_hand_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import examples.blackjack.cards { Card, Ace, Five, Nine, Ten, King, Queen, Clubs, Diamonds, Hearts, Spades } +import examples.blackjack.hand { Hand, hand_value, is_bust, is_blackjack } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn ace_nine() -> Hand { + Hand { + cards: [ + Card { rank: Ace, suit: Clubs }, + Card { rank: Nine, suit: Spades } + ] + } +} + +fn ace_ace_nine() -> Hand { + Hand { + cards: [ + Card { rank: Ace, suit: Clubs }, + Card { rank: Ace, suit: Diamonds }, + Card { rank: Nine, suit: Hearts } + ] + } +} + +fn ace_king() -> Hand { + Hand { + cards: [ + Card { rank: Ace, suit: Clubs }, + Card { rank: King, suit: Spades } + ] + } +} + +fn king_queen() -> Hand { + Hand { + cards: [ + Card { rank: King, suit: Clubs }, + Card { rank: Queen, suit: Spades } + ] + } +} + +fn king_nine_five() -> Hand { + Hand { + cards: [ + Card { rank: King, suit: Clubs }, + Card { rank: Nine, suit: Diamonds }, + Card { rank: Five, suit: Hearts } + ] + } +} + +fn ace_ace_ten() -> Hand { + Hand { + cards: [ + Card { rank: Ace, suit: Clubs }, + Card { rank: Ace, suit: Diamonds }, + Card { rank: Ten, suit: Hearts } + ] + } +} + +test fn ace_nine_is_soft_twenty() -> Bool { + let v = hand_value(hand: ace_nine()) + v.total == 20 && v.soft +} + +test fn ace_ace_nine_is_soft_twenty_one() -> Bool { + let v = hand_value(hand: ace_ace_nine()) + v.total == 21 && v.soft +} + +test fn ace_king_is_blackjack() -> Bool { + let v = hand_value(hand: ace_king()) + v.total == 21 && is_blackjack(hand: ace_king()) +} + +test fn king_queen_is_hard_twenty() -> Bool { + let v = hand_value(hand: king_queen()) + v.total == 20 && v.soft == false +} + +test fn king_nine_five_is_bust() -> Bool { + is_bust(v: hand_value(hand: king_nine_five())) +} + +test fn ace_ace_ten_is_hard_twelve() -> Bool { + let v = hand_value(hand: ace_ace_ten()) + v.total == 12 && v.soft == false +} \ No newline at end of file From 0b663fb6657bba901fe1dbb035d12b21dda03b91 Mon Sep 17 00:00:00 2001 From: Alex Rasevych Date: Sun, 27 Sep 2026 14:45:14 -0400 Subject: [PATCH 3/9] Milestone 3 complete - implemented round and test file --- dag/examples/blackjack/round.dag | 207 ++++++++++++++ .../examples/blackjack_round_witness_test.dag | 258 ++++++++++++++++++ 2 files changed, 465 insertions(+) create mode 100644 dag/test/claim/examples/blackjack_round_witness_test.dag diff --git a/dag/examples/blackjack/round.dag b/dag/examples/blackjack/round.dag index 936a45a0c54..ac1befe4757 100644 --- a/dag/examples/blackjack/round.dag +++ b/dag/examples/blackjack/round.dag @@ -6,4 +6,211 @@ module examples.blackjack.round // gunbc.plans.blackjack_onboarding). The variants are spelled PlayerHits / PlayerStands // rather than Hit / Stand because the corpus shares one name census and Hit is already a // variant of std.cache_interface; that section explains the naming rule. + +import examples.blackjack.cards { Card } +import examples.blackjack.hand { Hand, HandValue, hand_value, is_bust, is_blackjack, add_card } + type PlayerAction = PlayerHits | PlayerStands + +type BlackjackRules { dealer_hits_soft_17: Bool } + +type Shoe { cards: List } + +type RoundState + = PlayerTurn { player: Hand, dealer: Hand, shoe: Shoe } + | DealerTurn { player: Hand, dealer: Hand, shoe: Shoe } + | RoundComplete { player: Hand, dealer: Hand, outcome: RoundOutcome } + +type RoundOutcome = PlayerWon | DealerWon | Pushed + +type RoundRefusal + = ShoeExhausted + | ActionAfterRoundComplete + | DealerActedOutOfTurn + | PlayerActedOutOfTurn + +type RoundStep + = RoundStepped { state: RoundState } + | RoundRefused { cause: RoundRefusal } + +fn deal(shoe: Shoe) -> RoundStep { + match shoe.cards.first() { + Absent => RoundRefused { cause: ShoeExhausted } + Present { value: player_first } => match shoe.cards.skip(n: 1).first() { + Absent => RoundRefused { cause: ShoeExhausted } + Present { value: dealer_first } => match shoe.cards.skip(n: 2).first() { + Absent => RoundRefused { cause: ShoeExhausted } + Present { value: player_second } => match shoe.cards.skip(n: 3).first() { + Absent => RoundRefused { cause: ShoeExhausted } + Present { value: dealer_second } => { + let player = Hand { + cards: [player_first, player_second], + } + let dealer = Hand { + cards: [dealer_first, dealer_second], + } + let remaining_shoe = Shoe { + cards: shoe.cards.skip(n: 4), + } + + if is_blackjack(hand: player) && is_blackjack(hand: dealer) { + RoundStepped { + state: RoundComplete { + player: player, + dealer: dealer, + outcome: Pushed, + }, + } + } else if is_blackjack(hand: player) { + RoundStepped { + state: RoundComplete { + player: player, + dealer: dealer, + outcome: PlayerWon, + }, + } + } else if is_blackjack(hand: dealer) { + RoundStepped { + state: RoundComplete { + player: player, + dealer: dealer, + outcome: DealerWon, + }, + } + } else { + RoundStepped { + state: PlayerTurn { + player: player, + dealer: dealer, + shoe: remaining_shoe, + }, + } + } + } + } + } + } + } +} + + +fn apply_player_action(state: RoundState, action: PlayerAction) -> RoundStep { + match state { + RoundComplete { player: _, dealer: _, outcome: _ } => + RoundRefused { cause: ActionAfterRoundComplete } + + DealerTurn { player: _, dealer: _, shoe: _ } => + RoundRefused { cause: PlayerActedOutOfTurn } + + PlayerTurn { player: player, dealer: dealer, shoe: shoe } => match action { + PlayerStands => RoundStepped { + state: DealerTurn { + player: player, + dealer: dealer, + shoe: shoe, + }, + } + + PlayerHits => match shoe.cards.first() { + Absent => RoundRefused { cause: ShoeExhausted } + Present { value: next_card } => { + let new_player = add_card(hand: player, card: next_card) + let remaining_shoe = Shoe { + cards: shoe.cards.skip(n: 1), + } + + if is_bust(v: hand_value(hand: new_player)) { + RoundStepped { + state: RoundComplete { + player: new_player, + dealer: dealer, + outcome: DealerWon, + }, + } + } else { + RoundStepped { + state: PlayerTurn { + player: new_player, + dealer: dealer, + shoe: remaining_shoe, + }, + } + } + } + } + } + } +} + +fn play_dealer_turn(state: RoundState, rules: BlackjackRules) -> RoundStep { + match state { + RoundComplete { player: _, dealer: _, outcome: _ } => + RoundRefused { cause: ActionAfterRoundComplete } + + PlayerTurn { player: _, dealer: _, shoe: _ } => + RoundRefused { cause: DealerActedOutOfTurn } + + DealerTurn { player: player, dealer: dealer, shoe: shoe } => { + let dealer_value = hand_value(hand: dealer) + let should_hit = + dealer_value.total < 17 + || (rules.dealer_hits_soft_17 && dealer_value.total == 17 && dealer_value.soft) + + if should_hit { + match shoe.cards.first() { + Absent => RoundRefused { cause: ShoeExhausted } + Present { value: next_card } => { + let new_dealer = add_card(hand: dealer, card: next_card) + let remaining_shoe = Shoe { + cards: shoe.cards.skip(n: 1), + } + + if is_bust(v: hand_value(hand: new_dealer)) { + RoundStepped { + state: RoundComplete { + player: player, + dealer: new_dealer, + outcome: PlayerWon, + }, + } + } else { + play_dealer_turn( + state: DealerTurn { + player: player, + dealer: new_dealer, + shoe: remaining_shoe, + }, + rules: rules, + ) + } + } + } + } else { + RoundStepped { + state: RoundComplete { + player: player, + dealer: dealer, + outcome: settle( + player: hand_value(hand: player), + dealer: dealer_value, + ), + }, + } + } + } + } +} + +fn settle(player: HandValue, dealer: HandValue) -> RoundOutcome { + if player.total > 21 { + DealerWon + } else if dealer.total > 21 { + PlayerWon + } else if player.total > dealer.total { + PlayerWon + } else if player.total < dealer.total { + DealerWon + } else { + Pushed + } +} diff --git a/dag/test/claim/examples/blackjack_round_witness_test.dag b/dag/test/claim/examples/blackjack_round_witness_test.dag new file mode 100644 index 00000000000..0dfc7f133bb --- /dev/null +++ b/dag/test/claim/examples/blackjack_round_witness_test.dag @@ -0,0 +1,258 @@ +module test.claim.examples.blackjack_round_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import examples.blackjack.cards { Card, Ace, Five, Six, Nine, Ten, King, Queen, Clubs, Diamonds, Hearts, Spades } +import examples.blackjack.hand { Hand } +import examples.blackjack.round { + Shoe, + PlayerHits, + PlayerStands, + BlackjackRules, + PlayerTurn, + DealerTurn, + RoundComplete, + PlayerWon, + DealerWon, + Pushed, + ShoeExhausted, + ActionAfterRoundComplete, + DealerActedOutOfTurn, + PlayerActedOutOfTurn, + RoundStepped, + RoundRefused, + deal, + apply_player_action, + play_dealer_turn, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data standard_rules: BlackjackRules = BlackjackRules { + dealer_hits_soft_17: true, +} + +test fn deal_refuses_when_shoe_is_empty() -> Bool { + match deal(shoe: Shoe { cards: [] }) { + RoundRefused { cause: ShoeExhausted } => true + other => false + } +} + +test fn deal_starts_player_turn_with_four_non_natural_cards() -> Bool { + match deal( + shoe: Shoe { + cards: [ + Card { rank: Ten, suit: Clubs }, + Card { rank: Five, suit: Diamonds }, + Card { rank: Nine, suit: Hearts }, + Card { rank: King, suit: Spades }, + ], + }, + ) { + RoundStepped { + state: PlayerTurn { player: player, dealer: dealer, shoe: remaining_shoe }, + } => + player.cards.length() == 2 + && dealer.cards.length() == 2 + && remaining_shoe.cards.length() == 0 + + other => false + } +} + +test fn deal_completes_player_natural_blackjack() -> Bool { + match deal( + shoe: Shoe { + cards: [ + Card { rank: Ace, suit: Clubs }, + Card { rank: Nine, suit: Diamonds }, + Card { rank: King, suit: Hearts }, + Card { rank: Five, suit: Spades }, + ], + }, + ) { + RoundStepped { + state: RoundComplete { + player: _, + dealer: _, + outcome: PlayerWon, + }, + } => true + + other => false + } +} + +test fn player_action_refuses_after_round_complete() -> Bool { + match apply_player_action( + state: RoundComplete { + player: Hand { cards: [] }, + dealer: Hand { cards: [] }, + outcome: Pushed, + }, + action: PlayerHits, + ) { + RoundRefused { cause: ActionAfterRoundComplete } => true + other => false + } +} + +test fn player_action_refuses_during_dealer_turn() -> Bool { + match apply_player_action( + state: DealerTurn { + player: Hand { cards: [] }, + dealer: Hand { cards: [] }, + shoe: Shoe { cards: [] }, + }, + action: PlayerHits, + ) { + RoundRefused { cause: PlayerActedOutOfTurn } => true + other => false + } +} + +test fn dealer_turn_refuses_during_player_turn() -> Bool { + match play_dealer_turn( + state: PlayerTurn { + player: Hand { cards: [] }, + dealer: Hand { cards: [] }, + shoe: Shoe { cards: [] }, + }, + rules: standard_rules, + ) { + RoundRefused { cause: DealerActedOutOfTurn } => true + other => false + } +} + +test fn player_hit_bust_completes_round_with_dealer_win() -> Bool { + match apply_player_action( + state: PlayerTurn { + player: Hand { + cards: [ + Card { rank: Ten, suit: Clubs }, + Card { rank: Nine, suit: Diamonds }, + ], + }, + dealer: Hand { + cards: [ + Card { rank: Five, suit: Hearts }, + Card { rank: King, suit: Spades }, + ], + }, + shoe: Shoe { + cards: [Card { rank: Five, suit: Clubs }], + }, + }, + action: PlayerHits, + ) { + RoundStepped { + state: RoundComplete { + player: player, + dealer: _, + outcome: DealerWon, + }, + } => player.cards.length() == 3 + + other => false + } +} + +test fn player_stand_starts_dealer_turn() -> Bool { + match apply_player_action( + state: PlayerTurn { + player: Hand { + cards: [ + Card { rank: Ten, suit: Clubs }, + Card { rank: Nine, suit: Diamonds }, + ], + }, + dealer: Hand { + cards: [ + Card { rank: Five, suit: Hearts }, + Card { rank: King, suit: Spades }, + ], + }, + shoe: Shoe { cards: [] }, + }, + action: PlayerStands, + ) { + RoundStepped { + state: DealerTurn { + player: player, + dealer: dealer, + shoe: _, + }, + } => + player.cards.length() == 2 + && dealer.cards.length() == 2 + + other => false + } +} + +test fn dealer_draws_and_busts_for_player_win() -> Bool { + match play_dealer_turn( + state: DealerTurn { + player: Hand { + cards: [ + Card { rank: Ten, suit: Clubs }, + Card { rank: Nine, suit: Diamonds }, + ], + }, + dealer: Hand { + cards: [ + Card { rank: Ten, suit: Hearts }, + Card { rank: Five, suit: Spades }, + ], + }, + shoe: Shoe { + cards: [Card { rank: King, suit: Clubs }], + }, + }, + rules: standard_rules, + ) { + RoundStepped { + state: RoundComplete { + player: _, + dealer: dealer, + outcome: PlayerWon, + }, + } => dealer.cards.length() == 3 + + other => false + } +} + +test fn dealer_hits_soft_seventeen_when_rule_enabled() -> Bool { + match play_dealer_turn( + state: DealerTurn { + player: Hand { + cards: [ + Card { rank: Ten, suit: Clubs }, + Card { rank: Nine, suit: Diamonds }, + ], + }, + dealer: Hand { + cards: [ + Card { rank: Ace, suit: Hearts }, + Card { rank: Six, suit: Spades }, + ], + }, + shoe: Shoe { + cards: [Card { rank: Ten, suit: Clubs }], + }, + }, + rules: standard_rules, + ) { + RoundStepped { + state: RoundComplete { + player: _, + dealer: dealer, + outcome: PlayerWon, + }, + } => dealer.cards.length() == 3 + + other => false + } +} \ No newline at end of file From c6216abf1f771b010f604fe3960b1b2d8ad7f5a3 Mon Sep 17 00:00:00 2001 From: Alex Rasevych Date: Wed, 30 Sep 2026 03:05:25 -0400 Subject: [PATCH 4/9] Milestone 4 complete - implemented shuffle and test file --- dag/examples/blackjack/shuffle.dag | 52 +++++++++++++++++++ .../blackjack_shuffle_witness_test.dag | 42 +++++++++++++++ 2 files changed, 94 insertions(+) create mode 100644 dag/test/claim/examples/blackjack_shuffle_witness_test.dag diff --git a/dag/examples/blackjack/shuffle.dag b/dag/examples/blackjack/shuffle.dag index b1dc2b382e8..218edafeb20 100644 --- a/dag/examples/blackjack/shuffle.dag +++ b/dag/examples/blackjack/shuffle.dag @@ -5,4 +5,56 @@ module examples.blackjack.shuffle // (authority gunbc.plans.blackjack_onboarding). The anchor is the replay handle: a recorded // value, not an entropy source. Entropy is reached only through extdeps.entropy and only from // the one integration claim that section 6 of the brief describes. + +import std.integer { UInt8 } +import std.encoding { base64_octet_int } +import examples.blackjack.cards { Card } +import examples.blackjack.round { Shoe } + type ShuffleSeed { value: Int } + +type ShuffleState { + cards:List + seed: ShuffleSeed +} + +fn shuffle(deck: List, seed: ShuffleSeed) -> Shoe { + let final_state = fold( + deck, + init: ShuffleState { + cards: [], + seed: seed, + }, + f: (state, card) => + if ((next_seed(seed: state.seed).value / 65536) % 2) == 0 { + ShuffleState { + cards: concat([card], state.cards), + seed: next_seed(seed: state.seed), + } + } else { + ShuffleState { + cards: concat(state.cards, [card]), + seed: next_seed(seed: state.seed), + } + } + ) + + Shoe { cards: final_state.cards } +} + +fn next_seed(seed: ShuffleSeed) -> ShuffleSeed { + ShuffleSeed { + value: (seed.value * 1103515245 + 12345) % 2147483648 + } +} + +fn seed_from_octets(octets: List) -> ShuffleSeed { + ShuffleSeed { + value: fold( + octets, + init: 0, + f: (acc, octet) => + (acc * 256 + base64_octet_int(b: octet)) % 2147483648, + ) + } +} diff --git a/dag/test/claim/examples/blackjack_shuffle_witness_test.dag b/dag/test/claim/examples/blackjack_shuffle_witness_test.dag new file mode 100644 index 00000000000..f74b140681b --- /dev/null +++ b/dag/test/claim/examples/blackjack_shuffle_witness_test.dag @@ -0,0 +1,42 @@ +module test.claim.examples.blackjack_shuffle_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import examples.blackjack.cards { Card, standard_deck } +import examples.blackjack.shuffle { ShuffleSeed, shuffle, next_seed, seed_from_octets } +import std.integer { UInt8 } +import std.encoding { base64_decode, Standard } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +test fn next_seed_zero_is_pinned() -> Bool { + next_seed(seed: ShuffleSeed { value: 0 }).value == 12345 +} + +test fn seed_from_empty_octets_is_zero() -> Bool { + seed_from_octets(octets: []).value == 0 +} + +test fn shuffle_is_reproducible() -> Bool { + let seed = ShuffleSeed { value: 7 } + + shuffle(deck: standard_deck, seed: seed).cards + == shuffle(deck: standard_deck, seed: seed).cards +} + +test fn shuffle_is_a_standard_deck_permutation() -> Bool { + let shuffled = shuffle( + deck: standard_deck, + seed: ShuffleSeed { value: 7 }, + ) + + shuffled.cards.length() == standard_deck.length() + && all(standard_deck, card => shuffled.cards.contains(card)) +} + +test fn seed_from_octets_combines_bytes_big_endian() -> Bool { + match base64_decode(s: "AQI=", variant: Standard) { + Present { value: octets } => + seed_from_octets(octets: octets).value == 258 + Absent => false + } +} \ No newline at end of file From 7a1b61ac43a0fa101efd7ae2363a94ef13c6c1be Mon Sep 17 00:00:00 2001 From: Alex Rasevych Date: Fri, 2 Oct 2026 02:50:24 -0400 Subject: [PATCH 5/9] Milestone 5 Progress - finished simulation.dag file --- dag/examples/blackjack/simulation.dag | 49 +++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/dag/examples/blackjack/simulation.dag b/dag/examples/blackjack/simulation.dag index 177d15d1f1c..e80c45f41de 100644 --- a/dag/examples/blackjack/simulation.dag +++ b/dag/examples/blackjack/simulation.dag @@ -5,4 +5,53 @@ module examples.blackjack.simulation // summary_reconciles -- is specified in docs/plans/blackjack-onboarding.md section 4.5 // (authority gunbc.plans.blackjack_onboarding). The anchor is a teaching fixture and not // blackjack advice: the two thresholds the brief compares are both inhabitants of it. + +import examples.blackjack.cards { standard_deck } +import examples.blackjack.hand { Hand, hand_value } +import examples.blackjack.round { + BlackjackRules, + RoundOutcome, + PlayerAction, + PlayerHits, + PlayerStands, +} +import examples.blackjack.shuffle { ShuffleSeed } + type Strategy = HitBelow { threshold: Int } + +type SimulationPlan { + rounds: Int + seed: ShuffleSeed + rules: BlackjackRules + strategy: Strategy +} + +type SimulatedRound { + round_index: Int + seed: ShuffleSeed + player_actions: List + player_total: Int + dealer_total: Int + outcome: RoundOutcome +} + +type SimulationSummary { + rounds_requested: Int + rounds_completed: Int + player_wins: Int + dealer_wins: Int + pushes: Int + player_blackjacks: Int + player_busts: Int +} + +fn choose(strategy: Strategy, player: Hand) -> PlayerAction { + match strategy { + HitBelow { threshold: threshold } => + if hand_value(hand: player).total < threshold { + PlayerHits + } else { + PlayerStands + } + } +} \ No newline at end of file From 1383d4c13a73bae3bc9ab472e0e9a656b78d8d69 Mon Sep 17 00:00:00 2001 From: Brian Searls <11205878+briansrls@users.noreply.github.com> Date: Fri, 2 Oct 2026 17:11:45 -0400 Subject: [PATCH 6/9] Model engine refusals as first-class simulation outcomes (#13011) * blackjack brief: simulate stops the line on an engine refusal play_round was specified as -> SimulatedRound, a type that can only hold a completed round, while every engine call it drives returns RoundStep and may be RoundRefused. A learner had to fabricate a round or drop it silently. Inside a simulation every RoundRefusal cause is a driver defect (fresh 52-card shoe per round, the driver orders the calls), so a refusal is not a statistic: play_round returns RoundPlay = RoundPlayed | RoundPlayRefused, and simulate returns BlackjackSimulation = SimulationCompleted { rounds } | SimulationRefused { round_index, seed, cause }, stopping at the first refusal with what replays it. The summary loses the requested/completed pair (a run completes every round or refuses) and summarizes only a completed run. play_round_from_shoe is split out so the refusal route can execute in a test (short shoe -> ShoeExhausted). Acceptance bar and the simulation.dag marker updated; projection regenerated from expected_plan_md through gunbc.plan plan_generation. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019kAKvQXHWK1YxuJaKnhQg2 * blackjack brief: run the SimulationRefused arm through simulate itself The short-shoe test drove play_round_from_shoe directly, so the conversion from RoundPlayRefused to SimulationRefused inside simulate never executed: from a plan every shoe is a full deck and no round can refuse, so a simulate that fabricated a round, carried on, or attached the wrong index/seed passed every specified test. simulate is now simulate_shoes(seeded_shoes(plan), rules, strategy), with SeededShoe { seed, shoe } supplied as values. The prescribed test hands simulate_shoes three shoes whose second is short and asserts the whole SimulationRefused { round_index: 1, seed, cause: ShoeExhausted }; the real-route claim is that simulate(plan) completes exactly plan.rounds rounds. Projection regenerated through gunbc.plan plan_generation. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019kAKvQXHWK1YxuJaKnhQg2 --------- Co-authored-by: Claude --- dag/examples/blackjack/simulation.dag | 8 ++-- dag/gunbc/plans/blackjack_onboarding.dag | 19 ++++---- docs/plans/blackjack-onboarding.md | 56 ++++++++++++++++++------ 3 files changed, 58 insertions(+), 25 deletions(-) diff --git a/dag/examples/blackjack/simulation.dag b/dag/examples/blackjack/simulation.dag index e80c45f41de..4409549e445 100644 --- a/dag/examples/blackjack/simulation.dag +++ b/dag/examples/blackjack/simulation.dag @@ -1,9 +1,11 @@ module examples.blackjack.simulation // FILE MARKER FOR THE ONBOARDING PROJECT. The analysis pipeline -- SimulationPlan, -// SimulatedRound, SimulationSummary, choose, play_round, simulate, summarize, -// summary_reconciles -- is specified in docs/plans/blackjack-onboarding.md section 4.5 -// (authority gunbc.plans.blackjack_onboarding). The anchor is a teaching fixture and not +// SimulatedRound, RoundPlay, BlackjackSimulation, SeededShoe, SimulationSummary, choose, +// play_round_from_shoe, play_round, seeded_shoes, simulate_shoes, simulate, summarize, +// summary_reconciles -- is +// specified in docs/plans/blackjack-onboarding.md section 4.5 (authority +// gunbc.plans.blackjack_onboarding). The anchor is a teaching fixture and not // blackjack advice: the two thresholds the brief compares are both inhabitants of it. import examples.blackjack.cards { standard_deck } diff --git a/dag/gunbc/plans/blackjack_onboarding.dag b/dag/gunbc/plans/blackjack_onboarding.dag index 98a2226a143..5efd70e53a5 100644 --- a/dag/gunbc/plans/blackjack_onboarding.dag +++ b/dag/gunbc/plans/blackjack_onboarding.dag @@ -51,7 +51,7 @@ fn section_1_central_decision() -> List { li(text: "The same engine serves unit tests, interactive play, and Monte Carlo analysis. There is one blackjack, not three."), ]), p(text: "This is the repository's standing distinction between **interface, realization and policy** (DESIGN §3): what a dependency *means* (`extdeps.entropy` owns the shape), how it is *reached* (a shell transport today — not your concern), and how the application *uses* it (your `SimulationPlan` decides the seed) are three facts in three places."), - code(text: "External entropy extdeps.entropy (exists)\n |\n v\nRecorded seed ShuffleSeed { value: Int }\n |\n v\nDeterministic shuffle shuffle(deck, seed) -> Shoe examples.blackjack.shuffle\n |\n v\nOrdered Shoe Shoe { cards: List }\n |\n v\nPure round engine deal / apply_player_action / examples.blackjack.round\n | play_dealer_turn / settle\n v\nSimulatedRound one record per round\n |\n v\nAggregation summarize(observations) examples.blackjack.simulation\n |\n v\nSimulationSummary counts that must reconcile\n"), + code(text: "External entropy extdeps.entropy (exists)\n |\n v\nRecorded seed ShuffleSeed { value: Int }\n |\n v\nDeterministic shuffle shuffle(deck, seed) -> Shoe examples.blackjack.shuffle\n |\n v\nOrdered Shoe Shoe { cards: List }\n |\n v\nPure round engine deal / apply_player_action / examples.blackjack.round\n | play_dealer_turn / settle\n v\nBlackjackSimulation every round, or the first refusal\n |\n v\nAggregation summarize(rounds) examples.blackjack.simulation\n |\n v\nSimulationSummary counts that must reconcile\n"), ] } @@ -133,12 +133,14 @@ fn section_4_model() -> List { h3(text: "4.4 `examples.blackjack.shuffle` — the boundary"), p(text: "Anchor in the file: `ShuffleSeed`. Two pure functions and nothing else: a seed-to-permutation and a bytes-to-seed. The **only** effectful call in the whole project lives in one test (§7), not here."), - code(text: "module examples.blackjack.shuffle\n\nimport std.integer { UInt8 }\nimport std.encoding { base64_octet_int }\nimport examples.blackjack.cards { Card }\nimport examples.blackjack.round { Shoe }\n\ntype ShuffleSeed { value: Int }\n\n// Deterministic: same deck + same seed = same shoe. A linear congruential step\n// threaded through a fold over positions is enough; this is a teaching fixture,\n// not a claim about randomness quality.\nfn shuffle(deck: List, seed: ShuffleSeed) -> Shoe { … }\n\n// The step function of the generator, exposed so a test can pin its sequence.\nfn next_seed(seed: ShuffleSeed) -> ShuffleSeed { … }\n\n// The bridge from the entropy boundary. The octets arrive as the List that\n// std.encoding.base64_decode returns; base64_octet_int (same module) reads each one as an\n// Int, and a fold combines them. Take the real decoded type here -- do not mint an Int list.\nfn seed_from_octets(octets: List) -> ShuffleSeed { … }\n"), + code(text: "module examples.blackjack.shuffle\n\nimport std.integer { UInt8 }\nimport std.encoding { base64_decode }\nimport examples.blackjack.cards { Card }\nimport examples.blackjack.round { Shoe }\n\ntype ShuffleSeed { value: Int }\n\n// Deterministic: same deck + same seed = same shoe. A linear congruential step\n// threaded through a fold over positions is enough; this is a teaching fixture,\n// not a claim about randomness quality.\nfn shuffle(deck: List, seed: ShuffleSeed) -> Shoe { … }\n\n// The step function of the generator, exposed so a test can pin its sequence.\nfn next_seed(seed: ShuffleSeed) -> ShuffleSeed { … }\n\n// The bridge from the entropy boundary. The octets arrive as the List that\n// std.encoding.base64_decode returns, already admitted as octets by the decoder, and a fold\n// combines them. Take the real decoded type here -- do not mint an Int list, and do not re-admit\n// what the decoder has already established.\nfn seed_from_octets(octets: List) -> ShuffleSeed { … }\n"), h3(text: "4.5 `examples.blackjack.simulation` — analysis"), p(text: "Anchor in the file: `Strategy`. Reuses the engine; reimplements nothing. Each round emits one observation; a summary is a fold over observations; and the reconciliation invariant is a **test**, not an assumption of the report."), - code(text: "module examples.blackjack.simulation\n\nimport examples.blackjack.cards { Card, standard_deck }\nimport examples.blackjack.hand { Hand }\nimport examples.blackjack.round { BlackjackRules, RoundOutcome, RoundState, PlayerAction, deal, apply_player_action, play_dealer_turn }\nimport examples.blackjack.shuffle { ShuffleSeed, shuffle, next_seed }\n\n// Two fixtures, not blackjack advice: hit below the threshold, otherwise stand.\ntype Strategy = HitBelow { threshold: Int }\n\ntype SimulationPlan { rounds: Int, seed: ShuffleSeed, rules: BlackjackRules, strategy: Strategy }\n\ntype SimulatedRound {\n round_index: Int,\n seed: ShuffleSeed,\n player_actions: List,\n player_total: Int,\n dealer_total: Int,\n outcome: RoundOutcome,\n}\n\ntype SimulationSummary {\n rounds_requested: Int,\n rounds_completed: Int,\n player_wins: Int,\n dealer_wins: Int,\n pushes: Int,\n player_blackjacks: Int,\n player_busts: Int,\n}\n\nfn choose(strategy: Strategy, player: Hand) -> PlayerAction { … }\n\n// One full round from a seed: shuffle, deal, drive the player by strategy, dealer plays.\nfn play_round(index: Int, seed: ShuffleSeed, rules: BlackjackRules, strategy: Strategy) -> SimulatedRound { … }\n\n// rounds, each with next_seed(previous) — so round k of plan P is replayable alone.\nfn simulate(plan: SimulationPlan) -> List { … }\n\nfn summarize(plan: SimulationPlan, observations: List) -> SimulationSummary { … }\n\n// player_wins + dealer_wins + pushes == rounds_completed — a first-class test.\nfn summary_reconciles(s: SimulationSummary) -> Bool { … }\n"), + code(text: "module examples.blackjack.simulation\n\nimport examples.blackjack.cards { Card, standard_deck }\nimport examples.blackjack.hand { Hand }\nimport examples.blackjack.round { BlackjackRules, RoundOutcome, RoundRefusal, RoundState, RoundStep, Shoe, PlayerAction, deal, apply_player_action, play_dealer_turn }\nimport examples.blackjack.shuffle { ShuffleSeed, shuffle, next_seed }\n\n// Two fixtures, not blackjack advice: hit below the threshold, otherwise stand.\ntype Strategy = HitBelow { threshold: Int }\n\ntype SimulationPlan { rounds: Int, seed: ShuffleSeed, rules: BlackjackRules, strategy: Strategy }\n\ntype SimulatedRound {\n round_index: Int,\n seed: ShuffleSeed,\n player_actions: List,\n player_total: Int,\n dealer_total: Int,\n outcome: RoundOutcome,\n}\n\n// One round driven to its end, or the engine refusal that stopped it.\ntype RoundPlay = RoundPlayed { round: SimulatedRound } | RoundPlayRefused { cause: RoundRefusal }\n\n// Every requested round, or the first refusal -- with what replays it.\ntype BlackjackSimulation\n = SimulationCompleted { rounds: List }\n | SimulationRefused { round_index: Int, seed: ShuffleSeed, cause: RoundRefusal }\n\ntype SimulationSummary {\n rounds: Int,\n player_wins: Int,\n dealer_wins: Int,\n pushes: Int,\n player_blackjacks: Int,\n player_busts: Int,\n}\n\nfn choose(strategy: Strategy, player: Hand) -> PlayerAction { … }\n\n// One full round from an ordered shoe: deal, drive the player by strategy, dealer plays.\n// Every RoundStep is matched; a RoundRefused becomes RoundPlayRefused with its cause.\nfn play_round_from_shoe(index: Int, seed: ShuffleSeed, shoe: Shoe, rules: BlackjackRules, strategy: Strategy) -> RoundPlay { … }\n\n// shuffle(standard_deck, seed), then play_round_from_shoe.\nfn play_round(index: Int, seed: ShuffleSeed, rules: BlackjackRules, strategy: Strategy) -> RoundPlay { … }\n\n// The shoe one round is dealt from, with the seed that built it.\ntype SeededShoe { seed: ShuffleSeed, shoe: Shoe }\n\n// plan.rounds seeds, each next_seed(previous), each shuffled from standard_deck — so\n// round k of plan P is replayable alone.\nfn seeded_shoes(plan: SimulationPlan) -> List { … }\n\n// Plays the supplied shoes in order, round_index counting from 0. Stops at the first\n// RoundPlayRefused and returns SimulationRefused with that round's index and seed.\nfn simulate_shoes(shoes: List, rules: BlackjackRules, strategy: Strategy) -> BlackjackSimulation { … }\n\n// simulate_shoes(seeded_shoes(plan), plan.rules, plan.strategy).\nfn simulate(plan: SimulationPlan) -> BlackjackSimulation { … }\n\n// Only a completed run has a summary.\nfn summarize(rounds: List) -> SimulationSummary { … }\n\n// player_wins + dealer_wins + pushes == rounds — a first-class test.\nfn summary_reconciles(s: SimulationSummary) -> Bool { … }\n"), p(text: "`win_rate` is deliberately absent from the summary: a ratio is derived from two counts, so storing it beside them is a second copy of one fact (DESIGN §2). Compute it where it is displayed."), + p(text: "**A refusal inside a simulation is a defect, not a statistic.** `play_round` drives the engine itself from a freshly shuffled 52-card deck, so none of the four `RoundRefusal` causes is a nominal event there: an out-of-turn action or an action after `RoundComplete` means the driver called the engine in the wrong order, and `ShoeExhausted` means a round consumed more cards than one round can. So `simulate` does not count refused rounds and carry on — that would turn a bug into a row of the report (DESIGN §5's absorbing fallback). It stops at the first refusal and returns `SimulationRefused` with the round index, the seed and the cause: the line stops, the stop is typed and located, and the seed replays it. Do not reach for a fabricated `SimulatedRound` (totals of 0, an outcome of `Pushed`) or a `_ =>` arm; `RoundRefused` carries no completed state, so there is nothing honest to build one from. Because a run either completes every requested round or refuses, the summary needs no requested-versus-completed pair: `rounds` is one count, and the real-route test below asserts it."), + p(text: "`simulate` is split at its shoes so the refusal route can *execute*: from a plan, every shoe is a full shuffled deck and nothing can make a round refuse, so a test that only calls `simulate(plan)` never runs the `SimulationRefused` arm. `simulate_shoes` takes the shoes as supplied values instead. Hand it three seeded shoes whose second is too short to finish a round, and assert the whole result: `SimulationRefused \{ round_index: 1, seed: , cause: ShoeExhausted \}`. That one assertion goes red if the driver fabricates a round, carries on past the refusal, or attaches the wrong index or seed. Pair it with the real-route claim that `simulate(plan)` returns a `SimulationCompleted` of exactly `plan.rounds` rounds. And if the game later grows a nominal event — several rounds dealt from one shoe, where running low is ordinary — model it as a lawful transition (a reshuffle), not as a refusal; refusals are reserved for what must not happen, which is what makes stopping on them correct."), ] } @@ -153,7 +155,7 @@ fn section_5_tests() -> List { ol(items: [ li(text: "**Pure unit tests** supply cards, hands and values directly. Most of your tests."), li(text: "**State-transition tests** supply a complete `RoundState` and an action, and assert the exact next state or the exact refusal. One test per refusal arm."), - li(text: "**Boundary tests** supply the value an effectful producer *would* return — a `List` of octets (built with `std.encoding` `base64_octet_of_int`, the same constructor the decoder uses) handed to `seed_from_octets`, a `ShuffleSeed` handed to `shuffle` — without calling the producer."), + li(text: "**Boundary tests** supply the value an effectful producer *would* return — a `List` of octets written directly, which is exactly the type `std.encoding` `base64_decode` returns, handed to `seed_from_octets`, a `ShuffleSeed` handed to `shuffle` — without calling the producer."), li(text: "**One integration test** calls the real producer, `Urandom.ReadBytes`, and establishes only that its output inhabits the shape the boundary tests assumed (the right number of octets, decodable). It does not assert that a random shoe has any particular order."), ]), p(text: "Level 3 without level 4 is the trap DESIGN §3 names: a suite that is fast, green, and proves no program, because every boundary was supplied and none was ever executed. Level 4 is what turns your supplied inputs from hypotheses into readings. Keep it to one test, keep it narrow, and know that it is *wet* — it shells out — so it runs with `--wet` locally and is the one that can fail for reasons that are not yours."), @@ -165,15 +167,15 @@ fn section_5_tests() -> List { fn section_6_randomness() -> List { [ h2(text: "6. The randomness boundary"), - p(text: "Only after deterministic rounds run from hand-ordered shoes do you connect entropy — and even then, the connection is one function call in one test. `dag/test/claim/random_bytes_csprng_witness_test.dag` is the in-tree exemplar: it calls `Urandom.ReadBytes(count: 16).octets_b64`, base64-decodes it with `std.encoding` `base64_decode` to `List?`, and asserts the count. Your integration test does the same, matches the `Present` arm (the `Absent` arm is a refusal of the test, not a skip), hands that `List` to `seed_from_octets` unchanged — it takes the decoder's type, and reads each octet with `base64_octet_int` — then `shuffle`, and asserts that the result is a 52-card shoe containing each card exactly once. That last assertion is a property of `shuffle`, not of the entropy; it is here because it is the one place the whole route executes."), - p(text: "The seed is the replay handle. Every `SimulatedRound` carries the seed its shoe was built from, so a surprising row in a 10,000-round simulation is reproduced by one call to `play_round` with that seed — no reruns, no logging, no luck."), + p(text: "Only after deterministic rounds run from hand-ordered shoes do you connect entropy — and even then, the connection is one function call in one test. `dag/test/claim/random_bytes_csprng_witness_test.dag` is the in-tree exemplar: it calls `Urandom.ReadBytes(count: 16).octets_b64`, base64-decodes it with `std.encoding` `base64_decode` to `List?`, and asserts the count. Your integration test does the same, matches the `Present` arm (the `Absent` arm is a refusal of the test, not a skip), hands that `List` to `seed_from_octets` unchanged — it takes the decoder's type, and folds over those octets — then `shuffle`, and asserts that the result is a 52-card shoe containing each card exactly once. That last assertion is a property of `shuffle`, not of the entropy; it is here because it is the one place the whole route executes."), + p(text: "The seed is the replay handle. Every `SimulatedRound` carries the seed its shoe was built from, and a `SimulationRefused` carries the same seed beside its cause, so a surprising row — or a refusal — in a 10,000-round simulation is reproduced by one call to `play_round` with that seed — no reruns, no logging, no luck."), ] } fn section_7_analysis() -> List { [ h2(text: "7. Analysis"), - p(text: "`simulate` is a recursion over the round index threading the seed forward; `summarize` is a fold over observations; `summary_reconciles` is a test. The comparison you are after is two plans differing only in `strategy`, run from the same starting seed, so the two strategies see the *same* shoes — a paired comparison, which is the honest one. `HitBelow \{ threshold: 17 \}` against `HitBelow \{ threshold: 19 \}` is enough to see a difference; neither is a claim about optimal play."), + p(text: "`simulate` is a recursion over the round index threading the seed forward; `summarize` is a fold over a completed run's rounds; `summary_reconciles` is a test. The comparison you are after is two plans differing only in `strategy`, run from the same starting seed, so the two strategies see the *same* shoes — a paired comparison, which is the honest one. `HitBelow \{ threshold: 17 \}` against `HitBelow \{ threshold: 19 \}` is enough to see a difference; neither is a claim about optimal play."), p(text: "What the summary may and may not say (DESIGN §4d): the counts are deduced; any sentence of the form *strategy A is better* is an inference from a sample and belongs beside its sample size and seed, never in a bare field of the summary type."), ] } @@ -209,7 +211,8 @@ fn section_9_milestones() -> List { li(text: "shuffle output is reproducible from a recorded seed"), li(text: "no unit test depends on live entropy; exactly one test exercises the real entropy route"), li(text: "two strategies compare through the same engine over the same seeds"), - li(text: "`player_wins + dealer_wins + pushes == rounds_completed` is a test, and it is green"), + li(text: "`player_wins + dealer_wins + pushes == rounds` is a test, and it is green"), + li(text: "an engine refusal inside a round reaches the caller of `simulate` as `SimulationRefused` with its index, seed and cause — never a fabricated round — and a test drives `simulate_shoes` with a short second shoe to `SimulationRefused \{ round_index: 1, seed: , cause: ShoeExhausted \}`"), li(text: "every test names its case and can be made red by a mutation of the code it covers"), li(text: "the example's closure emits Rust and the crate passes `cargo check` unedited"), li(text: "the README explains the project through the lenses, not the rules"), diff --git a/docs/plans/blackjack-onboarding.md b/docs/plans/blackjack-onboarding.md index d33b3b8f8ee..e2af72c981c 100644 --- a/docs/plans/blackjack-onboarding.md +++ b/docs/plans/blackjack-onboarding.md @@ -48,10 +48,10 @@ Ordered Shoe Shoe { cards: List } Pure round engine deal / apply_player_action / examples.blackjack.round | play_dealer_turn / settle v -SimulatedRound one record per round +BlackjackSimulation every round, or the first refusal | v -Aggregation summarize(observations) examples.blackjack.simulation +Aggregation summarize(rounds) examples.blackjack.simulation | v SimulationSummary counts that must reconcile @@ -260,7 +260,7 @@ module examples.blackjack.simulation import examples.blackjack.cards { Card, standard_deck } import examples.blackjack.hand { Hand } -import examples.blackjack.round { BlackjackRules, RoundOutcome, RoundState, PlayerAction, deal, apply_player_action, play_dealer_turn } +import examples.blackjack.round { BlackjackRules, RoundOutcome, RoundRefusal, RoundState, RoundStep, Shoe, PlayerAction, deal, apply_player_action, play_dealer_turn } import examples.blackjack.shuffle { ShuffleSeed, shuffle, next_seed } // Two fixtures, not blackjack advice: hit below the threshold, otherwise stand. @@ -277,9 +277,16 @@ type SimulatedRound { outcome: RoundOutcome, } +// One round driven to its end, or the engine refusal that stopped it. +type RoundPlay = RoundPlayed { round: SimulatedRound } | RoundPlayRefused { cause: RoundRefusal } + +// Every requested round, or the first refusal -- with what replays it. +type BlackjackSimulation + = SimulationCompleted { rounds: List } + | SimulationRefused { round_index: Int, seed: ShuffleSeed, cause: RoundRefusal } + type SimulationSummary { - rounds_requested: Int, - rounds_completed: Int, + rounds: Int, player_wins: Int, dealer_wins: Int, pushes: Int, @@ -289,20 +296,40 @@ type SimulationSummary { fn choose(strategy: Strategy, player: Hand) -> PlayerAction { … } -// One full round from a seed: shuffle, deal, drive the player by strategy, dealer plays. -fn play_round(index: Int, seed: ShuffleSeed, rules: BlackjackRules, strategy: Strategy) -> SimulatedRound { … } +// One full round from an ordered shoe: deal, drive the player by strategy, dealer plays. +// Every RoundStep is matched; a RoundRefused becomes RoundPlayRefused with its cause. +fn play_round_from_shoe(index: Int, seed: ShuffleSeed, shoe: Shoe, rules: BlackjackRules, strategy: Strategy) -> RoundPlay { … } + +// shuffle(standard_deck, seed), then play_round_from_shoe. +fn play_round(index: Int, seed: ShuffleSeed, rules: BlackjackRules, strategy: Strategy) -> RoundPlay { … } + +// The shoe one round is dealt from, with the seed that built it. +type SeededShoe { seed: ShuffleSeed, shoe: Shoe } -// rounds, each with next_seed(previous) — so round k of plan P is replayable alone. -fn simulate(plan: SimulationPlan) -> List { … } +// plan.rounds seeds, each next_seed(previous), each shuffled from standard_deck — so +// round k of plan P is replayable alone. +fn seeded_shoes(plan: SimulationPlan) -> List { … } -fn summarize(plan: SimulationPlan, observations: List) -> SimulationSummary { … } +// Plays the supplied shoes in order, round_index counting from 0. Stops at the first +// RoundPlayRefused and returns SimulationRefused with that round's index and seed. +fn simulate_shoes(shoes: List, rules: BlackjackRules, strategy: Strategy) -> BlackjackSimulation { … } -// player_wins + dealer_wins + pushes == rounds_completed — a first-class test. +// simulate_shoes(seeded_shoes(plan), plan.rules, plan.strategy). +fn simulate(plan: SimulationPlan) -> BlackjackSimulation { … } + +// Only a completed run has a summary. +fn summarize(rounds: List) -> SimulationSummary { … } + +// player_wins + dealer_wins + pushes == rounds — a first-class test. fn summary_reconciles(s: SimulationSummary) -> Bool { … } ``` `win_rate` is deliberately absent from the summary: a ratio is derived from two counts, so storing it beside them is a second copy of one fact (DESIGN §2). Compute it where it is displayed. +**A refusal inside a simulation is a defect, not a statistic.** `play_round` drives the engine itself from a freshly shuffled 52-card deck, so none of the four `RoundRefusal` causes is a nominal event there: an out-of-turn action or an action after `RoundComplete` means the driver called the engine in the wrong order, and `ShoeExhausted` means a round consumed more cards than one round can. So `simulate` does not count refused rounds and carry on — that would turn a bug into a row of the report (DESIGN §5's absorbing fallback). It stops at the first refusal and returns `SimulationRefused` with the round index, the seed and the cause: the line stops, the stop is typed and located, and the seed replays it. Do not reach for a fabricated `SimulatedRound` (totals of 0, an outcome of `Pushed`) or a `_ =>` arm; `RoundRefused` carries no completed state, so there is nothing honest to build one from. Because a run either completes every requested round or refuses, the summary needs no requested-versus-completed pair: `rounds` is one count, and the real-route test below asserts it. + +`simulate` is split at its shoes so the refusal route can *execute*: from a plan, every shoe is a full shuffled deck and nothing can make a round refuse, so a test that only calls `simulate(plan)` never runs the `SimulationRefused` arm. `simulate_shoes` takes the shoes as supplied values instead. Hand it three seeded shoes whose second is too short to finish a round, and assert the whole result: `SimulationRefused { round_index: 1, seed: , cause: ShoeExhausted }`. That one assertion goes red if the driver fabricates a round, carries on past the refusal, or attaches the wrong index or seed. Pair it with the real-route claim that `simulate(plan)` returns a `SimulationCompleted` of exactly `plan.rounds` rounds. And if the game later grows a nominal event — several rounds dealt from one shoe, where running low is ordinary — model it as a lawful transition (a reshuffle), not as a refusal; refusals are reserved for what must not happen, which is what makes stopping on them correct. + ## 5. Tests, evidence, and what "mocking" means here Tests live under `dag/test/claim/` — that directory is what CI's witness floor discovers. Put yours at `dag/test/claim/examples/blackjack_hand_witness_test.dag`, `…_round_…`, `…_shuffle_…`, `…_simulation_…`, one file per module under test. A test file is an ordinary module whose functions are marked `test fn` and return `Bool`, plus one declaration every claim file carries: @@ -352,11 +379,11 @@ Every test you write must be one you can make go **red** by breaking the code it Only after deterministic rounds run from hand-ordered shoes do you connect entropy — and even then, the connection is one function call in one test. `dag/test/claim/random_bytes_csprng_witness_test.dag` is the in-tree exemplar: it calls `Urandom.ReadBytes(count: 16).octets_b64`, base64-decodes it with `std.encoding` `base64_decode` to `List?`, and asserts the count. Your integration test does the same, matches the `Present` arm (the `Absent` arm is a refusal of the test, not a skip), hands that `List` to `seed_from_octets` unchanged — it takes the decoder's type, and reads each octet with `base64_octet_int` — then `shuffle`, and asserts that the result is a 52-card shoe containing each card exactly once. That last assertion is a property of `shuffle`, not of the entropy; it is here because it is the one place the whole route executes. -The seed is the replay handle. Every `SimulatedRound` carries the seed its shoe was built from, so a surprising row in a 10,000-round simulation is reproduced by one call to `play_round` with that seed — no reruns, no logging, no luck. +The seed is the replay handle. Every `SimulatedRound` carries the seed its shoe was built from, and a `SimulationRefused` carries the same seed beside its cause, so a surprising row — or a refusal — in a 10,000-round simulation is reproduced by one call to `play_round` with that seed — no reruns, no logging, no luck. ## 7. Analysis -`simulate` is a recursion over the round index threading the seed forward; `summarize` is a fold over observations; `summary_reconciles` is a test. The comparison you are after is two plans differing only in `strategy`, run from the same starting seed, so the two strategies see the *same* shoes — a paired comparison, which is the honest one. `HitBelow { threshold: 17 }` against `HitBelow { threshold: 19 }` is enough to see a difference; neither is a claim about optimal play. +`simulate` is a recursion over the round index threading the seed forward; `summarize` is a fold over a completed run's rounds; `summary_reconciles` is a test. The comparison you are after is two plans differing only in `strategy`, run from the same starting seed, so the two strategies see the *same* shoes — a paired comparison, which is the honest one. `HitBelow { threshold: 17 }` against `HitBelow { threshold: 19 }` is enough to see a difference; neither is a claim about optimal play. What the summary may and may not say (DESIGN §4d): the counts are deduced; any sentence of the form *strategy A is better* is an inference from a sample and belongs beside its sample size and seed, never in a bare field of the summary type. @@ -403,7 +430,8 @@ Five, each ending in a small PR so review can focus on one conceptual layer. Eac - shuffle output is reproducible from a recorded seed - no unit test depends on live entropy; exactly one test exercises the real entropy route - two strategies compare through the same engine over the same seeds -- `player_wins + dealer_wins + pushes == rounds_completed` is a test, and it is green +- `player_wins + dealer_wins + pushes == rounds` is a test, and it is green +- an engine refusal inside a round reaches the caller of `simulate` as `SimulationRefused` with its index, seed and cause — never a fabricated round — and a test drives `simulate_shoes` with a short second shoe to `SimulationRefused { round_index: 1, seed: , cause: ShoeExhausted }` - every test names its case and can be made red by a mutation of the code it covers - the example's closure emits Rust and the crate passes `cargo check` unedited - the README explains the project through the lenses, not the rules From 07ba95337587988190835fd296861fc68bcf597a Mon Sep 17 00:00:00 2001 From: Alex Rasevych Date: Sat, 3 Oct 2026 03:51:39 -0400 Subject: [PATCH 7/9] Complete blackjack simulation milestone --- dag/examples/blackjack/simulation.dag | 300 +++++++++++++++++- .../blackjack_shuffle_witness_test.dag | 18 ++ .../blackjack_simulation_witness_test.dag | 151 +++++++++ 3 files changed, 459 insertions(+), 10 deletions(-) create mode 100644 dag/test/claim/examples/blackjack_simulation_witness_test.dag diff --git a/dag/examples/blackjack/simulation.dag b/dag/examples/blackjack/simulation.dag index 4409549e445..c07daa06c1d 100644 --- a/dag/examples/blackjack/simulation.dag +++ b/dag/examples/blackjack/simulation.dag @@ -1,25 +1,39 @@ module examples.blackjack.simulation // FILE MARKER FOR THE ONBOARDING PROJECT. The analysis pipeline -- SimulationPlan, -// SimulatedRound, RoundPlay, BlackjackSimulation, SeededShoe, SimulationSummary, choose, -// play_round_from_shoe, play_round, seeded_shoes, simulate_shoes, simulate, summarize, -// summary_reconciles -- is -// specified in docs/plans/blackjack-onboarding.md section 4.5 (authority -// gunbc.plans.blackjack_onboarding). The anchor is a teaching fixture and not +// SimulatedRound, SimulationSummary, choose, play_round, simulate, summarize, +// summary_reconciles -- is specified in docs/plans/blackjack-onboarding.md section 4.5 +// (authority gunbc.plans.blackjack_onboarding). The anchor is a teaching fixture and not // blackjack advice: the two thresholds the brief compares are both inhabitants of it. -import examples.blackjack.cards { standard_deck } +import examples.blackjack.cards { Card, standard_deck } import examples.blackjack.hand { Hand, hand_value } import examples.blackjack.round { BlackjackRules, RoundOutcome, + RoundRefusal, + RoundState, + RoundStep, + Shoe, PlayerAction, PlayerHits, PlayerStands, + deal, + apply_player_action, + play_dealer_turn, + RoundComplete, + PlayerTurn, + DealerTurn, + RoundStepped, + RoundRefused, + PlayerWon, + DealerWon, + Pushed, } -import examples.blackjack.shuffle { ShuffleSeed } +import examples.blackjack.shuffle { ShuffleSeed, shuffle, next_seed } -type Strategy = HitBelow { threshold: Int } +type Strategy + = HitBelow { threshold: Int } type SimulationPlan { rounds: Int @@ -37,9 +51,20 @@ type SimulatedRound { outcome: RoundOutcome } +type RoundPlay + = RoundPlayed { round: SimulatedRound } + | RoundPlayRefused { cause: RoundRefusal } + +type BlackjackSimulation + = SimulationCompleted { rounds: List } + | SimulationRefused { + round_index: Int + seed: ShuffleSeed + cause: RoundRefusal + } + type SimulationSummary { - rounds_requested: Int - rounds_completed: Int + rounds: Int player_wins: Int dealer_wins: Int pushes: Int @@ -47,6 +72,11 @@ type SimulationSummary { player_busts: Int } +type SeededShoe { + seed: ShuffleSeed + shoe: Shoe +} + fn choose(strategy: Strategy, player: Hand) -> PlayerAction { match strategy { HitBelow { threshold: threshold } => @@ -56,4 +86,254 @@ fn choose(strategy: Strategy, player: Hand) -> PlayerAction { PlayerStands } } +} + +fn play_round_from_shoe( + index: Int, + seed: ShuffleSeed, + shoe: Shoe, + rules: BlackjackRules, + strategy: Strategy, +) -> RoundPlay { + match deal(shoe: shoe) { + RoundStepped { state: state } => + drive_round( + index: index, + seed: seed, + state: state, + rules: rules, + strategy: strategy, + player_actions: [], + ) + RoundRefused { cause: cause } => + RoundPlayRefused { cause: cause } + } +} + +fn drive_round( + index: Int, + seed: ShuffleSeed, + state: RoundState, + rules: BlackjackRules, + strategy: Strategy, + player_actions: List, +) -> RoundPlay { + match state { + RoundComplete { player: player, dealer: dealer, outcome: outcome } => + RoundPlayed { + round: SimulatedRound { + round_index: index, + seed: seed, + player_actions: player_actions, + player_total: hand_value(hand: player).total, + dealer_total: hand_value(hand: dealer).total, + outcome: outcome, + } + } + + PlayerTurn { player: player, dealer: dealer, shoe: shoe } => + let action = choose(strategy: strategy, player: player) + match apply_player_action( + state: PlayerTurn { + player: player, + dealer: dealer, + shoe: shoe, + }, + action: action, + ) { + RoundStepped { state: next_state } => + drive_round( + index: index, + seed: seed, + state: next_state, + rules: rules, + strategy: strategy, + player_actions: concat(player_actions, [action]), + ) + RoundRefused { cause: cause } => + RoundPlayRefused { cause: cause } + } + + DealerTurn { player: player, dealer: dealer, shoe: shoe } => + match play_dealer_turn( + state: DealerTurn { + player: player, + dealer: dealer, + shoe: shoe, + }, + rules: rules, + ) { + RoundStepped { state: next_state } => + drive_round( + index: index, + seed: seed, + state: next_state, + rules: rules, + strategy: strategy, + player_actions: player_actions, + ) + RoundRefused { cause: cause } => + RoundPlayRefused { cause: cause } + } + } +} + +fn play_round( + index: Int, + seed: ShuffleSeed, + rules: BlackjackRules, + strategy: Strategy, +) -> RoundPlay { + play_round_from_shoe( + index: index, + seed: seed, + shoe: shuffle(deck: standard_deck, seed: seed), + rules: rules, + strategy: strategy, + ) +} + +fn seeded_shoes(plan: SimulationPlan) -> List { + seeded_shoes_from( + remaining: plan.rounds, + seed: plan.seed, + ) +} + +fn seeded_shoes_from( + remaining: Int, + seed: ShuffleSeed, +) -> List { + if remaining <= 0 { + [] + } else { + concat( + [ + SeededShoe { + seed: seed, + shoe: shuffle(deck: standard_deck, seed: seed), + } + ], + seeded_shoes_from( + remaining: remaining - 1, + seed: next_seed(seed: seed), + ), + ) + } +} + +fn simulate_shoes( + shoes: List, + rules: BlackjackRules, + strategy: Strategy, +) -> BlackjackSimulation { + simulate_shoes_from( + round_index: 0, + shoes: shoes, + rules: rules, + strategy: strategy, + ) +} + +fn simulate_shoes_from( + round_index: Int, + shoes: List, + rules: BlackjackRules, + strategy: Strategy, +) -> BlackjackSimulation { + match shoes.first() { + Absent => + SimulationCompleted { rounds: [] } + + Present { value: seeded_shoe } => + match play_round_from_shoe( + index: round_index, + seed: seeded_shoe.seed, + shoe: seeded_shoe.shoe, + rules: rules, + strategy: strategy, + ) { + RoundPlayRefused { cause: cause } => + SimulationRefused { + round_index: round_index, + seed: seeded_shoe.seed, + cause: cause, + } + + RoundPlayed { round: round } => + match simulate_shoes_from( + round_index: round_index + 1, + shoes: shoes.skip(n: 1), + rules: rules, + strategy: strategy, + ) { + SimulationCompleted { rounds: later_rounds } => + SimulationCompleted { + rounds: concat([round], later_rounds) + } + + SimulationRefused { + round_index: refused_index, + seed: refused_seed, + cause: refused_cause, + } => + SimulationRefused { + round_index: refused_index, + seed: refused_seed, + cause: refused_cause, + } + } + } + } +} + +fn simulate(plan: SimulationPlan) -> BlackjackSimulation { + simulate_shoes( + shoes: seeded_shoes(plan: plan), + rules: plan.rules, + strategy: plan.strategy, + ) +} + +fn summarize(rounds: List) -> SimulationSummary { + fold( + rounds, + init: SimulationSummary { + rounds: 0, + player_wins: 0, + dealer_wins: 0, + pushes: 0, + player_blackjacks: 0, + player_busts: 0, + }, + f: (summary, round) => + SimulationSummary { + rounds: summary.rounds + 1, + + player_wins: summary.player_wins + + if round.outcome == PlayerWon { 1 } else { 0 }, + + dealer_wins: summary.dealer_wins + + if round.outcome == DealerWon { 1 } else { 0 }, + + pushes: summary.pushes + + if round.outcome == Pushed { 1 } else { 0 }, + + player_blackjacks: summary.player_blackjacks + + if round.outcome == PlayerWon + && round.player_total == 21 + && round.player_actions.length() == 0 { + 1 + } else { + 0 + }, + + player_busts: summary.player_busts + + if round.player_total > 21 { 1 } else { 0 }, + }, + ) +} + +fn summary_reconciles(s: SimulationSummary) -> Bool { + s.player_wins + s.dealer_wins + s.pushes == s.rounds } \ No newline at end of file diff --git a/dag/test/claim/examples/blackjack_shuffle_witness_test.dag b/dag/test/claim/examples/blackjack_shuffle_witness_test.dag index f74b140681b..f188dfff5de 100644 --- a/dag/test/claim/examples/blackjack_shuffle_witness_test.dag +++ b/dag/test/claim/examples/blackjack_shuffle_witness_test.dag @@ -39,4 +39,22 @@ test fn seed_from_octets_combines_bytes_big_endian() -> Bool { seed_from_octets(octets: octets).value == 258 Absent => false } +} + +test fn wet_entropy_seeded_shuffle_is_standard_deck_permutation() -> Bool { + match base64_decode( + s: Urandom.ReadBytes(count: 160).octets_b64, + variant: Standard, + ) { + Present { value: octets } => { + let seed = seed_from_octets(octets: octets) + let shoe = shuffle(deck: standard_deck, seed: seed) + + shoe.cards.length() == 52 + && all(standard_deck, card => shoe.cards.contains(card)) + } + + Absent => + false + } } \ No newline at end of file diff --git a/dag/test/claim/examples/blackjack_simulation_witness_test.dag b/dag/test/claim/examples/blackjack_simulation_witness_test.dag new file mode 100644 index 00000000000..7d94d98bf18 --- /dev/null +++ b/dag/test/claim/examples/blackjack_simulation_witness_test.dag @@ -0,0 +1,151 @@ +module test.claim.examples.blackjack_simulation_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import examples.blackjack.cards { standard_deck } +import examples.blackjack.round { BlackjackRules, Shoe, ShoeExhausted } +import examples.blackjack.shuffle { ShuffleSeed, shuffle, next_seed } +import examples.blackjack.simulation { + HitBelow, + Strategy, + SimulationPlan, + SeededShoe, + SimulationCompleted, + SimulationRefused, + simulate, + simulate_shoes, + summarize, + summary_reconciles, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn rules() -> BlackjackRules { + BlackjackRules { dealer_hits_soft_17: false } +} + +fn short_shoes() -> List { + let first_seed = ShuffleSeed { value: 7 } + let second_seed = next_seed(seed: first_seed) + let third_seed = next_seed(seed: second_seed) + + [ + SeededShoe { + seed: first_seed, + shoe: shuffle(deck: standard_deck, seed: first_seed), + }, + SeededShoe { + seed: second_seed, + shoe: Shoe { cards: [] }, + }, + SeededShoe { + seed: third_seed, + shoe: shuffle(deck: standard_deck, seed: third_seed), + }, + ] +} + +fn plan() -> SimulationPlan { + SimulationPlan { + rounds: 3, + seed: ShuffleSeed { value: 7 }, + rules: rules(), + strategy: HitBelow { threshold: 19 }, + } +} + +test fn simulate_shoes_stops_on_second_short_shoe() -> Bool { + match simulate_shoes( + shoes: short_shoes(), + rules: rules(), + strategy: HitBelow { threshold: 19 }, + ) { + SimulationRefused { + round_index: round_index, + seed: seed, + cause: ShoeExhausted, + } => + round_index == 1 + && seed.value == next_seed(seed: ShuffleSeed { value: 7 }).value + + SimulationRefused { + round_index: _, + seed: _, + cause: _, + } => + false + + SimulationCompleted { rounds: _ } => + false + } +} + +test fn simulate_plan_completes_requested_rounds() -> Bool { + match simulate(plan: plan()) { + SimulationCompleted { rounds: rounds } => + rounds.length() == 3 + + SimulationRefused { + round_index: _, + seed: _, + cause: _, + } => + false + } +} + +test fn completed_simulation_summary_reconciles() -> Bool { + match simulate(plan: plan()) { + SimulationCompleted { rounds: rounds } => + summary_reconciles(s: summarize(rounds: rounds)) + + SimulationRefused { + round_index: _, + seed: _, + cause: _, + } => + false + } +} + +test fn paired_strategies_reconcile_over_same_seeded_shoes() -> Bool { + let comparison_plan = SimulationPlan { + rounds: 5, + seed: ShuffleSeed { value: 23 }, + rules: rules(), + strategy: HitBelow { threshold: 17 }, + } + + let shoes = seeded_shoes(plan: comparison_plan) + + match simulate_shoes( + shoes: shoes, + rules: rules(), + strategy: HitBelow { threshold: 17 }, + ) { + SimulationCompleted { rounds: seventeen_rounds } => + match simulate_shoes( + shoes: shoes, + rules: rules(), + strategy: HitBelow { threshold: 19 }, + ) { + SimulationCompleted { rounds: nineteen_rounds } => + seventeen_rounds.length() == nineteen_rounds.length() + && summary_reconciles(s: summarize(rounds: seventeen_rounds)) + && summary_reconciles(s: summarize(rounds: nineteen_rounds)) + + SimulationRefused { + round_index: _, + seed: _, + cause: _, + } => + false + } + + SimulationRefused { + round_index: _, + seed: _, + cause: _, + } => + false + } +} \ No newline at end of file From ef4ccbce53e3dfdd5dce4464daf50ac3aa818565 Mon Sep 17 00:00:00 2001 From: Alex Rasevych Date: Sat, 3 Oct 2026 23:36:44 -0400 Subject: [PATCH 8/9] Add blackjack project README --- dag/examples/blackjack/README.md | 70 ++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 dag/examples/blackjack/README.md diff --git a/dag/examples/blackjack/README.md b/dag/examples/blackjack/README.md new file mode 100644 index 00000000000..cf493999b11 --- /dev/null +++ b/dag/examples/blackjack/README.md @@ -0,0 +1,70 @@ +# Blackjack: a small Dag model + +This example is a guided tour of Dag’s four-view loop. It models a small +Blackjack domain; it is not gambling advice. + +## 1. Model the facts + +The model is split by responsibility: + +- `cards.dag` defines `Card`, `Rank`, `Suit`, and `standard_deck`. +- `hand.dag` derives a hand total, softness, bust status, and Blackjack status. +- `round.dag` is the pure round state machine. Invalid transitions are explicit + `RoundRefused` values rather than exceptions or default results. +- `shuffle.dag` turns a recorded `ShuffleSeed` into a deterministic `Shoe`. +- `simulation.dag` runs seeded rounds, aggregates completed observations, and + preserves any engine refusal with its replay seed and round index. + +## 2. Run a pure example + +A round has no hidden randomness. The same ordered shoe and rules always +produce the same result. + +Randomness is kept at the boundary: + +```text +Urandom.ReadBytes -> Base64 decode -> ShuffleSeed -> shuffle -> Shoe +``` + +Once a seed is recorded, a shuffle and every simulated round can be replayed. +Each simulated round uses a fresh shuffled 52-card shoe. + +## 3. Inspect test evidence + +Witness tests live under `dag/test/claim/examples/`. + +They cover hand evaluation, round transitions, deterministic shuffle behavior, +simulation reconciliation, and paired strategies running over the same seeded +shoes. The simulation witness also supplies a deliberately short second shoe +and verifies that the run stops with `SimulationRefused` at the correct index, +seed, and `ShoeExhausted` cause. + +The only entropy-dependent test is the wet shuffle-boundary test. It checks +that real decoded entropy produces a 52-card permutation, without asserting a +particular card order. + +## 4. Inspect emitted Rust + +Dag is the source program. Rust is a generated projection and must not be +edited by hand. + +```bash +OUT=$(mktemp -d) + +./target/release/gunbc compile \ + --source-root dag \ + --entry dag/examples/blackjack/simulation.dag \ + --output-dir "$OUT" \ + --target rust + +cargo check --manifest-path "$OUT/Cargo.toml" +``` + +The model’s key summary invariant is: + +```text +player_wins + dealer_wins + pushes == rounds +``` + +The summary reports observed counts. It does not store a `win_rate` or claim +that one strategy is universally better than another from a finite sample. \ No newline at end of file From 32e4cb491d090d7f5a875bb570d9f1276977f31e Mon Sep 17 00:00:00 2001 From: Alex Rasevych Date: Fri, 9 Oct 2026 03:42:17 -0400 Subject: [PATCH 9/9] Run blackjack entropy witness on wet lane --- dag/examples/blackjack/shuffle.dag | 4 ++-- dag/gunbc/ci/ci_layer_roots.dag | 11 ++++++++++ .../blackjack_shuffle_wet_witness_test.dag | 22 +++++++++++++++++++ .../blackjack_shuffle_witness_test.dag | 18 --------------- src/v2/workflow/local_repo_wet_terminal.dag | 9 ++++++++ 5 files changed, 44 insertions(+), 20 deletions(-) create mode 100644 dag/test/claim/examples/blackjack_shuffle_wet_witness_test.dag diff --git a/dag/examples/blackjack/shuffle.dag b/dag/examples/blackjack/shuffle.dag index 218edafeb20..2f6455ed333 100644 --- a/dag/examples/blackjack/shuffle.dag +++ b/dag/examples/blackjack/shuffle.dag @@ -7,7 +7,7 @@ module examples.blackjack.shuffle // the one integration claim that section 6 of the brief describes. import std.integer { UInt8 } -import std.encoding { base64_octet_int } + import examples.blackjack.cards { Card } import examples.blackjack.round { Shoe } @@ -54,7 +54,7 @@ fn seed_from_octets(octets: List) -> ShuffleSeed { octets, init: 0, f: (acc, octet) => - (acc * 256 + base64_octet_int(b: octet)) % 2147483648, + (acc * 256 + octet) % 2147483648, ) } } diff --git a/dag/gunbc/ci/ci_layer_roots.dag b/dag/gunbc/ci/ci_layer_roots.dag index 78617e3ebb5..857b5c80d61 100644 --- a/dag/gunbc/ci/ci_layer_roots.dag +++ b/dag/gunbc/ci/ci_layer_roots.dag @@ -405,6 +405,10 @@ data excl_local_repo_wet_tempdir_write_dissolve: DissolutionCondition = unbound_ data excl_local_repo_wet_enrolment_code_reason: String = "real host-effect execution witness over the approval broker's enrolment code whose subjects are reached only through two effects with no mock_response: a FILESYSTEM WRITE INTO A THROWAWAY TEMP DIRECTORY (shell.Mktemp.DirWithTemplate, then the enrolment slot's file CAS, then shell.Remove.RecursiveForce of that directory -- the same admitted effect excl_local_repo_wet_tempdir_write_reason names) and ONE READ OF THE KERNEL ENTROPY SOURCE (Urandom.ReadBytes, sixteen octets). The entropy read is named rather than folded into the tempdir row because it is a different effect: it writes nothing, and its value is deliberately unpredictable, so the claim that reads it asserts only the SHAPE the real read produces (32 lowercase hex characters) -- the inhabitance half of DESIGN section 3's pairing obligation, whose supplied-octets half runs hermetically in test.claim.approval_device_enrolment_code_witness_test. Shared negative half: no network, no cargo, no remote host, nothing outside a directory the witness created and removes. Excluded from the discovery corpus and executed by the required floor's local-repo wet lane (v2.workflow.local_repo_wet_terminal local_repo_wet_schedule), every function in the named file on that schedule." +data excl_local_repo_wet_blackjack_shuffle_reason: String = "real host-effect execution witness over the Blackjack shuffle: the claim makes one kernel-entropy read through Urandom.ReadBytes, writes nothing, and asserts only that decoding the result, deriving a seed, and shuffling the standard deck produces a 52-card permutation. Its deterministic counterpart supplies fixed octets in test.claim.examples.blackjack_shuffle_witness_test. Excluded from the discovery corpus and executed by the required floor's local-repo wet lane." + +data excl_local_repo_wet_blackjack_shuffle_dissolve: DissolutionCondition = unbound_dissolution(description: "a fixed-octets mock_response lands for Urandom.ReadBytes; then this claim re-enrols as an ordinary hermetic discovery row, drops off local_repo_wet_schedule, and this row deletes") + data excl_local_repo_wet_enrolment_code_dissolve: DissolutionCondition = unbound_dissolution(description: "mock_response coverage lands for shell.Mktemp.DirWithTemplate and the file CAS writes sufficient for the enrolment slot write to be driven under a fixed store, and a fixed-octets mock_response lands for Urandom.ReadBytes; then both fns re-enroll as ordinary hermetic discovery rows, drop off local_repo_wet_schedule, and this row deletes") data excl_local_repo_wet_ntfy_runtime_readback_reason: String = "real host-effect execution witness over the approval broker's enrolment-code root, gunbc.auth.approval_device_enrolment_code issue_device_enrolment_code, which accepts only a release revision and whose first effect is gunbc.auth.approval_ntfy_access_readback approval_ntfy_runtime_reading: READ-ONLY HOST PROCESS READS through shell.Exec.RunArgv (systemctl show, cat of /proc files, getconf, stat, id, the ntfy binary's version and access listing, tailscale serve status, several under sudo -n), for which the hermetic route has no published mock case. None of them writes; the claim asserts the verb refuses before any code is minted and that the store root is never created, and that holds on EVERY host because every reading's verdict is a refusal (a failed or inactive unit, a runtime gap, or -- the claim passing a revision that is never installed -- the per-release process-observation helper's read failing), so admitting it imports no host-conditional red. The same module's second claim runs that helper entry (gunbc.auth.approval_ntfy_runtime_observe approval_ntfy_runtime_observe) for real and asserts its printed outcome decodes through the verb's codec, which holds on every host (a refusal naming its read, or an observation). Every refusal arm is witnessed hermetically over supplied readings in test.claim.approval_ntfy_access_readback_witness_test; this is the one claim that runs the real root. Excluded from the discovery corpus and executed by the required floor's local-repo wet lane (v2.workflow.local_repo_wet_terminal local_repo_wet_schedule)." @@ -1180,6 +1184,12 @@ data witness_exclusion_frontier: List = [ classification: LocalRepoWetLane, reason: excl_local_repo_wet_enrolment_code_reason, dissolution: excl_local_repo_wet_enrolment_code_dissolve}, + WitnessExclusionRow { + pattern: "blackjack_shuffle_wet_witness_test.dag", + classification: LocalRepoWetLane, + reason: excl_local_repo_wet_blackjack_shuffle_reason, + dissolution: excl_local_repo_wet_blackjack_shuffle_dissolve, +}, WitnessExclusionRow { pattern: "approval_ntfy_access_readback_wet_witness_test.dag", classification: LocalRepoWetLane, @@ -1273,6 +1283,7 @@ data witness_exclusion_frontier: List = [ classification: LocalRepoWetLane, reason: excl_local_repo_wet_tun_real_reader_reason, dissolution: excl_local_repo_wet_tun_real_reader_dissolve} + ] fn witness_exclusion_row_is_offline(row: WitnessExclusionRow) -> Bool { diff --git a/dag/test/claim/examples/blackjack_shuffle_wet_witness_test.dag b/dag/test/claim/examples/blackjack_shuffle_wet_witness_test.dag new file mode 100644 index 00000000000..031db3d5fe7 --- /dev/null +++ b/dag/test/claim/examples/blackjack_shuffle_wet_witness_test.dag @@ -0,0 +1,22 @@ +module test.claim.examples.blackjack_shuffle_wet_witness_test + +import examples.blackjack.cards { standard_deck } +import examples.blackjack.shuffle { shuffle, seed_from_octets } +import std.encoding { base64_decode, Standard } +import extdeps.entropy { Urandom } + +test fn wet_entropy_seeded_shuffle_is_standard_deck_permutation_by_real_execution() -> Bool { + match base64_decode( + s: Urandom.ReadBytes(count: 16).octets_b64, + variant: Standard, + ) { + Present { value: octets } => { + let seed = seed_from_octets(octets: octets) + let shoe = shuffle(deck: standard_deck, seed: seed) + + shoe.cards.length() == 52 + && all(standard_deck, card => shoe.cards.contains(card)) + } + Absent => false + } +} \ No newline at end of file diff --git a/dag/test/claim/examples/blackjack_shuffle_witness_test.dag b/dag/test/claim/examples/blackjack_shuffle_witness_test.dag index f188dfff5de..f74b140681b 100644 --- a/dag/test/claim/examples/blackjack_shuffle_witness_test.dag +++ b/dag/test/claim/examples/blackjack_shuffle_witness_test.dag @@ -39,22 +39,4 @@ test fn seed_from_octets_combines_bytes_big_endian() -> Bool { seed_from_octets(octets: octets).value == 258 Absent => false } -} - -test fn wet_entropy_seeded_shuffle_is_standard_deck_permutation() -> Bool { - match base64_decode( - s: Urandom.ReadBytes(count: 160).octets_b64, - variant: Standard, - ) { - Present { value: octets } => { - let seed = seed_from_octets(octets: octets) - let shoe = shuffle(deck: standard_deck, seed: seed) - - shoe.cards.length() == 52 - && all(standard_deck, card => shoe.cards.contains(card)) - } - - Absent => - false - } } \ No newline at end of file diff --git a/src/v2/workflow/local_repo_wet_terminal.dag b/src/v2/workflow/local_repo_wet_terminal.dag index 536251cec66..dc97403ff23 100644 --- a/src/v2/workflow/local_repo_wet_terminal.dag +++ b/src/v2/workflow/local_repo_wet_terminal.dag @@ -321,6 +321,15 @@ fn local_repo_wet_schedule() -> List { function: "the_publish_realizer_reaches_the_heads_tree_in_a_real_repository_by_real_execution", expectation: ExpectedToHold {} }, + WetScheduledClaim { + identity: WitnessIdentity { + module_path: "test.claim.examples.blackjack_shuffle_wet_witness_test", + function: "wet_entropy_seeded_shuffle_is_standard_deck_permutation_by_real_execution", + }, + entry: "dag/test/claim/examples/blackjack_shuffle_wet_witness_test.dag", + function: "wet_entropy_seeded_shuffle_is_standard_deck_permutation_by_real_execution", + expectation: ExpectedToHold {}, + }, WetScheduledClaim { identity: WitnessIdentity { module_path: "test.claim.roadmap.roadmap_belt_base_advance_wet_witness_test", function: "the_base_advance_reaches_the_target_revisions_tree_in_a_real_repository_by_real_execution" }, entry: "dag/test/claim/roadmap/roadmap_belt_base_advance_wet_witness_test.dag",