Mx BigUint hooks

Makefile

@@ -1,49 +1,60 @@
-SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+RUST_SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
 RUST_PREPROCESSING_KOMPILED ::= .build/rust-preprocessing-kompiled
 RUST_PREPROCESSING_TIMESTAMP ::= $(RUST_PREPROCESSING_KOMPILED)/timestamp
 RUST_EXECUTION_KOMPILED ::= .build/rust-execution-kompiled
 RUST_EXECUTION_TIMESTAMP ::= $(RUST_EXECUTION_KOMPILED)/timestamp
-SYNTAX_INPUT_DIR ::= tests/syntax
-SYNTAX_OUTPUT_DIR ::= .build/syntax-output
+RUST_SYNTAX_INPUT_DIR ::= tests/syntax
+RUST_SYNTAX_OUTPUT_DIR ::= .build/syntax-output
 PREPROCESSING_INPUT_DIR ::= tests/preprocessing
 PREPROCESSING_OUTPUT_DIR ::= .build/preprocessing-output
 EXECUTION_INPUT_DIR ::= tests/execution
 EXECUTION_OUTPUT_DIR ::= .build/execution-output
 
-SYNTAX_INPUTS ::= $(wildcard $(SYNTAX_INPUT_DIR)/*.rs)
-SYNTAX_OUTPUTS ::= $(patsubst $(SYNTAX_INPUT_DIR)/%.rs,$(SYNTAX_OUTPUT_DIR)/%.rs-parsed,$(SYNTAX_INPUTS))
+SYNTAX_INPUTS ::= $(wildcard $(RUST_SYNTAX_INPUT_DIR)/*.rs)
+SYNTAX_OUTPUTS ::= $(patsubst $(RUST_SYNTAX_INPUT_DIR)/%.rs,$(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed,$(SYNTAX_INPUTS))
 
 PREPROCESSING_INPUTS ::= $(wildcard $(PREPROCESSING_INPUT_DIR)/*.rs)
 PREPROCESSING_OUTPUTS ::= $(patsubst $(PREPROCESSING_INPUT_DIR)/%,$(PREPROCESSING_OUTPUT_DIR)/%.preprocessed.kore,$(PREPROCESSING_INPUTS))
-PREPROCESSING_STATUSES ::= $(patsubst %.preprocessed.kore,%.status,$(PREPROCESSING_OUTPUTS))
 
 EXECUTION_INPUTS ::= $(wildcard $(EXECUTION_INPUT_DIR)/*.*.run)
 EXECUTION_OUTPUTS ::= $(patsubst $(EXECUTION_INPUT_DIR)/%,$(EXECUTION_OUTPUT_DIR)/%.executed.kore,$(EXECUTION_INPUTS))
-EXECUTION_STATUSES ::= $(patsubst %.executed.kore,%.status,$(EXECUTION_OUTPUTS))
 
-.PHONY: clean build test syntax-test preprocessing-test execution-test
+MX_SEMANTICS_FILES ::= $(shell find mx-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+MX_TESTING_KOMPILED ::= .build/mx-testing-kompiled
+MX_TESTING_TIMESTAMP ::= $(MX_TESTING_KOMPILED)/timestamp
+MX_TESTING_INPUT_DIR ::= tests/mx
+MX_TESTING_OUTPUT_DIR ::= .build/mx/output
+MX_TESTING_INPUTS ::= $(wildcard $(MX_TESTING_INPUT_DIR)/**/*.mx)
+MX_TESTING_OUTPUTS ::= $(patsubst $(MX_TESTING_INPUT_DIR)/%,$(MX_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_TESTING_INPUTS))
+
+.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test
 
 clean:
 	rm -r .build
 
-build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP)
+build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP) $(MX_TESTING_TIMESTAMP)
 
-test: syntax-test preprocessing-test execution-test
+test: syntax-test preprocessing-test execution-test mx-test
 
 syntax-test: $(SYNTAX_OUTPUTS)
 
 preprocessing-test: $(PREPROCESSING_OUTPUTS)
 
 execution-test: $(EXECUTION_OUTPUTS)
 
-$(RUST_PREPROCESSING_TIMESTAMP): $(SEMANTICS_FILES)
+mx-test: $(MX_TESTING_OUTPUTS)
+
+$(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 	$$(which kompile) rust-semantics/targets/preprocessing/rust.md --emit-json -o $(RUST_PREPROCESSING_KOMPILED)
 
-$(RUST_EXECUTION_TIMESTAMP): $(SEMANTICS_FILES)
+$(RUST_EXECUTION_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 	$$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED)
 
-$(SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
-	mkdir -p $(SYNTAX_OUTPUT_DIR)
+$(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES)
+	$$(which kompile) mx-semantics/targets/testing/mx.md -o $(MX_TESTING_KOMPILED) --debug
+
+$(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
+	mkdir -p $(RUST_SYNTAX_OUTPUT_DIR)
 	kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@
 
 $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
@@ -70,3 +81,13 @@ $(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST
 		-pTEST=$(CURDIR)/parse-test.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
+
+$(MX_TESTING_OUTPUT_DIR)/%.mx.executed.kore: $(MX_TESTING_INPUT_DIR)/%.mx $(MX_TESTING_TIMESTAMP)
+	mkdir -p $(dir $@)
+	krun \
+		$< \
+		--definition $(MX_TESTING_KOMPILED) \
+		--output kore \
+		--output-file $@.tmp
+	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f $@.tmp $@

mx-semantics/main/biguint/configuration.md

@@ -0,0 +1,14 @@
+```k
+
+module MX-BIGUINT-CONFIGURATION
+    imports INT
+    imports MAP
+
+    configuration
+        <mx-biguint>
+            <bigIntHeap> .Map </bigIntHeap>
+            <bigIntHeapNextId> 0 </bigIntHeapNextId>
+        </mx-biguint>
+endmodule
+
+```

mx-semantics/main/biguint/hooks.md

@@ -0,0 +1,101 @@
+```k
+
+module MX-BIGUINT-HOOKS
+    imports BOOL
+    imports COMMON-K-CELL
+    imports K-EQUAL-SYNTAX
+    imports MX-BIGUINT-CONFIGURATION
+    imports MX-COMMON-SYNTAX
+
+    rule
+        <k> MX#bigIntNew(mxIntValue(Value:Int)) => mxIntValue(NextId) ... </k>
+        <bigIntHeap> Ints:Map => Ints[NextId <- Value] </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+
+    rule
+        <k> MX#bigIntAdd(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        +Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    rule
+        <k> MX#bigIntSub(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        -Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    rule
+        <k> MX#bigIntMul(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        *Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    rule
+        <k> MX#bigIntDiv(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue(NextId)
+            ...
+        </k>
+        <bigIntHeap>
+            Ints:Map
+            => Ints [ NextId
+                    <-  {Ints[Id1] orDefault 0}:>Int
+                        /Int {Ints[Id2] orDefault 0}:>Int
+                    ]
+        </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+            andBool Ints[Id2] orDefault 0 =/=K 0
+
+    rule
+        <k> MX#bigIntCmp(mxIntValue(Id1:Int) , mxIntValue(Id2:Int))
+            => mxIntValue
+                ( #cmpInt
+                  ( {Ints[Id1] orDefault 0}:>Int
+                  , {Ints[Id2] orDefault 0}:>Int
+                  )
+                )
+            ...
+        </k>
+        <bigIntHeap> Ints:Map </bigIntHeap>
+        requires Id1 in_keys(Ints) andBool isInt(Ints[Id1] orDefault 0)
+            andBool Id2 in_keys(Ints) andBool isInt(Ints[Id2] orDefault 0)
+
+    syntax Int ::= #cmpInt ( Int , Int ) [function, total, symbol(cmpInt), smtlib(cmpInt)]
+    rule #cmpInt(I1, I2) => -1 requires I1  <Int I2
+    rule #cmpInt(I1, I2) =>  1 requires I1  >Int I2
+    rule #cmpInt(I1, I2) =>  0 requires I1 ==Int I2
+
+endmodule
+
+```

mx-semantics/main/configuration.md

@@ -0,0 +1,14 @@
+```k
+
+requires "biguint/configuration.md"
+
+module MX-COMMON-CONFIGURATION
+    imports MX-BIGUINT-CONFIGURATION
+
+    configuration
+        <mx-common>
+            <mx-biguint/>
+        </mx-common>
+endmodule
+
+```

mx-semantics/main/mx-common.md

@@ -0,0 +1,9 @@
+```k
+
+requires "biguint/hooks.md"
+
+module MX-COMMON
+    imports private MX-BIGUINT-HOOKS
+endmodule
+
+```

mx-semantics/main/syntax.md

@@ -0,0 +1,12 @@
+```k
+
+module MX-COMMON-SYNTAX
+    imports INT-SYNTAX
+
+    syntax MxValue ::= mxIntValue(Int)
+    syntax MxHookName ::= r"MX#[a-zA-Z][a-zA-Z0-9]*"  [token]
+    syntax MxHookArgs ::= List{MxValue, ","}
+    syntax HookCall ::= MxHookName "(" MxHookArgs ")"
+endmodule
+
+```

mx-semantics/targets/testing/configuration.md

@@ -0,0 +1,26 @@
+```k
+
+requires "../../test/configuration.md"
+requires "../../main/configuration.md"
+
+module COMMON-K-CELL
+    imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+    configuration
+        <k> $PGM:MxTest </k>
+endmodule
+
+module MX-CONFIGURATION
+    imports COMMON-K-CELL
+    imports MX-COMMON-CONFIGURATION
+    imports MX-TEST-CONFIGURATION
+
+    configuration
+        <mx-cfg>
+            <k/>
+            <mx-common/>
+            <mx-test/>
+        </mx-cfg>
+endmodule
+
+```

mx-semantics/targets/testing/mx.md

@@ -0,0 +1,19 @@
+```k
+
+requires "configuration.md"
+requires "../../main/mx-common.md"
+requires "../../main/syntax.md"
+requires "../../test/execution.md"
+
+module MX-SYNTAX
+    imports MX-COMMON-SYNTAX
+    imports MX-TEST-EXECUTION-PARSING-SYNTAX
+endmodule
+
+module MX
+    imports private MX-COMMON
+    imports private MX-CONFIGURATION
+    imports private MX-TEST-EXECUTION
+endmodule
+
+```

mx-semantics/test/configuration.md

@@ -0,0 +1,13 @@
+```k
+
+module MX-TEST-CONFIGURATION
+    imports MX-TEST-EXECUTION-PARSING-SYNTAX
+
+    configuration
+        <mx-test>
+            <mx-test-stack> .MxValueStack </mx-test-stack>
+        </mx-test>
+
+endmodule
+
+```

mx-semantics/test/execution.md

@@ -0,0 +1,82 @@
+```k
+
+module MX-TEST-EXECUTION-PARSING-SYNTAX
+    imports INT-SYNTAX
+    imports MX-COMMON-SYNTAX
+
+    syntax TestInstruction  ::= "push" MxValue
+                              | "call" argcount:Int MxHookName
+                              | "get_big_int"
+                              | getBigint(Int)
+                              | "check_eq" MxValue
+
+    syntax MxTest ::= NeList{TestInstruction, ";"}
+
+    syntax MxValueStack ::= List{MxValue, ","}
+endmodule
+
+module MX-TEST-EXECUTION
+    imports private COMMON-K-CELL
+    imports private INT
+    imports private MX-BIGUINT-TEST
+    imports private MX-TEST-CONFIGURATION
+    imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+    rule I:TestInstruction ; Is:MxTest => I ~> Is
+    rule .MxTest => .K
+
+    rule
+        <k> push V:MxValue => .K ... </k>
+        <mx-test-stack> L:MxValueStack => V , L </mx-test-stack>
+
+    rule
+        <k> call N:Int Hook:MxHookName => Hook(takeArgs(N, L)) ... </k>
+        <mx-test-stack> L:MxValueStack => drop(N, L) </mx-test-stack>
+
+    rule
+        <k> V:MxValue => .K ... </k>
+        <mx-test-stack> L:MxValueStack => V , L </mx-test-stack>
+
+    rule
+        <k> get_big_int => testGetBigInt(IntId) ... </k>
+        <mx-test-stack> mxIntValue(IntId) , L:MxValueStack => L </mx-test-stack>
+
+    rule
+        <k> check_eq V => .K ... </k>
+        <mx-test-stack> V , L:MxValueStack => L </mx-test-stack>
+
+    syntax MxHookArgs ::= takeArgs(Int, MxValueStack)  [function, total]
+    rule takeArgs(N:Int, _:MxValueStack) => .MxHookArgs
+        requires N <=Int 0
+    rule takeArgs(N:Int, (V:MxValue ,  Vs:MxValueStack)) => V , takeArgs(N -Int 1, Vs)
+        requires 0 <Int N
+
+    syntax MxValueStack ::= drop(Int, MxValueStack)  [function, total]
+    rule drop(N:Int, Vs:MxValueStack) => Vs
+        requires N <=Int 0
+    rule drop(N:Int, (_V:MxValue ,  Vs:MxValueStack)) => drop(N -Int 1, Vs)
+        requires 0 <Int N
+endmodule
+
+module MX-BIGUINT-TEST
+    imports private BOOL
+    imports private COMMON-K-CELL
+    imports INT
+    imports private MAP
+    imports private MX-BIGUINT-CONFIGURATION
+    imports private MX-COMMON-SYNTAX
+
+    syntax TestInstruction ::= testGetBigInt(Int)
+
+    rule
+        <k> testGetBigInt(IntId:Int)
+            => mxIntValue({Ints[IntId] orDefault 0}:>Int)
+            ...
+        </k>
+        <bigIntHeap> Ints:Map </bigIntHeap>
+        <bigIntHeapNextId> NextId => NextId +Int 1 </bigIntHeapNextId>
+        requires IntId in_keys(Ints) andBool isInt(Ints[IntId] orDefault 0)
+
+endmodule
+
+```