Skip to content

Commit 431a484

Browse files
fix(decode): accept signed enum tag scalars in _extract_tag (#954)
## Summary - Relax `_extract_tag` to accept both signed and unsigned `PrimitiveInt` tag metadata (`signed=_`). - Keep discriminant decoding based on raw tag bits (`int.from_bytes(..., signed=False)`), which is what variant dispatch needs. - Add a decode fixture for signed-tag metadata (`enum-3-variants-0-fields-signed-tag`). - Update the prove-rs case to a passing case and refresh its `show` snapshot. ## Problem (concrete case) This PR is motivated by: `kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs` ```rust #[repr(i8)] enum AccountState { Uninitialized = 0, Initialized = 1, Frozen = -1, } // main checks both byte-level and signed views of the same discriminant bits: // 255 maps to Frozen in the u8 path // -1 maps to Frozen in the i8 path ``` For this enum layout, the tag scalar metadata can be `signed=true` (I8), even though the stored discriminant bytes are still valid raw bytes for dispatch. ## Red (before this fix) `_extract_tag` only matched `PrimitiveInt(..., signed=False)`. When metadata was signed, decode failed with: ```text ValueError: Unsupported tag: Initialized(value=PrimitiveInt(length=I8, signed=True), ...) ``` That blocked the signed-discriminant path in proving. ## Green (after this fix) - `_extract_tag` now accepts either signedness metadata. - The same bytes are decoded as unsigned raw bits for dispatch. - The concrete program above now proves in integration tests: - input case is now `transmute-u8-to-enum-changed-discriminant-signed.rs` - expected proof snapshot is `show/transmute-u8-to-enum-changed-discriminant-signed.main.expected` - terminal `#EndProgram` is reached for `main` ## Why this is the right scope This change fixes tag extraction compatibility for signed discriminant metadata without changing enum dispatch semantics beyond that path. It is covered by both: - decode-value fixture (`enum-3-variants-0-fields-signed-tag`) and - end-to-end prove-rs integration snapshot for the concrete Rust program above. --------- Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>
1 parent 697e68a commit 431a484

6 files changed

Lines changed: 142 additions & 17 deletions

kmir/src/kmir/decoding.py

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -445,10 +445,12 @@ def _extract_tag(*, data: bytes, tag_offset: MachineSize, tag: Scalar) -> tuple[
445445
case Initialized(
446446
value=PrimitiveInt(
447447
length=length,
448-
signed=False,
448+
signed=_,
449449
),
450450
valid_range=_,
451451
):
452+
# Stable MIR enum discriminants are represented against the raw tag bits.
453+
# Use unsigned decoding even when the scalar metadata marks the tag as signed.
452454
tag_data = data[tag_offset.in_bytes : tag_offset.in_bytes + length.value]
453455
tag_value = int.from_bytes(tag_data, byteorder='little', signed=False)
454456
return tag_value, length
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Aggregate ( variantIdx ( 1 ) , .List )
Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
{
2+
"bytes": [
3+
0
4+
],
5+
"types": [],
6+
"typeInfo": {
7+
"EnumType": {
8+
"name": "OrderingLike",
9+
"adt_def": 72,
10+
"discriminants": [
11+
255,
12+
0,
13+
1
14+
],
15+
"fields": [
16+
[],
17+
[],
18+
[]
19+
],
20+
"layout": {
21+
"fields": {
22+
"Arbitrary": {
23+
"offsets": [
24+
{
25+
"num_bits": 0
26+
}
27+
]
28+
}
29+
},
30+
"variants": {
31+
"Multiple": {
32+
"tag": {
33+
"Initialized": {
34+
"value": {
35+
"Int": {
36+
"length": "I8",
37+
"signed": true
38+
}
39+
},
40+
"valid_range": {
41+
"start": 255,
42+
"end": 1
43+
}
44+
}
45+
},
46+
"tag_encoding": "Direct",
47+
"tag_field": 0,
48+
"variants": [
49+
{
50+
"fields": {
51+
"Arbitrary": {
52+
"offsets": []
53+
}
54+
},
55+
"variants": {
56+
"Single": {
57+
"index": 0
58+
}
59+
},
60+
"abi": {
61+
"Aggregate": {
62+
"sized": true
63+
}
64+
},
65+
"abi_align": 1,
66+
"size": {
67+
"num_bits": 8
68+
}
69+
},
70+
{
71+
"fields": {
72+
"Arbitrary": {
73+
"offsets": []
74+
}
75+
},
76+
"variants": {
77+
"Single": {
78+
"index": 1
79+
}
80+
},
81+
"abi": {
82+
"Aggregate": {
83+
"sized": true
84+
}
85+
},
86+
"abi_align": 1,
87+
"size": {
88+
"num_bits": 8
89+
}
90+
},
91+
{
92+
"fields": {
93+
"Arbitrary": {
94+
"offsets": []
95+
}
96+
},
97+
"variants": {
98+
"Single": {
99+
"index": 2
100+
}
101+
},
102+
"abi": {
103+
"Aggregate": {
104+
"sized": true
105+
}
106+
},
107+
"abi_align": 1,
108+
"size": {
109+
"num_bits": 8
110+
}
111+
}
112+
]
113+
}
114+
},
115+
"abi": {
116+
"Scalar": {
117+
"Initialized": {
118+
"value": {
119+
"Int": {
120+
"length": "I8",
121+
"signed": true
122+
}
123+
},
124+
"valid_range": {
125+
"start": 255,
126+
"end": 1
127+
}
128+
}
129+
}
130+
},
131+
"abi_align": 1,
132+
"size": {
133+
"num_bits": 8
134+
}
135+
}
136+
}
137+
}
138+
}

kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected

Lines changed: 0 additions & 15 deletions
This file was deleted.

kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs renamed to kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs

File renamed without changes.

kmir/src/tests/integration/test_integration.py

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,6 @@
5454
'assume-cheatcode-conflict-fail',
5555
'raw-ptr-cast-fail',
5656
'transmute-u8-to-enum-fail',
57-
'transmute-u8-to-enum-changed-discriminant-signed-fail',
5857
'assert-inhabited-fail',
5958
'iterator-simple',
6059
'unions-fail',

0 commit comments

Comments
 (0)