Skip to content

P-TOKEN-HOTFIX: Conversions between [u8;8] and u64 #697

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 9 commits into
base: feature/p-token
Choose a base branch
from
Open

P-TOKEN-HOTFIX: Conversions between [u8;8] and u64 #697

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
3753c54
P-TOKEN-HOTFIX: Conversions between [u8;8] and u64
Stevengre Sep 23, 2025
2e86a00
add symbolic attribute to => castAux rules
Stevengre Sep 25, 2025
2aa8c0c
constraint symbolic with symbolic(VAL)
Stevengre Sep 25, 2025
efb8dd9
add concrete Bs
Stevengre Sep 25, 2025
e802c88
remove the rule for `Transmute from [u8; 8] to u64`
Stevengre Sep 25, 2025
ec7b4b8
`no-evaluators` for castAux
Stevengre Sep 25, 2025
59b756c
simplify MaybeTypeInfo
Stevengre Sep 25, 2025
026f3ba
delete the rule that causes the long CI problem
Stevengre Sep 25, 2025
4527a09
remove the useless `symbolic` attribute.
Stevengre Sep 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -119,10 +119,18 @@ power of two but the semantics will always operate with these particular ones.
rule bitmask32 => ( 1 <<Int 32 ) -Int 1
rule bitmask64 => ( 1 <<Int 64 ) -Int 1
rule bitmask128 => ( 1 <<Int 128) -Int 1

```


## Simplifications for `Int` Inequalities

The following simplifications are useful for conditions in overflow checks and bitwise operations.

```k
rule [int-and-255-geq-0]: 0 <=Int _ &Int 255 => true [simplification, smt-lemma]
rule [int-and-255-lt-256]: _ &Int 255 <Int 256 => true [simplification, smt-lemma]
Comment on lines +130 to +131
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just to make sure I understand, this is stating: the result of any integers bitwise Anded with 255 will be bounded between 0 (inclusive) and 256 (not inclusive)?

I don't really understand how this works under the hood, but straight away I wonder if there should be any restriction on the integers. How does this work with negative numbers? Does this make assumptions about 2's complement?

I might be highlighting some misunderstanding I have by asking these questions, but it feels a bit suspicious to me.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How does this work with negative numbers? Does this make assumptions about 2's complement?

I think the answer is yes. We've checked and introduced similar simp rules for riscv-semantics.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No restriction on the integers. The way &Int works in K is that negative numbers are assumed to have an infinite prefix of ...111111 but that prefix becomes zero when applying &Int N with a positive N. So negative numbers become positive.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These two simp rules (smt-lemma) are used to return a true for the following expression.
andBool 0 <=Int B0 andBool B0 <Int 256
If we don't have these two rules, the corresponding rule cannot be applied.

I'm not sure the implementation detail of the backend. I think it might be a rewrite to the substitued terms to get this true. Another thing that I guess the backend can do is to interpret it in SMT, and let SMT solver to return true or false. I think haskell backend should have both way to tackle the require clause, like apply rewrites first, then give it to Z3. Am I right? @jberthold

```

```k
endmodule
```
53 changes: 53 additions & 0 deletions kmir/src/kmir/kdist/mir-semantics/rt/data.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe add no-evaluators to this function because it does not have equations, only simplifications

syntax MaybeTypeInfo ::= "Maybe" "(" TypeInfo ")" | "TypeInfoUnknown"
// ----------------------------------------------------------------
rule <k> #cast(VAL, CASTKIND, TyUnknown, TY_TARGET)
=> castAux(VAL, CASTKIND, TypeInfoUnknown, {TYPEMAP[TY_TARGET]}:>TypeInfo)
// castAux handles the actual casting
...
</k>
<types> TYPEMAP </types>
requires TY_TARGET in_keys(TYPEMAP)
andBool isTypeInfo(TYPEMAP[TY_TARGET])
[priority(160), preserves-definedness, symbolic]
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The previous one without symbolic leads to integration test timeout.

I don't know if this works, but just give it a try.

If you find something suspicious to slow down the symbolic/concrete execution, please let me know.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should be more specific. symbolic requires all variable bindings to be symbolic, but CASTKIND is never symbolic, and neither is TY_TARGET. Please try symbolic(1) here.
Interesting that it starts looping without the attribute...

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Interesting that it starts looping without the attribute...

Interesting... But why? Should we have an issue to store this problem and investigate it later?

Copy link
Contributor Author

@Stevengre Stevengre Sep 25, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please try symbolic(1) here.

I'm always confused with the number here. It starts with 1 rather than 0? But sure, let me try to constraint VAL.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I used symbolic(VAL) here: 2aa8c0c

// low priority, because this is only for writing simplification rules for now
// valid map lookups checked
rule <k> #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
...
</k>
<types> TYPEMAP </types>
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]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here, please try symbolic(1)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I used symbolic(VAL) here: 2aa8c0c


```

### Number Type Casts
Expand Down Expand Up @@ -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 <k> #cast(Range(ListItem(Integer(B0:Int, 8, false))
ListItem(Integer(B1:Int, 8, false))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could add more rules for the case of casting a byte array to an unsigned integer. And this could be handled by a function inside numbers.md maybe, so we don't keep adding to data.md?
Not going to block merging this single case first if it gets us further, though, but we should try to structure the K code more..

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've checked the semantics in numbers.md and still think this rule should be here for now, unless we move all the #cast rules into a single cell. My reason for this is:

  1. Currently, I don't understand the main point of number.md. It seems to gather things about Integer and Float. But for example, the number cast is still in data.md. And it will become hard to read if we move the number cast from data.md to numbers.md.
  2. All the #cast rules are in data.md. It's easy to find the rule and understand the rules in this location.

I think it should be a refactor to move all the cast things into one file. And it will be easy to refactor if this rule is in this location.

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 <<Int 8) +Int (B2 <<Int 16) +Int (B3 <<Int 24) +Int
(B4 <<Int 32) +Int (B5 <<Int 40) +Int (B6 <<Int 48) +Int (B7 <<Int 56),
64, false)
...
</k>
<types> TYPEMAP </types>
requires TY_TARGET in_keys(TYPEMAP)
andBool {TYPEMAP[TY_TARGET]}:>TypeInfo ==K typeInfoPrimitiveType(primTypeUint(uintTyU64))
andBool 0 <=Int B0 andBool B0 <Int 256
andBool 0 <=Int B1 andBool B1 <Int 256
andBool 0 <=Int B2 andBool B2 <Int 256
andBool 0 <=Int B3 andBool B3 <Int 256
andBool 0 <=Int B4 andBool B4 <Int 256
andBool 0 <=Int B5 andBool B5 <Int 256
andBool 0 <=Int B6 andBool B6 <Int 256
andBool 0 <=Int B7 andBool B7 <Int 256
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this rule should only fire when the B are concrete

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like the idea and added concrete(B0,B1,B2,B3,B4,B5,B6,B7). But after adding this, the following term will be unchanged, is that what we want? Actually, I think it should be simplier if we do this rewrite for the symbolic Bxs.

ListItem (typedValue (
    thunk ( #cast ( Range ( ListItem (Integer ( ARG_UINT214:Int , 8 , false ))
                ListItem (Integer ( ARG_UINT215:Int , 8 , false ))
                ListItem (Integer ( ARG_UINT216:Int , 8 , false ))
                ListItem (Integer ( ARG_UINT217:Int , 8 , false ))
                ListItem (Integer ( ARG_UINT218:Int , 8 , false ))
                ListItem (Integer ( ARG_UINT219:Int , 8 , false ))
                ListItem (Integer ( ARG_UINT220:Int , 8 , false ))
                ListItem (Integer ( ARG_UINT221:Int , 8 , false ))
         ) , castKindTransmute , ty ( 600087 ) , ty ( 600086 ) ) ) ,
    ty ( 600086 ),
    mutabilityNot )
)

After this analysis, I would like to delete this concrete attribute now. What about you?

```

### Other casts involving pointers
Expand Down
10 changes: 9 additions & 1 deletion kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -193,10 +193,18 @@ The code uses some helper sorts for better readability.
syntax List ::= #asU8s ( Int ) [function]
| #asU8List ( List , Int ) [function]
// -------------------------------------
rule #asU8s(X) => #asU8List(.List, X)
rule #asU8s(X) => #asU8List(.List, X) [concrete]
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this is a good idea. Requires testing, of course, but we want to avoid building up the list of bit-shifts and enable round-tripping, which this should do.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It works on test_process_burn.

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]

Expand Down
Loading