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

Biguint #106

Merged
merged 1 commit into from
Sep 27, 2024
Merged

Biguint #106

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 0 additions & 2 deletions mx-rust-semantics/main/expression/rust-to-mx.md
View file
Open in desktop
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
Open in desktop
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

```
180 changes: 177 additions & 3 deletions mx-rust-semantics/main/modules/biguint.md
View file
Open in desktop
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,160 @@ 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)
...
</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)
...
</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
Open in desktop
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
Loading