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 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 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/examples/blackjack/shuffle.dag b/dag/examples/blackjack/shuffle.dag index b1dc2b382e8..2f6455ed333 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 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 + octet) % 2147483648, + ) + } +} diff --git a/dag/examples/blackjack/simulation.dag b/dag/examples/blackjack/simulation.dag index 7e2669e8c3b..f9cf3214529 100644 --- a/dag/examples/blackjack/simulation.dag +++ b/dag/examples/blackjack/simulation.dag @@ -7,4 +7,335 @@ module examples.blackjack.simulation // 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. -type Strategy = HitBelow { threshold: Int } + +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, shuffle, next_seed } + +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 RoundPlay + = RoundPlayed { round: SimulatedRound } + | RoundPlayRefused { cause: RoundRefusal } + +type BlackjackSimulation + = SimulationCompleted { rounds: List } + | SimulationRefused { + round_index: Int + seed: ShuffleSeed + cause: RoundRefusal + } + +type SimulationSummary { + rounds: Int + player_wins: Int + dealer_wins: Int + pushes: Int + player_blackjacks: Int + player_busts: Int +} + +type SeededShoe { + seed: ShuffleSeed + shoe: Shoe +} + +fn choose(strategy: Strategy, player: Hand) -> PlayerAction { + match strategy { + HitBelow { threshold: threshold } => + if hand_value(hand: player).total < threshold { + PlayerHits + } else { + 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/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_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 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 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 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 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 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",