Merge branch 'master' into _update-deps/runtimeverification/mx-semantics

runtimeverification · Jul 4, 2024 · f0714e7 · f0714e7
2 parents 19ca1a8 + e32daf5
commit f0714e7
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/semantics/user-operations.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/lemmas/semantics/user-operations.md
@@ -8,7 +8,7 @@ module USER-OPERATIONS
   imports LIST
   imports PROOF-SYNTAX
 
-  syntax ProofUserOperation ::= basicListInduction(List)  [symbol, klabel(basicListInduction)]
+  syntax ProofUserOperation ::= basicListInduction(List)  [symbol(basicListInduction)]
 
   rule runProofStep(basicListInduction(L:List))
       => runProof(
@@ -17,7 +17,7 @@ module USER-OPERATIONS
               empty(nop)
           )
 
-  syntax ProofUserOperation ::= moduloBetween0AndM(number:Int, mod:Int)  [symbol, klabel(moduloBetween0AndM)]
+  syntax ProofUserOperation ::= moduloBetween0AndM(number:Int, mod:Int)  [symbol(moduloBetween0AndM)]
 
   rule runProofStep(moduloBetween0AndM(A:Int, M:Int))
       => runProof(
@@ -36,7 +36,7 @@ module USER-OPERATIONS
             )
           )
 
-  syntax ProofUserOperation ::= tModuloBetween0AndM(number:Int, mod:Int)  [symbol, klabel(tModuloBetween0AndM)]
+  syntax ProofUserOperation ::= tModuloBetween0AndM(number:Int, mod:Int)  [symbol(tModuloBetween0AndM)]
 
   rule runProofStep(tModuloBetween0AndM(A:Int, M:Int))
       => runProof(
@@ -55,15 +55,15 @@ module USER-OPERATIONS
             )
           )
 
-  syntax ProofUserOperation ::= numberAsTDivModulo(number:Int, mod:Int)  [symbol, klabel(numberAsTDivModulo)]
+  syntax ProofUserOperation ::= numberAsTDivModulo(number:Int, mod:Int)  [symbol(numberAsTDivModulo)]
 
   rule runProofStep(numberAsTDivModulo(A:Int, M:Int))
       => runProof(
             numberAsTDivModuloHelper(A, M, 0, A)
           )
 
   syntax ProofUserOperation ::= numberAsTDivModuloHelper(number:Int, mod:Int, divresult:Int, modresult:Int)
-      [symbol, klabel(numberAsTDivModuloHelper)]
+      [symbol(numberAsTDivModuloHelper)]
 
   rule runProofStep(numberAsTDivModuloHelper(A:Int, M:Int, Div:Int, Mod:Int))
       => runProof(
@@ -95,15 +95,15 @@ module USER-OPERATIONS
         )
 
 
-  syntax ProofUserOperation ::= numberAsDivModulo(number:Int, mod:Int)  [symbol, klabel(numberAsDivModulo)]
+  syntax ProofUserOperation ::= numberAsDivModulo(number:Int, mod:Int)  [symbol(numberAsDivModulo)]
 
   rule runProofStep(numberAsDivModulo(A:Int, M:Int))
       => runProof(
             numberAsDivModuloHelper(A, M, 0, A)
           )
 
   syntax ProofUserOperation ::= numberAsDivModuloHelper(number:Int, mod:Int, divresult:Int, modresult:Int)
-      [symbol, klabel(numberAsDivModuloHelper)]
+      [symbol(numberAsDivModuloHelper)]
 
   rule runProofStep(numberAsDivModuloHelper(A:Int, M:Int, Div:Int, Mod:Int))
       => runProof(
@@ -135,7 +135,7 @@ module USER-OPERATIONS
         )
 
   syntax ProofUserOperation ::= numberIsNumberMulDiv(number:Int, mod:Int)
-      [symbol, klabel(numberIsNumberMulDiv)]
+      [symbol(numberIsNumberMulDiv)]
 
   rule runProofStep(numberIsNumberMulDiv(A:Int, M:Int))
       => runProof(
@@ -164,7 +164,7 @@ module USER-OPERATIONS
 
 
   syntax ProofUserOperation ::= modAddMultiple(number:Int, multiplier: Int, mod:Int)
-      [symbol, klabel(modAddMultiple)]
+      [symbol(modAddMultiple)]
 
   rule runProofStep(modAddMultiple(A:Int, B:Int, M:Int))
       => runProof(

diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/proof-extensions.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/proof-extensions.md
@@ -5,7 +5,7 @@ module PROOF-EXTENSIONS
   imports ELROND
   imports WASM
 
-  syntax Instr ::= "infiniteLoop"  [symbol, klabel(infiniteLoop)]
+  syntax Instr ::= "infiniteLoop"  [symbol(infiniteLoop)]
   rule <instrs> (infiniteLoop ~> _:KItem => infiniteLoop) ... </instrs>
 
   syntax Bool ::= firstCommandIsNotException(K)  [function, total]