From 9e81b90f467f9b0ee1926aac32a033c40cd3b518 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 13 Nov 2025 13:10:18 +1000 Subject: [PATCH 1/8] Added test for transmuting integer to fieldless enum This test should fail the test suite as it thunks, but doesn't due to a hack rule that was introduced. This rule stops the thunk from occurring. --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 18 +++++++++++++++++- .../data/prove-rs/transmute-u8-to-enum.rs | 15 +++++++++++++++ 2 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index a3d30ac5d..d386f3ea2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1499,7 +1499,8 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. Another specialisation is getting the discriminant of `enum`s without fields after converting some integer data to it (see `#discriminant` and `rvalueDiscriminant`). -If none of the `enum` variants has any fields, the `Transmute` of a number to the `enum` data is necessarily just the discriminant itself., and can be returned as the integer value afgter adjusting to the byte length of the discriminant: +If none of the `enum` variants has any fields, the `Transmute` of a number to the `enum` data is necessarily just the discriminant itself., and can be returned as the integer value after adjusting to the byte length of the discriminant: + ```k rule #discriminant( @@ -1516,6 +1517,21 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th rule #isEnumWithoutFields(_OTHER) => false [owise] ``` +```k + rule + #cast( Integer ( VAL , 8 , false ) , castKindTransmute , _TY_FROM , TY_TO ) + => + Aggregate( variantIdx(VAL) , .List ) + ... + + requires #isEnumWithoutFields(lookupTy(TY_TO)) andBool #validDiscriminant(VAL, lookupTy(TY_TO)) + + syntax Bool ::= #validDiscriminant ( Int , TypeInfo ) [function, total] + // ------------------------------------------------------------------ + rule #validDiscriminant( VAL , typeInfoEnumType(_, _, DISCRIMINANTS, _, _) ) => variantIdx(VAL) ==K #findVariantIdx(VAL, DISCRIMINANTS) + rule #validDiscriminant(_, _) => false [owise] +``` + ### Other casts involving pointers diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum.rs b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum.rs new file mode 100644 index 000000000..631e08845 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum.rs @@ -0,0 +1,15 @@ +#[repr(u8)] +#[derive(Clone, Copy, Debug, PartialEq)] +pub enum AccountState { + Uninitialized, + Initialized, + Frozen, +} + +fn main() { + unsafe { + assert_eq!(core::mem::transmute::(0), AccountState::Uninitialized); + assert_eq!(core::mem::transmute::(1), AccountState::Initialized); + assert_eq!(core::mem::transmute::(2), AccountState::Frozen); + } +} From 0bca0e93f9e6869532ec7ee7b1755efce54e3e46 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 13 Nov 2025 15:16:34 +1000 Subject: [PATCH 2/8] Added some validation that the cast is same size and signedness --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 43 ++++++++++++++++++-- 1 file changed, 40 insertions(+), 3 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index d386f3ea2..5824d802c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1519,17 +1519,54 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th ```k rule - #cast( Integer ( VAL , 8 , false ) , castKindTransmute , _TY_FROM , TY_TO ) + #cast( Integer ( VAL , WIDTH , SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) => Aggregate( variantIdx(VAL) , .List ) ... - requires #isEnumWithoutFields(lookupTy(TY_TO)) andBool #validDiscriminant(VAL, lookupTy(TY_TO)) + requires #isEnumWithoutFields(lookupTy(TY_TO)) + andBool #tagCompatible(WIDTH, SIGNED, lookupTy(TY_TO)) + andBool #validDiscriminant(VAL, lookupTy(TY_TO)) syntax Bool ::= #validDiscriminant ( Int , TypeInfo ) [function, total] - // ------------------------------------------------------------------ + // ---------------------------------------------------------------------------- rule #validDiscriminant( VAL , typeInfoEnumType(_, _, DISCRIMINANTS, _, _) ) => variantIdx(VAL) ==K #findVariantIdx(VAL, DISCRIMINANTS) rule #validDiscriminant(_, _) => false [owise] + + syntax Bool ::= #tagCompatible ( Int, Bool, TypeInfo ) [function, total] + // ---------------------------------------------------------------------- + rule #tagCompatible( + WIDTH, + SIGNED, + typeInfoEnumType(... + name: _ + , adtDef: _ + , discriminants: _ + , fields: _ + , layout: + someLayoutShape(layoutShape(... + fields: _ + , variants: + variantsShapeMultiple( + mk(... + tag: scalarInitialized( + mk(... + value: primitiveInt(mk(... length: TAG_WIDTH, signed: TAG_SIGNED)) + , validRange: _ + ) + ) + , tagEncoding: _ + , tagField: _ + , variants: _ + ) + ) + , abi: _ + , abiAlign: _ + , size: _ + )) + ) + ) => WIDTH ==Int #byteLength(TAG_WIDTH) andBool SIGNED ==Bool TAG_SIGNED + rule #tagCompatible( _ , _ , _ ) => false [owise] ``` From dbce69af35c1bc8c0f926976cce33871aadcf4dc Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 13 Nov 2025 19:48:15 +1000 Subject: [PATCH 3/8] Added symbolic test to show unsound branch --- .../prove-rs/transmute-try-from-symbolic.rs | 40 +++++++++++++++++++ .../src/tests/integration/test_integration.py | 1 + 2 files changed, 41 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs b/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs new file mode 100644 index 000000000..617589302 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs @@ -0,0 +1,40 @@ +use std::convert::TryFrom; + +pub enum ProgramError { + InvalidAccountData +} + +#[repr(u8)] +#[derive(Clone, Copy, Debug, PartialEq)] +pub enum AccountState { + Uninitialized, + Initialized, + Frozen, +} + +impl TryFrom for AccountState { + type Error = ProgramError; + + #[inline(always)] + fn try_from(value: u8) -> Result { + match value { + // SAFETY: `value` is guaranteed to be in the range of the enum variants. + 0..=2 => Ok(unsafe { core::mem::transmute::(value) }), + _ => Err(ProgramError::InvalidAccountData), + } + } +} + +fn main() { + num_into_state(0); +} + +fn num_into_state(arg: u8) { + let state: Result = AccountState::try_from(arg); + + if arg <= 2 { + assert!(state.is_ok()); + } else { + assert!(state.is_err()); + } +} \ No newline at end of file diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 4bdd55b39..21920bf99 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -37,6 +37,7 @@ 'assume-cheatcode': ['check_assume'], 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], + 'transmute-try-from-symbolic': ['num_into_state'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', From 4e010d479ab80801016b17545c2aa1f97097471b Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 14 Nov 2025 01:31:40 +1000 Subject: [PATCH 4/8] Added tests and corrected rules: - Corrected rules to check discriminant is valid; - Aggregate returned uses the discriminant to look up the variant; - Added error condition to prevent thunk if discriminant is invalid; - Added fail and passing tests; --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 33 ++++++++- ...from-symbolic-fail.num_into_state.expected | 70 +++++++++++++++++++ .../transmute-u8-to-enum-fail.main.expected | 15 ++++ ...rs => transmute-try-from-symbolic-fail.rs} | 2 +- ...ansmute-u8-to-enum-changed-discriminant.rs | 15 ++++ .../prove-rs/transmute-u8-to-enum-fail.rs | 15 ++++ .../src/tests/integration/test_integration.py | 4 +- 7 files changed, 149 insertions(+), 5 deletions(-) create mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute-try-from-symbolic-fail.num_into_state.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected rename kmir/src/tests/integration/data/prove-rs/{transmute-try-from-symbolic.rs => transmute-try-from-symbolic-fail.rs} (99%) create mode 100644 kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-fail.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 5824d802c..22b478de0 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1518,20 +1518,47 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th ``` ```k + // Rough as but I just want to stop it thunking + syntax Value ::= "#UBErrorInvalidDiscriminantsInEnumCast" + rule + #cast( Integer ( VAL , _WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) ~> _REST + => + #UBErrorInvalidDiscriminantsInEnumCast + + requires #isEnumWithoutFields(lookupTy(TY_TO)) + andBool notBool #validDiscriminant(VAL, lookupTy(TY_TO)) + rule #cast( Integer ( VAL , WIDTH , SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) => - Aggregate( variantIdx(VAL) , .List ) + Aggregate( #findVariantIdxFromTy( VAL, lookupTy(TY_TO) ) , .List ) ... requires #isEnumWithoutFields(lookupTy(TY_TO)) andBool #tagCompatible(WIDTH, SIGNED, lookupTy(TY_TO)) andBool #validDiscriminant(VAL, lookupTy(TY_TO)) + syntax VariantIdx ::= #findVariantIdxFromTy ( Int , TypeInfo ) [function, total] + //------------------------------------------------------------------------------ + rule #findVariantIdxFromTy( VAL , typeInfoEnumType(_, _, DISCRIMINANTS, _, _) ) => #findVariantIdx( VAL, DISCRIMINANTS) + rule #findVariantIdxFromTy( _ , _ ) => err("NotAnEnum") [owise] + syntax Bool ::= #validDiscriminant ( Int , TypeInfo ) [function, total] // ---------------------------------------------------------------------------- - rule #validDiscriminant( VAL , typeInfoEnumType(_, _, DISCRIMINANTS, _, _) ) => variantIdx(VAL) ==K #findVariantIdx(VAL, DISCRIMINANTS) - rule #validDiscriminant(_, _) => false [owise] + rule #validDiscriminant( VAL , typeInfoEnumType(_, _, DISCRIMINANTS, _, _) ) => #validDiscriminantAux( VAL , DISCRIMINANTS ) + rule #validDiscriminant( _ , _ ) => false [owise] + + syntax Bool ::= #validDiscriminantAux ( Int , Discriminants ) [function, total] + // ---------------------------------------------------------------------------- + rule #validDiscriminantAux( VAL, discriminant(DISCRIMINANT) _REST ) => true + requires VAL ==Int DISCRIMINANT + rule #validDiscriminantAux( VAL, discriminant(mirInt(DISCRIMINANT)) _REST ) => true + requires VAL ==Int DISCRIMINANT + rule #validDiscriminantAux( VAL, discriminant(DISCRIMINANT) REST ) => #validDiscriminantAux( VAL, REST ) + requires VAL =/=Int DISCRIMINANT + rule #validDiscriminantAux( VAL, discriminant(mirInt(DISCRIMINANT)) REST ) => #validDiscriminantAux( VAL, REST ) + requires VAL =/=Int DISCRIMINANT + rule #validDiscriminantAux( _VAL, .Discriminants ) => false syntax Bool ::= #tagCompatible ( Int, Bool, TypeInfo ) [function, total] // ---------------------------------------------------------------------- diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-try-from-symbolic-fail.num_into_state.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-try-from-symbolic-fail.num_into_state.expected new file mode 100644 index 000000000..7f76635a1 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute-try-from-symbolic-fail.num_into_state.expected @@ -0,0 +1,70 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (65 steps) +├─ 3 (split) +│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) +┃ +┃ (branch) +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ notBool ARG_UINT1:Int <=Int 2 +┃ │ +┃ ├─ 4 +┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) +┃ │ +┃ │ (144 steps) +┃ ├─ 6 (terminal) +┃ │ #EndProgram ~> .K +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ #EndProgram ~> .K +┃ +┗━━┓ subst: .Subst + ┃ constraint: + ┃ ARG_UINT1:Int <=Int 2 + │ + ├─ 5 + │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) + │ + │ (12 steps) + ├─ 7 (split) + │ #cast ( Integer ( ARG_UINT1:Int , 8 , false ) , castKindTransmute , ty ( 9 ) , t + │ span: 72 + ┃ + ┃ (branch) + ┣━━┓ subst: .Subst + ┃ ┃ constraint: + ┃ ┃ #validDiscriminantAux ( ARG_UINT1:Int , discriminant ( 0 ) discriminant ( 1 ) discriminant ( 2 ) .Discriminants ) + ┃ │ + ┃ ├─ 8 + ┃ │ #cast ( Integer ( ARG_UINT1:Int , 8 , false ) , castKindTransmute , ty ( 9 ) , t + ┃ │ span: 72 + ┃ │ + ┃ │ (125 steps) + ┃ ├─ 10 (terminal) + ┃ │ #EndProgram ~> .K + ┃ │ + ┃ ┊ constraint: true + ┃ ┊ subst: ... + ┃ └─ 2 (leaf, target, terminal) + ┃ #EndProgram ~> .K + ┃ + ┗━━┓ subst: .Subst + ┃ constraint: + ┃ notBool #validDiscriminantAux ( ARG_UINT1:Int , discriminant ( 0 ) discriminant ( 1 ) discriminant ( 2 ) .Discriminants ) + │ + ├─ 9 + │ #cast ( Integer ( ARG_UINT1:Int , 8 , false ) , castKindTransmute , ty ( 9 ) , t + │ span: 72 + │ + │ (1 step) + └─ 11 (stuck, leaf) + #UBErrorInvalidDiscriminantsInEnumCast ~> .K + + + diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected new file mode 100644 index 000000000..28c85a672 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (13 steps) +└─ 3 (stuck, leaf) + #UBErrorInvalidDiscriminantsInEnumCast ~> .K + function: main + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs b/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic-fail.rs similarity index 99% rename from kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs rename to kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic-fail.rs index 617589302..c32a1118d 100644 --- a/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs +++ b/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic-fail.rs @@ -37,4 +37,4 @@ fn num_into_state(arg: u8) { } else { assert!(state.is_err()); } -} \ No newline at end of file +} diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant.rs b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant.rs new file mode 100644 index 000000000..9b7464adc --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant.rs @@ -0,0 +1,15 @@ +#[repr(u8)] +#[derive(Clone, Copy, Debug, PartialEq)] +pub enum AccountState { + Uninitialized = 11, + Initialized = 22, + Frozen = 33, +} + +fn main() { + unsafe { + assert_eq!(core::mem::transmute::(11), AccountState::Uninitialized); + assert_eq!(core::mem::transmute::(22), AccountState::Initialized); + assert_eq!(core::mem::transmute::(33), AccountState::Frozen); + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-fail.rs new file mode 100644 index 000000000..de873f9cb --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-fail.rs @@ -0,0 +1,15 @@ +#[repr(u8)] +#[derive(Clone, Copy, Debug, PartialEq)] +pub enum AccountState { + Uninitialized, + Initialized, + Frozen, +} + +fn main() { + unsafe { + std::hint::black_box( + core::mem::transmute::(4) + ); + } +} diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 21920bf99..ee502b7d9 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -37,7 +37,7 @@ 'assume-cheatcode': ['check_assume'], 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], - 'transmute-try-from-symbolic': ['num_into_state'], + 'transmute-try-from-symbolic-fail': ['num_into_state'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', @@ -54,6 +54,8 @@ 'niche-enum', 'assume-cheatcode-conflict-fail', 'raw-ptr-cast-fail', + 'transmute-u8-to-enum-fail', + 'transmute-try-from-symbolic-fail', ] From 830e45c2bfcda0a74095d673e5765d6486d423d4 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 14 Nov 2025 15:11:30 +1000 Subject: [PATCH 5/8] Removed `#tagCompatible` and special rule for discriminants with thunk --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 50 +------------------- 1 file changed, 2 insertions(+), 48 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 22b478de0..f8d5e0a1d 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1503,23 +1503,13 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th ```k - rule #discriminant( - thunk(#cast (Integer(DATA, _, false), castKindTransmute, _, TY)), - TY - ) => Integer(DATA, 0, false) // HACK: bit width 0 means "flexible" - ... - - requires #isEnumWithoutFields(lookupTy(TY)) - syntax Bool ::= #isEnumWithoutFields ( TypeInfo ) [function, total] // ---------------------------------------------------------------- rule #isEnumWithoutFields(typeInfoEnumType(_, _, _, FIELDSS, _)) => #noFields(FIELDSS) rule #isEnumWithoutFields(_OTHER) => false [owise] -``` -```k // Rough as but I just want to stop it thunking - syntax Value ::= "#UBErrorInvalidDiscriminantsInEnumCast" + syntax Evaulation ::= "#UBErrorInvalidDiscriminantsInEnumCast" rule #cast( Integer ( VAL , _WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) ~> _REST => @@ -1529,13 +1519,12 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th andBool notBool #validDiscriminant(VAL, lookupTy(TY_TO)) rule - #cast( Integer ( VAL , WIDTH , SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) + #cast( Integer ( VAL , _WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) // TODO: CONVERT SIGNED => Aggregate( #findVariantIdxFromTy( VAL, lookupTy(TY_TO) ) , .List ) ... requires #isEnumWithoutFields(lookupTy(TY_TO)) - andBool #tagCompatible(WIDTH, SIGNED, lookupTy(TY_TO)) andBool #validDiscriminant(VAL, lookupTy(TY_TO)) syntax VariantIdx ::= #findVariantIdxFromTy ( Int , TypeInfo ) [function, total] @@ -1559,41 +1548,6 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th rule #validDiscriminantAux( VAL, discriminant(mirInt(DISCRIMINANT)) REST ) => #validDiscriminantAux( VAL, REST ) requires VAL =/=Int DISCRIMINANT rule #validDiscriminantAux( _VAL, .Discriminants ) => false - - syntax Bool ::= #tagCompatible ( Int, Bool, TypeInfo ) [function, total] - // ---------------------------------------------------------------------- - rule #tagCompatible( - WIDTH, - SIGNED, - typeInfoEnumType(... - name: _ - , adtDef: _ - , discriminants: _ - , fields: _ - , layout: - someLayoutShape(layoutShape(... - fields: _ - , variants: - variantsShapeMultiple( - mk(... - tag: scalarInitialized( - mk(... - value: primitiveInt(mk(... length: TAG_WIDTH, signed: TAG_SIGNED)) - , validRange: _ - ) - ) - , tagEncoding: _ - , tagField: _ - , variants: _ - ) - ) - , abi: _ - , abiAlign: _ - , size: _ - )) - ) - ) => WIDTH ==Int #byteLength(TAG_WIDTH) andBool SIGNED ==Bool TAG_SIGNED - rule #tagCompatible( _ , _ , _ ) => false [owise] ``` From a31513c95468bfda28e1f574f977779ec217746d Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 14 Nov 2025 15:12:26 +1000 Subject: [PATCH 6/8] Changed `#validDiscriminantAux` to process disjunction to avoid branch --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index f8d5e0a1d..02b32dfa5 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1539,14 +1539,8 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th syntax Bool ::= #validDiscriminantAux ( Int , Discriminants ) [function, total] // ---------------------------------------------------------------------------- - rule #validDiscriminantAux( VAL, discriminant(DISCRIMINANT) _REST ) => true - requires VAL ==Int DISCRIMINANT - rule #validDiscriminantAux( VAL, discriminant(mirInt(DISCRIMINANT)) _REST ) => true - requires VAL ==Int DISCRIMINANT - rule #validDiscriminantAux( VAL, discriminant(DISCRIMINANT) REST ) => #validDiscriminantAux( VAL, REST ) - requires VAL =/=Int DISCRIMINANT - rule #validDiscriminantAux( VAL, discriminant(mirInt(DISCRIMINANT)) REST ) => #validDiscriminantAux( VAL, REST ) - requires VAL =/=Int DISCRIMINANT + rule #validDiscriminantAux( VAL, discriminant(mirInt(DISCRIMINANT)) REST ) => VAL ==Int DISCRIMINANT orBool #validDiscriminantAux( VAL, REST ) + rule #validDiscriminantAux( VAL, discriminant( DISCRIMINANT ) REST ) => VAL ==Int DISCRIMINANT orBool #validDiscriminantAux( VAL, REST ) rule #validDiscriminantAux( _VAL, .Discriminants ) => false ``` From c1aff197bfeaf481340b30e5d4ef98c819e936c1 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 14 Nov 2025 19:08:22 +1000 Subject: [PATCH 7/8] Changed rules to work with unsigned numbers and added some more tests - `#cast` uses `truncate` similar to `SwitchInt`; - Added test cases with negative discriminant; - Added test cases with positive discriminant and negative value; - Signed discriminants test fails but for unrelated reason I believe. --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 10 +-- ...from-symbolic-fail.num_into_state.expected | 70 ------------------- ...ged-discriminant-signed-fail.main.expected | 15 ++++ ...fail.rs => transmute-try-from-symbolic.rs} | 0 ...o-enum-changed-discriminant-signed-fail.rs | 20 ++++++ ...ansmute-u8-to-enum-changed-discriminant.rs | 11 ++- .../src/tests/integration/test_integration.py | 3 +- 7 files changed, 50 insertions(+), 79 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute-try-from-symbolic-fail.num_into_state.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected rename kmir/src/tests/integration/data/prove-rs/{transmute-try-from-symbolic-fail.rs => transmute-try-from-symbolic.rs} (100%) create mode 100644 kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 02b32dfa5..1f911091f 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1511,21 +1511,21 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th // Rough as but I just want to stop it thunking syntax Evaulation ::= "#UBErrorInvalidDiscriminantsInEnumCast" rule - #cast( Integer ( VAL , _WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) ~> _REST + #cast( Integer ( VAL , WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) ~> _REST => #UBErrorInvalidDiscriminantsInEnumCast requires #isEnumWithoutFields(lookupTy(TY_TO)) - andBool notBool #validDiscriminant(VAL, lookupTy(TY_TO)) + andBool notBool #validDiscriminant( truncate(VAL, WIDTH, Unsigned) , lookupTy(TY_TO) ) rule - #cast( Integer ( VAL , _WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) // TODO: CONVERT SIGNED + #cast( Integer ( VAL , WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) => - Aggregate( #findVariantIdxFromTy( VAL, lookupTy(TY_TO) ) , .List ) + Aggregate( #findVariantIdxFromTy( truncate(VAL, WIDTH, Unsigned), lookupTy(TY_TO) ) , .List ) ... requires #isEnumWithoutFields(lookupTy(TY_TO)) - andBool #validDiscriminant(VAL, lookupTy(TY_TO)) + andBool #validDiscriminant( truncate(VAL, WIDTH, Unsigned) , lookupTy(TY_TO)) syntax VariantIdx ::= #findVariantIdxFromTy ( Int , TypeInfo ) [function, total] //------------------------------------------------------------------------------ diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-try-from-symbolic-fail.num_into_state.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-try-from-symbolic-fail.num_into_state.expected deleted file mode 100644 index 7f76635a1..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute-try-from-symbolic-fail.num_into_state.expected +++ /dev/null @@ -1,70 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (65 steps) -├─ 3 (split) -│ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) -┃ -┃ (branch) -┣━━┓ subst: .Subst -┃ ┃ constraint: -┃ ┃ notBool ARG_UINT1:Int <=Int 2 -┃ │ -┃ ├─ 4 -┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) -┃ │ -┃ │ (144 steps) -┃ ├─ 6 (terminal) -┃ │ #EndProgram ~> .K -┃ │ -┃ ┊ constraint: true -┃ ┊ subst: ... -┃ └─ 2 (leaf, target, terminal) -┃ #EndProgram ~> .K -┃ -┗━━┓ subst: .Subst - ┃ constraint: - ┃ ARG_UINT1:Int <=Int 2 - │ - ├─ 5 - │ #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) ) - │ - │ (12 steps) - ├─ 7 (split) - │ #cast ( Integer ( ARG_UINT1:Int , 8 , false ) , castKindTransmute , ty ( 9 ) , t - │ span: 72 - ┃ - ┃ (branch) - ┣━━┓ subst: .Subst - ┃ ┃ constraint: - ┃ ┃ #validDiscriminantAux ( ARG_UINT1:Int , discriminant ( 0 ) discriminant ( 1 ) discriminant ( 2 ) .Discriminants ) - ┃ │ - ┃ ├─ 8 - ┃ │ #cast ( Integer ( ARG_UINT1:Int , 8 , false ) , castKindTransmute , ty ( 9 ) , t - ┃ │ span: 72 - ┃ │ - ┃ │ (125 steps) - ┃ ├─ 10 (terminal) - ┃ │ #EndProgram ~> .K - ┃ │ - ┃ ┊ constraint: true - ┃ ┊ subst: ... - ┃ └─ 2 (leaf, target, terminal) - ┃ #EndProgram ~> .K - ┃ - ┗━━┓ subst: .Subst - ┃ constraint: - ┃ notBool #validDiscriminantAux ( ARG_UINT1:Int , discriminant ( 0 ) discriminant ( 1 ) discriminant ( 2 ) .Discriminants ) - │ - ├─ 9 - │ #cast ( Integer ( ARG_UINT1:Int , 8 , false ) , castKindTransmute , ty ( 9 ) , t - │ span: 72 - │ - │ (1 step) - └─ 11 (stuck, leaf) - #UBErrorInvalidDiscriminantsInEnumCast ~> .K - - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected new file mode 100644 index 000000000..c9241f5cf --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (100 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toLocal ( 2 ) , thunk ( #decodeConstant ( constantKindAllo + span: 153 + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic-fail.rs rename to kmir/src/tests/integration/data/prove-rs/transmute-try-from-symbolic.rs diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs new file mode 100644 index 000000000..32e17dcff --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs @@ -0,0 +1,20 @@ +#[repr(i8)] +#[derive(Clone, Copy, Debug, PartialEq)] +pub enum AccountState { + Uninitialized = 0, + Initialized = 1, + Frozen = -1, +} + +fn main() { + unsafe { + assert_eq!(core::mem::transmute::(0), AccountState::Uninitialized); + assert_eq!(core::mem::transmute::(0), AccountState::Uninitialized); + + assert_eq!(core::mem::transmute::(1), AccountState::Initialized); + assert_eq!(core::mem::transmute::(1), AccountState::Initialized); + + assert_eq!(core::mem::transmute::(255), AccountState::Frozen); + assert_eq!(core::mem::transmute::(-1), AccountState::Frozen); + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant.rs b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant.rs index 9b7464adc..2ca4bd49c 100644 --- a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant.rs +++ b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant.rs @@ -3,13 +3,20 @@ pub enum AccountState { Uninitialized = 11, Initialized = 22, - Frozen = 33, + Frozen = 255, } fn main() { unsafe { assert_eq!(core::mem::transmute::(11), AccountState::Uninitialized); assert_eq!(core::mem::transmute::(22), AccountState::Initialized); - assert_eq!(core::mem::transmute::(33), AccountState::Frozen); + assert_eq!(core::mem::transmute::(255), AccountState::Frozen); + + // Compiler rejects transmuting between different width types + // assert_eq!(core::mem::transmute::(-1), AccountState::Frozen); + + // The within the same width the type can be different, here an `-1_i8` is used instead + // of a `255_u8`, but the bit pattern matches it creates the correct type + assert_eq!(core::mem::transmute::(-1), AccountState::Frozen); } } diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index ee502b7d9..3f5321351 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -37,7 +37,6 @@ 'assume-cheatcode': ['check_assume'], 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], - 'transmute-try-from-symbolic-fail': ['num_into_state'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', @@ -55,7 +54,7 @@ 'assume-cheatcode-conflict-fail', 'raw-ptr-cast-fail', 'transmute-u8-to-enum-fail', - 'transmute-try-from-symbolic-fail', + 'transmute-u8-to-enum-changed-discriminant-signed-fail', ] From 9d1dfa6375ff3cad1cd5a25827db5cf40c48d10a Mon Sep 17 00:00:00 2001 From: dkcumming Date: Sat, 15 Nov 2025 23:39:08 +1000 Subject: [PATCH 8/8] Updated documentation --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 1f911091f..bccdc3a03 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1497,10 +1497,17 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. rule #staticArrayLenBits(_OTHER) => 0 [owise] ``` -Another specialisation is getting the discriminant of `enum`s without fields after converting some integer data to it -(see `#discriminant` and `rvalueDiscriminant`). -If none of the `enum` variants has any fields, the `Transmute` of a number to the `enum` data is necessarily just the discriminant itself., and can be returned as the integer value after adjusting to the byte length of the discriminant: - +A transmutation from an integer to an enum is wellformed if: +- The bit width of the incoming integer is the same as the discriminant type of the enum + (e.g. `u8 -> i8` fine, `u8 -> u16` not fine) - this is guaranteed by the compiler; +- The incoming integer has a bit pattern that matches a discriminant of the enum + (e.g. `255_u8` and `-1_i8` fine iff `0b1111_1111` is a discriminant of the enum); + +Note that discriminants are stored as `u128` in the type data even if they are signed +or unsigned at the source level. This means that our approach to soundly transmute an +integer into a enum is to treat the incoming integer as unsigned (converting if signed), +and check if the value is in the discriminants. If yes, find the corresponding variant +index; if not, return `#UBErrorInvalidDiscriminantsInEnumCast`. ```k syntax Bool ::= #isEnumWithoutFields ( TypeInfo ) [function, total] @@ -1508,7 +1515,7 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th rule #isEnumWithoutFields(typeInfoEnumType(_, _, _, FIELDSS, _)) => #noFields(FIELDSS) rule #isEnumWithoutFields(_OTHER) => false [owise] - // Rough as but I just want to stop it thunking + // TODO: Connect this with MirError syntax Evaulation ::= "#UBErrorInvalidDiscriminantsInEnumCast" rule #cast( Integer ( VAL , WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) ~> _REST