Collected notes

To discuss

• Benchmarks of the prefix acc vs non-prefix acc -> relate to the Rust benchmarks. Otherwise there is not much to evaluate

Action items

• No opam install of our deps in Linden CI ✅
• Cherry pick changes that add may_erase ✅
  • Add non-det initialization of lazy-prefix piketree ✅
• Document the meta engine ✅
  • consider an optimization that detects anchored searches
• Rename the macro of the piketree nextt -> lazy_ ✅
• Move input_prefix to where strict_suffix but specify that it is for induction purposes and strict_suffix is the canonical repr ✅
• Presentation next week:

  • 20/25 min

  • present general progress about optimizations

  • Outline:

    1. Motivation: let’s verify real implementations
    2. Remind the project goal
    3. Talk about prefix acceleration and the implementation
       • Acceleration
       • Generation
       • Filtering
    4. Outline the proof for prefix acc
    5. Next steps: meta engine