It’s nice to do a wrap up of the year. A reflection on successes.

Last year https://www.philipzucker.com/2024_year/

I maintained my blog post a week even though it wasn’t my resolution. My resolution was to focus on health. I don’t think after the first month this year was notably healthy. I do ok. I started yoga recently because we moved right next door to a studio, so that’s good.

It might be good to recussitate “notes” as more systematic explanations rather than my link dumps for my current obsessions.

Looking at my posts, I feel like I wish they were a bit more varied. I’ve been hammering the same stuff over and over.

E-graphs Modulo Theories

I gave a talk on Egraphs modulo theories at the egraphs workshop at PLDI Korea. Super fun trip. It was a big push to get something coherent together enough to present. First time I’ve posted something on arxiv in a while. I feel like it ought to read more ocherently for all the work I put in it, but I’m learning. I think small workshops + arxiv posting is a pretty good lowkey way to get things done. The really big venues a. seem outside of my abilities b. maybe just not worth the pain? I kind of think smaller papers are better.

Really the basic idea I talked about was the same as that from the 2024 blog posts.

While I was writing it

Knuckledragger

I worked more on Knuckledragger

Hoo boy, so that makes it two years, since my first post was Jan 1 2024. Crazy.

I presented Knuckledragger at NEPLS which was good. Again, more stressful than it should have been to present.

A theme of just doing things on the z3 AST. I think this was kind of my super power and let things build on top of each other.

I was disappointed that it seems like no one is interested in using the system. But maybe that is for the best. I should make more decisions to be what I want rather than what I think someone else may want. I should go about building things in a way that they can but it’s ok if no one ever uses.

I should really try to write up something more paper-y and present it somewhere. I think the core of knuckledragger is pretty simple and neat. I tried describing it a bit in the “Meta SMT” blog post. I think I’ve recently been preferring the term “Big Step SMT”.

Assembly Verification

To some degree at work it is my job to figure out what I should be building. A gift and a curse. I’ve wanted to build a more interactive system in which you can annotate the assembly like Dafny or CBMC after the CBAT project. In some respects ASMC is CBAT 2, replacing BAP with ghidra pcode and ocaml with python. The more I do the more I realize how much work was put into CBAT by everyone. Oh well.

I think I have a pretty cool thing here that I don’t know what could replace it.

Type Theory for Dumbasses

Basically all are variations on trying to take seriously in mundane ways types = sets. Families of sets are as commonplace as nested loops

I never got the version about higher order contracts out there. All this really started with some ill formed goal of using sympy to describe for actual geometrical fibers. Learned a lot. Maybe should revisit that.

We were also reading Rijke’s Homotopy Type Theory textbook, which kept inciting questions.

House Fire

This was crazy. I think the knock on effects of all the stress were kind of alarming on my memory and brain function. Seems to be getting better now.

https://www.philipzucker.com/house_fire/

Things To Write About Next Year

How many from my 2024 list did I actually get to? Not that many. Maybe only Treeifying graphs and set theory in knuckledragger (I should get back to that one). I took some steps towards a superposition solver in python.

  • Algebra of assembly
  • SMTCC - use smt as compiler IR
  • ARIP - Write automated reasoning in python book. Probably self publish
  • Dynamic Datalog Stratification. Idea: Select a term ordering. Maintain a frontier of facts we know we won’t derive anything underneath. Only actually use negation if it is below frontier in term order. If we derive nothing new in an iteration, push the frontier forward to weakest negative facts. Prolog with term ordering. Use this to select goal to resolve out of goal stack.
  • ggkb. generalized ground knuth bendix
  • slotted egraphs and epr. Weakly ground terms have variables but no interesting overlaps with those variables. KB still finishes. X != Y constraints makes into slots
  • Tensor Grobner Bases
  • Semiring Grobner Bases for Seven Trees in One
  • Simplex, fourier motzkin and assymettric completion. z^2 = ax as representing inequalities and use grobner? z^4 = z^2
  • Unification vs Knuth Bendix as duals but also perhaps somewhat embeddable. The rewrite system returned can be considered as a substitution.
  • Inductionless induction / proof by consistency. Actually saturate a completion algorithm. Shows false is not derivable.
  • SES stochastic equational search. Why not more of this?
  • Atomic Type Theory - What does type theory look like if there are no compound symbols? What is an abstract bool?
  • Step Indexed Logical relations. stratify the values by observation time rather than creation time. Then it is finite enough to do in python sets. The 0th level of regular step indexing has all stuck values.
  • Incremental automata minimization - If you label some states as not observed or have a order describing degree of observation, you can still glue automata together at those edges, while minimizing / compacting the “inner states”. Hash consing is incremental minimization of algebraic expressions.
  • Chebyshev coefficients (or other coefficients) as codes (like godel coding). Converting higher order into first order data
  • Picking bidrectional synth/check as a constraint optimization problem. Pfenning heuristic is a decision heuristic
  • Z3 minikanren esimp style.
  • Arbitrary length bitvectors. Seq(BV1) seems fine?
  • Deicdable sets are like clopen sets, RE sets are like opens. But NP sets also kind of behave like opens, except that the intersections need to be “polynomial bounded” in size. The polynomial hierarchy is a lot like the arithemtic hierarchy in other words. I think there is something here in terms of the intuitive weirdness of co-NP vs NP.
  • Geometrical theorem proving

Knuckledragger

  • Push harder on concrete analysis problems (fuck filters)
  • Hyperreals
  • Verilog. Yosys ingest or pretty print out
  • CF abstract domain of known bits. Show is galois (best abstraction)
  • Chill out my dude

#

I did make progress this year, but a little bit felt like I was standing still. Did I do anythig really new for myself?

I yearn for new things, but I also have and do many of the things I do because I like and wanted them. I don’t have good flywheels going for this stuff. I’m obsessed with equations, maybe because I receive positive external feedback from that.

  • Computer graphics
  • More with my hands. Circuits
  • Physics

I will probably have the same list next year.

Ben’s son was born this year, that’s been a big change.

Did the minikanren committee. https://www.philipzucker.com/compose_datalog/ was to try and make something for minikanren, since I had such a ball in Korea I wanted to do ICFP too, but it’s a lot for one year.

https://news.ycombinator.com/item?id=46352930 If you don’t design your career, someone else will (2014) https://gregmckeown.com/if-you-dont-design-your-career-someone-else-will/

Been trying yoga lately since I moved next to a studio. I’m hoping that sticks. I think an hour every couple of days is really good for me. Yoga people do often seem like they’re in amazing shape.