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 all 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
```
25 changes: 25 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,31 @@ 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, no-evaluators]
syntax MaybeTypeInfo ::= 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]
// 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, {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]
rule castAux(VAL, CASTKIND, TYPE_SOURCE, TYPE_TARGET) => thunk(castAux(VAL, CASTKIND, TYPE_SOURCE, TYPE_TARGET)) [concrete]
// thunk to avoid re-evaluation of castAux
```

### Number Type Casts
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