Skip to content
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

More int types #164

Merged
merged 2 commits into from
Oct 22, 2024
Merged

More int types #164

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0c6f064
More int types
virgil-serbanuta Oct 17, 2024
5d2a9ed
Add TODO for removing additional int types
virgil-serbanuta Oct 21, 2024
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
21 changes: 4 additions & 17 deletions Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,35 +1,22 @@
ARG Z3_VERSION
ARG K_COMMIT

ARG Z3_VERSION=4.12.1
FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3
ARG LLVM_VERSION

ARG K_COMMIT
FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_COMMIT}

COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
FROM runtimeverificationinc/kframework-k:ubuntu-noble-${K_COMMIT}

RUN apt-get update \
&& apt-get upgrade --yes \
&& apt-get install --yes \
curl
# cmake \
# pandoc \
# python3 \
# python3-pip \
# wabt

ARG USER_ID=1000
ARG GROUP_ID=1000
ARG USER_ID=1001
ARG GROUP_ID=1001
RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user

USER user:user
WORKDIR /home/user

RUN curl -sSL https://install.python-poetry.org | python3 - --version 1.7.1

# RUN pip3 install --user \
# cytoolz \
# numpy

ENV PATH=/home/user/.local/bin:$PATH
110 changes: 28 additions & 82 deletions rust-semantics/expression/casts.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,89 +7,35 @@ module RUST-CASTS
rule implicitCast(V:Value, T:Type) => error("Unknown implicitCast.", ListItem(V) ListItem(T))
[owise]

// https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-implicitCast
// https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-cast

rule implicitCast(i8(Value), i8 ) => i8 (Value)
rule implicitCast(i8(Value), u8 ) => u8 (Value)
rule implicitCast(i8(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i8(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i8(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(i8(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(i8(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(i8(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))

rule implicitCast(u8(Value), i8 ) => i8 (Value)
rule implicitCast(u8(Value), u8 ) => u8 (Value)
rule implicitCast(u8(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(u8(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(u8(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u8(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u8(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u8(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))

rule implicitCast(i16(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(i16(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(i16(Value), i16) => i16(Value)
rule implicitCast(i16(Value), u16) => u16(Value)
rule implicitCast(i16(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(i16(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(i16(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(i16(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))

rule implicitCast(u16(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(u16(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(u16(Value), i16) => i16(Value)
rule implicitCast(u16(Value), u16) => u16(Value)
rule implicitCast(u16(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u16(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u16(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u16(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))

rule implicitCast(i32(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(i32(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(i32(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i32(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i32(Value), i32) => i32(Value)
rule implicitCast(i32(Value), u32) => u32(Value)
rule implicitCast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value)))

rule implicitCast(u32(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(u32(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(u32(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(u32(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(u32(Value), i32) => i32(Value)
rule implicitCast(u32(Value), u32) => u32(Value)
rule implicitCast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))


rule implicitCast(i64(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(i64(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(i64(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i64(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value)))
rule implicitCast(i64(Value), i64) => i64(Value)
rule implicitCast(i64(Value), u64) => u64(Value)

rule implicitCast(u64(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(u64(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(u64(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(u64(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u64(Value), i64) => i64(Value)
rule implicitCast(u64(Value), u64) => u64(Value)

rule implicitCast(u128(Value), i8 ) => i8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(u128(Value), u8 ) => u8 (Int2MInt(MInt2Signed(Value)))
rule implicitCast(u128(Value), i16) => i16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(u128(Value), u16) => u16(Int2MInt(MInt2Signed(Value)))
rule implicitCast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
rule implicitCast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
syntax ValueOrError ::= implicitCast(Int, Type) [function, total]
rule implicitCast(Value:Int, T:Type)
=> error("implicitCast(Int, Type)", ListItem(Value) ListItem(T))
[owise]
rule implicitCast(Value:Int, i8 ) => i8 (Int2MInt(Value))
rule implicitCast(Value:Int, u8 ) => u8 (Int2MInt(Value))
rule implicitCast(Value:Int, i16 ) => i16 (Int2MInt(Value))
rule implicitCast(Value:Int, u16 ) => u16 (Int2MInt(Value))
rule implicitCast(Value:Int, i32 ) => i32 (Int2MInt(Value))
rule implicitCast(Value:Int, u32 ) => u32 (Int2MInt(Value))
rule implicitCast(Value:Int, i64 ) => i64 (Int2MInt(Value))
rule implicitCast(Value:Int, u64 ) => u64 (Int2MInt(Value))
rule implicitCast(Value:Int, u128) => u128(Int2MInt(Value))
rule implicitCast(Value:Int, u160) => u160(Int2MInt(Value))
rule implicitCast(Value:Int, u256) => u256(Int2MInt(Value))

rule implicitCast(i8 (Value), T:Type ) => implicitCast(MInt2Signed(Value), T)
rule implicitCast(u8 (Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T)
rule implicitCast(i16 (Value), T:Type ) => implicitCast(MInt2Signed(Value), T)
rule implicitCast(u16 (Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T)
rule implicitCast(i32 (Value), T:Type ) => implicitCast(MInt2Signed(Value), T)
rule implicitCast(u32 (Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T)
rule implicitCast(i64 (Value), T:Type ) => implicitCast(MInt2Signed(Value), T)
rule implicitCast(u64 (Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T)
rule implicitCast(u128(Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T)
rule implicitCast(u160(Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T)
rule implicitCast(u256(Value), T:Type ) => implicitCast(MInt2Unsigned(Value), T)

rule implicitCast(V:Bool, bool) => V
rule implicitCast(S:String, str) => S
Expand Down
14 changes: 14 additions & 0 deletions rust-semantics/expression/comparisons.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,20 @@ module RUST-INTEGER-RELATIONAL-OPERATIONS
rule ptrValue(_, u128(A):Value) >= ptrValue(_, u128(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(_, u128(A):Value) <= ptrValue(_, u128(B):Value) => ptrValue(null, A <=uMInt B)

rule ptrValue(_, u160(A):Value) == ptrValue(_, u160(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, u160(A):Value) != ptrValue(_, u160(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, u160(A):Value) > ptrValue(_, u160(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(_, u160(A):Value) < ptrValue(_, u160(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(_, u160(A):Value) >= ptrValue(_, u160(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(_, u160(A):Value) <= ptrValue(_, u160(B):Value) => ptrValue(null, A <=uMInt B)

rule ptrValue(_, u256(A):Value) == ptrValue(_, u256(B):Value) => ptrValue(null, A ==MInt B)
rule ptrValue(_, u256(A):Value) != ptrValue(_, u256(B):Value) => ptrValue(null, A =/=MInt B)
rule ptrValue(_, u256(A):Value) > ptrValue(_, u256(B):Value) => ptrValue(null, A >uMInt B)
rule ptrValue(_, u256(A):Value) < ptrValue(_, u256(B):Value) => ptrValue(null, A <uMInt B)
rule ptrValue(_, u256(A):Value) >= ptrValue(_, u256(B):Value) => ptrValue(null, A >=uMInt B)
rule ptrValue(_, u256(A):Value) <= ptrValue(_, u256(B):Value) => ptrValue(null, A <=uMInt B)

endmodule

```
18 changes: 18 additions & 0 deletions rust-semantics/expression/integer-operations.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -86,6 +86,22 @@ module RUST-INTEGER-ARITHMETIC-OPERATIONS
rule ptrValue(_, u128(A):Value) % ptrValue(_, u128(B):Value) => ptrValue(null, u128(A %uMInt B))
requires B =/=K 0p128

rule ptrValue(_, u160(A):Value) * ptrValue(_, u160(B):Value) => ptrValue(null, u160(A *MInt B))
rule ptrValue(_, u160(A):Value) + ptrValue(_, u160(B):Value) => ptrValue(null, u160(A +MInt B))
rule ptrValue(_, u160(A):Value) - ptrValue(_, u160(B):Value) => ptrValue(null, u160(A -MInt B))
rule ptrValue(_, u160(A):Value) / ptrValue(_, u160(B):Value) => ptrValue(null, u160(A /uMInt B))
requires B =/=K 0p160
rule ptrValue(_, u160(A):Value) % ptrValue(_, u160(B):Value) => ptrValue(null, u160(A %uMInt B))
requires B =/=K 0p160

rule ptrValue(_, u256(A):Value) * ptrValue(_, u256(B):Value) => ptrValue(null, u256(A *MInt B))
rule ptrValue(_, u256(A):Value) + ptrValue(_, u256(B):Value) => ptrValue(null, u256(A +MInt B))
rule ptrValue(_, u256(A):Value) - ptrValue(_, u256(B):Value) => ptrValue(null, u256(A -MInt B))
rule ptrValue(_, u256(A):Value) / ptrValue(_, u256(B):Value) => ptrValue(null, u256(A /uMInt B))
requires B =/=K 0p256
rule ptrValue(_, u256(A):Value) % ptrValue(_, u256(B):Value) => ptrValue(null, u256(A %uMInt B))
requires B =/=K 0p256

endmodule


Expand All @@ -102,6 +118,8 @@ module RUST-INTEGER-RANGE-OPERATIONS
rule (ptrValue(_, i64(A):Value) .. ptrValue(_, i64(B):Value)):Expression => ptrValue(null, intRange(i64(A), i64(B)))
rule (ptrValue(_, u64(A):Value) .. ptrValue(_, u64(B):Value)):Expression => ptrValue(null, intRange(u64(A), u64(B)))
rule (ptrValue(_, u128(A):Value) .. ptrValue(_, u128(B):Value)):Expression => ptrValue(null, intRange(u128(A), u128(B)))
rule (ptrValue(_, u160(A):Value) .. ptrValue(_, u160(B):Value)):Expression => ptrValue(null, intRange(u160(A), u160(B)))
rule (ptrValue(_, u256(A):Value) .. ptrValue(_, u256(B):Value)):Expression => ptrValue(null, intRange(u256(A), u256(B)))

endmodule

Expand Down
11 changes: 11 additions & 0 deletions rust-semantics/expression/literals.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,9 @@ module RUST-EXPRESSION-INTEGER-LITERALS
rule findSuffix(S) => suffix(u32, 3) requires endsWith(S, "u32")
rule findSuffix(S) => suffix(i64, 3) requires endsWith(S, "i64")
rule findSuffix(S) => suffix(u64, 3) requires endsWith(S, "u64")
rule findSuffix(S) => suffix(u128, 4) requires endsWith(S, "u128")
rule findSuffix(S) => suffix(u160, 4) requires endsWith(S, "u160")
rule findSuffix(S) => suffix(u256, 4) requires endsWith(S, "u256")
rule findSuffix(_) => suffix(( ), 0) [owise]

syntax IntegerSuffix ::= suffix(Type, Int)
Expand Down Expand Up @@ -82,6 +85,12 @@ module RUST-EXPRESSION-INTEGER-LITERALS
requires sminMInt(64) <=Int I andBool I <=Int smaxMInt(64)
rule integerToValue(I:Int, u64) => u64(Int2MInt(I))
requires uminMInt(64) <=Int I andBool I <=Int umaxMInt(64)
rule integerToValue(I:Int, u128) => u128(Int2MInt(I))
requires uminMInt(128) <=Int I andBool I <=Int umaxMInt(128)
rule integerToValue(I:Int, u160) => u160(Int2MInt(I))
requires uminMInt(160) <=Int I andBool I <=Int umaxMInt(160)
rule integerToValue(I:Int, u256) => u256(Int2MInt(I))
requires uminMInt(256) <=Int I andBool I <=Int umaxMInt(256)
rule integerToValue(I:Int, ( )) => u128(Int2MInt(I))
rule integerToValue(I:Int, T:Type)
=> error("integerToValue: unimplemented", ListItem(I:Int:KItem) ListItem(T:Type:KItem))
Expand All @@ -97,6 +106,8 @@ module RUST-EXPRESSION-INTEGER-LITERALS
rule valueToInteger(i64(V:MInt{64})) => MInt2Signed(V)
rule valueToInteger(u64(V:MInt{64})) => MInt2Unsigned(V)
rule valueToInteger(u128(V:MInt{128})) => MInt2Unsigned(V)
rule valueToInteger(u160(V:MInt{160})) => MInt2Unsigned(V)
rule valueToInteger(u256(V:MInt{256})) => MInt2Unsigned(V)

syntax Bool ::= endsWith(containing:String, contained:String) [function, total]
rule endsWith(Containing:String, Contained:String)
Expand Down
43 changes: 17 additions & 26 deletions rust-semantics/expression/loops.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
```k

module RUST-LOOP-EXPRESSIONS
imports K-EQUAL-SYNTAX
imports RUST-REPRESENTATION

syntax IteratorLoopExpression ::= "for1" Pattern "limit" PtrValue BlockExpression
Expand Down Expand Up @@ -32,32 +33,22 @@ module RUST-LOOP-EXPRESSIONS
syntax LetStatement ::= incrementPatt(Identifier, Value) [function]

rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i8 (Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, i8 )
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u8 (Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, u8 )
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i16(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, i16)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u16(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, u16)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i32(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, i32)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u32(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, u32)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u64(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, u64)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i64(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, i64)
rule incrementPatt(Patt:Identifier, ComparisonValue:Value) =>
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u128(Int2MInt(1:Int)));
requires checkIntOfType(ComparisonValue, u128)
let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, oneOfSameType(ComparisonValue));
requires oneOfSameType(ComparisonValue) =/=K tuple(.ValueList)

syntax Value ::= oneOfSameType(Value) [function, total]
rule oneOfSameType(_) => tuple(.ValueList) [owise]
rule oneOfSameType(u8 (_)) => u8 (Int2MInt(1))
rule oneOfSameType(i8 (_)) => i8 (Int2MInt(1))
rule oneOfSameType(u16 (_)) => u16 (Int2MInt(1))
rule oneOfSameType(i16 (_)) => i16 (Int2MInt(1))
rule oneOfSameType(u32 (_)) => u32 (Int2MInt(1))
rule oneOfSameType(i32 (_)) => i32 (Int2MInt(1))
rule oneOfSameType(u64 (_)) => u64 (Int2MInt(1))
rule oneOfSameType(i64 (_)) => i64 (Int2MInt(1))
rule oneOfSameType(u128(_)) => u128(Int2MInt(1))
rule oneOfSameType(u160(_)) => u160(Int2MInt(1))
rule oneOfSameType(u256(_)) => u256(Int2MInt(1))

endmodule

Expand Down
5 changes: 5 additions & 0 deletions rust-semantics/helpers.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,9 @@ module RUST-HELPERS
rule isSameType(_, _) => false [owise]
rule isSameType(_:Value, & T => T)
rule isSameType(_, $selftype) => true
rule isSameType(u256(_), u256) => true
rule isSameType(u160(_), u160) => true
rule isSameType(u128(_), u128) => true
rule isSameType(i64(_), i64) => true
rule isSameType(u64(_), u64) => true
rule isSameType(i32(_), i32) => true
Expand All @@ -32,6 +35,8 @@ module RUST-HELPERS
rule isUnsignedInt(u32) => true
rule isUnsignedInt(u64) => true
rule isUnsignedInt(u128) => true
rule isUnsignedInt(u160) => true
rule isUnsignedInt(u256) => true
rule isUnsignedInt(&T => T)

syntax Bool ::= isSignedInt(Type) [function, total]
Expand Down
12 changes: 11 additions & 1 deletion rust-semantics/representation.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ module RUST-VALUE-SYNTAX
syntax MInt{32}
syntax MInt{64}
syntax MInt{128}
syntax MInt{160}
syntax MInt{256}

syntax SemanticsError ::= error(String, KItem)

Expand All @@ -25,6 +27,8 @@ module RUST-VALUE-SYNTAX
| i64(MInt{64})
| u64(MInt{64})
| u128(MInt{128})
| u160(MInt{160})
| u256(MInt{256})
| tuple(ValueList)
| struct(TypePath, Map) // Map from field name (Identifier) to value ID (Int)
| Range
Expand Down Expand Up @@ -116,6 +120,8 @@ module RUST-REPRESENTATION
| "i64" [token]
| "u64" [token]
| "u128" [token]
| "u160" [token]
| "u256" [token]
| "bool" [token]
| "str" [token]

Expand Down Expand Up @@ -150,7 +156,9 @@ module RUST-REPRESENTATION
rule checkIntOfType(i32(_), i32) => true
rule checkIntOfType(u64(_), u64) => true
rule checkIntOfType(i64(_), i64) => true
rule checkIntOfType(i64(_), u128) => true
rule checkIntOfType(u128(_), u128) => true
rule checkIntOfType(u160(_), u160) => true
rule checkIntOfType(u256(_), u256) => true
rule checkIntOfType(_, _) => false [owise]

rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u8) requires checkIntOfType(B, u8)
Expand All @@ -162,6 +170,8 @@ module RUST-REPRESENTATION
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u64) requires checkIntOfType(B, u64)
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, i64) requires checkIntOfType(B, i64)
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u128) requires checkIntOfType(B, u128)
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u160) requires checkIntOfType(B, u160)
rule checkIntOfSameType(A:Value, B:Value) => checkIntOfType(A, u256) requires checkIntOfType(B, u256)
rule checkIntOfSameType(_, _) => false [owise]

syntax TypePathOrError ::= TypePath | SemanticsError
Expand Down
Loading
Loading