Section Topics

1. Getting Started
2. Creating the Plugin File
3. Initial Structure of Plugin File
4. Template Plugin File
5. Implementing Basic Functionality
6. Adding and Recognizing Needed Justification Symbols to Kekinian
7. Testing Plugin Functionality

Getting Started

Return to Topics

1. Premilinaries
2. Important Folders
3. Basic Requirements

Premilinaries

1. Sireum and the Kekinian codebase is installed including having run the initial setup along with being at on its newest version.

2. The enviroment variable $SIREUM_HOME$ is set to your Kekinian installation.

This tutorial uses “kekinian folder” to refer to the location where kekinian is installed (i.e., the path given for the environment variable $SIREUM_HOME$ during the Sireum installation. When the tutorial provides a screen shot or path, the SIREUM_HOME folder should be understood to be the root.

3. A working installation of Sireum’s custom version of the Intellij IVE.

4. Make sure that you have $SIREUM_HOME$ open within Sireum Intellij (Kekinian folder). This can be accopmlished through File --> Open and then finding the directory of your codebase.

The source code for Logika is found in the logika folder within this SIREUM_HOME folder, and the source code for Logika plugins is held within the logika subfolder structure.

Important Folders

Your folder at SIREUM_HOME (the Kekinian folder) is the root for all of the following:

Plugins Folder: $SIREUM_HOME$/logika/shared/src/main/scala/org/sireum/logika/plugin

Logika Folder (Contains Logika.scala which has the list of plugins that are in use): $SIREUM_HOME$/logika/shared/src/main/scala/org/sireum/logika

Sireum CLI Object Folder: $SIREUM_HOME$/cli/jvm/src/main/scala/org/sireum

Sireum Build.cmd Folder: $SIREUM_HOME$/bin

Basic Requirements

Once the plugin file is created, listed below are the basic requirements for a plugin file. The requirements should also be met once the above sections are complete. If the file has the aspects mentioned in the step summary and the plugin is listed within the default plugin list, then you can rebuild your SIREUM_HOME installation (In your terminal, use the command:

MacOS / Linux:

${SIREUM_HOME}/bin/build.cmd setup

Windows:

${SIREUM_HOME}\bin\build.cmd setup

From there, you are able to utilize a proper plugin.

Creating the Plugin File

Return to Topics

While a developer can adapt where their plugin source is located within the SIREUM_HOME codebase, it is best practice to put plugin sources in the standard plugin location (/kekinian/logika/shared/src/main/scala/org.sireum.logika/plugin). The default plugins for Logika can be found in the plugin folder and may be studied as examples of how to code plugins. More important folders are listed below

To hold the source for a new plugin, create a scala file (<pluginName>.sc) in the plugin folder (/kekinian/logika/shared/src/main/scala/org.sireum.logika/plugin) (or copy an existing plugin file to adapt). The file name should be distinct from those of other plugins.

Step Summary

1. Locate the plugin folder (/kekinian/logika/shared/src/main/scala/org.sireum.logika/plugin)

2. Create a scala file with the appropriate name in the folder. The extension should be (file_name.scala)

Initial Structure of Plugin File

Return to Topics

• First Line
• Packaging
• Imports
• Plugin Definition
• Step Summary

Now that the plugin file is created, add the necessary content to make the file compatible with Logika’s expected structure for a plugin, as described below.

First Line

The first line of the plugin file must be:

 //# Sireum

This indicates that the source code of the file is within the Slang subset of Scala, and causes the Sireum IVE and compiler infrastructure to use the Slang extensions to the Scala compiler.

Packaging

The package name should be given as:

package org.sireum.logika.plugin

Imports

The imports for the file are given after the package name, as follows:

import org.sireum._   // must be listed first among the imports
import org.sireum.lang.{ast => AST}
import org.sireum.logika.{Logika, Smt2, State, StepProofContext}
import org.sireum.logika.Logika.Reporter

The import org.sireum._ must be listed first for the Slang compiler to work correctly (an error is reported if this import is not given first).

The other imports come from those used in the plugin class that all plugins must extend in their definition. A summary of the purpose of each is given below.

The org.sireum.lang.{ast => AST} import includes data types and methods for representing the abstract syntax of Slang – in particular, the syntax of boolean expressions, logical operators, identifiers, and proof language commands used by Slang contracts and Logika proofs.

The org.sireum.logika.{Logika, Smt2, State, StepProofContext} import brings in four seperate elements: the Logika, Smt2, State, and StepProofContext frameworks.

1. the Logika element evaluates and organizes the claims inherrent to a program or proof. This is where the defaultPlugin value originates from.

2. The Smt2 makes statements that are able to be fed to the smt2 solver.

3. The State element provides the framework and conversion of the code into a workable state of the program during proofs.

4. The StepProofContext import is for the structuring the typed proof lines into elements that can be made sense of to other sections of the evaluation, such as these plugins.

The org.sireum.logika.Logika.Reporter imports a reporter class that is specific to the Logika framework. It is important to keep in mind when using the report for plugin development that when the reporter is assigned to a global or local variable from a reporter that is passed in, the created reporter will be a copy, and it will not update with the original reporter, instead, they will function separately. If the original referenced reporter is to be updated, it will have to be done manually.

Plugin Definition

The follow datatype, value, and method declarations define the structure and content of the plugin.

Plugin definitions are phrased as Slang datatypes that extend Plugin.

@datatype class <pluginName> extends Plugin {
  ...
}

The following fields must be defined within the datatype body:

Values:

The name (string) of the plugin used as an identifier, e.g., in the default plugin list. It is good practice for this string to match the plugin file name. It is not required that the name matches the name of the class, however, it is otherwise not evident what the name refers to.

@pure def name: String = <plugin Name> 

canHandle Method

@pure def canHandle(logika: Logika, just: AST.ProofAst.Step.Justification): B

The canHandle method is meant to look at the step’s justification and determine if the corresponding plugin is able to handle the form that the justification is in. Usually, this means the method determines if the justification’s text matches one of the ids that this plugin can handle and then ensuring that the justification comes from the correct place in the heirarchy. More information on implementing the canHandle method is detailed in a later section.

handle Method

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

The handle method considers the details of the justification and its arguments along with the spcMap of previous steps in order to determine if the step is correct, and if it is, what it proves to the proof’s known claims. More information on implementing the handle method is detailed in a later section.

Step Summary

1. Have the first line of the plugin be: // #Sireum

2. The [package] of the file should be:

package org.sireum.logika.plugin 

3. The imports of the plugin should include:

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

4. The definition of the plugin should be given as a Slang data type that extends the Plugin class:

@datatype class Plugin_Name extends Plugin { ... }

Template Plugin File

Return to Topics

The following Slang code can be used as a template for creating a Logika plugin. The template is presented for a plugin named MyPlugin. Replace occurrences of “MyPlugin” with a name for your plugin the identifies its function with the Logika proof language.

[MyPlugin.scala]

// #Sireum  // indicates the file is in the Slang subset of Scala

//The package statement follows the other plugins.
package org.sireum.logika.plugin

//The four imports utilized by the base Plugin structure, which all plugins extend.
import org.sireum._
import org.sireum.lang.{ast => AST}
import org.sireum.logika.{Logika, Smt2, State, StepProofContext}
import org.sireum.logika.Logika.Reporter

// Slang datatype extending Plugin that provides the definition of the plugin.
//   The convention is that the name of the datatype matches the file name.
@datatype class MyPlugin extends Plugin {

  // Specify the name of the plugin.
  //   The convention is that the name of the datatype matches the file name.
  val name: String = "MyPlugin"

  // canHandle overrides a method from the Plugin datatype. 
  // Must return a Boolean denoting if a step can be handled by this plugin.
  @pure override def canHandle(logika: Logika, just: AST.ProofAst.Step.Justification): B = {
    return false
  }

  // handle overrides a method from the Plugin datatype. 
  // Must return a Plugin.Result indicating whether or not the application of the rule 
  // on the supplied argument holds.  If the rule holds, data structures associated with
  // the proof context are updated.
    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 = {
    return Plugin.Result(F,0,null)
  }
}

The important elements of the example are:

• The Package
• The Imports
• The Class Definition
• The canHandle Method
• The handle Method

Implementing Basic Functionality

Return to Topics

• Implementing canHandle Method
  • Justification Name and Justification Ids
  • Method Implementation
• Implementing Handle Method

Since the structure of how to create a plugin is reviewed in its basic requirements, this section will be going over the methods themselves beyond basic requirements.

Implementing canHandle Method

Justification Name and Justification Ids

The first thing to consider is the creation of two values:

Justification Name:

//Example from the Natural Deduction Predicate Logic Plugin (PredNatDedPlugin)
  val justificationName: ISZ[String] = ISZ("org", "sireum", "justification", "natded", "pred")

The justificationName value holds the path from the source root of the justification file (org/sireum/justification.scala) whose path file from the kekinian folder at SIREUM_HOME is (/runtime/library/shared/src/main/scala/org/sireum/justification.scala) and then the two nested objects inside the justification file “natded” and then “pred”. Inside this object is the justifications that are considered by the plugin. Your plugin should include a similar list of strings that correspond the relavant path.

Justification Ids:

//Example from the Natural Deduction Predicate Logic Plugin (PredNatDedPlugin)
val justificationIds: HashSet[String] = HashSet ++ ISZ[String]("AllI", "ExistsE")

Like the justification names this is a list, however, the list is of Hashsets of Strings. This is to make canHandle’s comparing to the current step’s arguments easier.

It should contain a hashset in conjunction with a list of strings that contain every justification that this specific plugin is meant to handle.

Method Implementation

The canHandle method is often handled in the following way for plugins that seek to provide implementation for a specific keyword or justification. For example, the PropNatDedPlugin and PredNatDedPlugins fall into this category, as they are a plugin that seeks to verifiy the validity of propositional or predicate logic rules that require a subproof. If a developer is implementing a plugin with this mentality, then the following process will suffice.

Assuming the justification names and Ids are implemented, then the following will filter based on their contents:

    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
    }

As shown in the code, the justification of the step is viewed, and must be of the type “Apply”, and the resolved information of the step must have a method (the justification written in the step) that matches one of the listed Ids for the plugin, and that justification must come from the correct directory (one that matches the elements of the justificationName value).

The plugins that by default do not operate under this method are the AutoPlugin, the InceptionPlugin, and the LiftPlugin.

The Auto Plugin handles the Premise steps, and the Premise justification is considered a “Ref” type, not an “Apply” type of justification. Also the Auto plugin handles the Auto symbol which is of the apply type, but contains no witnesses in its justification, and the structure of its canHandle method reflects this.

Essentially, the canHandle method needs to be ensuring that the justification type, the symbol used for the justification and the owner of that justification is of the expected type. At the canHandle level, our goal is determine if the justification has the specific identifiers that the plugin is looking for.

Implementing handle Method

While the implementation of the handle method is highly dependent on the plugin’s usage, there is a common pattern that can be loosely followed where applicable.

If your plugin is similar to any of the default plugins’ use cases, investigating those plugins’ handle methods may also be of use:

PropNatDedPlugin / PredNatDedPlugin - Handling proof rules that function off of the use of a subproof, using proposition and predicate logic processes respectively.

AutoPlugin - If you are considering making a plugin that works with premises directly or considers Logika’s auto methodology.

ClaimOfPlugin - If you are needing to use facts.

LiftPlugin - If the plugin is needing to lift the contracts of lemmas.

InceptionPlugin - Handling of nested and non-subproof logical rules.

Smt2Plugin - Elaborates logika’s interaction with smt2.

A general strategy that can contextualize your approach includes the following:

1. Store aspects of the step provided into values to make calls in later steps shorter. If you are utilizing a step that you know from your filtering in the canHandle method, the justification, resolved info, and argment of the step can be stored as:

val just = step.just.asInstanceOf[AST.ProofAst.Step.Justification.Apply]

val res = just.invokeIdent.attr.resOpt.get.asInstanceOf[AST.ResolvedInfo.Method]

val argsOpt = AST.Util.toStepIds(just.args, Logika.kind, reporter)

2. Define an empty result for easy error reporting.

@strictpure def emptyResult: Plugin.Result = Plugin.Result(F, state.nextFresh, ISZ())

Adding and Recognizing Needed Justification Symbols to Kekinian

Return to Topics

Adding Justifications to Appropriate Location Within Kekinian

the justifications that are meant to be handled by your plugin needs to be contained within the justification object at ($SIREUM_HOME$/runtime/library/shared/src/main/scala/org/sireum/justification.scala). The object can be structured like the following:

  object plugincategory {
    @just def myJustification: Unit = $
    @just("name") def myJustWithArgs(p: StepId, q: StepId): Unit = $  
  }

You will notice that there are other justifications already in this file, and already within with the justification object, or an object that is a child of the justification object.

Make sure that each of your justifications are within. If they contain arguments in their justification, it will be written as the second item above, and if they do not require agruments, they will resemble the first item.

Rebuilding SIREUM_HOME With Plugin and Justification Symbols Now Recognized

Once the plugin file is created, listed below are the basic requirements for a plugin file. The requirements should also be met once the above sections are complete. If the file has the aspects mentioned in the step summary and the plugin is listed within the default plugin list, then you can rebuild your SIREUM_HOME installation (In your terminal, use the command:

MacOS / Linux:

${SIREUM_HOME}/bin/build.cmd

Windows:

${SIREUM_HOME}\bin\build.cmd

From there, you are able to utilize a properly implemented plugin.

Testing Plugin Functionality

Return to Topics

A simple way for a developer to debug and test their plugin is through the use of calling Logika’s verifier through the the command line (Logika’s CLI). This can be done through the command line, however, it can also be ran through Sireum’s IVE. The following steps describe this method:

1. Locate the Sireum.scala file within cli. From your SIREUM_HOME installation, the directory is: (cli/jvm/src/main/scala/org/sireum/Sireum.scala).

2. Run the main method of the Sireum.scala file. This can be done by clicking the green arrow left of the method definition in the IVE.

3. Once the method finishes, and the build is done. The name of the configuration next to your build button and run button in the ribbon of the IVE should now say “Sireum”.

4. Click on the arrow next to the configuration name, and then select “Edit Configuration”. From here, in the agruments box, type the following, replacing “absolute_file_path” with the appropriate file path.

logika verifier absolute_file_path

5. Apply your changes and now you should be able to run the Sireum configuration, which should be selected, by clicking on the green triangle next to the configuration.

In order for Logika to utilize a plugin in its evaluation process, the plugin needs to be a part of its “defaultPlugins” list. When logika looks for a plugin to handle a given step in a deduction, it goes through this list, calling the canHandle method of each plugin in order until a plugin returns a T or says that it can handle it. Once that plugin is found, its handle method is called to evaluate the specific step. If no plugin in the defaultPlugins list returns true, Logika will report an error saying that it "Could not recognize justification form".

What If The Justification(s) From My Plugins Are Not Recognized?

If in the test file the justifications that you have added are not being recognized by the type checker (the justification is underlined in red), here is how you can ensure that everything is setup properly for use with your plugin.

1. In the test file, make sure that your first line is // #Sireum #Logika.

// #Sireum #Logika

2. In your test file, make sure that the justification is properly imported. It will follow the following form if namespace conventions have been followed:

import org.sireum.justification.nameOfMyPluginObject.nameOfMyJustificationWithinThePlugin

An example of a lawEM justification within a “tactics” plugin would be:

import org.sireum.justification.tactics.lawEM

It is also import to have the following import:

import org.sireum._

//This import includes the symbols that construct some of the base elements of a step when a user is writting a proof.

Other common imports that may be missing in your test file if other standard justifications are not being recognized are:

import org.sireum.justification._ //Premise
import org.sireum.justification.natded.prop._ //Propositional Logic (^,|,-->,!,_|_ Rules)
import org.sireum.justification.natded.pred._ //Predicate Logic (All, Exists Rules)

3. Make sure that the justification that is meant to be handled by your plugin is within the justification object at ($SIREUM_HOME$/runtime/library/shared/src/main/scala/org/sireum/justification.scala). The object can be structured like the following:

  object plugincategory {
    @just def myJustification: Unit = $
    @just("name") def myJustWithArgs(p: StepId, q: StepId): Unit = $  
  }

This process is describe in an earlier section.

4. Finally, rebuild Kekinian with any instance of the Sireum IVE closed.