Skip to content

Commit

Permalink
BigUint operations
Browse files Browse the repository at this point in the history
  • Loading branch information
@virgil-serbanuta
virgil-serbanuta committed Sep 26, 2024
1 parent 401f00f commit 4d08911
Show file tree
Hide file tree
Showing 24 changed files with 556 additions and 74 deletions.
2 changes: 0 additions & 2 deletions mx-rust-semantics/main/expression/rust-to-mx.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,7 @@ module MX-RUST-EXPRESSION-RUST-TO-MX
rule rustToMx(S:String => mxStringValue(S))
rule rustToMx(V:Value => mxIntValue({valueToInteger(V)}:>Int))
requires notBool isSemanticsError(valueToInteger(V))
rule rustToMx(tuple(V:ValueList)) => rustValuesToMxListValue(V, .MxValueList)
syntax RustMxInstruction ::= rustValuesToMxListValue(ValueListOrError, MxValueList)
rule rustValuesToMxListValue(.ValueList, L:MxValueList)
=> rustToMx(mxListValue(reverse(L, .MxValueList)))
rule (.K => rustToMx(HOLE)) ~> rustValuesToMxListValue(((HOLE:Value , V:ValueList) => V), _:MxValueList)
Expand Down
6 changes: 6 additions & 0 deletions mx-rust-semantics/main/glue.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,12 @@ module MX-RUST-GLUE
rule mxIntValue(0) ~> mxRustCheckMxStatus => .K
rule (.K => rustValuesToMxListValue(Values, .MxValueList))
~> rustMxCallHook(_, Values:ValueList)
rule (rustToMx(mxListValue(L:MxValueList)) ~> rustMxCallHook(Hook:MxHookName, _))
=> Hook(L)
rule L:MxValue ~> mxRustWrapInMxList => mxListValue(L)
endmodule
```
182 changes: 179 additions & 3 deletions mx-rust-semantics/main/modules/biguint.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
module MX-RUST-MODULES-BIGUINT
imports private COMMON-K-CELL
imports private MX-COMMON-SYNTAX
imports private MX-RUST-BIGUINT-OPERATORS
imports private MX-RUST-REPRESENTATION
imports private RUST-EXECUTION-CONFIGURATION
imports private RUST-REPRESENTATION
Expand All @@ -25,8 +26,15 @@ module MX-RUST-MODULES-BIGUINT
</k>
<values> ValueId |-> V:Value ... </values>
rule normalizedMethodCall
( #token("BigUint", "Identifier"):Identifier
, #token("zero", "Identifier"):Identifier
, .PtrList
)
=> mxRustBigIntNew(0)
// --------------------------------------
rule bigUintType
rule bigUintFromValueType
=> rustStructType
( #token("BigUint", "Identifier"):Identifier
, ( mxRustStructField
Expand All @@ -36,9 +44,19 @@ module MX-RUST-MODULES-BIGUINT
, .MxRustStructFields
)
)
rule bigUintFromIdType
=> rustStructType
( #token("BigUint", "Identifier"):Identifier
, ( mxRustStructField
( #token("mx_biguint_id", "Identifier"):Identifier
, i32
)
, .MxRustStructFields
)
)
// --------------------------------------
rule mxToRustTyped(#token("BigUint", "Identifier"):Identifier, V:MxValue)
=> mxToRustTyped(bigUintType, mxListValue(V))
=> mxToRustTyped(bigUintFromValueType, mxListValue(V))
rule (.K => MX#bigIntNew(mxIntValue(I)))
~> mxToRustTyped(MxRust#bigInt, mxIntValue(I:Int))
Expand All @@ -50,7 +68,7 @@ module MX-RUST-MODULES-BIGUINT
| "mxRustCreateBigUint"
rule mxRustBigIntNew(V:Int)
=> mxToRustTyped(bigUintType, mxListValue(mxIntValue(V)))
=> mxToRustTyped(bigUintFromValueType, mxListValue(mxIntValue(V)))
rule mxRustEmptyValue(rustType(#token("BigUint", "Identifier")))
=> mxRustBigIntNew(0)
Expand Down Expand Up @@ -89,4 +107,162 @@ module MX-RUST-MODULES-BIGUINT
endmodule
module MX-RUST-BIGUINT-OPERATORS
imports private COMMON-K-CELL
imports private MX-RUST-REPRESENTATION
imports private RUST-EXECUTION-CONFIGURATION
syntax MxRustInstruction ::= rustMxBinaryBigUintOperator(MxHookName, Value, Value)
rule
<k>
rustMxBinaryBigUintOperator
( Hook:MxHookName
, struct
( #token("BigUint", "Identifier"):Identifier #as BigUint:TypePath
, #token("mx_biguint_id", "Identifier"):Identifier |-> FirstId:Int
_:Map
)
, struct
( #token("BigUint", "Identifier"):Identifier #as BigUint:TypePath
, #token("mx_biguint_id", "Identifier"):Identifier |-> SecondId:Int
_:Map
)
)
=> rustMxCallHook(Hook, (V1, V2, .ValueList))
~> mxRustWrapInMxList
~> mxToRustTyped(bigUintFromIdType)
~> implicitCastTo(BigUint)
...
</k>
<values>
FirstId |-> V1:Value
SecondId |-> V2:Value
...
</values>
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
+ ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintOperator(MX#bigIntAdd, V1, V2)
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
- ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintOperator(MX#bigIntSub, V1, V2)
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
* ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintOperator(MX#bigIntMul, V1, V2)
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
/ ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintOperator(MX#bigIntDiv, V1, V2)
rule
(ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _)) #as V1:PtrValue)
+ (ptrValue(_, u64(_:MInt{64})) #as V2:PtrValue)
=> V1 + bigUintFrom(V2)
rule
(ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _)) #as V1:PtrValue)
- (ptrValue(_, u64(_:MInt{64})) #as V2:PtrValue)
=> V1 - bigUintFrom(V2)
rule
(ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _)) #as V1:PtrValue)
* (ptrValue(_, u64(_:MInt{64})) #as V2:PtrValue)
=> V1 * bigUintFrom(V2)
rule
(ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _)) #as V1:PtrValue)
/ (ptrValue(_, u64(_:MInt{64})) #as V2:PtrValue)
=> V1 / bigUintFrom(V2)
syntax Expression ::= bigUintFrom(Expression) [function, total]
rule bigUintFrom(V:Expression)
=> ( #token("BigUint", "Identifier"):Identifier
:: #token("from", "Identifier"):Identifier
:: .PathExprSegments
)
( V, .CallParamsList )
syntax MxRustInstruction ::= rustMxBinaryBigUintComparisonOperator(MxHookName, Value, Value)
rule
<k>
rustMxBinaryBigUintComparisonOperator
( Hook:MxHookName
, struct
( #token("BigUint", "Identifier"):Identifier
, #token("mx_biguint_id", "Identifier"):Identifier |-> FirstId:Int
_:Map
)
, struct
( #token("BigUint", "Identifier"):Identifier
, #token("mx_biguint_id", "Identifier"):Identifier |-> SecondId:Int
_:Map
)
)
=> rustMxCallHook(Hook, (V1, V2, .ValueList))
~> mxToRustTyped(i32)
~> implicitCastTo(i32)
...
</k>
<values>
FirstId |-> V1:Value
SecondId |-> V2:Value
...
</values>
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
== ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
~> mxRustEqResult
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
!= ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
~> mxRustNeResult
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
< ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value) // >
=> rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
~> mxRustLtResult
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
<= ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
~> mxRustLeResult
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
> ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
~> mxRustGtResult
rule
ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V1:Value)
>= ptrValue(_, struct(#token("BigUint", "Identifier"):Identifier, _) #as V2:Value)
=> rustMxBinaryBigUintComparisonOperator(MX#bigIntCmp, V1, V2)
~> mxRustGeResult
syntax MxRustInstruction ::= "mxRustEqResult"
| "mxRustNeResult"
| "mxRustGeResult"
| "mxRustGtResult"
| "mxRustLeResult"
| "mxRustLtResult"
rule V:PtrValue ~> mxRustEqResult => V == ptrValue(null, i32(0p32))
rule V:PtrValue ~> mxRustNeResult => V != ptrValue(null, i32(0p32))
rule V:PtrValue ~> mxRustGeResult => V >= ptrValue(null, i32(0p32))
rule V:PtrValue ~> mxRustGtResult => V > ptrValue(null, i32(0p32))
rule V:PtrValue ~> mxRustLtResult => V < ptrValue(null, i32(0p32)) // >
rule V:PtrValue ~> mxRustLeResult => V <= ptrValue(null, i32(0p32))
endmodule
```
84 changes: 42 additions & 42 deletions mx-rust-semantics/main/modules/proxy.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,75 +89,75 @@ module MX-RUST-MODULES-PROXY
<method-name> MethodName </method-name>
syntax RustMxInstruction ::= rustMxManagedExecuteOnDestContext
( destination: MxOrRustValueOrInstruction // MxOrRustValue
, egldValue: MxOrRustValueOrInstruction // MxOrRustValue
, mxTransfers: MxOrRustValueOrInstruction // MxOrRustValue
, gasLimit: MxOrRustValueOrInstruction // MxOrRustValue
, function: MxOrRustValueOrInstruction // MxOrRustValue
, args: MxOrRustValueOrInstruction // MxOrRustValue
( destination: RustToMxOrInstruction // RustToMx
, egldValue: RustToMxOrInstruction // RustToMx
, mxTransfers: RustToMxOrInstruction // RustToMx
, gasLimit: RustToMxOrInstruction // RustToMx
, function: RustToMxOrInstruction // RustToMx
, args: RustToMxOrInstruction // RustToMx
)
context rustMxManagedExecuteOnDestContext
(... destination: HOLE:MxOrRustValue => rustToMx(HOLE)
, egldValue: _:MxOrRustValue
, mxTransfers: _:MxOrRustValue
, gasLimit: _:MxOrRustValue
, function: _:MxOrRustValue
, args: _:MxOrRustValue
(... destination: HOLE:RustToMx => rustToMx(HOLE)
, egldValue: _:RustToMx
, mxTransfers: _:RustToMx
, gasLimit: _:RustToMx
, function: _:RustToMx
, args: _:RustToMx
)
[result(MxValue)]
context rustMxManagedExecuteOnDestContext
(... destination: Destination:MxOrRustValue
, egldValue: HOLE:MxOrRustValue => rustToMx(HOLE)
, mxTransfers: _:MxOrRustValue
, gasLimit: _:MxOrRustValue
, function: _:MxOrRustValue
, args: _:MxOrRustValue
(... destination: Destination:RustToMx
, egldValue: HOLE:RustToMx => rustToMx(HOLE)
, mxTransfers: _:RustToMx
, gasLimit: _:RustToMx
, function: _:RustToMx
, args: _:RustToMx
)
requires isMxValue(Destination)
[result(MxValue)]
context rustMxManagedExecuteOnDestContext
(... destination: Destination:MxOrRustValue
, egldValue: EgldValue:MxOrRustValue
, mxTransfers: HOLE:MxOrRustValue => rustToMx(HOLE)
, gasLimit: _:MxOrRustValue
, function: _:MxOrRustValue
, args: _:MxOrRustValue
(... destination: Destination:RustToMx
, egldValue: EgldValue:RustToMx
, mxTransfers: HOLE:RustToMx => rustToMx(HOLE)
, gasLimit: _:RustToMx
, function: _:RustToMx
, args: _:RustToMx
)
requires isMxValue(Destination)
andBool isMxValue(EgldValue)
[result(MxValue)]
context rustMxManagedExecuteOnDestContext
(... destination: Destination:MxOrRustValue
, egldValue: EgldValue:MxOrRustValue
, mxTransfers: MxTransfers:MxOrRustValue
, gasLimit: HOLE:MxOrRustValue => rustToMx(HOLE)
, function: _:MxOrRustValue
, args: _:MxOrRustValue
(... destination: Destination:RustToMx
, egldValue: EgldValue:RustToMx
, mxTransfers: MxTransfers:RustToMx
, gasLimit: HOLE:RustToMx => rustToMx(HOLE)
, function: _:RustToMx
, args: _:RustToMx
)
requires isMxValue(Destination)
andBool isMxValue(EgldValue)
andBool isMxValue(MxTransfers)
[result(MxValue)]
context rustMxManagedExecuteOnDestContext
(... destination: Destination:MxOrRustValue
, egldValue: EgldValue:MxOrRustValue
, mxTransfers: MxTransfers:MxOrRustValue
, gasLimit: GasLimit:MxOrRustValue
, function: HOLE:MxOrRustValue => rustToMx(HOLE)
, args: _:MxOrRustValue
(... destination: Destination:RustToMx
, egldValue: EgldValue:RustToMx
, mxTransfers: MxTransfers:RustToMx
, gasLimit: GasLimit:RustToMx
, function: HOLE:RustToMx => rustToMx(HOLE)
, args: _:RustToMx
)
requires isMxValue(Destination)
andBool isMxValue(EgldValue)
andBool isMxValue(MxTransfers)
andBool isMxValue(GasLimit)
[result(MxValue)]
context rustMxManagedExecuteOnDestContext
(... destination: Destination:MxOrRustValue
, egldValue: EgldValue:MxOrRustValue
, mxTransfers: MxTransfers:MxOrRustValue
, gasLimit: GasLimit:MxOrRustValue
, function: Function:MxOrRustValue
, args: HOLE:MxOrRustValue => rustToMx(HOLE)
(... destination: Destination:RustToMx
, egldValue: EgldValue:RustToMx
, mxTransfers: MxTransfers:RustToMx
, gasLimit: GasLimit:RustToMx
, function: Function:RustToMx
, args: HOLE:RustToMx => rustToMx(HOLE)
)
requires isMxValue(Destination)
andBool isMxValue(EgldValue)
Expand Down
Loading

0 comments on commit 4d08911

Please sign in to comment.