From a131661ad8f51c80964bdf0d852fa2b5cf580ed7 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 6 Nov 2025 22:25:50 +0800 Subject: [PATCH 1/7] feat(rt): support transmute byte casts --- .../kdist/mir-semantics/lemmas/kmir-lemmas.md | 13 +++ kmir/src/kmir/kdist/mir-semantics/rt/data.md | 86 +++++++++++++++++++ .../data/prove-rs/transmute-bytes.rs | 31 +++++++ 3 files changed, 130 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/transmute-bytes.rs 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 e0f2c8d00..66bdae56e 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -118,6 +118,19 @@ power of two but the semantics will always operate with these particular ones. rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma] ``` +```k + rule (VAL +Int 256 *Int REST) %Int 256 => VAL + requires 0 <=Int VAL + andBool VAL <=Int 255 + [simplification, preserves-definedness, smt-lemma] + + rule (VAL +Int 256 *Int REST) /Int 256 => REST + requires 0 <=Int VAL + andBool VAL <=Int 255 + andBool 0 <=Int REST + [simplification, preserves-definedness, smt-lemma] +``` + ```k endmodule diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 7adc8dd0f..667e171c8 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1406,6 +1406,92 @@ The first cast is reified as a `thunk`, the second one resolves it and eliminate andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant) ``` +Casting a byte array/slice to an integer reinterprets the bytes in little-endian order. + +```k + rule #cast( + Range(ELEMS), + castKindTransmute, + _TY_SOURCE, + TY_TARGET + ) + => + #intAsType( + #littleEndianFromBytes(ELEMS), + size(ELEMS) *Int 8, + #numTypeOf(lookupTy(TY_TARGET)) + ) + ... + + requires #isIntType(lookupTy(TY_TARGET)) + andBool size(ELEMS) *Int 8 ==Int #bitWidth(#numTypeOf(lookupTy(TY_TARGET))) + andBool #areLittleEndianBytes(ELEMS) + [preserves-definedness] // ensures #numTypeOf is defined + + syntax Bool ::= #areLittleEndianBytes ( List ) [function, total] + // ------------------------------------------------------------- + rule #areLittleEndianBytes(.List) => true + rule #areLittleEndianBytes(ListItem(Integer(_, 8, false)) REST) + => #areLittleEndianBytes(REST) + rule #areLittleEndianBytes(ListItem(_OTHER) _) => false [owise] + + syntax Int ::= #littleEndianFromBytes ( List ) [function] + // ----------------------------------------------------- + rule #littleEndianFromBytes(.List) => 0 + rule #littleEndianFromBytes(ListItem(Integer(BYTE, 8, false)) REST) + => BYTE +Int 256 *Int #littleEndianFromBytes(REST) +``` + +Casting an integer to a `[u8; N]` array materialises its little-endian bytes. + +```k + rule #cast( + Integer(VAL, WIDTH, _SIGNEDNESS), + castKindTransmute, + _TY_SOURCE, + TY_TARGET + ) + => + Range(#littleEndianBytesFromInt(VAL, WIDTH)) + ... + + requires #isStaticU8Array(lookupTy(TY_TARGET)) + andBool WIDTH >=Int 0 + andBool WIDTH %Int 8 ==Int 0 + andBool WIDTH ==Int #staticArrayLenBits(lookupTy(TY_TARGET)) + [preserves-definedness] // ensures element type/length are well-formed + + syntax List ::= #littleEndianBytesFromInt ( Int, Int ) [function] + // ------------------------------------------------------------- + rule #littleEndianBytesFromInt(VAL, WIDTH) + => #littleEndianBytes(truncate(VAL, WIDTH, Unsigned), WIDTH /Int 8) + requires WIDTH %Int 8 ==Int 0 + andBool WIDTH >=Int 0 + + syntax List ::= #littleEndianBytes ( Int, Int ) [function] + // ------------------------------------------------------------- + rule #littleEndianBytes(_, COUNT) + => .List + requires COUNT <=Int 0 + + rule #littleEndianBytes(VAL, COUNT) + => ListItem(Integer(VAL %Int 256, 8, false)) #littleEndianBytes(VAL /Int 256, COUNT -Int 1) + requires COUNT >Int 0 + + syntax Bool ::= #isStaticU8Array ( TypeInfo ) [function, total] + // ------------------------------------------------------------- + rule #isStaticU8Array(typeInfoArrayType(ELEM_TY, someTyConst(_))) + => lookupTy(ELEM_TY) ==K typeInfoPrimitiveType(primTypeUint(uintTyU8)) + rule #isStaticU8Array(_OTHER) => false [owise] + + syntax Int ::= #staticArrayLenBits ( TypeInfo ) [function, total] + // ------------------------------------------------------------- + rule #staticArrayLenBits(typeInfoArrayType(_, someTyConst(tyConst(KIND, _)))) + => readTyConstInt(KIND) *Int 8 + [preserves-definedness] + 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 afgter adjusting to the byte length of the discriminant: diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-bytes.rs b/kmir/src/tests/integration/data/prove-rs/transmute-bytes.rs new file mode 100644 index 000000000..654e6ca1e --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/transmute-bytes.rs @@ -0,0 +1,31 @@ +#![allow(clippy::transmute_bytes_to_bytes)] +#![allow(clippy::unnecessary_transmute)] + +use std::mem::transmute; + +fn bytes_to_u64(bytes: [u8; 8]) -> u64 { + let value = unsafe { transmute::<[u8; 8], u64>(bytes) }; + let roundtrip = unsafe { transmute::(value) }; + assert_eq!(roundtrip, bytes); + value +} + +fn u64_to_bytes(value: u64) -> [u8; 8] { + let bytes = unsafe { transmute::(value) }; + let roundtrip = unsafe { transmute::<[u8; 8], u64>(bytes) }; + assert_eq!(roundtrip, value); + bytes +} + +fn main() { + let bytes = [0x01, 0x23, 0x45, 0x67, 0x89, 0xAB, 0xCD, 0xEF]; + let int = bytes_to_u64(bytes); + assert_eq!(int, 0xEFCD_AB89_6745_2301); + + let roundtrip = u64_to_bytes(int); + assert_eq!(roundtrip, bytes); + + let value = 0x1020_3040_5060_7080_u64; + let value_roundtrip = bytes_to_u64(u64_to_bytes(value)); + assert_eq!(value_roundtrip, value); +} From 25f20ec3d007e16c262f1ed71790cbdc1103e562 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 6 Nov 2025 22:51:09 +0800 Subject: [PATCH 2/7] fix: make build --- kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 66bdae56e..395fa5710 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -119,7 +119,7 @@ power of two but the semantics will always operate with these particular ones. ``` ```k - rule (VAL +Int 256 *Int REST) %Int 256 => VAL + rule (VAL +Int 256 *Int _) %Int 256 => VAL requires 0 <=Int VAL andBool VAL <=Int 255 [simplification, preserves-definedness, smt-lemma] From 9ec997d7685eb2fa6b27426cf7ace9a90ddc2ea1 Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 6 Nov 2025 22:58:45 +0800 Subject: [PATCH 3/7] fix: make build --- kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md | 4 ++-- 1 file changed, 2 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 395fa5710..05c4cfd90 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -122,13 +122,13 @@ power of two but the semantics will always operate with these particular ones. rule (VAL +Int 256 *Int _) %Int 256 => VAL requires 0 <=Int VAL andBool VAL <=Int 255 - [simplification, preserves-definedness, smt-lemma] + [simplification, preserves-definedness] rule (VAL +Int 256 *Int REST) /Int 256 => REST requires 0 <=Int VAL andBool VAL <=Int 255 andBool 0 <=Int REST - [simplification, preserves-definedness, smt-lemma] + [simplification, preserves-definedness] ``` From 880521d9216fa277e88d78bb34159afd3e5ecaad Mon Sep 17 00:00:00 2001 From: Stevengre Date: Thu, 6 Nov 2025 23:21:13 +0800 Subject: [PATCH 4/7] test(prove-rs): add byte endian spec fixtures --- .../integration/data/prove-rs/byte-endian-fail.rs | 12 ++++++++++++ .../prove-rs/show/byte-endian-fail.main.expected | 14 ++++++++++++++ kmir/src/tests/integration/test_integration.py | 2 ++ 3 files changed, 28 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/byte-endian-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/byte-endian-fail.rs b/kmir/src/tests/integration/data/prove-rs/byte-endian-fail.rs new file mode 100644 index 000000000..877d9e5e7 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/byte-endian-fail.rs @@ -0,0 +1,12 @@ +fn main() { + let value = 0x0123_4567_89AB_CDEF_u64; + + let native_bytes = value.to_ne_bytes(); + assert_eq!(u64::from_ne_bytes(native_bytes), value); + + let little_bytes = value.to_le_bytes(); + assert_eq!(u64::from_le_bytes(little_bytes), value); + + let big_bytes = value.to_be_bytes(); + assert_eq!(u64::from_be_bytes(big_bytes), value); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected new file mode 100644 index 000000000..c2398ecb0 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected @@ -0,0 +1,14 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (332 steps) +└─ 3 (stuck, leaf) + #execIntrinsic ( IntrinsicFunction ( symbol ( "bswap" ) ) , operandMove ( place + + +┌─ 2 (root, leaf, target, terminal) +│ #EndProgram ~> .K + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a42265cc9..684ccdc2b 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -36,6 +36,7 @@ 'pointer-cast-length-test-fail': ['array_cast_test'], 'assume-cheatcode': ['check_assume'], 'assume-cheatcode-conflict-fail': ['check_assume_conflict'], + 'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'], } PROVE_RS_SHOW_SPECS = [ 'local-raw-fail', @@ -52,6 +53,7 @@ 'closure_access_struct', 'niche-enum', 'assume-cheatcode-conflict-fail', + 'byte-endian-fail', ] From 08309cbe3e97db881086b46a8550e3677b23b917 Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Fri, 7 Nov 2025 09:08:00 +0800 Subject: [PATCH 5/7] Update kmir/src/kmir/kdist/mir-semantics/rt/data.md Co-authored-by: Jost Berthold --- 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 667e171c8..d61206070 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1467,6 +1467,7 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. => #littleEndianBytes(truncate(VAL, WIDTH, Unsigned), WIDTH /Int 8) requires WIDTH %Int 8 ==Int 0 andBool WIDTH >=Int 0 + [preserves-definedness] syntax List ::= #littleEndianBytes ( Int, Int ) [function] // ------------------------------------------------------------- From eb6be665f53b60155afb621bf6f79b1d05ac54c4 Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Fri, 7 Nov 2025 09:08:08 +0800 Subject: [PATCH 6/7] Update kmir/src/kmir/kdist/mir-semantics/rt/data.md Co-authored-by: Jost Berthold --- 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 d61206070..61302443c 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1478,6 +1478,7 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes. rule #littleEndianBytes(VAL, COUNT) => ListItem(Integer(VAL %Int 256, 8, false)) #littleEndianBytes(VAL /Int 256, COUNT -Int 1) requires COUNT >Int 0 + [preserves-definedness] syntax Bool ::= #isStaticU8Array ( TypeInfo ) [function, total] // ------------------------------------------------------------- From b101337bf90c383cb3a62a2260019ee2be72c92f Mon Sep 17 00:00:00 2001 From: Stevengre Date: Fri, 7 Nov 2025 09:13:50 +0800 Subject: [PATCH 7/7] fix: apply suggestions --- .../kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md | 3 ++- .../integration/data/prove-rs/byte-endian-fail.rs | 12 ------------ .../prove-rs/show/byte-endian-fail.main.expected | 14 -------------- kmir/src/tests/integration/test_integration.py | 1 - 4 files changed, 2 insertions(+), 28 deletions(-) delete mode 100644 kmir/src/tests/integration/data/prove-rs/byte-endian-fail.rs delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected 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 05c4cfd90..0c9ca8957 100644 --- a/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md +++ b/kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md @@ -119,9 +119,10 @@ power of two but the semantics will always operate with these particular ones. ``` ```k - rule (VAL +Int 256 *Int _) %Int 256 => VAL + rule (VAL +Int 256 *Int REST) %Int 256 => VAL requires 0 <=Int VAL andBool VAL <=Int 255 + andBool 0 <=Int REST [simplification, preserves-definedness] rule (VAL +Int 256 *Int REST) /Int 256 => REST diff --git a/kmir/src/tests/integration/data/prove-rs/byte-endian-fail.rs b/kmir/src/tests/integration/data/prove-rs/byte-endian-fail.rs deleted file mode 100644 index 877d9e5e7..000000000 --- a/kmir/src/tests/integration/data/prove-rs/byte-endian-fail.rs +++ /dev/null @@ -1,12 +0,0 @@ -fn main() { - let value = 0x0123_4567_89AB_CDEF_u64; - - let native_bytes = value.to_ne_bytes(); - assert_eq!(u64::from_ne_bytes(native_bytes), value); - - let little_bytes = value.to_le_bytes(); - assert_eq!(u64::from_le_bytes(little_bytes), value); - - let big_bytes = value.to_be_bytes(); - assert_eq!(u64::from_be_bytes(big_bytes), value); -} diff --git a/kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected deleted file mode 100644 index c2398ecb0..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/byte-endian-fail.main.expected +++ /dev/null @@ -1,14 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (332 steps) -└─ 3 (stuck, leaf) - #execIntrinsic ( IntrinsicFunction ( symbol ( "bswap" ) ) , operandMove ( place - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index 684ccdc2b..387dc40d6 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -53,7 +53,6 @@ 'closure_access_struct', 'niche-enum', 'assume-cheatcode-conflict-fail', - 'byte-endian-fail', ]