Summary
if/then/else as a statement containing setStructMember/setMapping/setStorage in branches is not covered by the SupportedStmtFragment grammar in TypedIRCompilerCorrectness.lean. The ite expression form works for pure computations, but control-flow branching with storage-modifying arms has no Layer 2 proof.
Motivation
Nearly every Morpho Blue core function uses this pattern:
-- shares math branching
if assets > 0 then
finalShares := mulDivUp assets (add totalShares_ 1000000) (add totalAssets_ 1)
else
finalAssets := mulDivDown shares (add totalAssets_ 1) (add totalShares_ 1000000)
-- zeroFloorSub pattern
if totalBorrowAssets_ >= finalAssets then
setStructMember marketSlot id "totalBorrowAssets" (sub totalBorrowAssets_ finalAssets)
else
setStructMember marketSlot id "totalBorrowAssets" 0
-- bad debt socialization
if newCollateral == 0 then
setStructMember2 positionSlot id borrower "borrowShares" 0
setStructMember marketSlot id "totalBorrowShares" (sub newTotalBorrowShares badDebtShares)
...
else
setStructMember marketSlot id "totalBorrowShares" newTotalBorrowShares
...
Proposed approach
Add SupportedStmtFragment variants for if/else with supported statement lists in both arms. Once storage writes (#1618) are proved per-statement, the if/else composer needs to handle:
- Condition evaluation (already proved for
ite expressions)
- Each branch as a
SupportedStmtList (recursive)
- State merge at the join point
Impact
- morpho-verity:
accrueInterest (nested if/else with fee logic), all shares-math functions (if/else for assets vs shares path), liquidate (bad debt socialization branch), repay/liquidate (zeroFloorSub pattern)
- General: Any non-trivial contract with conditional state modifications
Related
Summary
if/then/elseas a statement containingsetStructMember/setMapping/setStoragein branches is not covered by theSupportedStmtFragmentgrammar inTypedIRCompilerCorrectness.lean. Theiteexpression form works for pure computations, but control-flow branching with storage-modifying arms has no Layer 2 proof.Motivation
Nearly every Morpho Blue core function uses this pattern:
Proposed approach
Add
SupportedStmtFragmentvariants for if/else with supported statement lists in both arms. Once storage writes (#1618) are proved per-statement, the if/else composer needs to handle:iteexpressions)SupportedStmtList(recursive)Impact
accrueInterest(nested if/else with fee logic), all shares-math functions (if/else for assets vs shares path),liquidate(bad debt socialization branch),repay/liquidate(zeroFloorSub pattern)Related