cboddeposit-00-deposit-kernel.spp

cboddeposit/calculation/cboddeposit-00-deposit-kernel.spp

Download original file · Bank deposit source contents

1domain cboddeposit;23// Source-derived KSADEP0 4110/4111 and balance formulas in 4150.4// Account is an immutable input snapshot; plan contains proposed changes.56Role DepositRequest {7    BigDecimal(19, 2) amount;8    String currency;9    int valueDate;10}1112Role DepositAccount {13    String accountNumber;14    quantum BigDecimal(19, 2) interestBase;15    quantum BigDecimal(19, 2) frozenAmount;16    quantum BigDecimal(19, 2) authorizedAmount;17    quantum BigDecimal(19, 2) overdraftInterest;18    quantum BigDecimal(19, 2) collectionInterest;19    quantum BigDecimal(19, 2) overdraftPrincipal;20    quantum BigDecimal(19, 2) overdraftExposure;21    LoanState loanState; // Normal, BadDebt, WrittenOff: decoded business states, not deployment flags.22}2324Role DepositPlan {25    BigDecimal(19, 2) interestPaid;26    BigDecimal(19, 2) collectionInterestPaid;27    BigDecimal(19, 2) principalPaid;28    BigDecimal(19, 2) newInterestBase;29    BigDecimal(19, 2) newAvailableBalance;30    BigDecimal(19, 2) newOverdraftExposure;31    BigDecimal(19, 2) newAccountBalance;32    BigDecimal(19, 2) interestBaseIncrease;33    BigDecimal(19, 2) interestBaseDecrease;34}3536atomic check checkKernelInput(DepositRequest) {37    require(DepositRequest.amount >= 0, "E1095");38}3940atomic calculate calculateDepositPlan(DepositRequest, DepositAccount, DepositPlan) {41    boolean principalFirst = DepositAccount.loanState == LoanState.BAD_DEBT42        || DepositAccount.loanState == LoanState.WRITTEN_OFF;43    BigDecimal remaining = DepositRequest.amount + DepositAccount.interestBase - DepositAccount.frozenAmount;44    DepositPlan.interestPaid = 0;45    DepositPlan.collectionInterestPaid = 0;46    DepositPlan.principalPaid = 0;47    DepositPlan.newOverdraftExposure = DepositAccount.overdraftExposure;48    if (remaining > 0) {49        if (principalFirst) {50            DepositPlan.principalPaid = min(remaining, DepositAccount.overdraftPrincipal);51            if (remaining <= DepositAccount.overdraftPrincipal) {52                DepositPlan.newOverdraftExposure = max(53                    0,54                    DepositAccount.overdraftExposure - DepositPlan.principalPaid55                );56            } else {57                DepositPlan.newOverdraftExposure = 0;58            }59            remaining -= DepositPlan.principalPaid;60        }61        DepositPlan.interestPaid = min(remaining, DepositAccount.overdraftInterest);62        remaining -= DepositPlan.interestPaid;63        DepositPlan.collectionInterestPaid = min(remaining, DepositAccount.collectionInterest);64        remaining -= DepositPlan.collectionInterestPaid;65        if (!principalFirst && remaining > 0) {66            DepositPlan.principalPaid = min(remaining, DepositAccount.overdraftPrincipal);67            if (remaining <= DepositAccount.overdraftPrincipal) {68                DepositPlan.newOverdraftExposure = max(69                    0,70                    DepositAccount.overdraftExposure - DepositPlan.principalPaid71                );72            } else {73                DepositPlan.newOverdraftExposure = 0;74            }75            remaining -= DepositPlan.principalPaid;76        }77    }78    DepositPlan.newInterestBase = DepositAccount.interestBase79        + DepositRequest.amount80        - DepositPlan.interestPaid81        - DepositPlan.collectionInterestPaid82        - DepositPlan.principalPaid;83    DepositPlan.newAvailableBalance = max(84        0,85        DepositPlan.newInterestBase - DepositAccount.frozenAmount - DepositAccount.authorizedAmount86    );87    DepositPlan.newAccountBalance = DepositPlan.newInterestBase88        - (DepositAccount.overdraftInterest89        - DepositPlan.interestPaid)90        - (DepositAccount.collectionInterest91        - DepositPlan.collectionInterestPaid)92        - (DepositAccount.overdraftPrincipal93        - DepositPlan.principalPaid);94    DepositPlan.interestBaseIncrease = max(0, DepositPlan.newInterestBase - DepositAccount.interestBase);95    DepositPlan.interestBaseDecrease = max(0, DepositAccount.interestBase - DepositPlan.newInterestBase);96}9798atomic check checkPlan(DepositRequest, DepositAccount, DepositPlan) {99    // Derived arithmetic invariant, rather than DepositAccount new claim about COBOL checks.100    require(101        DepositPlan.newAccountBalance == DepositAccount.interestBase102            - DepositAccount.overdraftInterest103            - DepositAccount.collectionInterest104            - DepositAccount.overdraftPrincipal105            + DepositRequest.amount,106        "net balance invariant"107    );108}109110take BankAccount as DepositAccount {111    mapsame;112}