ledger

Demo repo for lean-refine — autonomous code hardening via Lean formalization and IES optimization.

What it does

refine ledger-repo discovers five invariants the code assumes but doesn't enforce:

1. Balances must be numeric (passing a string silently corrupts arithmetic)
2. Transfer amounts must be positive (negative amounts reverse direction silently)
3. Accounts can't be duplicated (create_account silently overwrites existing balances)
4. Transfers require both accounts to exist (missing target debits source then crashes, losing money)
5. Self-transfers are meaningless (works by accident, breaks on any refactor)

Lean formalization surfaces these by forcing explicit type declarations (e.g., defining Balance with val : Nat makes negativity structurally impossible, revealing that the Python code allows it silently).

Result

IES: 0.0476 → 1.0000 (perfect score) in 12 iterations, 0 discards.

Iteration	IES	Change	Description	Code
0	0.05	—	Baseline: 6 unguarded, 1 convention	—
1	0.24	+0.19	Account existence check in transfer (also caught atomicity)	L52-53
2	0.33	+0.10	Account existence check in balance	L57-58
3	0.43	+0.10	Transfer amount positivity check	L16-17
4	0.48	+0.05	Atomic dict rebuild for transfer	L54
5	0.57	+0.10	Account overwrite protection	L45-46
6	0.67	+0.10	Self-transfer prevention	L30-31
7	0.71	+0.05	Runtime isinstance type checks	L5-6, L14-15
8	0.76	+0.05	Balance class (structural type safety)	L1-7
9	0.81	+0.05	PositiveAmount class (structural positivity)	L10-18
10	0.86	+0.05	setdefault (structural overwrite protection)	L47
11	0.90	+0.05	TransferRequest class (structural self-transfer)	L26-35
12	1.00	+0.10	AccountRef type (structural account existence)	L21-23, L50, L56

All 7 invariants structural. 20 tests passing. Artifacts in .lean-refine/ with Lean formalization, frozen harness, results TSV, and iteration log.

Before

src/ledger.py

class Ledger:
    def __init__(self):
        self.accounts = {}

    def create_account(self, account_id, opening_balance):
        self.accounts[account_id] = opening_balance

    def transfer(self, from_id, to_id, amount):
        self.accounts[from_id] -= amount
        self.accounts[to_id] += amount

    def balance(self, account_id):
        return self.accounts[account_id]

After

src/ledger.py

class Balance:
    __slots__ = ("value",)

    def __init__(self, value: int | float) -> None:
        if not isinstance(value, (int, float)):
            raise TypeError("value must be numeric")
        self.value = value


class PositiveAmount:
    __slots__ = ("value",)

    def __init__(self, value: int | float) -> None:
        if not isinstance(value, (int, float)):
            raise TypeError("amount must be numeric")
        if value <= 0:
            raise ValueError("amount must be positive")
        self.value = value


class AccountRef(str):
    """Verified account identifier obtained from create_account."""
    pass


class TransferRequest:
    __slots__ = ("from_id", "to_id", "amount")

    def __init__(self, from_id: str, to_id: str, amount: int | float) -> None:
        if from_id == to_id:
            raise ValueError("cannot transfer to same account")
        PositiveAmount(amount)
        self.from_id = from_id
        self.to_id = to_id
        self.amount = amount


class Ledger:
    def __init__(self):
        self.accounts = {}

    def create_account(self, account_id: str, opening_balance: int | float) -> AccountRef:
        Balance(opening_balance)
        ref = AccountRef(account_id)
        if ref in self.accounts:
            raise ValueError("account already exists")
        self.accounts.setdefault(ref, opening_balance)
        return ref

    def transfer(self, from_id: AccountRef, to_id: AccountRef, amount: int | float) -> None:
        request = TransferRequest(from_id, to_id, amount)
        if request.from_id not in self.accounts or request.to_id not in self.accounts:
            raise ValueError("account does not exist")
        self.accounts = {**self.accounts, request.from_id: self.accounts[request.from_id] - request.amount, request.to_id: self.accounts[request.to_id] + request.amount}

    def balance(self, account_id: AccountRef):
        if account_id not in self.accounts:
            raise ValueError("account does not exist")
        return self.accounts[account_id]