Marcus (agent-cos)
1cbad9d756
- x in someSet → someSet.has(x) - x in someMap.keys → someMap.has(x) - x notIn someMap.keys → !someMap.has(x) - m[k] → m.get(k) for Map state variables - s.size() → s.size (property, not method) - Track Map-typed state variables via mapVarNames for accurate .get() translation - Thread mapVarNames through emitAction and rewriteExpr All 41 tests passing. TigerBeetleLedger now generates correct TypeScript with .get() for Map access and .has() for Set membership. Part of M0.1: Fix TS generator bugs (speckl#18)
143 lines
12 KiB
TypeScript
143 lines
12 KiB
TypeScript
// Auto-generated by speckl-compile from TigerBeetleLedger
|
|
// DO NOT EDIT MANUALLY — regenerate from .speckdl source
|
|
|
|
export const TigerBeetleLedgerState = {
|
|
Open: 'open',
|
|
Closed: 'closed',
|
|
} as const;
|
|
export type TigerBeetleLedgerState = typeof TigerBeetleLedgerState[keyof typeof TigerBeetleLedgerState];
|
|
|
|
|
|
|
|
|
|
export class TigerBeetleLedgerMachine {
|
|
accounts: Map<number, Account>;
|
|
transfers: Map<number, Transfer>;
|
|
pending: Set<number>;
|
|
replicaState: Map<number, Replica>;
|
|
log: LogEntry[];
|
|
commitIndex: number;
|
|
leader: number;
|
|
decisionLog: any[] = [];
|
|
|
|
constructor() {
|
|
// No init block defined
|
|
}
|
|
|
|
CreateTransfer(t: Transfer) {
|
|
// precondition: !this.transfers.has(t.id)
|
|
if (!(!this.transfers.has(t.id))) throw new Error('Precondition failed: !this.transfers.has(t.id)');
|
|
// precondition: this.accounts.has(t.from)
|
|
if (!(this.accounts.has(t.from))) throw new Error('Precondition failed: this.accounts.has(t.from)');
|
|
// precondition: this.accounts.has(t.to)
|
|
if (!(this.accounts.has(t.to))) throw new Error('Precondition failed: this.accounts.has(t.to)');
|
|
// precondition: t.from != t.to
|
|
if (!(t.from != t.to)) throw new Error('Precondition failed: t.from != t.to');
|
|
// precondition: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft
|
|
if (!(this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft)) throw new Error('Precondition failed: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft');
|
|
// postcondition: this.transfers.get(t.id) == t
|
|
if (!(this.transfers.get(t.id) == t)) throw new Error('Postcondition failed: this.transfers.get(t.id) == t');
|
|
// postcondition: this.pending == new Set([...this.pending, t.id])
|
|
if (!(this.pending == new Set([...this.pending, t.id]))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending, t.id])');
|
|
// postcondition: this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount
|
|
if (!(this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.from).debits_pending == this.accounts.get(t.from).debits_pending + t.amount');
|
|
// postcondition: this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount
|
|
if (!(this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.to).credits_pending == this.accounts.get(t.to).credits_pending + t.amount');
|
|
}
|
|
|
|
CommitTransfer(id: number) {
|
|
// precondition: this.pending.has(id)
|
|
if (!(this.pending.has(id))) throw new Error('Precondition failed: this.pending.has(id)');
|
|
// precondition: this.transfers.has(id)
|
|
if (!(this.transfers.has(id))) throw new Error('Precondition failed: this.transfers.has(id)');
|
|
// precondition: this.transfers.get(id).pending == true
|
|
if (!(this.transfers.get(id).pending == true)) throw new Error('Precondition failed: this.transfers.get(id).pending == true');
|
|
// postcondition: this.pending == new Set([...this.pending].filter(x => x !== id))
|
|
if (!(this.pending == new Set([...this.pending].filter(x => x !== id)))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending].filter(x => x !== id))');
|
|
// postcondition: this.transfers.get(id).pending == false
|
|
if (!(this.transfers.get(id).pending == false)) throw new Error('Postcondition failed: this.transfers.get(id).pending == false');
|
|
// postcondition: this.transfers.get(id).posted == true
|
|
if (!(this.transfers.get(id).posted == true)) throw new Error('Postcondition failed: this.transfers.get(id).posted == true');
|
|
// postcondition: this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted
|
|
if (!(this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_posted === this.accounts.get(this.transfers.get(id).from).debits_posted');
|
|
// postcondition: this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted
|
|
if (!(this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_posted === this.accounts.get(this.transfers.get(id).to).credits_posted');
|
|
// postcondition: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending
|
|
if (!(this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending');
|
|
// postcondition: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending
|
|
if (!(this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending');
|
|
}
|
|
|
|
VoidTransfer(id: number) {
|
|
// precondition: this.pending.has(id)
|
|
if (!(this.pending.has(id))) throw new Error('Precondition failed: this.pending.has(id)');
|
|
// precondition: this.transfers.has(id)
|
|
if (!(this.transfers.has(id))) throw new Error('Precondition failed: this.transfers.has(id)');
|
|
// precondition: this.transfers.get(id).pending == true
|
|
if (!(this.transfers.get(id).pending == true)) throw new Error('Precondition failed: this.transfers.get(id).pending == true');
|
|
// postcondition: this.pending == new Set([...this.pending].filter(x => x !== id))
|
|
if (!(this.pending == new Set([...this.pending].filter(x => x !== id)))) throw new Error('Postcondition failed: this.pending == new Set([...this.pending].filter(x => x !== id))');
|
|
// postcondition: this.transfers.get(id).pending == false
|
|
if (!(this.transfers.get(id).pending == false)) throw new Error('Postcondition failed: this.transfers.get(id).pending == false');
|
|
// postcondition: this.transfers.get(id).voided == true
|
|
if (!(this.transfers.get(id).voided == true)) throw new Error('Postcondition failed: this.transfers.get(id).voided == true');
|
|
// postcondition: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending
|
|
if (!(this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).from).debits_pending === this.accounts.get(this.transfers.get(id).from).debits_pending');
|
|
// postcondition: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending
|
|
if (!(this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending)) throw new Error('Postcondition failed: this.accounts.get(this.transfers.get(id).to).credits_pending === this.accounts.get(this.transfers.get(id).to).credits_pending');
|
|
}
|
|
|
|
PostTransfer(t: Transfer) {
|
|
// precondition: !this.transfers.has(t.id)
|
|
if (!(!this.transfers.has(t.id))) throw new Error('Precondition failed: !this.transfers.has(t.id)');
|
|
// precondition: this.accounts.has(t.from)
|
|
if (!(this.accounts.has(t.from))) throw new Error('Precondition failed: this.accounts.has(t.from)');
|
|
// precondition: this.accounts.has(t.to)
|
|
if (!(this.accounts.has(t.to))) throw new Error('Precondition failed: this.accounts.has(t.to)');
|
|
// precondition: t.from != t.to
|
|
if (!(t.from != t.to)) throw new Error('Precondition failed: t.from != t.to');
|
|
// precondition: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft
|
|
if (!(this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft)) throw new Error('Precondition failed: this.accounts.get(t.from).balance >= t.amount || this.accounts.get(t.from).flags.allows_overdraft');
|
|
// postcondition: this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false }
|
|
if (!(this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false })) throw new Error('Postcondition failed: this.transfers.get(t.id) == { ...t, pending: false, posted: true, voided: false }');
|
|
// postcondition: this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount
|
|
if (!(this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.from).debits_posted == this.accounts.get(t.from).debits_posted + t.amount');
|
|
// postcondition: this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount
|
|
if (!(this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount)) throw new Error('Postcondition failed: this.accounts.get(t.to).credits_posted == this.accounts.get(t.to).credits_posted + t.amount');
|
|
}
|
|
|
|
BecomeLeader(replica: number, term: number) {
|
|
// precondition: this.replicaState.has(replica)
|
|
if (!(this.replicaState.has(replica))) throw new Error('Precondition failed: this.replicaState.has(replica)');
|
|
// precondition: this.replicaState.get(replica).role == "candidate"
|
|
if (!(this.replicaState.get(replica).role == "candidate")) throw new Error('Precondition failed: this.replicaState.get(replica).role == "candidate"');
|
|
// precondition: this.replicaState.get(replica).currentTerm < term
|
|
if (!(this.replicaState.get(replica).currentTerm < term)) throw new Error('Precondition failed: this.replicaState.get(replica).currentTerm < term');
|
|
// postcondition: this.leader == replica
|
|
if (!(this.leader == replica)) throw new Error('Postcondition failed: this.leader == replica');
|
|
// postcondition: this.replicaState.get(replica).role == "this.leader"
|
|
if (!(this.replicaState.get(replica).role == "this.leader")) throw new Error('Postcondition failed: this.replicaState.get(replica).role == "this.leader"');
|
|
// postcondition: this.replicaState.get(replica).currentTerm == term
|
|
if (!(this.replicaState.get(replica).currentTerm == term)) throw new Error('Postcondition failed: this.replicaState.get(replica).currentTerm == term');
|
|
}
|
|
|
|
AppendEntry(entry: LogEntry, term: number) {
|
|
// precondition: entry.index == length(this.log) + 1
|
|
if (!(entry.index == length(this.log) + 1)) throw new Error('Precondition failed: entry.index == length(this.log) + 1');
|
|
// precondition: term >= this.commitIndex
|
|
if (!(term >= this.commitIndex)) throw new Error('Precondition failed: term >= this.commitIndex');
|
|
// postcondition: this.log == append(this.log, entry)
|
|
if (!(this.log == append(this.log, entry))) throw new Error('Postcondition failed: this.log == append(this.log, entry)');
|
|
// postcondition: this.commitIndex == entry.index
|
|
if (!(this.commitIndex == entry.index)) throw new Error('Postcondition failed: this.commitIndex == entry.index');
|
|
}
|
|
|
|
|
|
|
|
// V1: Always(AccountBalanceInvariant)
|
|
async verify1(): Promise<boolean> {
|
|
// TODO: Model-check or monitor
|
|
// Temporal: Always(AccountBalanceInvariant)
|
|
return true;
|
|
}
|
|
}
|