-
Notifications
You must be signed in to change notification settings - Fork 39
KeYmaera X Developer Startup
This page contains exercises and resources for people who want to work with the KeYmaera X codebase, either for course projects or for their own purposes. Before you can do these exercises, you will need to set up the KeYmaera X development environment, as covered in the Readme. The recommended development environment is IntelliJ IDEA. You can always edit the source in favorite text editor instead, but then you might have to invoke the sbt build system manually from the command line (as covered in the README).
Other useful wiki articles:
Other useful resources:
KeYmaera X API Documentation explains the package layout: http://keymaeraX.org/scaladoc
build.sbt - SBT configuration file.
The project is split into two subprojects, keymaerax-core for the core functionalities of the prover and keymaerax-webui for everything else.
keymaerax-core/src/ - Source code directory
keymaerax-core/src/main/scala - source code (edu.cmu.cs.ls.keymaerax)
keymaerax-webui/src/ - Source code directory for Web UI etc.
keymaerax-webui/src/test/scala - tests run by `sbt test`
keymaerax-core/target/scala-2.11/api/ - Target directory for sbt doc documentation.
target/ - Generated files directory created by sbt on first compilation.
target/scala-2.11/classes/ - Target directory for sbt compilation.
target/scala-2.11/unidoc/ - Target directory for sbt unidoc documentation.
No matter what kind of project you're doing, you will inevitably have to work with hybrid programs and dL formulas (and dL terms and ODEs). These data structures are all defined in the file Expression.scala. The definitions in KeYmaera X contain some constructs that are usually not discussed in the theory. For example, DifferentialProgramConstants are variables that can be replaced with programs. Similar constructs exist for terms, formulas and ODEs as well. These advanced constructs are not needed for most tasks unless you get really deep into the internals of how the basic proof rules are implemented. It's also worth noting that the Formula datatype has a lot of different operators in it. For example, even though And can be implemented with Or and Not, it has its own constructor in the datatype. This is nice because a user can type in an intuitive-looking formula and KeYmaera X will understand and remember it, but the cost is that if you want to write a function that works for all formulas, it has to have cases for operators like -> and <-> that aren't strictly necessary in the theory.
Exercise Address the above problems. First follow the instructions in How to Add Tests to add your own test file, then implement a function normalize which takes an Expression and simplifies all the redundant operators like -> and <-> into more basic operators. That way if you call normalize before running your code, you don't have to implement the extra cases. Now write a function isConcrete which returns true iff an Expression only contains the dL constructs that we've used on paper and/or in KeYmaeraX and not additional operators like DifferentialProgramConst that are only used internally. Note also that the KeYmaera X codebase has lots of contracts using the functions require and ensure. You are encouraged to use contracts in your own code as well, and in fact an example of a good contract would be to require that expressions are concrete when you either can't or don't want to implement the cases for abstract expressions.
If you want to write any sort of proof automation, you'll need to familiarize yourself with the KeYmaeraX proof libraries. One nice thing about KeYmaera X from a user's perspective is that there are very few lines of code that could possibly be responsible for a soundness bug. This is achieved using what's known as the LCF architecture, which does require a little more work from you when you're developing new code. The idea behind the LCF architecture is that there's an abstract type of "proofs", and the only way to prove something is to use the operations provided on the proof type. If you want to do some really complicated proof rule like ODE solving, you're not allowed to just say some random formula is the solution to the ODE, but rather you would need to figure out how to implement ODE solving using the basic rules that are already provided to you. These rules are provided in Provable.scala and include basic sequent calculus rules. You will notice that they do not include axioms for hybrid programs: the axioms are stored separately in AxiomBase.scala. Applying propositional sequent rules is straightforward; for applying axioms see the next paragraph.
Most interesting proofs are too painful to do by hand using the basic rules. This is where the other part of the LCF approach comes in: tactics. Tactics are programs that build up complicated proofs from basic proof steps for you. In the KeYmaera X web UI, you can type out proofs as tactics using our custom Bellerophon proof language. When you're developing KeYmaera X, you can continue to write Bellerophon tactics, but you are also allowed to write arbitrary Scala code to implement your tactics, which is helpful for complicated proof tasks (these are called DependentTactics, and can be written using "by" from Idioms.scala).
More generally, there are many tactics available to you, and the best way to learn how to write new ones is by reading what we already have. Some of the highlights:
- TactixLibrary: The "main" tactics library containing most of the tactics usable from the Web UI
- AxiomaticODESolver: an ODE solver implemented as a tactic
- SimplifierV3: A tactic that tries to simplify formulas and arithmetic wherever possible
- HilbertCalculus.useAt: Used to apply axioms
- HilbertCalculus.chase: Gets rid of all the "easy" formulas and programs, leaving behind ODEs and loops
We have an extensive test suite, so the best way to figure out how to use tactics is by looking at their tests, which will also show you how to write your own tests (most basic tests can be written by handing a tactic and formula to proveBy and inspecting the results)
Exercises: Learn how to write DependentTactics, since this is the single biggest difference from writing proofs in the Web UI. To start out with, reimplement the prop tactic which gets rid of all propositional operators. Do this by case-analyzing the formula and applying the appropriate sequent rule in each case. Also note there are some minor syntactic differences between Bellerophon-inside-Scala and Bellerophon-in-Web-UI. 15-424 students: Try turning your Lab 3 proof into a scala proof in a test case somewhere. Can you find anything that you could simplify in this proof by writing your own DependentTactics?