PropNatDedPlugin File

Below is the entire plugin and, it will be broken into sections and explained. The plugin file can be found at this location within your Kekinian installation ().

// #Sireum
/*
 Copyright (c) 2017-2022, Robby, Kansas State University
 All rights reserved.
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
 1. Redistributions of source code must retain the above copyright notice, this
    list of conditions and the following disclaimer.
 2. Redistributions in binary form must reproduce the above copyright notice,
    this list of conditions and the following disclaimer in the documentation
    and/or other materials provided with the distribution.
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
 ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
 ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package org.sireum.logika.plugin

import org.sireum._
import org.sireum.lang.{ast => AST}
import org.sireum.logika.{Logika, Smt2, State, StepProofContext}
import org.sireum.logika.Logika.Reporter

@datatype class PropNatDedPlugin extends Plugin {

  val name: String = "PropNatDedPlugin"

  val justificationIds: HashSet[String] = HashSet ++ ISZ[String]("OrE", "ImplyI", "NegI", "BottomE", "PbC")

  val justificationName: ISZ[String] = ISZ("org", "sireum", "justification", "natded", "prop")

  val bottom: AST.Exp = AST.Exp.LitB(F, AST.Attr(None()))

  @pure override def canHandle(logika: Logika, just: AST.ProofAst.Step.Justification): B = {
    just match {
      case just: AST.ProofAst.Step.Justification.Apply =>
        just.invokeIdent.attr.resOpt.get match {
          case res: AST.ResolvedInfo.Method => return justificationIds.contains(res.id) && res.owner == justificationName
          case _ => return F
        }
      case _ => return F
    }
  }

  override def handle(logika: Logika,
                      smt2: Smt2,
                      cache: Smt2.Cache,
                      log: B,
                      logDirOpt: Option[String],
                      spcMap: HashSMap[AST.ProofAst.StepId, StepProofContext],
                      state: State,
                      step: AST.ProofAst.Step.Regular,
                      reporter: Reporter): Plugin.Result = {
    @pure def isBuiltIn(exp: AST.Exp.Binary, kind: AST.ResolvedInfo.BuiltIn.Kind.Type): B = {
      exp.attr.resOpt.get match {
        case res: AST.ResolvedInfo.BuiltIn if res.kind == kind => return T
        case _ => return F
      }
    }
    @pure def isUBuiltIn(exp: AST.Exp, kind: AST.ResolvedInfo.BuiltIn.Kind.Type): B = {
      exp match {
        case exp: AST.Exp.Unary =>
          exp.attr.resOpt.get match {
            case res: AST.ResolvedInfo.BuiltIn if res.kind == kind => return T
            case _ =>
          }        case _ =>
      }
      return F
    }
    @pure def isBottom(exp: AST.Exp): B = {
      if (exp == bottom) {
        return T
      }
      val res: AST.ResolvedInfo = exp match {
        case exp: AST.Exp.Ident => exp.attr.resOpt.get
        case exp: AST.Exp.Select => exp.attr.resOpt.get
        case _ => return F
      }
      res match {
        case res: AST.ResolvedInfo.Var => return res.id === "F" && res.owner == AST.Typed.sireumName
        case _ =>return F
      }
    }
    val just = step.just.asInstanceOf[AST.ProofAst.Step.Justification.Apply]
    val res = just.invokeIdent.attr.resOpt.get.asInstanceOf[AST.ResolvedInfo.Method]
    @strictpure def emptyResult: Plugin.Result = Plugin.Result(F, state.nextFresh, state.claims)
    val argsOpt = AST.Util.toStepIds(just.args, Logika.kind, reporter)
    if (argsOpt.isEmpty) {
      return emptyResult
    }
    val args = argsOpt.get
    res.id match {
      case string"OrE" =>
        val ISZ(orClaimNo, leftSubProofNo, rightSubProofNo) = args
        val orClaim: AST.Exp.Binary = spcMap.get(orClaimNo) match {
          case Some(StepProofContext.Regular(_, exp: AST.Exp.Binary, _)) if isBuiltIn(exp, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr) => exp
          case _ =>
            reporter.error(orClaimNo.posOpt, Logika.kind, s"Expecting a proof step with a disjunction binary expression claim")
            return emptyResult
        }
        val leftSubProof: HashSet[AST.Exp] = spcMap.get(leftSubProofNo) match {
          case Some(sp@StepProofContext.SubProof(_, exp, _)) if exp == AST.Util.normalizeExp(orClaim.left) => HashSet ++ sp.claims
          case _ =>
            reporter.error(leftSubProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the left-operand of $orClaimNo's claim")
            return emptyResult
        }
        val rightSubProof: HashSet[AST.Exp] = spcMap.get(rightSubProofNo) match {
          case Some(sp@StepProofContext.SubProof(_, exp, _)) if exp == AST.Util.normalizeExp(orClaim.right) => HashSet ++ sp.claims
          case _ =>
            reporter.error(rightSubProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the right-operand of $orClaimNo's claim")
            return emptyResult
        }
        val stepClaim = step.claimNorm
        val ok = leftSubProof.contains(stepClaim) && rightSubProof.contains(stepClaim)
        if (!ok) {
          stepClaim match {
            case stepClaim: AST.Exp.Binary if isBuiltIn(stepClaim, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr) && leftSubProof.contains(AST.Util.normalizeExp(stepClaim.left)) && rightSubProof.contains(AST.Util.normalizeExp(stepClaim.right)) =>
            case _ =>
              reporter.error(step.id.posOpt, Logika.kind, s"Could not infer the stated claim from both sub-proofs $leftSubProofNo and $rightSubProofNo using ${just.invokeIdent.id.value}")
              return emptyResult
          }
        }
      case string"ImplyI" =>
        val claim: AST.Exp.Binary = step.claim match {
          case stepClaim: AST.Exp.Binary if isBuiltIn(stepClaim, AST.ResolvedInfo.BuiltIn.Kind.BinaryImply) => stepClaim
          case _ =>
            reporter.error(step.claim.posOpt, Logika.kind, s"Expecting an implication")
            return emptyResult
        }
        val ISZ(subProofNo) = args
        val subProof: HashSet[AST.Exp] = spcMap.get(subProofNo) match {
          case Some(sp: StepProofContext.SubProof) if sp.assumption == AST.Util.normalizeExp(claim.left) => HashSet ++ sp.claims + sp.assumption
          case _ =>
            reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the antecedent of step ${step.id}'s claim")
            return emptyResult
        }
        if (!subProof.contains(AST.Util.normalizeExp(claim.right))) {
          reporter.error(subProofNo.posOpt, Logika.kind, s"Could not find the consequent of step ${step.id}'s claim in sub-proof $subProofNo")
          return emptyResult
        }
      case string"NegI" =>
        val claim: AST.Exp.Unary = step.claim match {
          case stepClaim: AST.Exp.Unary if isUBuiltIn(stepClaim, AST.ResolvedInfo.BuiltIn.Kind.UnaryNot) => stepClaim
          case _ =>
            reporter.error(step.claim.posOpt, Logika.kind, s"Expecting an implication")
            return emptyResult
        }
        val ISZ(subProofNo) = args
        val subProof: ISZ[AST.Exp] = spcMap.get(subProofNo) match {
          case Some(sp: StepProofContext.SubProof) if sp.assumption == AST.Util.normalizeExp(claim.exp) => sp.claims
          case _ =>
            reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the operand of step ${step.id}'s claim")
            return emptyResult
        }
        if (!ops.ISZOps(subProof).exists(isBottom _)) {
          reporter.error(subProofNo.posOpt, Logika.kind, s"Could not find F in sub-proof $subProofNo")
          return emptyResult
        }
      case string"BottomE" =>
        val ISZ(bottomNo) = args
        spcMap.get(bottomNo) match {
          case Some(sp: StepProofContext.Regular) if isBottom(sp.exp) =>
          case _ =>
            reporter.error(bottomNo.posOpt, Logika.kind, s"Expecting F as step $bottomNo's claim")
            return emptyResult
        }
      case string"PbC" =>
        val ISZ(subProofNo) = args
        val subProof: ISZ[AST.Exp] = spcMap.get(subProofNo) match {
          case Some(sp: StepProofContext.SubProof) if isUBuiltIn(sp.assumption, AST.ResolvedInfo.BuiltIn.Kind.UnaryNot) => sp.claims
          case _ =>
            reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the negation of step ${step.id}'s claim")
            return emptyResult
        }
        if (!ops.ISZOps(subProof).exists(isBottom _)) {
          reporter.error(subProofNo.posOpt, Logika.kind, s"Could not find F in sub-proof $subProofNo")
          return emptyResult
        }
    }
    val (status, nextFresh, claims, claim) = logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
    if (status) {
      val desc = st"${res.id} (of ${(res.owner, ".")})".render
      reporter.inform(step.claim.posOpt.get, Reporter.Info.Kind.Verified,
        st"""Accepted by using the $desc
            |proof tactic implemented in the $name""".render)
    }
    return Plugin.Result(status, nextFresh, claims :+ claim)
  }
}

Packaging and Imports

PropNatDedPlugin.sc code for imports and plugins:

// #Sireum
/*
 Copyright (c) 2017-2022, Robby, Kansas State University
 All rights reserved.
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
 1. Redistributions of source code must retain the above copyright notice, this
    list of conditions and the following disclaimer.
 2. Redistributions in binary form must reproduce the above copyright notice,
    this list of conditions and the following disclaimer in the documentation
    and/or other materials provided with the distribution.
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
 ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
 ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package org.sireum.logika.plugin

import org.sireum._
import org.sireum.lang.{ast => AST}
import org.sireum.logika.{Logika, Smt2, State, StepProofContext}
import org.sireum.logika.Logika.Reporter

The first line of any plugin must include:

// #Sireum

This is because the plugins utilize Sireum, and this is a requirement of Sireum.

Package

It is good practice for all plugins within Logika to be under the package below. The PropNatDedPlugin follows this rule.

package org.sireum.logika.plugin

Imports

The PropNatDedPlugin retains all of the default plugins required of a plugin with no additional imports.

Definition and Class Values

Definition

The definition of the PropNatDedPlugin is as follows:

@datatype class PropNatDedPlugin extends Plugin {

}

Plugins must extend the Plugin type. The name of the plugin reflecting the string utilized in the default plugin list. It is good practice that they match the name of the file itself.

Class-Level Variables

The ClaimOfPlugin contains four class-level variables that are used in evalution that are also a part of any plugin:

  val name: String = "PropNatDedPlugin"

  val justificationIds: HashSet[String] = HashSet ++ ISZ[String]("OrE", "ImplyI", "NegI", "BottomE", "PbC")

  val justificationName: ISZ[String] = ISZ("org", "sireum", "justification", "natded", "prop")

  val bottom: AST.Exp = AST.Exp.LitB(F, AST.Attr(None()))

The name string reflects the name of the plugin itself. It is used to communicate within the plugin itself and the systems outside the file.

The justificationIds value is a HashSet of Strings that contains the keywords or justifications that are used in the proof step (“OrE”, “ImplyI”, “NegI”, “BottomE”, “PbC”)

The justificationName value provides the path from which the justification symbols handled by this plugin are located.

The bottom value is a representation for the bottom symbology.

canHandle Method

The can handle the method of a plugin, and therefore the PropNatDedPlugin works to determine whether or not the plugin is able to handle the step provided. This a required method of any plugin, but in the PropNatDedPlugin’s implementation of the method, it utilizes a methodology to determine its ability to solve the step using the following structured approach:

 @pure override def canHandle(logika: Logika, just: AST.ProofAst.Step.Justification): B = {
    just match {
      case just: AST.ProofAst.Step.Justification.Apply =>
        just.invokeIdent.attr.resOpt.get match {
          case res: AST.ResolvedInfo.Method => return justificationIds.contains(res.id) && res.owner == justificationName
          case _ => return F
        }
      case _ => return F
    }
  }

The canHandle method takes in logika and the justification that the method is seeing if it can handle.

The method then goes into a match block in order to branch into two pathways:

1. If the justification is of the type Apply… then the method evaluates a sub-match block:

   1. If the resulting operation of the justification is of the type method, return the boolean evaluation of (justificationIds.contains(res.id) && res.owner == justificationName). This expression only evaulates to true when the justification’s id is in the listed justifications of the justificationIds values, and the location of the this justification matches the justificationName value defined at the class level.
   2. If the justification is not of the type method, the program will instead just return false.

2. Otherwise, the justification is not of the type Apply, and it returns false, that it can not handle the step’s justification provided.

Simply, this method will only return true if:

1. The justification is of the type Apply
2. The resulting operation of the justification is of the type method.
3. The resulting operation of the justification has an Id that matches on of the Ids listed in the class value.
4. The resulting operation of the justification has is of the path matching the justificationName class level value.

In any other case, it returns false. The reason that this is not a singluar statement chekcing for all of these conditions is that some conditions are predicated on the justification or resulting operation of the justification being of the required type.

Handle Method

The handle method of the PropNatDedPlugin class, or any plugin, is called after its canHandle method returns true. The Logika.scala file’s method once again is the moderator for these calls, however, when determining how we construct a given plugin’s handle method, we can keep in mind that whatever information on the nature of the step and its justification that can be gleaned from the canHandle method is applicable.

Definition

override def handle(logika: Logika, smt2: Smt2, cache: Smt2.Cache, log: B, logDirOpt: Option[String], spcMap: HashSMap[AST.ProofAst.StepId, StepProofContext], state: State, step: AST.ProofAst.Step.Regular, reporter: Reporter): Plugin.Result = {

Since there is a default implementation of the handle method that is provided by the Plugin trait itself, a plugin must use the override keyword. The rest of the definition is a mirror of the Plugin trait’s implementation (src/main/scala/org/sireum/logika/plugin/Plugin.scala). The types and names of the parameters are self explanatory, however, anytime that an option type is presented, it is used to allow for an Option.none() value which can function as a null value of the given type.

Implementation: pure and strictpure Methods

Unlikely the previously described claimOfPlugin, this plugin has to handle multiple different keywords that provide different and destinct functionality. This example is meant to demonstrate that use.

This method has three pure methods, isBuiltIn, isUBuiltIn, and isBottom.

This method also contains one strictpure method, emptyResult.

isBuiltin Method

The isBuiltIn method returns a boolean value that determines if the resulting operation of the expression is BuiltIn and the kind value of that resulting operation is equal to the kind value provided to the method. (TODO)

@pure def isBuiltIn(exp: AST.Exp.Binary, kind: AST.ResolvedInfo.BuiltIn.Kind.Type): B = {
      exp.attr.resOpt.get match {
        case res: AST.ResolvedInfo.BuiltIn if res.kind == kind => return T
        case _ => return F
      }
    }

isBuiltin Method

The isUBuiltIn method returns a boolean value that returns true if the expresion is of the Unary type and the resulting operation of that Unary type is of the BuiltIn type, and the resulting operation must have a kind value matching the kind value passed into the method. Any other situation returns false.

    @pure def isUBuiltIn(exp: AST.Exp, kind: AST.ResolvedInfo.BuiltIn.Kind.Type): B = {
      exp match {
        case exp: AST.Exp.Unary =>
          exp.attr.resOpt.get match {
            case res: AST.ResolvedInfo.BuiltIn if res.kind == kind => return T
            case _ =>
          }        case _ =>
      }

isBottom Method

The isBottom method returns a boolean value that evaluates to true if the expression delivered is equalivalent to the bottom expression. Any other expression returns false.

@pure def isBottom(exp: AST.Exp): B = {
      if (exp == bottom) {
        return T
      }
      val res: AST.ResolvedInfo = exp match {
        case exp: AST.Exp.Ident => exp.attr.resOpt.get
        case exp: AST.Exp.Select => exp.attr.resOpt.get
        case _ => return F
      }
      res match {
        case res: AST.ResolvedInfo.Var => return res.id === "F" && res.owner == AST.Typed.sireumName
        case _ =>return F
      }
    }

emptyResult Method

The strictpure method returns an empty result when an empty argument option is present in the justification being analyzed.

Implementation: Primary

override def handle(logika: Logika,
                      smt2: Smt2,
                      cache: Smt2.Cache,
                      log: B,
                      logDirOpt: Option[String],
                      spcMap: HashSMap[AST.ProofAst.StepId, StepProofContext],
                      state: State,
                      step: AST.ProofAst.Step.Regular,
                      reporter: Reporter): Plugin.Result = {
    @pure def isBuiltIn(exp: AST.Exp.Binary, kind: AST.ResolvedInfo.BuiltIn.Kind.Type): B = {
      //Ommited for clarity.
    }
    @pure def isUBuiltIn(exp: AST.Exp, kind: AST.ResolvedInfo.BuiltIn.Kind.Type): B = {
      //Ommited for clarity.
    }
    @pure def isBottom(exp: AST.Exp): B = {
      //Ommited for clarity.
    }
    val just = step.just.asInstanceOf[AST.ProofAst.Step.Justification.Apply]
    val res = just.invokeIdent.attr.resOpt.get.asInstanceOf[AST.ResolvedInfo.Method]
    @strictpure def emptyResult: Plugin.Result = Plugin.Result(F, state.nextFresh, state.claims)
    val argsOpt = AST.Util.toStepIds(just.args, Logika.kind, reporter)
    if (argsOpt.isEmpty) {
      return emptyResult
    }
    val args = argsOpt.get
    res.id match {
      //Deals with special cases, omitted for clarity.
    }
    val (status, nextFresh, claims, claim) = logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
    if (status) {
      val desc = st"${res.id} (of ${(res.owner, ".")})".render
      reporter.inform(step.claim.posOpt.get, Reporter.Info.Kind.Verified,
        st"""Accepted by using the $desc
            |proof tactic implemented in the $name""".render)
    }
    return Plugin.Result(status, nextFresh, claims :+ claim)
  }

The method begins by placing the justification of the step parameter into a value “just” as an instance of Apply. Then, a value named “res” is created that is the resulting operation of the “just” value as an instance of the Method type. Finally, the value “argsOpt” is created that is the argument options of the “just” value. These three values are used to simplify the readablity of evaluation. Then, the “res” value’s id is evaluated in a match statement that looks to see if it’s Id is equal to any of the following special cases: “OrE, ImplyI, NegI, BottomE, PbC”. The special cases are all justifications that utilize subproofs with different requirements, so it is evaluated in a distinct manner. Regardless of whether or not a justification is one with a special case, it then makes a call to logika’s evaulate regular step claim method, and then checks the status informing the reporter that it is accepted if the status is true. Then a Plugin.Result is returned.

OrE (Or Elimination)

case string"OrE" =>
        val ISZ(orClaimNo, leftSubProofNo, rightSubProofNo) = args
        val orClaim: AST.Exp.Binary = spcMap.get(orClaimNo) match {
          case Some(StepProofContext.Regular(_, exp: AST.Exp.Binary, _)) if isBuiltIn(exp, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr) => exp
          case _ =>
            reporter.error(orClaimNo.posOpt, Logika.kind, s"Expecting a proof step with a disjunction binary expression claim")
            return emptyResult
        }
        val leftSubProof: HashSet[AST.Exp] = spcMap.get(leftSubProofNo) match {
          case Some(sp@StepProofContext.SubProof(_, exp, _)) if exp == AST.Util.normalizeExp(orClaim.left) => HashSet ++ sp.claims
          case _ =>
            reporter.error(leftSubProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the left-operand of $orClaimNo's claim")
            return emptyResult
        }
        val rightSubProof: HashSet[AST.Exp] = spcMap.get(rightSubProofNo) match {
          case Some(sp@StepProofContext.SubProof(_, exp, _)) if exp == AST.Util.normalizeExp(orClaim.right) => HashSet ++ sp.claims
          case _ =>
            reporter.error(rightSubProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the right-operand of $orClaimNo's claim")
            return emptyResult
        }
        val stepClaim = step.claimNorm
        val ok = leftSubProof.contains(stepClaim) && rightSubProof.contains(stepClaim)
        if (!ok) {
          stepClaim match {
            case stepClaim: AST.Exp.Binary if isBuiltIn(stepClaim, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr) && leftSubProof.contains(AST.Util.normalizeExp(stepClaim.left)) && rightSubProof.contains(AST.Util.normalizeExp(stepClaim.right)) =>
            case _ =>
              reporter.error(step.id.posOpt, Logika.kind, s"Could not infer the stated claim from both sub-proofs $leftSubProofNo and $rightSubProofNo using ${just.invokeIdent.id.value}")
              return emptyResult
          }
        }

The OrE case begins with populating the relavant values, “orClaimNo, leftSubProofNo, and rightSubProofNo”. If you recall, this is mimicing the structure of a OrE justification… OrE 1 2 5 (OrE orClaimNo leftSubProofNo rightSubProofNo). This case then looks at the map of claims that we know, and pulls the one indexed at orClaimNo (The Or statement’s number). If the option returned is an appropriate binary expression of a claim:

          case Some(StepProofContext.Regular(_, exp: AST.Exp.Binary, _)) if isBuiltIn(exp, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr) => exp

Then it goes on to evaluate the left subProof. It does a match to the map of claims at the leftSubProofNo this time.

It makes sure that its assumptive step is equal to the left side of the Or claim.

Consider the following line:

          case Some(sp@StepProofContext.SubProof(_, exp, _)) if exp == AST.Util.normalizeExp(orClaim.left) => HashSet ++ sp.claims

The section AST.Util.normalizeExp(orClaim.left) looks at the larger Or claim and provides the left side.

For instance, if…

• exp == p, and orClaim == p | q,

Then,

• AST.Util.normalizeExp(orClaim.left) would provide us with p.

and

• exp == AST.Util.normalizeExp(orClaim.left)

If it does not meet the above case for the left subproof, it returns an empty result using the emptyResult strictpure.

The right side subproof is then evaluated to the same effect as the left using the same strategy.

Finally, the OrE case then looks evaluates the subproofs looking for the conclusion in the claim step.

val stepClaim = step.claimNorm
        val ok = leftSubProof.contains(stepClaim) && rightSubProof.contains(stepClaim)
        if (!ok) {
          stepClaim match {
            case stepClaim: AST.Exp.Binary if isBuiltIn(stepClaim, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr) && leftSubProof.contains(AST.Util.normalizeExp(stepClaim.left)) && rightSubProof.contains(AST.Util.normalizeExp(stepClaim.right)) =>
            case _ =>
              reporter.error(step.id.posOpt, Logika.kind, s"Could not infer the stated claim from both sub-proofs $leftSubProofNo and $rightSubProofNo using ${just.invokeIdent.id.value}")
              return emptyResult
          }

If they do not match, it will throw an error and return the emptyResult strictpure method’s return value.

ImplyI (Implies Introduction)

case string"ImplyI" =>
        val claim: AST.Exp.Binary = step.claim match {
          case stepClaim: AST.Exp.Binary if isBuiltIn(stepClaim, AST.ResolvedInfo.BuiltIn.Kind.BinaryImply) => stepClaim
          case _ =>
            reporter.error(step.claim.posOpt, Logika.kind, s"Expecting an implication")
            return emptyResult
        }
        val ISZ(subProofNo) = args
        val subProof: HashSet[AST.Exp] = spcMap.get(subProofNo) match {
          case Some(sp: StepProofContext.SubProof) if sp.assumption == AST.Util.normalizeExp(claim.left) => HashSet ++ sp.claims + sp.assumption
          case _ =>
            reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the antecedent of step ${step.id}'s claim")
            return emptyResult
        }
        if (!subProof.contains(AST.Util.normalizeExp(claim.right))) {
          reporter.error(subProofNo.posOpt, Logika.kind, s"Could not find the consequent of step ${step.id}'s claim in sub-proof $subProofNo")
          return emptyResult
        }

The ImplyI case begins by opening a match statement that looks at the step’s claim. If the step’s claim is a binary expresssion (AST.Exp.Binary), and if the step’s claim if it is built in accordance with the imply form (isBuiltin(stepClaim, AST.ResolvedInfo.BuiltIn.Kind.BinaryImply)) then the “claim” value is populated with step.claim’s value. If the step’s claim does not meet those conditions, then an error is reported, and the emptyResult is returned.

Then, the arguments of the claim are put into the value “subProofNo”.

A match statement is then opened that evaluates the map of known claim’s at the subProofNo. If the get call is some SubProof context and that context begins with an assumption that is equal to the left hand side of the claim (sp.assumption == AST.Util.normalizeExp(claim.left)) then the “subProof” value is set to a HashSet with the subproof’s map’s claims and assumptions. If it does not meet those requirements, an error is reported to the reporter, and then the emptyResult is returned.

Finally, the ImplyI case checks to see if the “subProof” value does not contain the right side of the “claim” value. If it does not contain the right side, the reporter is given an error and an emptyResult is returned.

NegI (Negation Introduction)

case string"NegI" =>
        val claim: AST.Exp.Unary = step.claim match {
          case stepClaim: AST.Exp.Unary if isUBuiltIn(stepClaim, AST.ResolvedInfo.BuiltIn.Kind.UnaryNot) => stepClaim
          case _ =>
            reporter.error(step.claim.posOpt, Logika.kind, s"Expecting an implication")
            return emptyResult
        }
        val ISZ(subProofNo) = args
        val subProof: ISZ[AST.Exp] = spcMap.get(subProofNo) match {
          case Some(sp: StepProofContext.SubProof) if sp.assumption == AST.Util.normalizeExp(claim.exp) => sp.claims
          case _ =>
            reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the operand of step ${step.id}'s claim")
            return emptyResult
        }
        if (!ops.ISZOps(subProof).exists(isBottom _)) {
          reporter.error(subProofNo.posOpt, Logika.kind, s"Could not find F in sub-proof $subProofNo")
          return emptyResult
        }

The NegI case begins by opening a match statement that looks at the step’s claim. If the step’s claim is of the type Unary (Unary is used with any of the negation tatics), and the step’s claim is of the format for a Unary Not, then the “claim” value is set to the step’s claim. If these requirements are not met, it the reporter is given an error, and the emptyResult is returned.

Next, the case will populate a value, “subProofNo” with the appropriate arguement.

Then, the NegI case opens a match case considering the step proof context from map of claims value at the sub proof’s step id (val subProof: ISZ[AST.Exp] = spcMap.get(subProofNo) match {}). If this sub proof context is of the type SubProof and the assumption of this context is claim’s expression, then the value subProof is populated with subproof’s claims. If these requirements are not met, then the reporter is given an error and the emptyResult is returned.

Finally, the NegI case checks if there does not exist a bottom operator (or equvilant) in the subproof, if there is not one, it will send an error to the reporter and return the emptyResult.

BottomE (Bottom Elimination)

case string"BottomE" =>
        val ISZ(bottomNo) = args
        spcMap.get(bottomNo) match {
          case Some(sp: StepProofContext.Regular) if isBottom(sp.exp) =>
          case _ =>
            reporter.error(bottomNo.posOpt, Logika.kind, s"Expecting F as step $bottomNo's claim")
            return emptyResult
        }

The BottomE case begins by storing the argument stepId into a value called “bottomNo”.

Then the case opens a match statement that considers the step proof context found at the bottomNo index of the claims map. If the context is of the Regular type (regular meaning a standard proof line, not an assumption or subproof or other) and the context’s expression is a bottom expression, then the match statement terminates. If the context does not meet these requirements, the reporter is sent an error and the emptyResult is returned.

PbC (Proof By Contradiction)

case string"PbC" =>
        val ISZ(subProofNo) = args
        val subProof: ISZ[AST.Exp] = spcMap.get(subProofNo) match {
          case Some(sp: StepProofContext.SubProof) if isUBuiltIn(sp.assumption, AST.ResolvedInfo.BuiltIn.Kind.UnaryNot) => sp.claims
          case _ =>
            reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the negation of step ${step.id}'s claim")
            return emptyResult
        }
        if (!ops.ISZOps(subProof).exists(isBottom _)) {
          reporter.error(subProofNo.posOpt, Logika.kind, s"Could not find F in sub-proof $subProofNo")
          return emptyResult
        }

The PbC case begins by storing the argument of the step into the value “subProofNo”.

Then the PbC case opens a match statement that considers the step proof context found at the subProofNo index of the claims map. If the context is of the SubProof type, and the assumption is built in unary in the form of Not, then the value “subProof” is populated with the context’s claims. Otherwise, the reporter is given an error and the emptyResult is returned.

Post Match Statement and Regular Step Evaluation

After any of the noted cases above are considered, then the handle method continues into another section of code that finished the evaluation of the step. If the claim being evaluated is not one of the types above then the handle method should have never been called in the first place. The PropNatDedPlugin only handles the justifications in that have a case within the match statement, any other propositional logic justification are handled by the Inception plugin. This plugin only handles propositional logic rules that use subproofs in their evaluation, or have to consider a bottom operator:

val (status, nextFresh, claims, claim) = logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
    if (status) {
      val desc = st"${res.id} (of ${(res.owner, ".")})".render
      reporter.inform(step.claim.posOpt.get, Reporter.Info.Kind.Verified,
        st"""Accepted by using the $desc
            |proof tactic implemented in the $name""".render)
    }
    return Plugin.Result(status, nextFresh, claims :+ claim)

This section of the method begins by instantiating the “status”, “nextFresh”, “claims”, and “claim” values by calling the method logika.evalRegularStepClaim(…). This method evaluates and takes the now updated values and determines if logika succeeds or fails to prove the step. If it does prove it, it will return true for the “status” value. The nextFresh is value is TODO. The claim and prior claims are passed on a successful evaluation as the updated map of known claims.