diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md index e9a8c4374..858b6529c 100644 --- a/prover/lang/kore-lang.md +++ b/prover/lang/kore-lang.md @@ -163,6 +163,7 @@ only in this scenario*. | "\\forall" "{" Patterns "}" Pattern [klabel(forall)] | "\\mu" SetVariable "." Pattern [klabel(mu)] + | "\\nu" SetVariable "." Pattern [klabel(nu)] /* Sugar for \iff, \mu and application */ | "\\iff-lfp" "(" Pattern "," Pattern ")" [klabel(ifflfp)] @@ -354,6 +355,7 @@ module KORE-HELPERS requires getReturnSort(P) =/=K S rule getReturnSort(\mu _ . Phi) => getReturnSort(Phi) + rule getReturnSort(\nu _ . Phi) => getReturnSort(Phi) rule getReturnSort(\or(P, Ps)) => unionSort(getReturnSort(P), getReturnSort(\or(Ps))) rule getReturnSort(\or(.Patterns)) => BottomSort rule getReturnSort(\and(P, Ps)) => intersectSort(getReturnSort(P), getReturnSort(\and(Ps))) @@ -604,6 +606,8 @@ where the term being unfolded has been replace by `#hole`. rule subst(X:Variable,Y:Variable,V) => X requires X =/=K Y rule subst(X:SetVariable,Y:SetVariable,V) => X requires X =/=K Y rule subst(X:Variable,P:Pattern, V) => X requires notBool(isVariable(P) orBool isVariableName(P)) + rule subst(X:SetVariable,P:Pattern, V) => X + requires notBool(isSetVariable(P)) rule subst(I:Int, X, V) => I rule subst(\top(),_,_)=> \top() rule subst(\bottom(),_,_) => \bottom() @@ -680,6 +684,7 @@ Alpha renaming: Rename all bound variables. Free variables are left unchanged. rule alphaRename(\exists { Fs:Patterns } P:Pattern) => #fun(RENAMING => \exists { Fs[RENAMING] } alphaRename(substMap(P,RENAMING))) ( makeFreshSubstitution(Fs) ) rule alphaRename(\mu X . P:Pattern) => \mu !X . alphaRename(subst(P, X, !X)) + rule alphaRename(\nu X . P:Pattern) => \nu !X . alphaRename(subst(P, X, !X)) rule alphaRename(\equals(L, R)) => \equals(alphaRename(L), alphaRename(R)) rule alphaRename(\not(Ps)) => \not(alphaRename(Ps)) rule alphaRename(\functionalPattern(Ps)) => \functionalPattern(alphaRename(Ps)) @@ -753,12 +758,14 @@ single symbol applied to multiple arguments. rule #nnf(S:Symbol(Args)) => S(#nnfPs(Args)) rule #nnf( \or(Ps)) => \or(#nnfPs(Ps)) rule #nnf(\and(Ps)) => \and(#nnfPs(Ps)) + rule #nnf(\implies(L, R)) => #nnf(\or(\not(L), R)) rule #nnf(\not(P)) => \not(P) requires isDnfAtom(P) rule #nnf(\not(S:Symbol(Args))) => \not(S(#nnfPs(Args))) rule #nnf(\not( \or(Ps))) => \and(#nnfPs(#not(Ps))) rule #nnf(\not(\and(Ps))) => \or(#nnfPs(#not(Ps))) rule #nnf(\not(\not(P))) => #nnf(P) + rule #nnf(\not(\implies(L, R))) => #nnf(\not(\or(\not(L), R))) syntax Bool ::= isDnfAtom(Pattern) [function] rule isDnfAtom(V:Variable) => true @@ -768,9 +775,11 @@ single symbol applied to multiple arguments. rule isDnfAtom(\exists{Vs}_) => true rule isDnfAtom(\forall{Vs}_) => true rule isDnfAtom(\mu X . _) => true + rule isDnfAtom(\nu X . _) => true rule isDnfAtom(implicationContext(_, _)) => true rule isDnfAtom(\and(_)) => false rule isDnfAtom(\or(_)) => false + rule isDnfAtom(\implies(_, _)) => false rule isDnfAtom(S:Symbol(ARGS)) => false rule isDnfAtom(\not(P)) => false ``` diff --git a/prover/prover.md b/prover/prover.md index 783474d17..a88ecea0a 100644 --- a/prover/prover.md +++ b/prover/prover.md @@ -56,7 +56,7 @@ module STRATEGIES-EXPORTED-SYNTAX | "right-unfold" "(" "symbols" ":" Patterns "," "bound" ":" Int ")" | "kt" | "kt" "#" KTFilter | "kt-unf" | "kt-unf" "#" KTFilter - | "kt-gfp" | "kt-gfp" "#" KTFilter + | "gfp" | "kt-solve-implications" "(" Strategy ")" | "instantiate-universals-with-ground-terms" | "instantiate-separation-logic-axioms" | "pto-is-injective" diff --git a/prover/strategies/core.md b/prover/strategies/core.md index 3a2b3cefb..633dd9854 100644 --- a/prover/strategies/core.md +++ b/prover/strategies/core.md @@ -26,7 +26,7 @@ module PROVER-CORE-SYNTAX | Strategy "&" Strategy [right, format(%1%n%2 %3)] | Strategy "|" Strategy [right, format(%1%n%2 %3)] syntax Strategy ::= "or-split" | "and-split" | "or-split-rhs" | "and-split-rhs" - syntax Strategy ::= "rhs-top" + syntax Strategy ::= "rhs-top" | "contradiction" syntax Strategy ::= "prune" "(" Patterns ")" syntax Strategy ::= Strategy "{" Int "}" @@ -294,6 +294,14 @@ Internal strategy used to implement `or-split` and `and-split`. rhs-top => success ... ``` +`contradiction` evaluates to success if the second clause is the negation of the first +clause in the LHS conjunction + +```k + rule \implies(\and(P, \not(P), REST), RHS) + contradiction => success ... +``` + If-then-else-fi strategy is useful for implementing other strategies: ```k diff --git a/prover/strategies/knaster-tarski.md b/prover/strategies/knaster-tarski.md index 01c67a1e6..e1e16ee98 100644 --- a/prover/strategies/knaster-tarski.md +++ b/prover/strategies/knaster-tarski.md @@ -249,6 +249,12 @@ for guessing an instantiation of the inductive hypothesis. rule kt-subst(.Patterns, ARGs) => noop ... + // TODO: combine with other kt-unfold rules + rule \implies(LHS, \nu X . P) + => \implies(LHS, subst(P, X, alphaRename(LHS))) + + gfp => noop ... + // unfolded fixed point, HEAD, LRP variables, RHS syntax Pattern ::= substituteBRPs(Pattern, Symbol, Patterns, Pattern) [function] rule substituteBRPs(P:Int, RP, Vs, RHS) => P diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index f4967fcac..935cd07a8 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -206,6 +206,17 @@ Recurse over assoc-only constructors (including `pto`): , rest: REST ) + // Both term and pattern are a nu: + // Recurse over pattern with same fresh variable for each nu term + rule #matchAssoc( terms: (\nu X . T), Ts + => subst(T, X, !F:SetVariable), Ts + , pattern: (\nu Y . P), Ps + => subst(P, Y, !F), Ps + , variables: Vs + , subst: SUBST + , rest: REST + ) + // ground variable: identical rule #matchAssoc( terms: P:Variable, Ts => Ts , pattern: P, Ps => Ps diff --git a/prover/strategies/unfolding.md b/prover/strategies/unfolding.md index 3a37b7db3..fa65ded06 100644 --- a/prover/strategies/unfolding.md +++ b/prover/strategies/unfolding.md @@ -13,6 +13,7 @@ module STRATEGY-UNFOLDING axiom _: \forall { Vs } \iff-lfp(S(Vs), DEF) requires getFreeVariables(DEF) -Patterns Vs =/=K .Patterns rule unfold(\mu X . P) => subst(P, X, alphaRename(\mu X . P)) + rule unfold(\nu X . P) => subst(P, X, alphaRename(\nu X . P)) syntax SymbolDeclaration ::= getSymbolDeclaration(Symbol) [function] rule [[ getSymbolDeclaration(S) => DECL ]] @@ -33,6 +34,8 @@ module STRATEGY-UNFOLDING requires isUnfoldable(R) rule getUnfoldables(\mu X . P, REST) => \mu X . P, getUnfoldables(REST) + rule getUnfoldables(\nu X . P, REST) + => \nu X . P, getUnfoldables(REST) rule getUnfoldables(S:Symbol, REST) => getUnfoldables(REST) requires notBool isUnfoldable(S) @@ -44,6 +47,8 @@ module STRATEGY-UNFOLDING => getUnfoldables(REST) rule getUnfoldables(V:Variable, REST) => getUnfoldables(REST) + rule getUnfoldables(X:SetVariable, REST) + => getUnfoldables(REST) rule getUnfoldables(\not(Ps), REST) => getUnfoldables(Ps) ++Patterns getUnfoldables(REST) rule getUnfoldables(\and(Ps), REST) @@ -88,7 +93,7 @@ module STRATEGY-UNFOLDING left-unfold-oneBody(LRP, \exists { _ } \and(BODY)) => noop ... .K => left-unfold-oneBody(LRP, \and(BODY)) ... - requires #hole { getReturnSort(LRP) } in getFreeVariables(subst(LHS, LRP, #hole { getReturnSort(LRP) })) + requires #hole { TopSort } in getFreeVariables(subst(LHS, LRP, #hole { TopSort })) ``` ### Left Unfold Nth diff --git a/prover/t/ltl/ind.kore b/prover/t/ltl/ind.kore new file mode 100644 index 000000000..32c3f525d --- /dev/null +++ b/prover/t/ltl/ind.kore @@ -0,0 +1,19 @@ +symbol next(TopSort) : TopSort + +// there is always a next state +axiom inf: next(\top()) + +// one-path next implies all-path next +axiom lin: \implies(next(#X), \not(next(\not(#X)))) + +// IND: phi /\ [](phi -> next(phi)) -> []phi +claim \implies( \and( #PHI + , \nu #X . \or(\exists { } \and(\implies(#PHI, next(#PHI)), next(#X))) + ) + , \nu #X . \or(\exists { } \and(#PHI, next(#X))) + ) + +strategy gfp . normalize . left-unfold-Nth(0) . normalize . lift-or . and-split . normalize + . ( ( patterns-equal . rhs-top ) + | ( contradiction ) + )