More int types

Pi-Squared-Inc · Oct 18, 2024 · 0c6f064 · 0c6f064
1 parent 810fb1c
commit 0c6f064
Show file tree

Hide file tree

Showing 12 changed files with 243 additions and 135 deletions.
diff --git a/Dockerfile b/Dockerfile
@@ -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
diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md
@@ -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

diff --git a/rust-semantics/expression/comparisons.md b/rust-semantics/expression/comparisons.md
@@ -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
 
 ```
diff --git a/rust-semantics/expression/integer-operations.md b/rust-semantics/expression/integer-operations.md
@@ -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
 
 
@@ -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
 

diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md
@@ -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)
@@ -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))
@@ -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)

diff --git a/rust-semantics/expression/loops.md b/rust-semantics/expression/loops.md
@@ -1,6 +1,7 @@
 ```k
 
 module RUST-LOOP-EXPRESSIONS
+    imports K-EQUAL-SYNTAX
     imports RUST-REPRESENTATION
 
     syntax IteratorLoopExpression ::=  "for1" Pattern "limit" PtrValue BlockExpression
@@ -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
 

diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md
@@ -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
@@ -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]

diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
@@ -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)
 
@@ -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
@@ -116,6 +120,8 @@ module RUST-REPRESENTATION
                         | "i64"  [token]
                         | "u64"  [token]
                         | "u128"  [token]
+                        | "u160"  [token]
+                        | "u256"  [token]
                         | "bool" [token]
                         | "str"  [token]
 
@@ -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) 
@@ -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