TODOs

README.md

@@ -67,18 +67,3 @@ and [cvc5](https://cvc5.github.io/) by setting the
 [RSMT2_CVC4_CMD](https://docs.rs/rsmt2/latest/rsmt2/conf/constant.CVC4_ENV_VAR.html)
 environmental variable to the SMT solver's invocation command (`cvc4` or
 `cvc5`).
-
-## Todo List
-
-- [ ] Intern variable names
-- [ ] Tweak log system to expect exact target match
-- [ ] C front-end
-- [ ] Tune R1CS optimizer
-   - [ ] Less hash maps
-   - [ ] Consider using ff/ark-ff instead of gmp
-   - [ ] Consider a lazy merging strategy
-- [ ] remove synchronization from term representation (or explore parallelism!)
-- [ ] More SMT solver support
-   - [ ] Parse cvc4 models
-- [ ] A more configurable term distribution (for fuzzing)
-- [ ] Add user-defined (aka opaque) operator to IR

TODO.md

@@ -1,10 +1,8 @@
-Passes to write:
-
+Concrete:
 [ ] shrink bit-vectors using range analysis.
   * IR analysis infrastructure
   * shrink comparisons too
     * generalized version of constant comparison?
-[ ] FE analysis infrastructure
 [ ] common sub-expression grouping
   * for commutative/associative ops?
   * after flattening
@@ -22,14 +20,33 @@ Passes to write:
 [ ] Improving/parameterizing our IR term distribution
   * We use it to fuzz IR passes
   * General problem: Fuzzing language FEs
+[ ] Implement sorts using hash-consing.
+
+Vague:
+[ ] FE analysis infrastructure
 [ ] Recursive proving.
 [ ] Incorporate verifier challenges.
 [ ] Support functions in the compiler.
 [ ] Equality saturation/e-graphs?
 
 
+Small research questions:
+[ ] Model a RAM-extraction pass in Coq and prove it correct.
+  * input: a term-graph computation that uses functional arrays
+  * output: a term-graph computation that has RAM transcripts attached, has
+    *no* array sorts, and is provably equivalent.
+  * Passes that are likely important:
+    * Replace array variables with mass stores
+    * Lift tuples out of arrays with AoS -> SoA transformation
+    * Scalarize array equality with a big AND of EQ
+    * Flatten nested arrays? I haven't though this out. Requires scalarizing some stores/selects.
+    * Do a RAM extraction pass that assumes all arrays have primitive keys and value.
+[ ] Model a RAM-extraction pass in Coq and prove it correct.
+  * pretty printing term DAGs with letification
+  * Like LaTeX meets letification.
+
 Bigger research questions:
 [ ] SoK: compiling to R1CS
   * focus on embedding complex datatypes:
     * use lookups
-[ ] Compiling to branching programs
+[ ] Compiling to branching programs