Infrastructure for the UKM semantics

.github/workflows/build-and-test.yaml

@@ -23,7 +23,27 @@
         - name: 'Build the semantics'
           run: docker exec -t k-rust-demo-${{ github.sha }} /bin/bash -c 'make build -j4'
         - name: 'Run Tests'
-          run: docker exec -t k-rust-demo-${{ github.sha }} /bin/bash -c 'make -j4 test'
+          run: docker exec -t k-rust-demo-${{ github.sha }} /bin/bash -c 'make test -j4'
+        - name: 'Tear down Docker'
+          if: always()
+          run: |
+            docker stop k-rust-demo-${{ github.sha }}
+    build-test-legacy:
+      name: 'Build And Test the deprecated Mx semantics'
+      runs-on: [self-hosted, linux, normal]
+      steps:
+        - name: 'Check out code'
+          uses: actions/checkout@v3
+          with:
+            submodules: recursive
+        - name: 'Set up Docker'
+          uses: ./.github/actions/with-docker
+          with:
+            container-name: k-rust-demo-${{ github.sha }}
+        - name: 'Build the semantics'
+          run: docker exec -t k-rust-demo-${{ github.sha }} /bin/bash -c 'make build-legacy -j4'
+        - name: 'Run Tests'
+          run: docker exec -t k-rust-demo-${{ github.sha }} /bin/bash -c 'make test-legacy -j4'
         - name: 'Tear down Docker'
           if: always()
           run: |

Makefile

@@ -59,7 +59,18 @@ DEMOS_TESTING_OUTPUT_DIR ::= .build/demos/output
 DEMOS_TESTING_INPUTS ::= $(wildcard $(DEMOS_TESTING_INPUT_DIR)/*.run)
 DEMOS_TESTING_OUTPUTS ::= $(patsubst $(DEMOS_TESTING_INPUT_DIR)/%,$(DEMOS_TESTING_OUTPUT_DIR)/%.executed.kore,$(DEMOS_TESTING_INPUTS))
 
-.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
+UKM_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+
+UKM_EXECUTION_KOMPILED ::= .build/ukm-execution-kompiled
+UKM_EXECUTION_TIMESTAMP ::= $(UKM_EXECUTION_KOMPILED)/timestamp
+
+UKM_PREPROCESSING_KOMPILED ::= .build/ukm-preprocessing-kompiled
+UKM_PREPROCESSING_TIMESTAMP ::= $(UKM_PREPROCESSING_KOMPILED)/timestamp
+
+UKM_TESTING_KOMPILED ::= .build/ukm-testing-kompiled
+UKM_TESTING_TIMESTAMP ::= $(UKM_TESTING_KOMPILED)/timestamp
+
+.PHONY: clean build build-legacy test test-legacy syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
 
 all: build test
 
@@ -68,13 +79,21 @@ clean:
 
 build: $(RUST_PREPROCESSING_TIMESTAMP) \
 				$(RUST_EXECUTION_TIMESTAMP) \
-				$(MX_TESTING_TIMESTAMP) \
-				$(MX_RUST_TIMESTAMP) \
-				$(MX_RUST_TESTING_TIMESTAMP) \
-				$(MX_RUST_CONTRACT_TESTING_TIMESTAMP) \
-				$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
+				$(UKM_EXECUTION_TIMESTAMP) \
+				$(UKM_PREPROCESSING_TIMESTAMP) \
+				$(UKM_TESTING_TIMESTAMP)
+
+build-legacy: \
+		$(MX_TESTING_TIMESTAMP) \
+		$(MX_RUST_TIMESTAMP) \
+		$(MX_RUST_TESTING_TIMESTAMP) \
+		$(MX_RUST_CONTRACT_TESTING_TIMESTAMP) \
+		$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
 
-test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
+
+test: build syntax-test preprocessing-test execution-test
+
+test-legacy: mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
 
 syntax-test: $(SYNTAX_OUTPUTS)
 
@@ -139,6 +158,30 @@ $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTI
 			-I . \
 			--debug
 
+$(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
+	# Workaround for https://github.com/runtimeverification/k/issues/4141
+	-rm -r $(UKM_EXECUTION_KOMPILED)
+	$$(which kompile) ukm-semantics/targets/execution/ukm-target.md \
+			--emit-json -o $(UKM_EXECUTION_KOMPILED) \
+			-I . \
+			--debug
+
+$(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
+	# Workaround for https://github.com/runtimeverification/k/issues/4141
+	-rm -r $(UKM_PREPROCESSING_KOMPILED)
+	$$(which kompile) ukm-semantics/targets/preprocessing/ukm-target.md \
+			--emit-json -o $(UKM_PREPROCESSING_KOMPILED) \
+			-I . \
+			--debug
+
+$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
+	# Workaround for https://github.com/runtimeverification/k/issues/4141
+	-rm -r $(UKM_TESTING_KOMPILED)
+	$$(which kompile) ukm-semantics/targets/testing/ukm-target.md \
+			--emit-json -o $(UKM_TESTING_KOMPILED) \
+			-I . \
+			--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 > [email protected] && mv -f [email protected] $@

rust-semantics/config.md

@@ -1,5 +1,8 @@
 ```k
 
+requires "execution/configuration.md"
+requires "preprocessing/configuration.md"
+
 module RUST-CONFIGURATION
     imports RUST-EXECUTION-CONFIGURATION
     imports RUST-PREPROCESSING-CONFIGURATION

rust-semantics/full-preprocessing.md

@@ -0,0 +1,26 @@
+```k
+
+requires "error.md"
+requires "expression/bool-operations.md"
+requires "expression/casts.md"
+requires "expression/constants.md"
+requires "expression/integer-operations.md"
+requires "expression/literals.md"
+requires "preprocessing.md"
+requires "representation.md"
+requires "rust-common-syntax.md"
+
+module RUST-FULL-PREPROCESSING
+    imports private RUST-BOOL-OPERATIONS
+    imports private RUST-ERROR
+    imports private RUST-EXPRESSION-CONSTANTS
+    imports private RUST-EXPRESSION-LITERALS
+    imports private RUST-INTEGER-OPERATIONS
+    imports private RUST-PREPROCESSING
+    imports private RUST-REPRESENTATION
+
+    // Making a warning go away
+    rule isLocalVariable(_) => false
+endmodule
+
+```

rust-semantics/targets/preprocessing/rust.md

@@ -1,32 +1,16 @@
 ```k
 
 requires "configuration.md"
-requires "../../error.md"
-requires "../../expression/bool-operations.md"
-requires "../../expression/casts.md"
-requires "../../expression/constants.md"
-requires "../../expression/integer-operations.md"
-requires "../../expression/literals.md"
-requires "../../preprocessing.md"
-requires "../../representation.md"
+requires "../../full-preprocessing.md"
 requires "../../rust-common-syntax.md"
 
 module RUST-SYNTAX
     imports RUST-COMMON-SYNTAX
 endmodule
 
 module RUST
-    imports private RUST-BOOL-OPERATIONS
-    imports private RUST-ERROR
-    imports private RUST-EXPRESSION-CONSTANTS
-    imports private RUST-EXPRESSION-LITERALS
-    imports private RUST-INTEGER-OPERATIONS
-    imports private RUST-PREPROCESSING
-    imports private RUST-REPRESENTATION
+    imports private RUST-FULL-PREPROCESSING
     imports private RUST-RUNNING-CONFIGURATION
-
-    // Making a warning go away
-    rule isLocalVariable(_) => false
 endmodule
 
 ```

ukm-semantics/main/configuration.md

@@ -0,0 +1,8 @@
+```k
+
+module UKM-CONFIGURATION
+    configuration
+        <ukm> .K </ukm>
+endmodule
+
+```

ukm-semantics/main/decoding.md

@@ -0,0 +1,8 @@
+```k
+
+requires "decoding/syntax.md"
+
+module UKM-DECODING
+endmodule
+
+```

ukm-semantics/main/decoding/syntax.md

@@ -0,0 +1,10 @@
+```k
+
+module UKM-DECODING-SYNTAX
+    imports BYTES-SYNTAX
+
+    syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes)
+
+endmodule
+
+```

ukm-semantics/main/encoding.md

@@ -0,0 +1,8 @@
+```k
+
+requires "encoding/syntax.md"
+
+module UKM-ENCODING
+endmodule
+
+```

ukm-semantics/main/encoding/syntax.md

@@ -0,0 +1,10 @@
+```k
+
+module UKM-ENCODING-SYNTAX
+    imports BYTES-SYNTAX
+
+    syntax UKMInstruction ::= "ukmEncodePreprocessedCell"
+
+endmodule
+
+```

ukm-semantics/main/execution.md

@@ -0,0 +1,8 @@
+```k
+
+requires "execution/syntax.md"
+
+module UKM-EXECUTION
+endmodule
+
+```

ukm-semantics/main/execution/syntax.md

@@ -0,0 +1,10 @@
+```k
+
+module UKM-EXECUTION-SYNTAX
+    imports INT-SYNTAX
+
+    syntax UKMInstruction ::= ukmExecute(accountId : Int)
+
+endmodule
+
+```

ukm-semantics/main/preprocessed-configuration.md

@@ -0,0 +1,19 @@
+```k
+
+module UKM-PREPROCESSED-CONFIGURATION
+    configuration
+        <ukm-preprocessed> .K </ukm-preprocessed>
+endmodule
+
+module UKM-FULL-PREPROCESSED-CONFIGURATION
+    imports RUST-PREPROCESSING-CONFIGURATION
+    imports UKM-PREPROCESSED-CONFIGURATION
+
+    configuration
+        <ukm-full-preprocessed>
+            <ukm-preprocessed/>
+            <preprocessed/>
+        </ukm-full-preprocessed>
+endmodule
+
+```

ukm-semantics/main/preprocessing.md

@@ -0,0 +1,8 @@
+```k
+
+requires "preprocessing/syntax.md"
+
+module UKM-PREPROCESSING
+endmodule
+
+```

ukm-semantics/main/preprocessing/syntax.md

@@ -0,0 +1,7 @@
+```k
+
+module UKM-PREPROCESSING-SYNTAX
+    syntax UKMInstruction ::= "ukmPreprocessCrates"
+endmodule
+
+```

ukm-semantics/targets/execution/configuration.md

@@ -0,0 +1,35 @@
+```k
+
+requires "../../main/configuration.md"
+requires "../../main/preprocessed-configuration.md"
+requires "rust-semantics/config.md"
+
+module COMMON-K-CELL
+    imports private BYTES-SYNTAX
+    imports private INT-SYNTAX
+    imports private UKM-DECODING-SYNTAX
+    imports private UKM-EXECUTION-SYNTAX
+
+    configuration
+        <k>
+            ukmDecodePreprocessedCell($PGM:Bytes)
+            ~> ukmExecute($ACCTCODE:Int)
+        </k>
+endmodule
+
+module UKM-TARGET-CONFIGURATION
+    imports COMMON-K-CELL
+    imports RUST-EXECUTION-CONFIGURATION
+    imports UKM-CONFIGURATION
+    imports UKM-FULL-PREPROCESSED-CONFIGURATION
+
+    configuration
+        <ukm-target>
+            <ukm-full-preprocessed/>
+            <ukm/>
+            <execution/>
+            <k/>
+        </ukm-target>
+endmodule
+
+```

ukm-semantics/targets/execution/ukm-target.md

@@ -0,0 +1,19 @@
+```k
+
+requires "../../main/decoding.md"
+requires "../../main/execution.md"
+requires "configuration.md"
+requires "rust-semantics/rust-common.md"
+requires "rust-semantics/rust-common-syntax.md"
+
+module UKM-TARGET-SYNTAX
+endmodule
+
+module UKM-TARGET
+    imports private RUST-COMMON
+    imports private UKM-DECODING
+    imports private UKM-EXECUTION
+    imports private UKM-TARGET-CONFIGURATION
+endmodule
+
+```

ukm-semantics/targets/preprocessing/configuration.md

@@ -0,0 +1,36 @@
+```k
+
+requires "../../main/configuration.md"
+requires "../../main/preprocessed-configuration.md"
+requires "rust-semantics/config.md"
+requires "rust-semantics/full-preprocessing.md"
+requires "rust-semantics/rust-common-syntax.md"
+
+module COMMON-K-CELL
+    imports private RUST-PREPROCESSING-SYNTAX
+    imports private UKM-ENCODING-SYNTAX
+    imports private UKM-PREPROCESSING-SYNTAX
+
+    configuration
+        <k>
+            crateParser($CRATE1:Crate)
+            ~> crateParser($CRATE2:Crate)
+            ~> crateParser($CRATE3:Crate)
+            ~> crateParser($CRATE4:Crate)
+            ~> ukmPreprocessCrates
+            ~> ukmEncodePreprocessedCell
+        </k>
+endmodule
+
+module UKM-TARGET-CONFIGURATION
+    imports COMMON-K-CELL
+    imports UKM-FULL-PREPROCESSED-CONFIGURATION
+
+    configuration
+        <ukm-target>
+            <ukm-full-preprocessed/>
+            <k/>
+        </ukm-target>
+endmodule
+
+```

ukm-semantics/targets/preprocessing/ukm-target.md

@@ -0,0 +1,17 @@
+```k
+
+requires "../../main/encoding.md"
+requires "../../main/preprocessing.md"
+requires "configuration.md"
+
+module UKM-TARGET-SYNTAX
+endmodule
+
+module UKM-TARGET
+    imports private RUST-FULL-PREPROCESSING
+    imports private UKM-ENCODING
+    imports private UKM-PREPROCESSING
+    imports private UKM-TARGET-CONFIGURATION
+endmodule
+
+```