From 3753c546fdfeac406a565b653aead33f04e5479a Mon Sep 17 00:00:00 2001 From: Stevengre Date: Tue, 23 Sep 2025 16:46:58 +0800 Subject: [PATCH 1/9] P-TOKEN-HOTFIX: Conversions between [u8;8] and u64 --- .../kdist/mir-semantics/lemmas/kmir-lemmas.md | 10 +++- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 53 +++++++++++++++++++ .../kdist/mir-semantics/symbolic/p-token.md | 10 +++- 3 files changed, 71 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md index 5dbd60d37..6feadad80 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -119,10 +119,18 @@ power of two but the semantics will always operate with these particular ones. rule bitmask32 => ( 1 < ( 1 < ( 1 < true [simplification, smt-lemma] +rule [int-and-255-lt-256]: _ &Int 255 true [simplification, smt-lemma] +``` + ```k endmodule ``` \ No newline at end of file diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 78bf6d132..692ac78c5 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1067,6 +1067,30 @@ Type casts between a number of different types exist in MIR. ```k syntax Evaluation ::= #cast( Evaluation, CastKind, MaybeTy, Ty ) [strict(1)] + syntax Evaluation ::= castAux ( Value, CastKind, MaybeTypeInfo, TypeInfo ) [function] + syntax MaybeTypeInfo ::= "Maybe" "(" TypeInfo ")" | "TypeInfoUnknown" + // ---------------------------------------------------------------- + rule #cast(VAL, CASTKIND, TyUnknown, TY_TARGET) + => castAux(VAL, CASTKIND, TypeInfoUnknown, {TYPEMAP[TY_TARGET]}:>TypeInfo) + // castAux handles the actual casting + ... + + TYPEMAP + requires TY_TARGET in_keys(TYPEMAP) + andBool isTypeInfo(TYPEMAP[TY_TARGET]) + [priority(160), preserves-definedness] + // low priority, because this is only for writing simplification rules for now + // valid map lookups checked + rule #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET) + => castAux(VAL, CASTKIND, Maybe({TYPEMAP[TY_SOURCE]}:>TypeInfo), {TYPEMAP[TY_TARGET]}:>TypeInfo) + // castAux handles the actual casting + ... + + TYPEMAP + requires TY_SOURCE in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_SOURCE]) + andBool TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) + [priority(160), preserves-definedness] + ``` ### Number Type Casts @@ -1279,6 +1303,35 @@ What can be supported without additional layout consideration is trivial casts b andBool TY_TARGET in_keys(TYPEMAP) andBool TYPEMAP[TY_SOURCE] ==K TYPEMAP[TY_TARGET] [preserves-definedness] // valid map lookups checked + + // Transmute from [u8; 8] to u64 + rule #cast(Range(ListItem(Integer(B0:Int, 8, false)) + ListItem(Integer(B1:Int, 8, false)) + ListItem(Integer(B2:Int, 8, false)) + ListItem(Integer(B3:Int, 8, false)) + ListItem(Integer(B4:Int, 8, false)) + ListItem(Integer(B5:Int, 8, false)) + ListItem(Integer(B6:Int, 8, false)) + ListItem(Integer(B7:Int, 8, false))), + castKindTransmute, + _TY_SOURCE, + TY_TARGET) + => Integer(B0 +Int (B1 < + TYPEMAP + requires TY_TARGET in_keys(TYPEMAP) + andBool {TYPEMAP[TY_TARGET]}:>TypeInfo ==K typeInfoPrimitiveType(primTypeUint(uintTyU64)) + andBool 0 <=Int B0 andBool B0 #asU8List(.List, X) + rule #asU8s(X) => #asU8List(.List, X) [concrete] rule #asU8List(ACC, _) => ACC requires 8 <=Int size(ACC) [priority(40)] // always cut at 8 bytes rule #asU8List(ACC, X) => #asU8List( ACC ListItem(Integer( X &Int 255, 8, false)) , X >>Int 8) [preserves-definedness] + // mapping an offset over bytes produced by #asU8s has no effect + rule #mapOffset(#asU8s(X), _) => #asU8s(X) [simplification, preserves-definedness] + + // Shortcut transmute: [u8; 8] (from #asU8s) to u64 + rule castAux(Range(#asU8s(X)), castKindTransmute, _TY_SOURCE, TY_TARGET) => Integer(X, 64, false) + requires TY_TARGET ==K typeInfoPrimitiveType(primTypeUint(uintTyU64)) + [simplification, preserves-definedness] + rule toAmount(fromAmount(AMT)) => AMT [simplification, preserves-definedness] rule fromAmount(toAmount(VAL)) => VAL [simplification, preserves-definedness] From 2e86a00f0d74eab90c75184899a6eff9629b0b0b Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 25 Sep 2025 09:30:57 +0800 Subject: [PATCH 2/9] add symbolic attribute to => castAux rules --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 692ac78c5..4fa6a012d 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1078,7 +1078,7 @@ Type casts between a number of different types exist in MIR. TYPEMAP requires TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) - [priority(160), preserves-definedness] + [priority(160), preserves-definedness, symbolic] // low priority, because this is only for writing simplification rules for now // valid map lookups checked rule #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET) @@ -1089,7 +1089,7 @@ Type casts between a number of different types exist in MIR. TYPEMAP requires TY_SOURCE in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_SOURCE]) andBool TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) - [priority(160), preserves-definedness] + [priority(160), preserves-definedness, symbolic] ``` From 2aa8c0c80f935167e50412e96cc9551d858096d8 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 25 Sep 2025 11:11:37 +0800 Subject: [PATCH 3/9] constraint symbolic with symbolic(VAL) --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 4fa6a012d..eb1d60e36 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1078,7 +1078,7 @@ Type casts between a number of different types exist in MIR. TYPEMAP requires TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) - [priority(160), preserves-definedness, symbolic] + [priority(160), preserves-definedness, symbolic(VAL)] // low priority, because this is only for writing simplification rules for now // valid map lookups checked rule #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET) @@ -1089,7 +1089,7 @@ Type casts between a number of different types exist in MIR. TYPEMAP requires TY_SOURCE in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_SOURCE]) andBool TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) - [priority(160), preserves-definedness, symbolic] + [priority(160), preserves-definedness, symbolic(VAL)] ``` From efb8dd9ca166370102fbd4db55135830bf4b17a8 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 25 Sep 2025 11:25:54 +0800 Subject: [PATCH 4/9] add concrete Bs --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 1 + 1 file changed, 1 insertion(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index eb1d60e36..c7a3594a4 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1332,6 +1332,7 @@ What can be supported without additional layout consideration is trivial casts b andBool 0 <=Int B5 andBool B5 Date: Thu, 25 Sep 2025 11:45:13 +0800 Subject: [PATCH 5/9] remove the rule for `Transmute from [u8; 8] to u64` --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 30 -------------------- 1 file changed, 30 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index c7a3594a4..b29ed69fc 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1303,36 +1303,6 @@ What can be supported without additional layout consideration is trivial casts b andBool TY_TARGET in_keys(TYPEMAP) andBool TYPEMAP[TY_SOURCE] ==K TYPEMAP[TY_TARGET] [preserves-definedness] // valid map lookups checked - - // Transmute from [u8; 8] to u64 - rule #cast(Range(ListItem(Integer(B0:Int, 8, false)) - ListItem(Integer(B1:Int, 8, false)) - ListItem(Integer(B2:Int, 8, false)) - ListItem(Integer(B3:Int, 8, false)) - ListItem(Integer(B4:Int, 8, false)) - ListItem(Integer(B5:Int, 8, false)) - ListItem(Integer(B6:Int, 8, false)) - ListItem(Integer(B7:Int, 8, false))), - castKindTransmute, - _TY_SOURCE, - TY_TARGET) - => Integer(B0 +Int (B1 < - TYPEMAP - requires TY_TARGET in_keys(TYPEMAP) - andBool {TYPEMAP[TY_TARGET]}:>TypeInfo ==K typeInfoPrimitiveType(primTypeUint(uintTyU64)) - andBool 0 <=Int B0 andBool B0 Date: Thu, 25 Sep 2025 11:47:03 +0800 Subject: [PATCH 6/9] `no-evaluators` for castAux --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index b29ed69fc..37385d3c1 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1067,7 +1067,7 @@ Type casts between a number of different types exist in MIR. ```k syntax Evaluation ::= #cast( Evaluation, CastKind, MaybeTy, Ty ) [strict(1)] - syntax Evaluation ::= castAux ( Value, CastKind, MaybeTypeInfo, TypeInfo ) [function] + syntax Evaluation ::= castAux ( Value, CastKind, MaybeTypeInfo, TypeInfo ) [function, no-evaluators] syntax MaybeTypeInfo ::= "Maybe" "(" TypeInfo ")" | "TypeInfoUnknown" // ---------------------------------------------------------------- rule #cast(VAL, CASTKIND, TyUnknown, TY_TARGET) From 59b756ca706918b174eaf011ea8237080bd15401 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 25 Sep 2025 12:12:38 +0800 Subject: [PATCH 7/9] simplify MaybeTypeInfo --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 37385d3c1..d6cd87ade 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1068,7 +1068,7 @@ Type casts between a number of different types exist in MIR. ```k syntax Evaluation ::= #cast( Evaluation, CastKind, MaybeTy, Ty ) [strict(1)] syntax Evaluation ::= castAux ( Value, CastKind, MaybeTypeInfo, TypeInfo ) [function, no-evaluators] - syntax MaybeTypeInfo ::= "Maybe" "(" TypeInfo ")" | "TypeInfoUnknown" + syntax MaybeTypeInfo ::= TypeInfo | "TypeInfoUnknown" // ---------------------------------------------------------------- rule #cast(VAL, CASTKIND, TyUnknown, TY_TARGET) => castAux(VAL, CASTKIND, TypeInfoUnknown, {TYPEMAP[TY_TARGET]}:>TypeInfo) @@ -1082,7 +1082,7 @@ Type casts between a number of different types exist in MIR. // low priority, because this is only for writing simplification rules for now // valid map lookups checked rule #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET) - => castAux(VAL, CASTKIND, Maybe({TYPEMAP[TY_SOURCE]}:>TypeInfo), {TYPEMAP[TY_TARGET]}:>TypeInfo) + => castAux(VAL, CASTKIND, {TYPEMAP[TY_SOURCE]}:>TypeInfo, {TYPEMAP[TY_TARGET]}:>TypeInfo) // castAux handles the actual casting ... From 026f3ba9d453575e0c433c5e37de744becb59fc6 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 25 Sep 2025 18:20:25 +0800 Subject: [PATCH 8/9] delete the rule that causes the long CI problem --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index d6cd87ade..17b1f4229 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1081,15 +1081,15 @@ Type casts between a number of different types exist in MIR. [priority(160), preserves-definedness, symbolic(VAL)] // low priority, because this is only for writing simplification rules for now // valid map lookups checked - rule #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET) - => castAux(VAL, CASTKIND, {TYPEMAP[TY_SOURCE]}:>TypeInfo, {TYPEMAP[TY_TARGET]}:>TypeInfo) - // castAux handles the actual casting - ... - - TYPEMAP - requires TY_SOURCE in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_SOURCE]) - andBool TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) - [priority(160), preserves-definedness, symbolic(VAL)] + // rule #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET) + // => castAux(VAL, CASTKIND, {TYPEMAP[TY_SOURCE]}:>TypeInfo, {TYPEMAP[TY_TARGET]}:>TypeInfo) + // // castAux handles the actual casting + // ... + // + // TYPEMAP + // requires TY_SOURCE in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_SOURCE]) + // andBool TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) + // [priority(160), preserves-definedness, symbolic(VAL)] ``` From 4527a0930ddcf43ecc422058476fad1b3b0b57b4 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 26 Sep 2025 10:35:54 +0800 Subject: [PATCH 9/9] remove the useless `symbolic` attribute. Introduce concrete rule for castAux for thunk --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 23 ++++++++++---------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 17b1f4229..0de30d00d 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1078,19 +1078,20 @@ Type casts between a number of different types exist in MIR. TYPEMAP requires TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) - [priority(160), preserves-definedness, symbolic(VAL)] + [priority(160), preserves-definedness] // low priority, because this is only for writing simplification rules for now // valid map lookups checked - // rule #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET) - // => castAux(VAL, CASTKIND, {TYPEMAP[TY_SOURCE]}:>TypeInfo, {TYPEMAP[TY_TARGET]}:>TypeInfo) - // // castAux handles the actual casting - // ... - // - // TYPEMAP - // requires TY_SOURCE in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_SOURCE]) - // andBool TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) - // [priority(160), preserves-definedness, symbolic(VAL)] - + rule #cast(VAL, CASTKIND, TY_SOURCE:Ty, TY_TARGET) + => castAux(VAL, CASTKIND, {TYPEMAP[TY_SOURCE]}:>TypeInfo, {TYPEMAP[TY_TARGET]}:>TypeInfo) + // castAux handles the actual casting + ... + + TYPEMAP + requires TY_SOURCE in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_SOURCE]) + andBool TY_TARGET in_keys(TYPEMAP) andBool isTypeInfo(TYPEMAP[TY_TARGET]) + [priority(160), preserves-definedness] + rule castAux(VAL, CASTKIND, TYPE_SOURCE, TYPE_TARGET) => thunk(castAux(VAL, CASTKIND, TYPE_SOURCE, TYPE_TARGET)) [concrete] + // thunk to avoid re-evaluation of castAux ``` ### Number Type Casts