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

Stevengre · 2025-09-24T16:37:06Z

This PR is to tackle issue: [FEATURE] Hard-wire conversions between [u8;8] and u64 solana-token#6
Changes includes:
kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md: simp rules to make other simp rules' require clause can be satisfied.
kmir/src/kmir/kdist/mir-semantics/rt/data.md:
- castAux function to bring TypeInfo into a function without configuration, allowing simplification rules for #cast.
- A rewrite rule to transmute from [u8; 8] to u64
kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md:
- make #asU8s's rule concrete to simplify the result for symbolic value
- rules for #asU8s(X)

Stevengre · 2025-09-25T01:43:37Z

kmir/src/kmir/kdist/mir-semantics/rt/data.md

+       <types> TYPEMAP </types>
+    requires TY_TARGET in_keys(TYPEMAP)
+     andBool isTypeInfo(TYPEMAP[TY_TARGET])
+    [priority(160), preserves-definedness, symbolic] 


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.

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...

Interesting that it starts looping without the attribute...

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

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.

I used symbolic(VAL) here: 2aa8c0c

dkcumming · 2025-09-25T02:23:54Z

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

+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]


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.

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.

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.

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

jberthold · 2025-09-25T02:48:35Z

kmir/src/kmir/kdist/mir-semantics/rt/data.md

+       <types> TYPEMAP </types>
+    requires TY_TARGET in_keys(TYPEMAP)
+     andBool isTypeInfo(TYPEMAP[TY_TARGET])
+    [priority(160), preserves-definedness, symbolic] 


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...

jberthold · 2025-09-25T02:48:57Z

kmir/src/kmir/kdist/mir-semantics/rt/data.md

+       <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]


Same here, please try symbolic(1)

I used symbolic(VAL) here: 2aa8c0c

jberthold · 2025-09-25T02:52:08Z

kmir/src/kmir/kdist/mir-semantics/rt/data.md

+  // Transmute from [u8; 8] to u64
+  rule <k> #cast(Range(ListItem(Integer(B0:Int, 8, false))
+                       ListItem(Integer(B1:Int, 8, false))


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..

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:

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.

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.

jberthold · 2025-09-25T02:57:24Z

kmir/src/kmir/kdist/mir-semantics/symbolic/p-token.md

                | #asU8List ( List , Int ) [function]
  // -------------------------------------
-  rule #asU8s(X) => #asU8List(.List, X)
+  rule #asU8s(X) => #asU8List(.List, X) [concrete]


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.

It works on test_process_burn.

jberthold · 2025-09-25T03:09:52Z

kmir/src/kmir/kdist/mir-semantics/rt/data.md

+      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


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

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?

jberthold · 2025-09-25T03:39:49Z

kmir/src/kmir/kdist/mir-semantics/rt/data.md


 ```k
  syntax Evaluation ::= #cast( Evaluation, CastKind, MaybeTy, Ty ) [strict(1)]
+  syntax Evaluation ::= castAux ( Value, CastKind, MaybeTypeInfo, TypeInfo ) [function]


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

jberthold · 2025-09-25T04:07:30Z

kmir/src/kmir/kdist/mir-semantics/rt/data.md

+  syntax Evaluation ::= castAux ( Value, CastKind, MaybeTypeInfo, TypeInfo ) [function, no-evaluators]
+  syntax MaybeTypeInfo ::= "Maybe" "(" TypeInfo ")" | "TypeInfoUnknown" 
+  // ----------------------------------------------------------------
+  rule <k> #cast(VAL, CASTKIND, TyUnknown, TY_TARGET)
+        => castAux(VAL, CASTKIND, TypeInfoUnknown, {TYPEMAP[TY_TARGET]}:>TypeInfo)


two small suggestions:

syntax MaybeTypeInfo ::= TypeInfo | NoTypeInfo

maybe these rules should move to p-token?

I applied the first one.

For the second one, I think it will be good to refactor like this way. Without castAux, we cannot introduce any simp rules for #cast. So, I want to leave these rules here.

I'll mark the pr as automerge, but please let me know if you have any other thoughts on it.

jberthold · 2025-09-25T06:34:44Z

Something is wrong with the latest changes in the PR, the integration test is running for >2h now. Removing automerge

Code caused the integration test proofs to loop, revision in progress

Introduce concrete rule for castAux for thunk

Stevengre added 2 commits September 25, 2025 00:35

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

3753c54

add symbolic attribute to => castAux rules

2e86a00

Stevengre commented Sep 25, 2025

View reviewed changes

Stevengre requested review from dkcumming, jberthold and tothtamas28 September 25, 2025 01:43

Stevengre marked this pull request as ready for review September 25, 2025 01:44

dkcumming reviewed Sep 25, 2025

View reviewed changes

jberthold reviewed Sep 25, 2025

View reviewed changes

Stevengre added 2 commits September 25, 2025 11:11

constraint symbolic with symbolic(VAL)

2aa8c0c

add concrete Bs

efb8dd9

jberthold reviewed Sep 25, 2025

View reviewed changes

Stevengre added 2 commits September 25, 2025 11:45

remove the rule for Transmute from [u8; 8] to u64

e802c88

no-evaluators for castAux

ec7b4b8

jberthold previously approved these changes Sep 25, 2025

View reviewed changes

Stevengre self-assigned this Sep 25, 2025

Stevengre added the automerge label Sep 25, 2025

jberthold reviewed Sep 25, 2025

View reviewed changes

Stevengre removed the automerge label Sep 25, 2025

simplify MaybeTypeInfo

59b756c

Stevengre added the automerge label Sep 25, 2025

jberthold removed the automerge label Sep 25, 2025

delete the rule that causes the long CI problem

026f3ba

remove the useless symbolic attribute.

4527a09

Introduce concrete rule for castAux for thunk

		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]

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

Are you sure you want to change the base?

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

Uh oh!

Conversation

Stevengre commented Sep 24, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Stevengre Sep 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Stevengre Sep 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jberthold commented Sep 25, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Stevengre commented Sep 24, 2025 •

edited

Loading

Stevengre Sep 25, 2025 •

edited

Loading

Stevengre Sep 25, 2025 •

edited

Loading