Quit Handling and Scale-Typed Global Pools in Vegas

[elazarg]

1. What a Vegas game looks like

Vegas programs are written as game blocks. A game either:

• reaches a terminal withdraw { ... } (the only money-moving construct), or
• transfers control to another game (structurally, by inlining; there is no runtime call stack).

A minimal example:

game TakeAll[A | pool$2]() {
  withdraw { A -> 2 }
}

game main() {
  join Alice() $1 Bob() $1;           // instance locks a single pool P
  yield Bob(ok: bool) || TakeAll();   // if Bob quits here, go to TakeAll[Alice]
  withdraw { Alice -> 0; Bob -> 2 }   // normal outcome: Bob takes all
}

Intuition:

• The instance locks a single pool P.
• The program proceeds until it reaches a terminal withdraw.
• At certain points (join/yield/reveal), a role may Quit; || specifies what happens in that case.

main() is the entrypoint game. For now, main has no parameters; later it may, but that is out of scope here.

---

2. Core execution and money model

2.1 One locked global pool; one terminal allocation

A game instance locks a single global pool P when roles join. During gameplay there are no transfers. Money moves only once, at the end:

withdraw { Role1 -> a1; Role2 -> a2; ... }

2.2 Conservation

Defined here: terminal withdrawals must allocate the pool exactly.

• The sum of all payouts in withdraw { ... } must be exactly P.
• There is no implicit burn and no implicit “dust”.

A dedicated burn/sink mechanism may be added later (see Future directions).

---

3. Quit semantics and timeouts

3.1 Quit is a strategic role action

At the language level, Quit is a move made by the role. Whether the real-world cause is strategic abandonment, a timeout, or a connectivity failure is irrelevant to the game-theoretic model in this document.

3.2 Backend timeouts are an implementation mechanism

Backends may implement Quit via:

• explicit on-chain quit actions, and/or
• timeout-triggered forced transitions after a deadline.

The language and analysis treat these as the same: the role has Quit available at that point.

---

4. Handlers: specifying what happens on Quit

Vegas supports Quit handlers only at single-actor sites in this design.

4.1 || selects the Quit continuation

A handler is written with ||:

yield Bob(ok: bool) || TakeAll();

Meaning:

• If Bob provides ok, continue normally.
• If Bob Quits instead, take the handler branch (TakeAll() here).

This is not exception handling and not a “time player”. It is simply “what happens if the role chooses Quit at this point”.

4.2 Supported handler sites

Defined here: handlers are supported only for the following single-actor constructs:

1. join (role fails to join / effectively quits during setup)

join Alice() $1 || Refund();

2. yield (role fails to provide an input)

yield Alice(x: int) || Catch();

3. reveal (role fails to reveal a committed value)

reveal Alice(x) || Catch();

4.3 Availability rule (scope discipline)

Defined here: the handler is typechecked in the environment before the attempted action.

So:

• Values that would have been produced by the attempted action are not in scope in the handler.

Example:

yield Alice(x:int) || { /* x is NOT available here */ ... }

This makes Quit branches well-defined and prevents recovery code from depending on missing inputs/secrets.

4.4 Recipient ambiguity rule

Handlers often redistribute the outcome among remaining roles.

Defined here: whenever it is ambiguous which roles are meant to receive payouts, roles must be passed explicitly. Vegas does not infer recipients “by symmetry” or “by remaining players” in this design.

---

5. Subgames and composition

5.1 Subgames are structural (inlined)

Calling a subgame is not a runtime call. Semantics are defined by inlining into one whole-program control flow. There is no return value; control flow ends when a terminal withdraw is reached.

This design relies on hygienic inlining (renaming to avoid collisions) as a compiler responsibility.

---

6. Scale-typed global pools

This section defines how a game can be written once and instantiated at many stake sizes without rewriting logic.

6.1 Coefficients and a global scale k

Numeric literals in payouts are coefficients. At instantiation time the instance chooses a global scale k > 0, and a literal n denotes n·k units.

6.2 Pool weight annotation pool$W

A game may annotate the required weight of the global pool:

game TakeAll[A | pool$2]() {
  withdraw { A -> 2 }
}

Meaning:

• The instance pool satisfies P = 2·k for some k > 0.
• The withdrawal allocates exactly P.

6.3 Compiler obligations

Defined here: the compiler/backend must ensure:

• k > 0,
• the locked pool P is exactly W·k where W is the declared pool weight,
• every terminal withdraw sums exactly to P (conservation).

In the integer-only setting of this design, this is equivalent to: P divisible by W, with k = P/W.

---

7. Multiple leavers: what is covered vs deferred

7.1 Covered: sequential Quit at single-actor sites

Multiple Quits over time are expressible when they occur at distinct single-actor sites, because each site can have its own handler.

7.2 Deferred: simultaneous actions and staged multi-party failures

Not defined here: Quit handlers for multi-actor “simultaneous” constructs, including commit–reveal protocols where multiple parties may fail at different stages (commit vs reveal).

Reason: once multiple roles can fail within a single conceptual step, a handler must refer to (a) which subset failed and (b) how recipients are chosen among the remaining roles—both require additional surface design (e.g., explicit subset matching and/or symmetry annotations).

Parser/validator rule (recommended):

• The grammar may accept || on simultaneous constructs, but the validator must reject it with a clear error (“handlers currently supported only for single-actor join/yield/reveal; please desugar/unroll”).

---

8. Future directions (non-binding)

These are explicitly not part of the defined design, but are expected extensions:

1. Burn/sink support
   A dedicated BURN recipient (or equivalent) to explicitly destroy value while preserving “withdraw sums exactly to P” as a structural invariant.

2. Simultaneous handlers
   A handler form for multi-actor steps that deliberately provides no access to missing committed/hidden values and can transition to a subgame with fewer participants.

3. Symmetry annotations / inference
   A way to mark subgames as symmetric under permutation of certain roles, allowing safe inference of recipient mapping in otherwise ambiguous handlers.

---

9. Summary

This design defines a compact, compiler-checkable core:

• A single locked global pool P.
• A single terminal withdraw that must allocate exactly P.
• Quit as a role move; timeouts are backend mechanics.
• || handlers for Quit at single-actor join/yield/reveal sites, with a strict availability rule.
• Scale-typed pools (pool$W) so games are written in coefficients and instantiated via a positive scale k.
• No simultaneous-action recovery in this design; it is explicitly deferred.

The result is implementable, analyzable, and avoids ambiguous “who failed / who gets paid” cases until the language has the machinery to express them precisely.

[elazarg]

Possible grammar file:

grammar Vegas;

// Top-level program consists of types, macros, and game definitions.
// 'main' is just a game convention, not a distinct grammar rule.
program : (typeDec | macroDec | gameDec)* EOF ;

// -------------------------------------------------------------------------
// Declarations
// -------------------------------------------------------------------------

typeDec : 'type' name=typeId '=' typeExp ;

macroDec
    : 'macro' name=varId
      '(' (params+=paramDec (',' params+=paramDec)*)? ')'
      ':' resultType=typeExp
      '=' body=exp
      ';'?
    ;

// Functional Game Definition
// Example: game Split[A, B | pool$2](amount: int) { ... }
// Example: game main() { ... }
gameDec
    : 'game' name=(varId | roleId)
      // Optional Configuration Block: Roles and Pool Weight
      ('[' (roles+=roleId (',' roles+=roleId)*)? ('|' 'pool' '$' weight=INT)? ']')?
      // Explicit Parameters (State)
      '(' (params+=paramDec (',' params+=paramDec)*)? ')'
      '{' ext '}'
    ;

paramDec
    : name=varId ':' type=typeExp
    ;

varDec 
    : name=varId ':' hidden='hidden'? type=typeExp
    ;

// -------------------------------------------------------------------------
// Control Flow & Actions (Extensions)
// -------------------------------------------------------------------------

ext 
    : kind=('join' | 'yield' | 'reveal' | 'random') query+ ';' ext   # ReceiveExt
    | 'withdraw' outcome                                             # WithdrawExt
    | tail=gameCall                                                  # TailCallExt
    ;

// A query (action) with optional recovery handler
// Example: yield Alice(x: int) || Refund(10);
query 
    : role=roleId ('(' (decls+=varDec (',' decls+=varDec)*)? ')')? 
      ('$' deposit=INT)? 
      ('where' cond=exp)? 
      ('||' recovery=gameCall)? 
    ;

// Game Transition / Call
// distinct from exp-level calls to allow UpperCase game names (e.g., Refund)
gameCall 
    : callee=(varId | roleId) '(' (args+=exp (',' args+=exp)*)? ')' 
    ;

// -------------------------------------------------------------------------
// Expressions & Types
// -------------------------------------------------------------------------

outcome
    : <assoc=right> cond=exp '?' ifTrue=outcome ':' ifFalse=outcome  # IfOutcome
    | 'let' dec=varDec '=' init=exp 'in' body=outcome                # LetOutcome
    | '(' outcome ')'                                                # ParenOutcome
    | '{' items+=item+ '}'                                           # OutcomeExp
    ;

item : (role=roleId '->' exp ';'?) ;

exp
    : '(' exp ')'                                            # ParenExp
    | role=roleId '.' field=varId                            # MemberExp
    | callee=varId '(' (args+=exp (',' args+=exp)*)?  ')'    # CallExp
    | op=('-' | '!') exp                                     # UnOpExp
    | left=exp op=('*' | '/' | '%') right=exp                # BinOpMultExp
    | left=exp op=('+' | '-') right=exp                      # BinOpAddExp
    | exp op=('!='|'==') 'null'                              # UndefExp
    | left=exp op=('<' | '<=' | '>=' | '>') right=exp        # BinOpCompExp
    | left=exp op=('==' | '!=' | '<->' | '<-!->') right=exp  # BinOpEqExp
    | left=exp op=('&&' | '||') right=exp                    # BinOpBoolExp
    | <assoc=right> cond=exp '?' ifTrue=exp ':' ifFalse=exp  # IfExp
    | ('true'|'false')                                       # BoolLiteralExp
    | name=varId                                             # IdExp
    | INT                                                    # NumLiteralExp
    | ADDRESS                                                # AddressLiteralExp
    | 'let!' dec=varDec '=' init=exp 'in' body=exp           # LetExp
    ;

typeExp
    : '{' vals+=INT (',' vals+=INT)* '}'   # SubsetTypeExp
    | '{' start=INT '..' end=INT '}'       # RangeTypeExp
    | name=typeId                          # IdTypeExp
    ;

// -------------------------------------------------------------------------
// Lexer
// -------------------------------------------------------------------------

typeId: LOWER_ID ;
varId : LOWER_ID ;
roleId: ROLE_ID ;

ROLE_ID: [A-Z][a-zA-Z_0-9]*;
LOWER_ID: [a-z][a-zA-Z_0-9]*;
INT: ([1-9][0-9]* | [0]) ;
ADDRESS: '0x'([1-9a-fA-F][0-9a-fA-F]* | [0]) ;
STRING: '"' ( ~('"'|'\\') )* '"' ;

BlockComment : '/*' .*? '*/' -> skip ;
LineComment : '//' ~[\n]* -> skip ;
WS : [ \t\r\n]+ -> skip;

[elazarg]

Below is Claude's summary, after trying to implement this feature:

Original Motivation
  Blockchain games have inherent timeouts—players can quit or fail to act. When a multi-party step fails because some (not all) participants quit, we need a fair way to distribute funds:
  - split: Survivors get their stake back, plus forfeited deposits divided evenly
  - burn: Survivors get their stake back, forfeited deposits are destroyed
  The key question: Who counts as a "survivor"?
  ---
  The Liveness Predicate
  Definition
  alive(r) = "Role r has fulfilled all their participation obligations"
  This determines who receives payouts when a handler fires.
  The Subtle Case: Commit-Reveal
  For simultaneous actions, we use commit-reveal to prevent front-running:
  yield Alice(x: hidden bool) Bob(y: hidden bool) || split;
  reveal Alice(x) Bob(y);
  Question: If Alice commits but never reveals, is she "alive"?
  Answer: No. A commit is a promise to participate; the reveal is actual participation. Committing garbage you can never reveal is not participation.
  Implication: alive(r) must check reveal completion, not commit completion.
  ---
  Issue 1: Obligation Checking (Straightforward)
  When computing liveness for a handler, we need to check whether obligations were fulfilled.
  Not a Time Machine
  At the point where payoffs are computed, all relevant information exists:
  // For a commit-reveal pair, liveness checks the reveal
  alive(Alice) = IsDefined(Alice.x_revealed)  // Not Alice.x_committed
  This is just conditional branching in the IR—no temporal paradox.
  Encoding Approach
  Track which fields represent obligations vs. fulfillments:
  - COMMIT visibility → creates obligation
  - REVEAL visibility → fulfills obligation
  - PUBLIC visibility → immediate participation (no obligation)
  Liveness only counts REVEAL and PUBLIC completions.
  ---
  Issue 2: Where Does the Handler Fire? (The Time Machine)
  The Scenario
  yield Alice(x: hidden bool) || split;   // Step 1: Alice commits
  yield Bob(y: bool) || split;             // Step 2: Bob acts
  reveal Alice(x);                         // Step 3: Alice should reveal
  Alice commits at Step 1 (creating an obligation), then fails to reveal at Step 3.
  The Question
  Alice's failure to reveal means she didn't truly participate at Step 1. Semantically, Step 1's handler should fire—but execution has already passed Step 1.
  This is the time machine problem: discovering at Step 3 that Step 1's handler should have fired.
  Why It's Hard
  1. Bob already acted at Step 2, assuming the game continued past Step 1
  2. If Step 1's handler had fired immediately, Bob might never have acted
  3. We can't retroactively undo Bob's action
  Possible Approaches
  A. Handler fires at the reveal step, not the commit step
  Reframe: "Alice failed to reveal" is a failure at Step 3, not Step 1. The reveal step's handler catches it.
  Limitation: What if there's no handler on the reveal step?
  B. Commit step's handler has deferred trigger conditions
  The handler on Step 1 is defined to fire if:
  - Alice doesn't commit, OR
  - Alice commits but later fails to reveal
  Implementation: All handlers defer resolution to game end, checking full obligation state.
  C. Restrict handler placement
  Prohibit handlers on steps that create obligations (commits) unless the reveal is in the same concurrent step.
  // Allowed: concurrent commit-reveal
  yield Alice(x: hidden bool) Bob(y: hidden bool) || split;
  // Prohibited: handler on commit with separate reveal
  yield Alice(x: hidden bool) || split;  // ERROR
  reveal Alice(x);
  ---
  Design Considerations
  What Needs to Be Decided
  1. Liveness semantics: Confirm that alive(r) requires reveal completion for commit-reveal pairs (Issue 1—this seems clearly correct)
  2. Handler trigger semantics: When obligation fails, which step's handler fires? (Issue 2—requires design choice)
  3. Placement restrictions: Should we limit where handlers can appear to avoid the time machine?
  Trade-offs
  | Approach                 | Expressiveness | Complexity | User Surprise                                 |
  |--------------------------|----------------|------------|-----------------------------------------------|
  | Reveal-step handler only | Lower          | Low        | Medium ("why can't I put handler on commit?") |
  | Deferred resolution      | Higher         | High       | Low                                           |
  | Restrict placement       | Lower          | Low        | Medium                                        |
  Recommendation
  Start with restricted placement (approach C):
  - Handlers only on steps where all participants have PUBLIC or REVEAL visibility
  - No handlers on pure COMMIT steps with pending reveals
  - Clear, predictable semantics
  If expressiveness is needed later, add deferred resolution.
  ---
  Key Takeaways
  1. Commit ≠ Participation: A commit creates an obligation; only reveal fulfills it. Liveness must respect this.
  2. Two separate problems: Obligation checking (straightforward encoding) vs. handler trigger location (semantic design choice).
  3. The time machine is real: If obligation failure should trigger the obligation-creating step's handler, we need deferred resolution or must accept that Bob acted under false assumptions.
  4. Restriction is a valid choice: Limiting handler placement avoids the time machine entirely, at cost of some expressiveness.
  5. This affects subgames too: If subgames can be invoked as handlers, the same obligation/liveness questions apply to subgame entry conditions.

[elazarg]

idea:
commit is a dedicated instruction, not only a type.
the value has a type +exists obligation + terminating handler (or continuation)

problem: two commit handlers might fire at once.
policy: earlier wins. commit handlers (including for simultaneous commits) should be completely ordered.

[elazarg]

Design Document: Security Bond (Liveness Penalty)

1. Abstract

The Security Bond is a protocol-level mechanism that enforces incentive compatibility in Vegas games by requiring each role to post a separate collateral that is strictly at risk for Liveness Failures (e.g., ghosting, timing out, withholding required information, or failing to discharge a protocol obligation).

This cleanly separates:

• the financial risk of losing the game (the game deposit / pot), from
• the financial penalty of breaking the protocol (the security bond).

As a result, rational players prefer honest play or an explicit, protocol-supported Fair Quit over malicious or strategic abandonment.

This document is written to be compatible with the Gas Bank (Automated Progress Reimbursement) mechanism (#47). The Security Bond is a stick for liveness; the Gas Bank is a lubricant to remove "gas cost" as an excuse to stall.

---

2. Motivation

2.1 The "Nothing at Stake" problem

In many cryptographic protocols and games (e.g., Vickrey auctions, poker-like commit/reveal games), a player can find themselves in a losing position where their best move is to stop cooperating.

• Example: In a sealed-bid auction, a bidder may refuse to reveal a commitment after learning (or suspecting) they are disadvantaged.
• Current failure mode: If the only penalty is losing part of the game deposit, then the penalty interacts with the game’s handler logic (split, null, etc.), which can unintentionally make cheating profitable or partially refunded.

The key pathology is conflation: losing the game vs violating the protocol.

2.2 The "Rational Apathy" problem

If ghosting has low penalty, players effectively gain a free option to abort whenever the outcome looks unfavorable. This breaks game-theoretic properties and makes equilibrium analysis meaningless, because "quitting" becomes a dominant strategic move in many states.

2.3 Design goal

We want:

1. Protocol integrity: liveness failures are always punished, regardless of game payout logic.
2. Composability: game designers can write payoffs and handlers without accidentally weakening liveness incentives.
3. Clean analysis: strategies are evaluated primarily on game payoffs, not on runtime or protocol-abuse loopholes.
4. Compatibility with cost reimbursement: players should not be able to justify ghosting because "execution costs too much", when the system supports Gas Bank reimbursement.

---

3. Model: Two-deposit system (separation of concerns)

Each role’s funds are split into distinct buckets with different seizure rules.

3.1 Game Deposit ($)

• Purpose: the "pot": bets, transfers, game outcomes.
• Seizure condition: game logic (who wins/loses), including user-defined handlers.
• Handler interaction: if a player times out and the protocol triggers a timeout handler, the game deposit is processed by the handler (split, null, etc.). This is intentional: it is part of the game definition.

3.2 Security Bond (@bond)

• Purpose: protocol integrity (liveness + obligation discharge).

• Seizure condition: liveness failure:

  • failure to act within timeout windows when obligated,
  • failure to discharge obligations by game end,
  • providing invalid protocol data when obligated (e.g., bad reveal).

• Handler interaction: never processed by game handlers. It is purely system-level.

Rationale for strict separation: game handlers exist to define fair economic outcomes under game-defined contingencies; they should not define or weaken punishment for protocol violations.

---

4. Obligations and liveness failures (what the bond is "insuring")

The protocol defines a set of obligations that roles incur as play progresses. Examples:

• Reveal obligation after a commit.
• Response obligation in dispute/verification subprotocols.
• Close/withdraw obligation (if the protocol requires a role to finalize a step to let others proceed).
• Any action that must be performed by a specific role to keep the state machine live.

A liveness failure occurs when:

1. an obligation becomes due and is not discharged before timeout, or
2. the game reaches a state where the role still has outstanding obligations (unfinished commitments / unresolved protocol steps).

This is intentionally broader than "timeout was called"; it targets the meaning (protocol stuck due to that role) rather than a specific runtime trigger.

---

5. Mechanism lifecycle

5.1 Initialization (Join)

On joining, the player deposits:

• GameDeposit → credited to game balances/pot.
• SecurityBond → credited to bonds[role].

The bond is locked and cannot be used for bets, transfers, or ordinary game outcomes.

5.2 Active play

The bond remains locked while the role is "still potentially obligated" by the protocol.

Important compatibility note (with Gas Bank):
The bond is not used for reimbursement. It is a penalty collateral. If the Gas Bank feature is enabled, it has its own progress-collateral accounting.

5.3 Termination and bond resolution states

State A: Protocol completion (Honest play)

The role has discharged all obligations and can no longer be asked by the protocol to do anything.

• Outcome: bonds[role] is returned to the role.

Revised precision:
The bond is returned only when the protocol can conclude the role is in a no-future-obligations state. In the simplest implementation this means "at terminal state". More refined implementations may return earlier if the compiler can certify a "done" region for that role.

Motivation: If we return the bond merely after one successful reveal, the role could still ghost later when a new obligation arises.

State B: Fair Quit (Explicit impossibility / surrender)

The role cannot or will not continue but chooses a protocol-defined escape hatch (e.g., impossible) that keeps the protocol live by explicitly signaling defeat and enabling closure.

• Outcome: bonds[role] is returned to the role.
• Game outcome: determined by the impossible handler (game-defined).

Rationale: the player did not break liveness; they completed the protocol by choosing an explicit, analyzable exit.

State C: Liveness failure (Cheating / ghosting / withholding)

The role fails to act when obligated, or the game ends with obligations unfulfilled.

• Outcome: bonds[role] is seized unconditionally.
• Game deposit: resolved by game handlers (e.g., timeout handler), independently.

Rationale: the role imposed costs and uncertainty on others and violated the protocol state machine.

---

6. Seizure mechanics: where does seized bond value go?

A seized bond must create strong incentives to:

1. call the timeout / close (so games don’t linger), and
2. avoid creating a new side jackpot that incentivizes censorship/grief.

6.1 Default: bounded keeper bounty + remainder sink

When a bond is seized due to a liveness failure:

• Priority 1: Keeper bounty

  • Pay the caller of the timeout/close function a bounded bounty sufficient to cover execution cost plus margin.
  • This incentivizes third parties (keepers) and/or opponents to close the game.

• Priority 2: Remainder

  • The remainder is burned or donated to protocol treasury (default), or
  • optionally routed to a designated sink (e.g., a public goods address).

Why not pay the full bond to the opponent?
Because it creates a griefing / censorship incentive: opponents may attempt to prevent timely transactions to force a timeout and collect the bond. Burning/donation avoids turning the bond into an opponent-controlled bounty pot.

6.2 Interaction with Gas Bank collateral (normative rule)

If the Gas Bank feature is enabled (progress reimbursement), then on liveness failure by role r:

• the remaining security bond is seized (this document),
• and the remaining Gas Bank collateral for role r is also seized into the same liveness-failure pool,
• the keeper bounty is paid once (not double-dipped),
• remainder is burned/donated (or sinked), as above.

Motivation: otherwise, a player could ghost while still reclaiming unused "progress collateral", weakening the penalty and reintroducing "cheap ghosting".

---

7. Syntax

The join statement accepts a secondary bond amount:

game Auction() {
  // Player puts $100 into the pot, and posts a $50 bond for protocol integrity.
  join Bidder() $100 @bond $50;

  // If Bidder fails to reveal:
  // 1) bond ($50) is seized by system rules (keeper bounty + burn/donate remainder)
  // 2) game deposit ($100) is handled by the game-defined handler (e.g., split/null)
  reveal Bidder(bid: int) || split;
  ...
}

---

8. Interaction with @expensive and impossible

Some obligations may be expensive (e.g., ZK proofs, heavy computations, or off-chain burdens). Vegas may allow marking an obligation as @expensive and providing a impossible handler:

reveal Prover(x: int)
  where @expensive check(x)
  || impossible {
    // Fair Quit: bond returned, but game logic applies:
    Prover -> 0; Verifier -> 100;
  };

Rule:

• impossible is the only protocol-defined escape that:

  • preserves liveness, and
  • returns the bond.

Absent impossible, failing an expensive obligation counts as liveness failure and seizes the bond (because the protocol became stuck due to that role).

Motivation: This forces protocol designers to make "expensive steps" explicit, and gives players an analyzable, honest exit rather than incentivizing silent abandonment.

---

9. Backend implementation (EVM example)

This section is illustrative. The design itself is chain-agnostic: it requires (a) a bond store, (b) timeout closure, (c) obligation tracking.

9.1 Storage

mapping(Role => uint256) public bonds;   // bond in wei (separate from game funds)
mapping(Role => bool) public obligated;  // simplified; real impl tracks obligations per action

(If Gas Bank is enabled, it has its own storage and is integrated at seizure time per Section 6.2.)

9.2 Discharging obligations and releasing bond

Do not release the bond merely because "the current step succeeded."
Release only when the role is in a compiler-certified "no-future-obligations" state (or at terminal state).

Illustrative snippet:

function dischargeReveal(Role r, int x, uint salt) internal {
    require(hash(x, salt) == commitments[r], "Bad reveal");
    obligated[r] = false;
    // bond is NOT necessarily returned here
}

function finalize(Role r) internal {
    require(noFutureObligations(r), "still obligated"); // compiler-defined condition
    uint256 b = bonds[r];
    bonds[r] = 0;
    (bool ok,) = payable(roleAddress[r]).call{value: b}("");
    require(ok, "bond refund failed");
}

9.3 Timeout: seizing bond + bounded bounty

function timeout(Role r) public {
    require(block.timestamp > deadline[r], "Too early");
    require(isObligationOverdue(r), "No overdue obligation");

    uint256 b = bonds[r];
    bonds[r] = 0;

    uint256 bounty = keeperBounty(); // bounded, policy-defined
    uint256 pay = b < bounty ? b : bounty;

    // Pay keeper
    (bool ok1,) = payable(msg.sender).call{value: pay}("");
    require(ok1, "bounty pay failed");

    // Burn/donate remainder
    uint256 rem = b - pay;
    if (rem > 0) {
        (bool ok2,) = payable(TREASURY_OR_BURN).call{value: rem}("");
        require(ok2, "sink pay failed");
    }

    // Trigger game-defined handler for game deposit (split/null/etc)
    runTimeoutHandler(r);
}

Notes:

• Use call, not transfer. Prefer pull-payments for maximum robustness.
• The "bounty" should be bounded and not scale linearly with bond size, to avoid turning bond into a jackpot.

---

10. Security considerations

1. Bond must dominate the incentive to ghost
   Bond sizing is part of protocol design. If bond is tiny relative to the value of stalling/withholding, the mechanism fails economically (even if correct technically).

2. No premature bond release
   The bond must remain locked until the role is provably unable to create future liveness failures.

3. Avoid opponent jackpot
   Paying full seized bond to the opponent incentivizes adversarial "timeout forcing" behaviors (including censorship). Default burn/donate + bounded keeper bounty avoids this.

4. Compatibility with Gas Bank
   If Gas Bank exists, remaining progress collateral for a liveness-failing role should be seized alongside the bond (Section 6.2), or else ghosting becomes cheaper.

---

11. Summary

The Security Bond enforces protocol integrity by making liveness failures strictly costly, independently of game payoff logic. By separating the pot from the protocol penalty, Vegas games preserve clean game-theoretic meaning: players compete over the game deposit, but they must respect the protocol to recover their bond.

The design is compatible with the Gas Bank mechanism: Gas Bank removes execution cost as an excuse to stall; the bond punishes stalling anyway. The only critical integration requirements are:

• don’t return bonds prematurely,
• avoid double-paying keepers,
• seize remaining progress collateral on liveness failure.