proofrules.maude

fmod INTERSECT-REACHFORM is
  pr REACH-PROOF-GOAL-SIMPLIFICATION .
  pr TRANSITION-OPERATIONS .
  pr TRANSITIONSET-RENAME .
  pr TRANSITIONSET-SUBSTITUTION .
  var U : Module . var UL : ModuleList .
  var T : Term . var C C' : QFForm? . var D TST : QFCTermSet . var R : ReachForm .
  var FSS : FOFormSubstPairSet . var S : Substitution .

  op intersectReachform : Module QFCTermSet ReachForm -> ReachFormSet .
  eq intersectReachform(U,TST,(T | C) => D) = intersectReachform(U,#intersect(U,(T | C),TST),(T | C) => D) .

  op intersectReachform : Module FOFormSubstPair ReachForm -> ReachFormSet .
  eq intersectReachform(U,mtFSPS,R) = mt .
  eq intersectReachform(U,(C',S) | FSS,R) =
    renameVars(0,conj-antc(R << S,C')) & intersectReachform(U,FSS,R) .

  --- OUT: simplify the result of intersecting a reachability formula with a pattern predicate
  ---  NB: we need multiple module arguments for the simplify function
  op simplifyIntersectReachform : NeModuleList QFCTermSet ReachForm -> ReachFormSubstPairSet .
  eq simplifyIntersectReachform(U ; UL,TST,R) = goal-simplify(U ; UL,liftRFSS(intersectReachform(U,TST,R))) .
endfm

fmod REACH-PROOF-GOAL-SUBSUMPTION is
  pr REACH-PROOF-STATE-OPS                 . --- state getters
  pr RLTOOL-BACKEND-IMPL                   . --- checkVal/checkUnsat
  pr CONSTRAINED-TERMSET-MATCH             . --- subsumeByMatch
  pr INTERSECT-REACHFORM                   . --- intersectReachform

  var D : ProofMetadata . var MA : QFCTerm . var MF MF' TST : QFCTermSet .
  var B : Bool . var MB : MaybeBool .
  var F F' : QFForm? . var FSS : FOFormSubstPairSet . var S : Substitution .
  var U : Module . var R : ReachForm . var RS : ReachFormSet .
  var VS : VariableSet .
  var RSS : ReachFormSubstPairSet .

  --- OUT: True if the first set gets subsumed by the second
  op syn-subsume? : ProofMetadata QFCTermSet QFCTermSet -> MaybeBool .
  eq syn-subsume?(D,MF,MF') = subsumeByMatch(get-mod(D),MF,MF') .

  --- PRE: MatchAtom and MatchForm are well-defined with respect to ProofMetadata
  --- OUT: Bool is true means parameterized; otherwise unparameterized
  ----     True if formula generated by subsumeIfValid() is not satisfiable
  op sem-subsume? : ProofMetadata VariableSet QFCTermSet QFCTermSet -> MaybeBool .
  op sem-subsume? : ProofMetadata VariableSet QFCTerm    QFCTermSet -> MaybeBool .
  eq sem-subsume?(D,VS,MA,MF)  = checkVal(D,subsumeIfValid(get-mod(D),VS,MA,MF)) .
  eq sem-subsume?(D,VS,MF,MF') =
    errb('Internal 'Error: 'Semantic 'subsumption 'only 'supports 'term 'sets 'on 'RHS) [owise] .

  op subsume? : ProofMetadata VariableSet ReachForm -> MaybeBool .
  eq subsume?(D,VS,MA => MF) = sem-subsume?(D,VS,MA,MF) .

  op subsume? : ProofMetadata VariableSet ReachFormSubstPairSet -> MaybeBool .
  eq subsume?(D,VS,(R,S) & RSS) = strict-and(subsume?(D,captureNewVars(VS,S),R),subsume?(D,VS,RSS)) .
  eq subsume?(D,VS,mtRFSS) = true .

  --- OUT: true iff the QFCTermSet is disjoint from the head of the reachform or
  ---      the intersected goal is provably subsumed
  op disjointOrSubsume : ProofMetadata VariableSet QFCTermSet ReachForm -> MaybeBool .
  eq disjointOrSubsume(D,VS,TST,MA => MF) =
    subsume?(D,VS,simplifyIntersectReachform(get-mod(D) ; if enableVarUnifSimp then getModByImpl(D,'varsat) else noModule fi,TST,MA => MF)) .
endfm

--- This module defines a function to apply a list of axioms (labelled reach formulas)
--- to a reach formula that represent a goal that we wish to prove.
--- The result is a data structure that records the new goal that would be generated
--- after applying the axiom as well as any formula which we need to prove valid in
--- order to apply the axiom --- i.e. to prove that the axiom LHS constrained term
--- subsumes the LHS constrained term of the reach formula in an unparameterized way
--- N.B. we cannot reuse the subsumption code above we that code only generates the
---      formula we would need to prove validity, but it does not give us access to
---      the substitutions that axiom rule application generated which are needed in
---      order to compute axiom rule successors.
fmod TRANSITION-APPLICATION is
  pr TRANSITIONSET-SUBSTITUTION            .
  pr TRANSITION-CONVERSIONS                .
  pr FOFORMSUBSTITUTION-PAIRSET            .
  pr FOFORM-TRANSITIONSET-PAIR-LIST        .
  pr LABEL-TRANSITION-CONVERSIONS          .
  pr DEBUG-PRINT                           . --- debug-print()
  pr AXIOM-RESULT                          .
  pr CONSTRAINED-TERMSET-MATCH             .
  pr PATTERN-OPS                           .

  var U : Module . var QF QF' : QFForm? .
  var F F' : ReachForm . var AX : LabelReachForm . var AXL : LabelReachFormList .
  var S : Substitution . var FSPS : FOFormSubstPairSet .
  var FK : [FOFormSubstPairSet] . var AK : [LabelReachForm] .

  op apply-axioms : Module ReachForm LabelReachFormList -> [AxiomResultList] .
  eq apply-axioms(U,F,AX ; AXL) = if apply-syn-axiom(U,F,AX) =/= nilax
                                    then apply-syn-axiom(U,F,AX)
                                    else apply-sem-axiom(U,F,AX)
                                  fi apply-axioms(U,F,AXL) .
  eq apply-axioms(U,F,nil) = nilax .
  eq apply-axioms(U,F,AK) = errAxiomResult('Internal 'Error: 'apply-axioms 'ill-formed 'axiomlist '\n) .

  op apply-syn-axiom : Module ReachForm LabelReachForm -> AxiomResultList .
  eq apply-syn-axiom(U,F,AX) = apply-axiom(F,AX,matches(U,antc(trans(AX)),antc(F))) .

  op apply-sem-axiom : Module ReachForm LabelReachForm -> AxiomResultList .
  eq apply-sem-axiom(U,F,AX) = apply-axiom(F,AX,
    apply-sem-axiom(lhs-cond(F),applyMatchToCond(U,none,antc(F),antc(trans(AX))))) .

  op apply-sem-axiom : QFForm? FOFormSubstPairSet ~> FOFormSubstPairSet .
  eq apply-sem-axiom(QF,(QF',S) | FSPS) = (QF ==> QF',S) | apply-sem-axiom(QF,FSPS) .
  eq apply-sem-axiom(QF,mtFSPS)         = mtFSPS .

  --- NB:  This is a helper function that replaces the antecedent of the original ReachForm
  ---      by the succedent of the instantiated axiom ReachForm
  op apply-axiom : ReachForm LabelReachForm FOFormSubstPairSet -> AxiomResultList .
  eq apply-axiom(F,AX,(QF,S) | FSPS) = axrule(AX,S,QF,divide(conj(succ(trans(AX)) << S,lhs-cond(F)) => succ(F))) apply-axiom(F,AX,FSPS) .
  eq apply-axiom(F,AX,mtFSPS) = nilax .
  eq apply-axiom(F,AX,FK) = errAxiomResult(errFOFormSubstPairMsg(FK)) [owise] .
endfm

--- Implementation of reach proof rules follows a few important conventions:
--- [1] the ProofMetadata which contains all of the information needed to complete
---     any operation is passed along as needed
--- [2] each operation extracts out the values it needs from the ProofMetadata before
---     evaluating further --- this eases debugging since the ProofMetadata object can
---     be hidden, allowing only the "real" arguments to appear
--- [3] the result of a proof operation is a ProofUpdate object which, in fact, is
---     isomporphic to the NormalProof itself --- however, the meaning of a ProofUpdate
---     computed from a proof step is NOT to replace the NormalProof --- rather, a
---     merge rule will be called, merging the ProofUpdate into the NormalProof object
---     to produce a new NormalProof
---     NB: essentially, this is a generalization of MSOS write-only fields
--- In the end, we have a system that has:
--- [a] easy extensibility - if we need to pass more arguments along, we can
--- [b] easy debuggability - function returns only interesting data
fmod REACH-PROOF-RULES-AUX is
  pr REACH-PROOF-GOAL .
  pr LCCRULE-NARROWING .
  pr REACH-PROOF-GOAL-SUBSUMPTION .
  pr TRANSITION-APPLICATION .
  pr TRANSITION-TUPLES .
  pr FOFORMSET-RENAME .
  pr TRANSITIONSET-RENAME .
  pr RLTOOL-SWITCHES .
  pr SUBSTITUTIONSET-AUX .

  var ID GN VC : Nat . var CNT : FindResult . var MQ : MaybeQid .
  var V : Variable . var TS : TermSet .
  var QF QF' : QFForm . var QF? : QFForm? . var F F' : ReachForm . var FS : ReachFormSet .
  var G : ProofGoal . var GS : ProofGoalSet .
  var AR : AxiomResult . var ARL ARL' : AxiomResultList .

  var U : Module .
  var LRS : LabelLCCRuleSet .
  var TST : QFCTermSet .
  var S : Substitution .
  var CN CN' : ProofStrat .
  var D D' : ProofMetadata .
  var B : Bool .
  var BK : [Bool] .
  var MB : MaybeBool .
  var RSS : ReachFormSubstPairSet .
  var SRS : StepResultSet .
  var AXL : LabelReachFormList .
  var AX : LabelReachForm .
  var PU : [ProofUpdate] .
  var STR : String .

  var MG  : MaybeProofGoal .
  var MGK : [MaybeProofGoal] .
  var QL  : QidList .
  var SRSK : [StepResultSet] .
  var ARLK : [AxiomResultList] .

  op simp-action : ProofMetadata Module Bool ProofGoal -> ProofUpdate .
  eq simp-action(D,U,B,G) = (none ||
    newChildGoals(G,goal-simplify(U ; if enableVarUnifSimp and B then getModByImpl(D, 'varunif) else noModule fi,liftRFSS(simpDebugPrint(getbody(G)))))) .

  op simpDebugPrint : ReachForm -> ReachForm .
  eq simpDebugPrint(F) = simpDebugPrint2(lhs-cond(F),F) .

  op simpDebugPrint2 : QFForm? ReachForm -> ReachForm .
  eq simpDebugPrint2(QF?,F) = F [print "Constraint: " QF?] .

  op termcheck-action : ProofMetadata Module QFCTermSet ProofGoal -> ProofUpdate .
  op termcheck-action : ProofMetadata Module Bool ProofGoal -> ProofUpdate .
  eq termcheck-action(D,U,TST,G) = termcheck-action(D,U,disjointOrSubsume(D,getvars(G),TST,getbody(G)),G) .
  eq termcheck-action(D,U,MB,G) =
    if MB == true
      then (none || copyGoalToChild(G))
      else (out('\r 'Warning: 'goal &sp printGoalIds(G) &sp 'may 'have 'terminated '\o '\n) || copyGoalToChild(G))
    fi .
  eq [handle-error] :
     termcheck-action(D,U,BK,G) = (out('\r 'Warning: 'termination 'check 'on &sp printGoalIds(G) &sp 'encountered 'an 'error boolErrMsg(BK) '\o '\n)) [owise] .

  --- NOTE: we filter successfully generated step successors through
  ---       renaming + normalization and since A/C/U matching often
  ---       leads to redundant goals being generated
  op step-action : ProofMetadata Module LabelLCCRuleSet ProofGoal -> ProofUpdate .
  op step-action : ProofMetadata Module [StepResultSet] ProofGoal -> ProofUpdate .
  eq step-action(D,U,LRS,G) = step-action(D,U,#top-narrow(U,LRS,getbody(G)),G) .
  eq step-action(D,U,SRS,G) =
     if SRS == noSteps or not wellFormed(U,toReachFormSet(SRS)) then
       (if SRS == noSteps then out('\r 'Warning: 'narrowing 'on 'goal &sp printGoalIds(G) &sp 'generated 'zero 'successors '\o '\n) else none fi ;
        if not wellFormed(U,toReachFormSet(SRS)) then out('\r 'Warning: 'narrowing 'on 'goal printGoalIds(G) 'generated 'ill-formed 'successors '\o '\n) else none fi)
     else
       (none || deleteDuplGoals(0,renameNormalizeGoal(U,get-cnt(D),newChildGoals(G,toReachFormSubstPairSet(SRS)))))
     fi .
  eq [handle-error] :
     step-action(D,U,SRSK,G) =
     (if SRSK :: StepResultSet then none else out('\r 'Warning: 'narrowing 'on 'goal &sp printGoalIds(G) &sp 'encountered 'an 'error errStepResultSetMsg(SRSK) '\o '\n) fi) [owise] .

  op sub-action : ProofMetadata Module ProofGoal -> ProofUpdate .
  op sub-action1 : ProofMetadata Module Bool   ProofGoal -> ProofUpdate .
  op sub-action2 : ProofMetadata Module [Bool] ProofGoal -> ProofUpdate .
  eq sub-action(D,U,G) = sub-action1(D,U,coerceBool(checkUnsat(D,lhs-cond(getbody(G))),false),G) .
  eq sub-action1(D,U,true,G)  = (none || mt) .
  eq sub-action1(D,U,false,G) = sub-action2(D,U,subsume?(D,getvars(G),getbody(G)),G) .
  eq sub-action2(D,U,MB,G) =
    if MB == true
      then (none || mt)
      else if MB == nobool
        then (out('\r 'Warning: 'goal &sp printGoalIds(G) &sp 'satisfaction 'unknown: 'conservatively 'retaining 'goal '\o '\n) || copyGoalToChild(G))
        else (none || copyGoalToChild(G))
      fi
    fi .
  eq [handle-error] :
     sub-action2(D,U,BK,G) = (st(err) ; out('\r 'Warning: 'checking 'goal &sp printGoalIds(G) &sp 'satisfaction 'encountered 'an 'error boolErrMsg(BK) '\o '\n)) [owise] .

  op ax-action : ProofMetadata Module LabelReachForm ProofGoal -> ProofUpdate .
  op ax-action : ProofMetadata Module LabelReachForm [AxiomResultList] ProofGoal -> ProofUpdate .
  op ax-action : ProofMetadata Module ProofMetadata [MaybeBool] AxiomResultList AxiomResultList ProofGoal -> ProofUpdate .
  eq ax-action(D,U,AX,G) = ax-action(D,U,AX,apply-axioms(U,getbody(G),AX),G) .
  eq ax-action(D,U,AX,nilax,G) = (if printAxiomFailures then st(err) ; out('\r 'Notice: 'no 'syntactically 'usable 'instances 'of 'axiom name(AX) 'found 'for &sp printGoalIds(G) '\o '\n) else none fi) .
  eq ax-action(D,U,AX,AR ARL,G) = ax-action(D,U,none,checkVal(D,arCond(AR)),ARL,AR,G) .
  eq [handle-error] :
     ax-action(D,U,AX,ARLK,G) = (st(err) ; out('\r 'Warning: 'generating 'axiom name(AX) 'successors 'for &sp printGoalIds(G) &sp 'encountered 'an 'error errAxiomResultMsg(ARLK) '\o '\n)) [owise] .

  eq ax-action(D,U,D',BK,AR ARL,ARL',G) =
     if BK == true
       then (his(insert(getid(G),usedAxRec(ARL',AR ARL),empty)) || newChildGoalsAddVars(G,arRes(ARL')))
       else ax-action(D,U,printAxFailure(D',U,BK,arAx(ARL'),G), checkVal(D,arCond(AR)), ARL,AR ARL', G)
     fi .
  eq ax-action(D,U,D',BK,nilax,ARL',G) =
     if BK == true
       then (his(insert(getid(G),usedAxRec(ARL',nilax),empty)) || newChildGoalsAddVars(G,arRes(ARL')))
       else (printAxFailure(D',U,BK,arAx(ARL'),G) ; his(insert(getid(G),axrec(ARL'),empty)))
     fi .

  op printAxFailure : ProofMetadata Module [MaybeBool] LabelReachForm ProofGoal -> ProofMetadata .
  eq printAxFailure(D',U,MB,AX,G) = D' ; if printAxiomFailures and MB == nobool then out('\r 'Notice: 'axiom name(AX) 'validity 'for 'goal &sp printGoalIds(G) &sp 'unknown '\o '\n) else none fi .
  eq printAxFailure(D',U,BK,AX,G) = D' ; out('\r 'Warning: 'axiom name(AX) 'validity 'check 'for 'goal &sp printGoalIds(G) &sp 'encountered 'an 'error boolErrMsg(BK) '\o '\n) .

  op usedAxRec : AxiomResultList AxiomResultList -> AxiomRecord .
  eq usedAxRec(ARL,ARL') = axrec(head(ARL),delete(head(ARL),ARL')) .

  --- Derived Rules

  op case-action : ProofMetadata Module Variable TermSet ProofGoal -> ProofUpdate .
  eq case-action(D,U,V,TS,G) =
    if V in vars(antc(getbody(G))) == true
      then if intersection(vars(TS),getvars(G) ; vars(getbody(G))) == none
        then if wellFormedSet(U,assignments(V,TS)) == true
          then (none || newChildGoals(G,getbody(G) RFSS<< assignments(V,TS)))
          else (out('\r 'Warning: 'case 'rule 'substitution 'is 'not 'well-formed '\o '\n))
        fi else (out('\r 'Warning: 'case 'rule 'terms 'intersect 'unsafely 'with 'goal 'target '\o '\n))
      fi else (out('\r 'Warning: 'case 'rule 'variable 'must 'be 'in 'goal 'head '\o '\n))
    fi .

  op split-action : ProofMetadata Module Bool QFForm QFForm ProofGoal -> ProofUpdate .
  op split-action2 : ProofMetadata Module Bool QFForm QFForm ProofGoal -> ProofUpdate .

  eq split-action(D,U,true,QF,QF',G) = split-action2(D,U,true,QF /\ lhs-cond(getbody(G)),QF' /\ lhs-cond(getbody(G)),G) .
  eq split-action(D,U,false,QF,QF',G) = split-action2(D,U,true,QF,QF',G) .

  eq split-action2(D,U,B,QF,QF',G) =
    if QF == QF' then
      (out('\r 'Warning: 'prevented 'attempted 'split 'on 'identical 'formulas '\o))
    else if QF == ff then
      (st(err) ; out('\r 'Error: 'invalid 'split 'value '\o))
    else if safeVars(gather(getbody(G) & set-lhs-cond(getbody(G),QF) & if QF' =/= ff then set-lhs-cond(getbody(G),QF') else mt fi))
      then (out('\r if B or-else checkVal(D,lhs-cond(getbody(G)) <==> QF \/ QF') == true
                  then nil
                  else 'For 'full 'verification '`, &sp 'check 'formula 'equivalence 'manually '\n
                fi '\o)
            || newChildGoalsAddVars(G,conj-antc(getbody(G),QF) & if QF' == ff then mt else conj-antc(getbody(G),QF') fi))
      else (st(err) ; out('\r 'Warning: 'split 'rule 'formulas 'have 'unsafe 'variable 'sharing '\o '\n))
    fi fi fi .

  var PA : ProofRuleAction .

  --- TODO: add flag (or separate function) for one-off runs, to support use-cases like the split rule
  ---       so that we do not invalidate a goal after failing to apply the rule
  op apply-proof-strat : ProofMetadata ProofGoal -> ProofMetadata? .
  eq apply-proof-strat(D,G) = lift-result(G,getstrat(G),D,apply-proof-action(D,nextaction(getstrat(G)),G)) .

  op printStep : Bool String [ProofUpdate] -> ProofUpdate .
  eq printStep(true, STR,(D')) = (D') [print STR " step checked failure"] .
  eq printStep(true, STR,(D' || GS)) =
    if STR == "term-action" or-else STR == "pause-action" then (D' || GS) else printStepNum(STR,numGoals(GS),overlappingVarNames(getbody(GS)),(D' || GS)) fi .
  eq printStep(true, STR,PU) = PU [print STR " ERROR step unchecked failure!" owise label printStepFail] .
  eq printStep(false,STR,PU) = PU .

  op printStepNum : String Nat QidSet [ProofUpdate] -> ProofUpdate .
  eq printStepNum(STR,GN,none,        PU) = PU [print STR " step successors: " GN] .
  eq printStepNum(STR,GN,NQS:NeQidSet,PU) = PU [print STR " step successors: " GN " and overlapping vars: " NQS:NeQidSet] .

  op apply-proof-action : ProofMetadata ProofStrat ProofGoal -> ProofUpdate .
  eq apply-proof-action(D,simplify(B),G)= printStep(printStepName,"simp-action",simp-action(D,get-mod(D),B,G)) .
  eq apply-proof-action(D,subsume,G)    = printStep(printStepName,"sub-action",sub-action(D,get-mod(D),G)) .
  eq apply-proof-action(D,termcheck,G)  = printStep(printStepName,"term-action",termcheck-action(D,get-mod(D),get-tst(D),G)) .
  eq apply-proof-action(D,step,G)       = printStep(printStepName,"step-action",step-action(D,get-mod(D),get-rls(D),G)) .
  eq apply-proof-action(D,axiom(AX),G)  = printStep(printStepName,"ax-action",ax-action(D,get-mod(D),AX,G)) .
  eq apply-proof-action(D,case(V,TS),G) = printStep(printStepName,"case-action",case-action(D,get-mod(D),V,TS,G)) .
  eq apply-proof-action(D,split(B,QF,QF'),G) = printStep(printStepName,"split-action",split-action(D,get-mod(D),B,QF,QF',G)) .
  eq apply-proof-action(D,pause,G)      = printStep(printStepName,"pause-action",(none || newChildGoalWithStrat(G,getstrat(G),paused,getbody(G)))) .
  eq apply-proof-action(D,giveup,G)     = printStep(printStepName,"giveup-action",(none || newChildGoalWithStrat(G,getstrat(G),inactive,getbody(G)))) .

  op lift-result : ProofGoal ProofStrat ProofMetadata ProofUpdate -> ProofMetadata? .
  eq lift-result(G,CN,D,(D')) =
    if update(false,CN) == giveup
      then lift-result(G,D,raw-set(D',out('\r 'Notice: 'proof 'branch 'failed: &sp printGoalIds(G) '\o '\n)),mt)
      else lift-result(G,D,D',newChildGoalWithStrat(G,update(false,CN),active,getbody(G)))
    fi .
  eq lift-result(G,CN,D,(D' || GS)) =
    if update(true,CN) == giveup
      then lift-result(G,D,raw-set(D',out('\r 'Notice: 'proof 'branch 'failed: &sp printGoalIds(G) '\o '\n)),mt)
      else lift-result(G,D,D',setstrat(GS,update(true,CN)))
    fi .
endfm

mod REACH-PROOF-RULES is
  pr REACH-PROOF-RULES-AUX .

  var D : ProofMetadata .
  var P P2 : Parent .
  var ID ID2 : Nat .
  var CN CN2 : ProofStrat .
  var PS PS2 : ProofGoalStatus .
  var PPS : ProofStatus .
  var F : ReachForm .
  var GS : ProofGoalSet .

  rl [select-goal] :
     {D ; st(PPS) ; prf(GS)}
  => if getActiveGoal(GS) :: ProofGoal
       then [merge(D ; prf(delgl(GS,getActiveGoal(GS))) ; st(PPS), apply-proof-strat(D,getActiveGoal(GS)))]
       else [D ; st(done) ; prf(GS)]
     fi .
endm