Skip to content

Commit f72b8c3

Browse files
ttuegelttuegel
committed
Add test/issue-2244
1 parent 5892a0e commit f72b8c3

File tree

4 files changed

+37782
-0
lines changed

4 files changed

+37782
-0
lines changed

‎test/issue-2244/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
include $(CURDIR)/../include.mk

‎test/issue-2244/spec.kore

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
[]
2+
module LISTSUM-SPEC
3+
4+
// imports
5+
import VERIFICATION []
6+
7+
8+
// claims
9+
// claim `<generatedTop>`(`<michelsonTop>`(_0,_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14,`<k>`(inj{Instruction,KItem}(`ITER___MICHELSON-COMMON-SYNTAX_Instruction_AnnotationList_Block`(`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList),`{_}_MICHELSON-COMMON-SYNTAX_Block_DataList`(`_;__MICHELSON-COMMON-SYNTAX_DataList_Data_DataList`(inj{Instruction,Data}(`DROP__MICHELSON-COMMON-SYNTAX_Instruction_AnnotationList`(`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList))),`_;__MICHELSON-COMMON-SYNTAX_DataList_Data_DataList`(inj{Instruction,Data}(`PUSH____MICHELSON-COMMON-SYNTAX_Instruction_AnnotationList_Type_Data`(`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList),`___MICHELSON-COMMON-SYNTAX_Type_NullaryTypeName_AnnotationList`(inj{NumTypeName,NullaryTypeName}(`int_MICHELSON-COMMON-SYNTAX_NumTypeName`(.KList)),`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList)),inj{Int,Data}(#token("1","Int")))),inj{Instruction,DataList}(`ADD__MICHELSON-COMMON-SYNTAX_Instruction_AnnotationList`(`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList))))))))),`<stack>`(inj{Stack,InternalStack}(`_;__MICHELSON-COMMON_Stack_StackElement_Stack`(`[__]_MICHELSON-COMMON_StackElement_TypeName_Data`(`___MICHELSON-COMMON_TypeName_UnaryTypeName_TypeName`(`list_MICHELSON-COMMON-SYNTAX_UnaryTypeName`(.KList),inj{NumTypeName,TypeName}(`int_MICHELSON-COMMON-SYNTAX_NumTypeName`(.KList))),inj{InternalList,Data}(IntList)),`_;__MICHELSON-COMMON_Stack_StackElement_Stack`(`[__]_MICHELSON-COMMON_StackElement_TypeName_Data`(inj{NumTypeName,TypeName}(`int_MICHELSON-COMMON-SYNTAX_NumTypeName`(.KList)),inj{Int,Data}(I)),`.List{"_;__MICHELSON-COMMON_Stack_StackElement_Stack"}_Stack`(.KList))))),_15,_16,_17,_18,_19,_20,_21,_22,_23),_DotVar0)=>`<generatedTop>`(`<michelsonTop>`(_0,_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14,`<k>`(.K),`<stack>`(inj{Stack,InternalStack}(`_;__MICHELSON-COMMON_Stack_StackElement_Stack`(`[__]_MICHELSON-COMMON_StackElement_TypeName_Data`(inj{NumTypeName,TypeName}(`int_MICHELSON-COMMON-SYNTAX_NumTypeName`(.KList)),inj{Int,Data}(?I)),`.List{"_;__MICHELSON-COMMON_Stack_StackElement_Stack"}_Stack`(.KList)))),_15,_16,_17,_18,_19,_20,_21,_22,_23),_DotVar0) requires #token("true","Bool") ensures `_==Int_`(?I,`_+Int_`(`size(_,_)_MICHELSON-COMMON_Int_InternalList_Int`(IntList,#token("0","Int")),I)) [contentStartColumn(8), contentStartLine(10), org.kframework.attributes.Location(Location(10,8,12,46)), org.kframework.attributes.Source(Source(/Users/skeirik/work/michelson-semantics/././tests/proofs/listsum-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "ensures" Bool [klabel(#ruleEnsures), symbol])]
10+
claim{} \implies{SortGeneratedTopCell{}} (
11+
\and{SortGeneratedTopCell{}} (
12+
\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'michelsonTop'-GT-'{}(Var'Unds'0:SortParamtypeCell{},Var'Unds'1:SortParamvalueCell{},Var'Unds'2:SortStoragetypeCell{},Var'Unds'3:SortStoragevalueCell{},Var'Unds'4:SortMybalanceCell{},Var'Unds'5:SortMyamountCell{},Var'Unds'6:SortMynowCell{},Var'Unds'7:SortMyaddrCell{},Var'Unds'8:SortKnownaddrsCell{},Var'Unds'9:SortSourceaddrCell{},Var'Unds'10:SortSenderaddrCell{},Var'Unds'11:SortMychainidCell{},Var'Unds'12:SortNonceCell{},Var'Unds'13:SortBigmapsCell{},Var'Unds'14:SortScriptCell{},Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInstruction{}, SortKItem{}}(LblITER'UndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'AnnotationList'Unds'Block{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}(),Lbl'LBraUndsRBraUnds'MICHELSON-COMMON-SYNTAX'Unds'Block'Unds'DataList{}(Lbl'UndsSClnUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'DataList'Unds'Data'Unds'DataList{}(inj{SortInstruction{}, SortData{}}(LblDROP'UndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'AnnotationList{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}())),Lbl'UndsSClnUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'DataList'Unds'Data'Unds'DataList{}(inj{SortInstruction{}, SortData{}}(LblPUSH'UndsUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'AnnotationList'Unds'Type'Unds'Data{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}(),Lbl'UndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Type'Unds'NullaryTypeName'Unds'AnnotationList{}(inj{SortNumTypeName{}, SortNullaryTypeName{}}(Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()),Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}()),inj{SortInt{}, SortData{}}(\dv{SortInt{}}("1")))),inj{SortInstruction{}, SortDataList{}}(LblADD'UndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'AnnotationList{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}()))))))),dotk{}())),Lbl'-LT-'stack'-GT-'{}(inj{SortStack{}, SortInternalStack{}}(Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(Lbl'UndsUndsUnds'MICHELSON-COMMON'Unds'TypeName'Unds'UnaryTypeName'Unds'TypeName{}(Lbllist'Unds'MICHELSON-COMMON-SYNTAX'Unds'UnaryTypeName{}(),inj{SortNumTypeName{}, SortTypeName{}}(Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}())),inj{SortInternalList{}, SortData{}}(VarIntList:SortInternalList{})),Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(inj{SortNumTypeName{}, SortTypeName{}}(Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()),inj{SortInt{}, SortData{}}(VarI:SortInt{})),Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}())))),Var'Unds'15:SortInputstackCell{},Var'Unds'16:SortExpectedCell{},Var'Unds'17:SortPreCell{},Var'Unds'18:SortPostCell{},Var'Unds'19:SortInvsCell{},Var'Unds'20:SortSymbolsCell{},Var'Unds'21:SortReturncodeCell{},Var'Unds'22:SortAssumeFailedCell{},Var'Unds'23:SortTraceCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
13+
\exists{SortGeneratedTopCell{}} (Var'Ques'I:SortInt{},
14+
\and{SortGeneratedTopCell{}} (
15+
\equals{SortBool{},SortGeneratedTopCell{}}(
16+
Lbl'UndsEqlsEqls'Int'Unds'{}(Var'Ques'I:SortInt{},Lbl'UndsPlus'Int'Unds'{}(Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(VarIntList:SortInternalList{},\dv{SortInt{}}("0")),VarI:SortInt{})),
17+
\dv{SortBool{}}("true")), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'michelsonTop'-GT-'{}(Var'Unds'0:SortParamtypeCell{},Var'Unds'1:SortParamvalueCell{},Var'Unds'2:SortStoragetypeCell{},Var'Unds'3:SortStoragevalueCell{},Var'Unds'4:SortMybalanceCell{},Var'Unds'5:SortMyamountCell{},Var'Unds'6:SortMynowCell{},Var'Unds'7:SortMyaddrCell{},Var'Unds'8:SortKnownaddrsCell{},Var'Unds'9:SortSourceaddrCell{},Var'Unds'10:SortSenderaddrCell{},Var'Unds'11:SortMychainidCell{},Var'Unds'12:SortNonceCell{},Var'Unds'13:SortBigmapsCell{},Var'Unds'14:SortScriptCell{},Lbl'-LT-'k'-GT-'{}(dotk{}()),Lbl'-LT-'stack'-GT-'{}(inj{SortStack{}, SortInternalStack{}}(Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(inj{SortNumTypeName{}, SortTypeName{}}(Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()),inj{SortInt{}, SortData{}}(Var'Ques'I:SortInt{})),Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}()))),Var'Unds'15:SortInputstackCell{},Var'Unds'16:SortExpectedCell{},Var'Unds'17:SortPreCell{},Var'Unds'18:SortPostCell{},Var'Unds'19:SortInvsCell{},Var'Unds'20:SortSymbolsCell{},Var'Unds'21:SortReturncodeCell{},Var'Unds'22:SortAssumeFailedCell{},Var'Unds'23:SortTraceCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})))))
18+
[org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/skeirik/work/michelson-semantics/././tests/proofs/listsum-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}(), contentStartLine{}(), contentStartColumn{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(10,8,12,46)")]
19+
20+
endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(7,1,14,9)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/skeirik/work/michelson-semantics/././tests/proofs/listsum-spec.k)")]

‎test/issue-2244/test-issue-2244.sh

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#!/bin/sh
2+
exec kore-exec \
3+
vdefinition.kore \
4+
--module VERIFICATION \
5+
--strategy all \
6+
--smt-timeout 40 \
7+
--smt-reset-interval 100 \
8+
--smt z3 \
9+
--log-level \
10+
warning \
11+
--enable-log-timestamps \
12+
--prove spec.kore \
13+
--spec-module LISTSUM-SPEC \
14+
--graph-search breadth-first \
15+
\
16+
\
17+
"$@"

0 commit comments

Comments
 (0)