2022 Goals

[radumereuta]

A few general directions that we would like to follow in developing K in the year 2022:

• Get K into a stable and usable state. Talking with internal users of K that maintain large definitions, I sense a sentiment of frustration because of the poor performance and frequent bugs. It's not fun working on something if your tools are not helping you.

• Interoperability between tools. At one point, we need to be able to create spinoff tools for different semantics, depending on the needs of auditors. We need to have some kind of infrastructure in place for them.

• More robust scripting api for k. Pyk is a start in this direction which could use some improvements (#2379)

  1. cleanup pyk into a production library,
  2. tighten its integration with the frontend (currently it uses textual interface, for example), and
  3. get people used to building tools with it.

• More frequent release schedule. 3-5 per year? We should target versions that feel stable. Large features that may prove problematic should be tested thoroughly.

• Keep large definitions up to date.

• https://github.com/kframework/k/issues/1655

• https://github.com/kframework/k/issues/1657

• https://github.com/kframework/k/issues/2386

[radumereuta]

From Everett:

• Have our tools be 10x faster on symbolic execution
• quickly spin up web interfaces for definitions which would allow people to start 'hacking' with K.
• also lots of libraries so people can make their own scripts

[radumereuta]

Mid-year progress:

K

• improving support for Apple silicon (in progress) (Bruce, Sam)
• remove the Ocaml backend (Dwight)
• improve scanner caching (Dwight)
• improve error messages (Bruce, Erik, Radu, Dwight...)
  • print source lines in error messages
  • report wrong parameters sent to kompile
  • new hires had a big role in updating the tutorial and documentation
• improvements to parsing time and type inference (Radu, Dwight)
  • removed some performance hotspots in grammar generator
  • optimize the work sent to Z3
  • find a stable Z3 version - 4.8.15
  • some pathological cases dropped from 5m to 1m30s
  • typical EVM proof spends ~10-15s in the front end compared to ~25-30s
  • new parser kernel, cleaner implementation (Dwight)
  • improve interoperability with other tools (Radu)
  • allow specifying kompiled directories directly
  • JSON v2 for front-end K - more complete and allows external tools to apply post-processing steps
  • make kprovex the default (Bruce)

CI

• improve CI infrastructure (in progress) (Everett, Freeman)
  • faster hardware, soon an M1 machine
  • NIX infrastructure (Sam)
  • fix caching for faster and more robust builds (Sam)
• we can consider adding the large semantics to be tested automatically (periodically?)

Haskell-backend

• improved compilation time (Jost)
• fixed some laziness issues (Jost)
• improved time spent in rejecting rules (Dwight)
• added support for \equals simplification rules (Ana)
• added several CL options for improving usability (Ana, Max, Andrei B.)
• got us access to better profiling tools (Sam, Max)
• overall speed improvements (in-progress) (Serokell)
• kore-server interface for ease of building tools over the backend (in-progress) (Sam, Jost, Ana)
• support for symbolic Sets (in-progress) (Ana, Denis)
• improving \ceil simplification time (in-progress) (Ana)
• adding support for equational claims (in-progress) (Max)

LLVM-backend

• improve debugger support on OSX (use lldb)
• improved KORE parsing by adding support for a KORE binary format (Bruce)
• improve garbage collection performance by allowing collections to happen at any time (in-progress) (Theo, Dwight)

PYK

• improved interoperability with kompile via JSON

[radumereuta]

second half of the year progress:

K

• add LLDB as a debugger for Macs (Bruce)
• allow the kast tool to parse rules (Radu)
• move macro attribute from rules to syntax (Erik)
• begin work on the K repl
• updated simple-untyped to work with the llvm-backend (Nishant and Radu)
• update the bug report templates (Freeman)
• reduce simplification rule duplication with the comm attribute (Radu)
• more type inferencing speedups by optimizing the interaction with Z3 (Dwight)
• kprove options to filter claims (Radu)
• add log hook to K-IO module (Dwight)
• add #trace hook to K-IO module (Bruce)
• replace functional attribute with function, total (Dwight)
• Implement python bindings option in kompile (Bruce)
• improve error messages:
  • forbid anywhere and simplification on rules (Radu)
  • Add warning for syntax priority / associativity mismatch (Bruce)
  • check to detect duplicate cell declarations (Erik)
  • Emit error from k frontend when kore-exec fails (Erik)
  • Improve error handling in k-util.sh (Bruce)
  • Print intermediate timing information about backend steps (Radu)
  • err on anywhere rules not supported by the haskell backend (Radu, Bruce)
  • relax module duplication check (Radu)
  • LHS of #Exists binds variables (Radu)
  • Err when declaring generated cells (Radu)

CI

• Apple silicone is now integrated into CI
• updated to GitHub workflow CI (mostly Everett and Freeman)
• update/consolidate CACHIX caching of various dependencies and speed up build times (Sam, Freeman, Everett)
  • LLVM backend CI matrix is now run entirely using Nix, rather than the old ad-hoc ciscript (Bruce)

Nix

• added/updated nix flakes in the main repos, i.e. haskell/llvm-backend, k, evm-semantics, ksummarize, avm-semantic... (Sam, Bruce, Everett)
  • added the kup tool to help with installing K and it's dependencies and keeping everything up to date (Sam)

Haskell-backend

• kore-rpc-server, JSON-RPC API for symbolic execution (Jost, Sam, Ana)
• add option to serialize definition (Dwight, Ana)
• add (or improve) various other options (Sam, Jost, Ana)
• add IO hooks (partially done) (Sam)
• algorithmic improvements:
  • change internal representation of various internal types (Sam)
  • move expensive function argument unification at start-up (Ana)
  • refactor and simplify internal execution strategy (Jost)
  • new matcher (Dwight)
  • new unifier (Dwight)
  • refactor and simplify handling of \\ceil (Ana)
  • handle symbolic sets properly (partially done) (Ana, Jost)
• support \\not simplification rules (Jost)
• improve property testing infrastructure (Jost)
• support for GHC 9 (Sam)
• automatic profiling reports (Sam, Jost, Freeman)
• string interning (team + Serokell)
• various refactorings and clean-ups (Serokell)
• better specialization, monomorphization (Serokell)
• improve time spent hashing (Jost + Serokell)
• develop new fast symbolic execution engine hs-backend-booster (in progress) (Everett, Jost, Ana, Sam)

LLVM-backend

• fixes to binary KORE serialization for symbols with sort parameters (e.g. amb, inj) (Bruce)
• implement debugging #trace hook that prints K terms in surface syntax (Bruce)
• performance improvements to macro expander (kore-expand-macros) (Bruce):
  • better use of collections
  • improved algorithm that doesn't try to check every term against every KORE symbol, instead caching which symbols have the macro or macro-rec attribute and only checking the top-level term against those
• rewrite of llvm-kompile to support friendlier option parsing (Bruce)
• bindings from the LLVM backend to other languages (Bruce, Tamas, Sam):
  • Python bindings split into two components; one that is independent of a definition (e.g. for constructing an AST), and one that depends on a particular definition (e.g. to take concrete execution steps from a starting configuration)
  • C bindings that allow for simplification of Boolean terms via configuration construction; the idea for these is to pull them into the Haskell backend so that concrete side conditions can be checked faster.
• Documentation of the matching algorithm + paper submission (Dwight, Bruce, Theo)
• Better error messages from hooks - the name of a hook in which a crash happens is printed, and the concrete argument values in cases where they can be printed (Bruce, Theo)

PYK

• pull out to runtimeverification/pyk: fast CI pipeline, lightweight distribution
• project health: move to poetry, full type checking, integrate code formatters, add linting plugins, move to pytest, extract runtimeverification/python-project-template
• pyk.kore: KORE AST, parser, kore-rpc client
• pyk.kllvm: integrate the LLVM backend's Python bindings
• pyk.ktool: integrate kast and krun, implement kprove based on kore-rpc
• kompilation features: KORE-KAST conversion, type inference
• pyk.kbuild: design and proof of concept implementation
• pyk.krepl: design and skeleton implementation
• pyk.krepl_web: design and skeleton implementation
• several improvments and bug fixes