Current Work Items (as of October 1, 2021)

Big Items

• Compiling our code [Bryan, Chris]
  • Erasing ghost/annotations
  • Two steps of erasure (spec, then code)
• Dedicated syntax
  • Keeping Rust-like syntax
  • Ideally via parser generator
    • Ideally in Rust
• Datatypes, and references (inout) [Andrea, design doc]
• Mutable references (inout) [Andrea]
• The View trait [Andrea, design doc]
  • Resolver support for automatic .view()
• Traits
  • Needs design work
• Module functors?
  • Do in our own language and then encode in Rust?
    • Traits may suffice for our purposes; see Refinement via Rust Traits

Small-Medium Items

• Mutually recursive functions [Bryan]
  • SCC computation, so we don't need functions topologically sorted in the file
• Pattern matching [Andrea]
• Hoist statements out of expressions
• Currently not handling variable shadowing
• Collections [if you pick this up, talk to Andrea about the View trait]
  • Vec, Seq, HashSet, Map
• Modules + datatype hiding
  • Datatype with all private fields should be abstract type elsewhere
  • Per module verification
• Make it easier to add comments to AIR; e.g., in func_to_air.rs, it would be nice to be able to add comments to the various emitted axioms, but we don't have an air_context available to use
• Make sure Dust has easy access to Z3 bit-vector reasoning; maybe autogenerate some of the Verve-style encoding? [Bryan, Yi, Chanhee]
• Better error messages when failing an assert [Bryan]
• CI [Chanhee]
• IDE integration [Chanhee]

Long-Term

• Interactive debugging [Bryan, Yi, Chanhee]
• Decreases for while loops
• Benchmark performance and pick a reasonable multiplier when setting Z3's rlimit.