From 22d8848aa905950ce1a4fa392324bb83f41fe437 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 19 Dec 2025 14:27:30 +0800 Subject: [PATCH 1/2] feat(spl): simplify rent minimum_balance float calculation Add a K rule to directly simplify the rent exemption threshold pattern `(int)((float)PRODUCT * 2.0)` to `PRODUCT * 2`, avoiding intermediate float thunks during symbolic execution. --- .../kdist/mir-semantics/symbolic/spl-token.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md index 8f7b3505c..1a7e7f208 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -533,6 +533,22 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami [preserves-definedness] ``` +## Rent minimum_balance calculation simplification + +The rent exemption check involves: `(int)((float)(data_len * lamports_per_byte_year) * 2.0)` +Since float casts create thunks, we simplify this pattern directly to `PRODUCT * 2`. + +```k + // Simplify: (int)((float)PRODUCT * 2.0) => PRODUCT * 2 + rule #cast( + thunk(#applyBinOp(binOpMul, + thunk(#cast(Integer(PRODUCT:Int, 64, false), castKindIntToFloat, _TY1, _TY2)), + Float(0.20000000000000000e1, 64), + false)), + castKindFloatToInt, _TY3, _TY4) + => Integer(PRODUCT *Int 2, 64, false) +``` + ```k endmodule ``` From 0e79d2a60eff4df0f9d027f3fba6e46a204465c5 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 19 Dec 2025 18:17:07 +0800 Subject: [PATCH 2/2] round-trip track --- kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md index 1a7e7f208..ecc009c64 100644 --- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md +++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md @@ -542,10 +542,10 @@ Since float casts create thunks, we simplify this pattern directly to `PRODUCT * // Simplify: (int)((float)PRODUCT * 2.0) => PRODUCT * 2 rule #cast( thunk(#applyBinOp(binOpMul, - thunk(#cast(Integer(PRODUCT:Int, 64, false), castKindIntToFloat, _TY1, _TY2)), + thunk(#cast(Integer(PRODUCT:Int, 64, false), castKindIntToFloat, INT_TY, FLOAT_TY)), Float(0.20000000000000000e1, 64), false)), - castKindFloatToInt, _TY3, _TY4) + castKindFloatToInt, FLOAT_TY, INT_TY) => Integer(PRODUCT *Int 2, 64, false) ```