ClaimOfPlugin File

This is the entire plugin, below, 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.symbol.Info
import org.sireum.lang.{ast => AST}
import org.sireum.logika.{Logika, Smt2, State, StepProofContext}
import org.sireum.logika.Logika.Reporter

@datatype class ClaimOfPlugin extends Plugin {

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

  val name: String = "ClaimOfPlugin"

  @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 res.id == "ClaimOf" && 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 = {
    @strictpure def err(): Plugin.Result = Plugin.Result(F, state.nextFresh, state.claims)
    val just = step.just.asInstanceOf[AST.ProofAst.Step.Justification.Apply]
    val arg: AST.Exp = just.args(0) match {
      case a: AST.Exp.Eta => a.ref.asExp
      case a =>
        reporter.error(a.posOpt, Logika.kind, s"Expecting an eta expansion of a fact, theorem, or lemma")
        return err()
    }
    val (name, targs): (ISZ[String], ISZ[AST.Typed]) = arg match {
      case arg: AST.Exp.Ident =>
        arg.attr.resOpt.get match {
          case res: AST.ResolvedInfo.Fact => (res.name, ISZ())
          case res: AST.ResolvedInfo.Theorem => (res.name, ISZ())
          case _ =>
            reporter.error(arg.posOpt, Logika.kind, s"Expecting a fact, theorem, or lemma")
            return err()
        }
      case arg: AST.Exp.Select =>
        arg.attr.resOpt.get match {
          case res: AST.ResolvedInfo.Fact => (res.name, for (t <- arg.targs) yield t.typedOpt.get)
          case res: AST.ResolvedInfo.Theorem => (res.name, ISZ())
          case _ =>
            reporter.error(arg.posOpt, Logika.kind, s"Expecting a fact, theorem, or lemma")
            return err()
        }
      case arg =>
        reporter.error(arg.posOpt, Logika.kind, s"Expecting a name, but found $arg")
        return err()
    }

    val (kind, typeParams, claims): (String, ISZ[AST.TypeParam], ISZ[AST.Exp]) = logika.th.nameMap.get(name).get match {
      case inf: Info.Fact => ("Fact", inf.ast.typeParams, inf.ast.claims)
      case inf: Info.Theorem => (if (inf.ast.isLemma) "Lemma" else "Theorem", inf.ast.typeParams, ISZ(inf.ast.claim))
      case _ => halt("Infeasible")
    }
    val sm = lang.tipe.TypeChecker.buildTypeSubstMap(name, arg.posOpt, typeParams, targs, reporter).get
    val stepClaim = AST.Util.normalizeExp(step.claim)
    for (claim <- claims) {
      val normClaim = AST.Util.normalizeExp(claim)
      val substNormClaim = AST.Util.substExpSkipResolvedInfo(normClaim, sm)
      if (stepClaim == substNormClaim) {
        val claimPos = claim.posOpt.get
        val q = logika.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
        val (stat, nextFresh, claims) = (q._1, q._2, q._3 :+ q._4)
        if (stat) {
          reporter.inform(step.claim.posOpt.get, Reporter.Info.Kind.Verified,
            st"""Accepted by using $kind ${(name, ".")}'s claim at [${claimPos.beginLine}, ${claimPos.beginColumn}], i.e.:
                |
                |$claim
                |""".render)
        }
        return Plugin.Result(stat, nextFresh, claims)
      }
    }

    reporter.error(step.claim.posOpt, Logika.kind, st"Could not find the stated claim in $kind ${(name, ".")}".render)
    return err()
  }

}

Packaging and Imports

---

claimOfPlugin.sc Code:

// #Sireum

package org.sireum.logika.plugin

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

---

First Line

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 ClaimOfPlugin follows this rule.

package org.sireum.logika.plugin

Imports

The ClaimOfPlugin retains all of the default plugins required of a plugin with the addition of the import:

import org.sireum.lang.symbol.Info

This import provides access to the facts and theorm structures that this plugin works within in order to make proof progress.

Definition and Class Values

Definition

The definition of the ClaimOfPlugin is as follows:

@datatype class ClaimOfPlugin 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 two class-level variables that are used in evalution that are also a part of any plugin:

val justificationName: ISZ[String] = ISZ(“org”, “sireum”, “justification”)

val name: String = “ClaimOfPlugin”

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

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.

canHandle Method

The can handle the method of a plugin, and therefore the ClaimOfPlugin 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 ClaimOfPlugin’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 res.id == "ClaimOf" && res.owner == justificationName
          case _ => return F
        }
      case _ => return F
    }
  }

1. Looking at the justification passed into the method (the justification is a child of the step at the Logika level, which is not a direct part of the plugin architecture), the method determines if it is of the type, Apply, if it is not, it returns F, otherwise, it continues.

2. Now, looking at the resulting operation of the justification (just.invokeIdent.attr.resOpt.get), the methods makes sure that the ID is equivalent to “ClaimOf”, and the justificationName class-level (recall that this is the package that we expect the ClaimOf justification to reside in) is equal to the owner property of this justification. If it is not both of these, it will return false, but if both are satisfied, then it will return true.

In short, the canHandle method will only return true if the justification of the step is equal to the relevant keyword, “ClaimOf”, and the use of that key word comes from the appropriate directory with the overall justification being of the appropriate type, Apply. Any other outcome provides a false result.

The ClaimOfPlugin provides a best practice structure from which similar plugins can build their own canHandle methods, testing against similar stored values or literals when appropriate. It is imperative that the methodology for determining the ability of a plugin to handle a step only returns true for a situation that it can handle, and that it is not handling something that another plugin should handle as Logika’s system of determining what plugin to have handle a given line stops asking plugins if it can handle a step once a single plugin has returned that it can. This means that if a plugin appears earlier in the list of plugins that Logika inquiries and has some error in its determination, it could potentially handle errors that are meant for other plugins, or that the plugin can simply not handle.

Handle Method

The handle method of the ClaimOfPlugin 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

There is a definition of a strict pure method within the handle method, and this method, err, returns a Plugin result that denotes an error in the processing of the step provided.

ClaimOfPlugin’s handle method goes through a process resembling the following:

1. Define a value that stores the justification of the step.
2. Determine whether the first expression of the justification’s arguments is any of the eta type, reporting an error and returning if it is not. If so, the value of the expression is held within a value in the method.
3. If the argument is of the type Ident
   1. If the resulting operation of the argument is a fact or a theorem, use the result’s name and an empty list to populate the values name and targs at the method level. If it is neither of these things, report an error and return.
4. If the argument is of the type select
   1. If the resulting operation of the argument is a fact, populate the name value at the method level with the result’s name and a list of the typed options for argument’s targs for the targs at the method level. If the resulting operation of the argument is a theorem, populate the name value at the method level with the result’s name and an empty list for the targs value at the method level.
5. If the argument is not the ident or select type, report an error and return.
   1. Now, if the info from the (logika.th.nameMap.get(name).get) is of the subtype, Fact, the method values kind is set to “Fact”, typeParams is set to the typeParams fo the info, and the claims is set to the claims of the claims. If the info is of the subtype, Theorem, it populates the kind value with whether it is a Lemma or a Theorem (checked via subtype), and then the typeParams is stored in the typeParams at the method level, and an immutable list of claims with the info’s claim stored inside the list.
6. Create a populate values for the substitute map and the stepClaim.
7. Now, for every claim:
   1. Normalize the claim
   2. Substitute the normalized claim, skipping info that is already resolved with respect to the submap.
   3. Then, if the Step’s normalized claim is equal to this current claims normalized and substituted form, then check if logika’s evaluation of the regular step claim returns true, if it does inform the reporter that the claim was accepted. Regardless of whether or not it returned true, return a Plugin.result containing the evaluations information.
8. Finally, if the program reaches the end of this method by any means, report an error and return the @strictpure error just like any other error in this method.