Update wasm-semantics regression tests (#1847)

Author: ana-pantilie

test/regression-wasm-semantics-75baf9b/Makefile renamed to test/regression-wasm-semantics-5372938/Makefile

@@ -25,19 +25,14 @@ for spec in \
     simple-arithmetic \
     locals \
     loops \
-    memory-symbolic-type
+    memory
 do
     kollect "test-$spec" \
         ./kwasm prove --backend haskell \
             tests/proofs/"$spec"-spec.k \
             --def-module KWASM-LEMMAS
 done
 
-kollect "test-memory-concrete-type" \
-    ./kwasm prove --backend haskell \
-        tests/proofs/memory-concrete-type-spec.k \
-        --def-module MEMORY-CONCRETE-TYPE-LEMMAS
-
 kollect "test-wrc20" \
     ./kwasm prove --backend haskell \
         tests/proofs/wrc20-spec.k \

test/regression-wasm-semantics-75baf9b/generate.sh renamed to test/regression-wasm-semantics-5372938/generate.sh

@@ -6,12 +6,12 @@ import KWASM-LEMMAS []
 
 
 // claims
-// rule `<generatedTop>`(`<wasm>`(`<k>`(inj{Instrs,KItem}(`___WASM_Instrs_Instr_Instrs`(inj{FoldedInstr,Instr}(`(_)_WASM-TEXT_FoldedInstr_PlainInstr`(`local.get__WASM_PlainInstr_Index`(inj{Int,Index}(X)))),`___WASM_Instrs_Instr_Instrs`(inj{FoldedInstr,Instr}(`(_)_WASM-TEXT_FoldedInstr_PlainInstr`(`local.set__WASM_PlainInstr_Index`(inj{Int,Index}(X)))),inj{EmptyStmts,Instrs}(`.List{"___WASM_EmptyStmts_EmptyStmt_EmptyStmts"}_EmptyStmts`(.KList)))))~>DotVar2),_4,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2,_3),_5,_6,_7,_8,_9,_10,_11),DotVar0)=>`<generatedTop>`(`<wasm>`(`<k>`(DotVar2),_4,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2,_3),_5,_6,_7,_8,_9,_10,_11),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(10), contentStartLine(6), org.kframework.attributes.Location(Location(6,10,9,19)), org.kframework.attributes.Source(Source(/home/ana/kore/wasm-semantics/tests/proofs/locals-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
+// rule `<generatedTop>`(`<wasm>`(`<k>`(inj{Instrs,KItem}(`___WASM_Instrs_Instr_Instrs`(inj{FoldedInstr,Instr}(`(_)_WASM-TEXT_FoldedInstr_PlainInstr`(`local.get__WASM_PlainInstr_Index`(inj{Int,Index}(X)))),`___WASM_Instrs_Instr_Instrs`(inj{FoldedInstr,Instr}(`(_)_WASM-TEXT_FoldedInstr_PlainInstr`(`local.set__WASM_PlainInstr_Index`(inj{Int,Index}(X)))),inj{EmptyStmts,Instrs}(`.List{"___WASM_EmptyStmts_EmptyStmt_EmptyStmts"}_EmptyStmts`(.KList)))))~>DotVar2),_3,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2),_4,_5,_6,_7,_8,_9,_10),DotVar0)=>`<generatedTop>`(`<wasm>`(`<k>`(DotVar2),_3,`<curFrame>`(`<locals>`(`_|->_`(inj{Int,KItem}(X),inj{Val,KItem}(`<_>__WASM-DATA_Val_AValType_Number`(ITYPE,VAL)))),_0,_1,_2),_4,_5,_6,_7,_8,_9,_10),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(10), contentStartLine(6), org.kframework.attributes.Location(Location(6,10,9,19)), org.kframework.attributes.Source(Source(/home/ana/kore/wasm-semantics/tests/proofs/locals-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])]
   claim{} \implies{SortGeneratedTopCell{}} (
       \and{SortGeneratedTopCell{}} (
-      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInstrs{}, SortKItem{}}(Lbl'UndsUndsUnds'WASM'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortFoldedInstr{}, SortInstr{}}(Lbl'LParUndsRParUnds'WASM-TEXT'Unds'FoldedInstr'Unds'PlainInstr{}(Lbllocal'Stop'get'UndsUnds'WASM'Unds'PlainInstr'Unds'Index{}(inj{SortInt{}, SortIndex{}}(VarX:SortInt{})))),Lbl'UndsUndsUnds'WASM'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortFoldedInstr{}, SortInstr{}}(Lbl'LParUndsRParUnds'WASM-TEXT'Unds'FoldedInstr'Unds'PlainInstr{}(Lbllocal'Stop'set'UndsUnds'WASM'Unds'PlainInstr'Unds'Index{}(inj{SortInt{}, SortIndex{}}(VarX:SortInt{})))),inj{SortEmptyStmts{}, SortInstrs{}}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM'Unds'EmptyStmts'Unds'EmptyStmt'Unds'EmptyStmts'QuotRBraUnds'EmptyStmts{}())))),VarDotVar2:SortK{})),Var'Unds'4:SortValstackCell{},Lbl'-LT-'curFrame'-GT-'{}(Lbl'-LT-'locals'-GT-'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(VarX:SortInt{}),inj{SortVal{}, SortKItem{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'AValType'Unds'Number{}(VarITYPE:SortAValType{},VarVAL:SortNumber{})))),Var'Unds'0:SortLocalIdsCell{},Var'Unds'1:SortCurModIdxCell{},Var'Unds'2:SortLabelDepthCell{},Var'Unds'3:SortLabelIdsCell{}),Var'Unds'5:SortModuleRegistryCell{},Var'Unds'6:SortModuleIdsCell{},Var'Unds'7:SortModuleInstancesCell{},Var'Unds'8:SortNextModuleIdxCell{},Var'Unds'9:SortMainStoreCell{},Var'Unds'10:SortDeterministicMemoryGrowthCell{},Var'Unds'11:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
+      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInstrs{}, SortKItem{}}(Lbl'UndsUndsUnds'WASM'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortFoldedInstr{}, SortInstr{}}(Lbl'LParUndsRParUnds'WASM-TEXT'Unds'FoldedInstr'Unds'PlainInstr{}(Lbllocal'Stop'get'UndsUnds'WASM'Unds'PlainInstr'Unds'Index{}(inj{SortInt{}, SortIndex{}}(VarX:SortInt{})))),Lbl'UndsUndsUnds'WASM'Unds'Instrs'Unds'Instr'Unds'Instrs{}(inj{SortFoldedInstr{}, SortInstr{}}(Lbl'LParUndsRParUnds'WASM-TEXT'Unds'FoldedInstr'Unds'PlainInstr{}(Lbllocal'Stop'set'UndsUnds'WASM'Unds'PlainInstr'Unds'Index{}(inj{SortInt{}, SortIndex{}}(VarX:SortInt{})))),inj{SortEmptyStmts{}, SortInstrs{}}(Lbl'Stop'List'LBraQuotUndsUndsUnds'WASM'Unds'EmptyStmts'Unds'EmptyStmt'Unds'EmptyStmts'QuotRBraUnds'EmptyStmts{}())))),VarDotVar2:SortK{})),Var'Unds'3:SortValstackCell{},Lbl'-LT-'curFrame'-GT-'{}(Lbl'-LT-'locals'-GT-'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(VarX:SortInt{}),inj{SortVal{}, SortKItem{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'AValType'Unds'Number{}(VarITYPE:SortAValType{},VarVAL:SortNumber{})))),Var'Unds'0:SortCurModIdxCell{},Var'Unds'1:SortLabelDepthCell{},Var'Unds'2:SortLabelIdsCell{}),Var'Unds'4:SortModuleRegistryCell{},Var'Unds'5:SortModuleIdsCell{},Var'Unds'6:SortModuleInstancesCell{},Var'Unds'7:SortNextModuleIdxCell{},Var'Unds'8:SortMainStoreCell{},Var'Unds'9:SortDeterministicMemoryGrowthCell{},Var'Unds'10:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
       \and{SortGeneratedTopCell{}} (
-      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'k'-GT-'{}(VarDotVar2:SortK{}),Var'Unds'4:SortValstackCell{},Lbl'-LT-'curFrame'-GT-'{}(Lbl'-LT-'locals'-GT-'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(VarX:SortInt{}),inj{SortVal{}, SortKItem{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'AValType'Unds'Number{}(VarITYPE:SortAValType{},VarVAL:SortNumber{})))),Var'Unds'0:SortLocalIdsCell{},Var'Unds'1:SortCurModIdxCell{},Var'Unds'2:SortLabelDepthCell{},Var'Unds'3:SortLabelIdsCell{}),Var'Unds'5:SortModuleRegistryCell{},Var'Unds'6:SortModuleIdsCell{},Var'Unds'7:SortModuleInstancesCell{},Var'Unds'8:SortNextModuleIdxCell{},Var'Unds'9:SortMainStoreCell{},Var'Unds'10:SortDeterministicMemoryGrowthCell{},Var'Unds'11:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{}))))
+      \top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'wasm'-GT-'{}(Lbl'-LT-'k'-GT-'{}(VarDotVar2:SortK{}),Var'Unds'3:SortValstackCell{},Lbl'-LT-'curFrame'-GT-'{}(Lbl'-LT-'locals'-GT-'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortInt{}, SortKItem{}}(VarX:SortInt{}),inj{SortVal{}, SortKItem{}}(Lbl'-LT-Unds-GT-UndsUnds'WASM-DATA'Unds'Val'Unds'AValType'Unds'Number{}(VarITYPE:SortAValType{},VarVAL:SortNumber{})))),Var'Unds'0:SortCurModIdxCell{},Var'Unds'1:SortLabelDepthCell{},Var'Unds'2:SortLabelIdsCell{}),Var'Unds'4:SortModuleRegistryCell{},Var'Unds'5:SortModuleIdsCell{},Var'Unds'6:SortModuleInstancesCell{},Var'Unds'7:SortNextModuleIdxCell{},Var'Unds'8:SortMainStoreCell{},Var'Unds'9:SortDeterministicMemoryGrowthCell{},Var'Unds'10:SortNextFreshIdCell{}),VarDotVar0:SortGeneratedCounterCell{}))))
   [org'Stop'kframework'Stop'attributes'Stop'Source{}(), org'Stop'kframework'Stop'definition'Stop'Production{}(), contentStartLine{}(), contentStartColumn{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}()]
 
 endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}(), org'Stop'kframework'Stop'attributes'Stop'Source{}()]