PLDI 2023 notes
EGRAPHS 2023
I was really here for EGRAPHS (well and because we had a paper! Better Together: Unifying Datalog and Equality Saturation). It helps a lot to have a more connected group of people who recognize each other.
https://www.youtube.com/watch?v=6NIDzKKkpF0&ab_channel=ACMSIGPLAN streaming
egraph based workbench for CAS and numerical proving. Tower of number
Constraint aware datapath optimization
RTL circuit optimization.
Constraint aware datapath optimization  sam coward
x > 0 ? abs(x) : x
can you rewrite abs(x) > x
with context. How do you do that without going global. Idea: use assume nodes as context tags / domain restriction operations.
Domain restrition operatons  hmm this is another example of the refining equality idea. colored egraphs is more general solution A notion of context. Explicit context tagging. Algrbao f contexts assume(x + y , x  y == 0) rule assume(X, X == Y) = assume(Y, X == Y) Assume is a nice encoding of context.
Extraction criteria is minimum delay, minimal area.
egglog tutorial
oliver crushed it with an egglog tutorial. I loved the graphics and I think the example is pretty good for avoiding divide by zero.
hyroflow
stateful dataflow https://arxiv.org/abs/2306.10585 hydro site tim in rewrite rules
python egglog
saul python egglog a community of intercommunicating modules  is ths a solutuon to the diamond problem?
pip install egglog
fantastic
%%egglog
jupyter magic
from egglog import *
egraph = EGraph()
Wait. Maybe pyegglog is the glue to clingopy https://eggsmolpython.readthedocs.io/en/latest/explanation/pldi_2023_presentation.html https://arxiv.org/abs/2305.04311
quantifier elimination
partally complete quantifier elimination The problem is extracting a “good” complete equational term system out of the compressed egraph. Good in this case means ripe for existential quantifier elimination. This is a cool subproblem.
exstential quantifier elmin exists x, x > 5 /\ y > x —> y > 6
exists f(x) > 5 quantifier free does not exst boolean formula psapce complt
QElite in z3 variables subttiotn rule exsists x, x = t /\ ph —> phi[x > t] provoded phi convertig egraph back to a set of equalities “representatib funcions” some are admissible. Aso at CAV? varabl is elminated has a ground dfintion This also seems rip for ASP
QSAT and spacer
ackermannization + extraction CAV’23
Kestrel  program alignment for relational verificaion
Robert Dickerson and Ben Delaware
product program
loop invariants need to be inferred
A made more real world version of popl23 BiKat
shuffling par and seq.
< a ; b  a1 ; b1 > > <a ; a1 > ; < b ; b1 >
Buried the lead on MCMC extraction though. This is a very intriguing generally appliable technique for profile guided optimization. I bet this is a very effective method. data driven sampling of search space mcmc sampling extraction via simulatwd annealing  data driven . Can do without cost analytic function. That’s a great idea. Try swapping candidates. Rust annotated with pre and post conditions seaborn loop contig approach v simulated annealing
Even just simulated annealing jiggling sounds pretty smart with no egraph. Maybe with z3 equivalence oracles or syntactic similarity metrics.
Termination and Tree Automata Completion
termination  yihong tree automata completion ordered edge Termination term rewriting and eqsat are mutally not omplyng refinment / rewriteablity vs https://www.oflatt.com/magicterms.html https://effect.systems/blog/tacompletion.html
Depth bounded. Iterative depth bounded
aegraphs
chris fallin slides cranelift ssa input, four isas used in production as wasmtime jit focsed, impliity, verifisabiliy, research frienliness gvn is cse rle redudnatn lodad elmintin th pass order problem
NEXT_PASS gcc passes.def jamey sharp optir cfg sskeleton. half cfg, half graph elaboraton > extraction bck to cfg scpd albarain rematrializaton parent pointers and reinterining. The actual congruence couse apply rewrites befre you put in eager rewrtingbecause we refer to final eclass. union nodes. instruction scheduling i a problem egraph invernitng ~ gvn ende are stored as instructions instruction selection as extraction
Aegrapgs
Is eager rewriting + turn off rebuilding similar to aegraph: elis suggestion
risinglight
rule based optimizer vs cost basd optmizr
tensor
Taco vs starmething
https://rustmagazine.org/issue2/writeasqloptimizerusingegg/
Binding
Binding in egraphs. Destrucitve rewrite + free variable analysis.
Ilp extraction
Greedy / Dynamic programmign extraction gets an optimal term. We want to include sharing constraints. We want to extract an optimal DAG. Cycle breaking constraints / Acyclicity constraints. We ned better compairsons. ILP vs Maxsat EXTRACTcomp https://pldi23.sigplan.org/details/egraphs2023papers/3/ImprovingTermExtractionwithAcyclicConstraints slides
ZDD extraction
Eli. Represent set of all valid extraction. Tunable knob eagerly extract out . Allows evaluattion of arbtrarily complex objective functions which is cool. Represent extraction as sequence of choices?
PLDI
Saturday
Cool sounding stuff I missed
 K tutorial. K is a rewriting system framework thing for programming language and system semantics.
 LLVM getting started
 Scallop tutorial https://pldi23.sigplan.org/details/pldi2023tutorials/7/NeurosymbolicProgramminginScallop Scallop is a neurosymbolic datalog
 Flux refinement types keynote
Everyone is all over sparse computation
PLARCH
https://pldi23.sigplan.org/details/plarch2023papers/9/GoalsforamodernISAspecification alasatri reid  isa specification consistency. multi use  compiler gen, hardware gen, 70s  pdp 11 spec  gordon bell. So we used to do this more
Gus smith Research journal. That’s a fun idea. generate compiler from hardware models https://pldi23.sigplan.org/details/plarch2023papers/7/GenerateCompilersfromHardwareModels The hardware lottery sara hooker https://arxiv.org/abs/2009.06489 syntehsizing lakeroad
Timing channels anish chronitron “Chroniton is a tool for verifying constanttime behavior of cryptographic software. Instead of using leakage models, Chroniton directly verifies software with respect to a hardware implementation at the RTL level.” rosette processor specific https://pdos.csail.mit.edu/papers/chroniton:plarch23.pdf
hardware software codesign for spere meltdown serberus
https://verinum.org/ formally verified floating point
Formal Verification in Scientific ComputingInvited Talk JeanBaptiste Jeannin
reflow lauro titolo polyp precisa fcrok laura titolo
dafny tutorial cedar database ncy
let lifting for extracting common shared subxpressions costs
Jeremy Siek compiler course https://iucompilercourse.github.io/tutorialwebpage/ Hmm. Maybe this simplest version of a compiler is interesting. remove complex operands register alloc is not gonna work well using C for comm stinks. Is it that bad? Because we have sharing… No. It’s not that bad. n! becomes n + n1 +… = n^2 (a * b * c) a a + b 1 a + (b + c) b +
Sunday
Infer SIL smallfoot intermediate langguage textual ir clone of sil easy to write by had entry door for new frontends Hmm. CPS style gotos instead of phi.
clang is moving to MLIR?
entry(n)
rule (fib(N) > ) rule (block(A,B,C) > body) rule (block() > )
Similarly: jmp block  labdel(block,stmt) > stmt
Optitrust https://pldi23.sigplan.org/details/ARRAY2023papers/4/OptiTrustanInteractiveOptimizationFramework
Egraphs 2023
The big event.
See notes above
Evening
Santosh. Huge linear programming systems (billions of constraints, 10 variables). Rlibm is sweet. Random sampling works somehow? Randomized algorithms. Something to do with lattice basis finding? Somehow going to 64 bit?
A funny little trick: let bindings for sharing in egraphs. I guess this is dumb to make an algebraic encoding of sharing. We explode the egraph when it instrinsically is sharing. But it is a fun trick.
; let binding. Skolemized variable trick.
(rewrite ?x (Let (Var ?x) ?x (Var ?x)))
; explicit sharing. Let is "idempotent"
(rewrite (Let ?x ?e (Let ?x ?e ?b)) (Let ?x ?e ?b))
; lets permute
(rewrite (Let ?x ?e (Let ?y ?f ?b)) (Let ?y ?f (Let ?x ?e ?b)))
; lets float
(rewrite (Add (Let ?x ?e ?b) ?y)) (Let ?x ?e (Add ?b ?y))))
; variable usage only cost one but may represent large expression
(rewrite (cost (Var ?x)) 1)
(rewrite (cost (Let ?x ?e ?b)) (+ (cost ?e) (cost ?b)))
Asp ackermannization for the spacer extraction problem
Extract for ac like beta Defunctionalize but with rule optimization?
Keep named and de bruijn.
Put the theories in the constructors?
Subsumption as a I am king
Ssi Pdos Llvm poison sure. Frawk Onecell++ Bumpalo Cranelift Isle Sunfishdan Emptyheaded, dynamic variable ordering
Monday
Mosaic https://pldi23.sigplan.org/details/pldi2023pldi/17/MosaicAnInteroperableCompilerforTensorAlgebra https://dl.acm.org/doi/10.1145/3591236 Sparse matrix multiply. Cblas mkl taco Mosaic compiler Stardust tblis It can use a bunch of disparate tensor systems
Cryptopt Parameter specific c Random local search Hmm. This is like peephole search?
Regehr is making a superiptimizet using sail
Sythesizing milp Translating frim smt to milp via sygus
Elevate thomas rule rewirting strategies
Lapping plates curvature 3 plates can then do cubes / right angles Carpentry paper Linear programs with large number of constraints billions
Eid(n) {eclass(,)} : eid(N). : not eid(root)
Undefined behavior sabitizers and optimizers. Sanizie at different optimization levels
Zdd of the well founded selections Thinas kahler said dijstra of decision paths (?) This is also what eli described What if our lambdas were typed. Then they are literally sets. Normalization by evaluation into bdds
Denali into hla style trees high level assembly is this superior? Weird extraction problem maybe to re linearize
Indexed stream Scallop
Typeof relation + an algebra of finite sets
Scallop for extraction : examples of good extractions Scallop for asp selection. Does asp have provenance? Anti provenance. Rules or tuples that would have derived it. Scallop for end to end read formula and give equivalent version?
Instcombine as peephole optimizations
Souper ir Go ir for peephole
Optitrust Jsutified c transformations Ocaml dsl
http://files.inria.fr/optitrust/
Run herbie in vscode some tool Grammatech mnemosyne
Odysseey is new herbie interactive
Tuesday
filament
Filament timeline types. A parameter for time Aetherling. Calyx. Reticle Clash bluespec Dahlia Diospyros
Parallel Fucntional programming with effects
Mpl Go did surprisingly well Entanglement allowed by pinning
Lambda set specialization
Morphiclang.org
Asp for egglog rule synthesis
2011 jean xaiver student canonicalizing egraph? JeanBaptiste Tristan Evaluating ValueGraph Translation Validation for LLVM
Copy_term. Aegraph does help because there is a (better) notion of child egraph Moebous inversion
Isca famous arhcitects? Vlsi
Hyperscan
Asp for heap analysis. Generating or verifying separation logic? Model checking maybe?
Proving program equivalencr
Grounding asp requires context of the assumed negations. We can’t be destructive. Use terminating variant if egglog (either pure congruence closure or non producing) Scasp for flp?
Eggkanren
Stream complexity class  Eoin Hurley. Really nice dude. https://arxiv.org/abs/2007.07874 Reconfigruable networks. Cornell https://www.cs.cornell.edu/content/optimalobliviousreconfigurablenetworks Tegan Wilson
Wednesday
Separation logic leancop solver? Whaaa. Some kind of Iris automation
Expanders Ramsey Ryan odonnell. Theory of computation Princeton companion to math Higher fourier Arithmetic prgoression
Extensible inductive datatypes
Defunctionalizatipn Gadts defunctionalize for system f
Region types  subtle typing is wrong. Regions are like passing in arenas, but you connect a parameter in the arena Refinement types rust flux  strong reference type
Coinductive definitions > bisimulairty collapse Stream programs.
Fo+lfp. Pick only the trees out of a graph. Avoid loops, avoid sharing. What is least about recursive typed
Hd(Addstream(a,b)) = a + b Tl(addstream(a,b)) = addstream(b,a)
It should learn addstream(a,b) = addstream(b,a) from commutaitovty
Can I do this in mcrl2?
Why? So that we can model
Double copy. Semantic and syntactic version
Jeopardy rveersiblr language. Sparcle
Auto diff. Gilbert x*x is silly when shared. Ok should use squared kernel. But we may need to move things around. Better than interval analysis which could happen in egraph itself. Well, it is kind of nice to compile a shared version if you wanted runtime intervals to be better
Cubical agda tutorial Ground coinductive definitions. Not rewrite rules…?
Ruler: enumerate rules, verify in z3, compress as you go in egraph to avoid asking again. Use egraph to orthogonalize
Interval parsing 
random access pattern chase pointers to parse elf data depebent grammars. PADS, Yakker, Parsely
imperative specification Kaitai, Nail, Datascript use goto statements
interval on each term attributes generate ocaml parsers fastish , pretty expressive, handles a number of interesting formats
FLAP
Goddamn this line of work is cool. Algebraic staged parsing to the next level. Interesting how the presentation did not talk about staged metaprogramming at all. I guess that isn’t the point from their perspective? It’s all the normal forms of the grammars?
Foolin Around
# use "topfind";;
#require "hashcons";;
(* Normalization by evaluatios into bdds *)
type bdd = bdd_node hashed
and bdd_node = ITE of int * bdd * bdd
# use "topfind";;
(* #require "hashcons";; *)
(* hashconsing + normalization ~~ aegraph ? *)
type 'a hashed =
Node {node : 'a; tag : int; hash : int}
 Union {tag : int ; left : 'a hashed ; right : 'a hashed }
type expr = expr_node hashed
and 'a expr_node = Add of expr * expr  Lit of int  Var of string
let hash = function
 Lit n > hash_int n
 Add (x,y) > x.hash + 19*(y.hash + 1)
let tbl = Hashtbl.create 251
let rules =
let hashcons e =
match Hashtbl.find e tbl with
 Some e > e
 None >
let t = { hash = hash e}
Hashtbl.put
apply_rule
(* constant prop is in the constructor *)
let add x y =
match x,y with
 Lit n, Lit m > lit (n + m)
 _ > hashcons (Add (x,y))
(rewrite (Seq a (Seq b c)) (Seq b (Seq a c))
;re
(datatype Math
(Add Math Math)
(Lit i64)
(LVar Math)
(Let Math Math) ; we don't need to name variables.
)
; idempotence aka identify sharing
(rewrite ((Let x (Let x b)) (Let x b)))
(rewrite (Add x y) (Let (Add x y) (LVar (Add x y)))) ; let insertion
(function mincost (Math) :merge (min old new))
; remove complex oreands
(function rco (Stmt) Stmt)
(function var (Expr) Id) ; let skolem trick
(rewrite
(rco (Seq (set x (Add x y)) xs) (Seq (x y))
)
(function rco (Expr) Stmt)
(rewrite (rco (Add x y)) (append (rco x) (rco y)))
; uniquify vars
; Use the ctx trick to name vars.
;(relation label (String Stmt))
;(function label (String) Stmt)
;(function goto (String) Stmt)
;(function )
; low level rewrite (peephole)
(rewrite (seq (mov a a) b) b)
; high level rewrite
(rewrite (+ a b) (+ b a))
(movq a b)
x = (+ 10 x)
> addq $10, x
undefined behavior checking from order of execution. When I pick an arbitrary order of execution, if we don’t find those are equal, something is up.
type var = string
type lvar = Lit of int  Add of expr * expr  Read  Let of var * lvar * lvar  Var of var
type ctx = Top  LetB var * lvar  LetE var * lvar  AddL of expr  AddR of expr
type trailatom = AddL  AddR  LetB  LetE
type trail = trailatom list
module StringMap = Map.Make(String)
let uniquify prog =
let rec worker vmap prefix = function
 Let (v,e,b) >
Let (fresh, uniquify vmap (prefix ^ "e") e, (* amusing way of doing context.*)
let vmap = StringMap.add v prefix in
uniquify vmap (prefix ^ "b") b)
 Var v > StringMap.find v vmap
 Add(x,y) > Add (uniquify x, uniquify y)
 x > x
in
worker StringMap.empty "" prog
let flatten prog =
let rec worker = function

 Add(x,y) > let flatten x
let flatten y
 x > x
let select prog =
 Let x >
let assign_home
Decompilation micropass
Decompilation is compilation though.
let anti_select x86 = function
 (* common sequences. *)
 [MOV ] > Assign (x, )
 [Add(r1,r2)]  is_reg r1 > Assign (r, )
(* we still need to uniquify diffrent usages *)
let uniquify =
let restructure =
function


let dead_code =
let assign_home = (* THings that live at the same tme may want to be realiased for impertive looks *)
;re
(datatype Stmt)
(datatype SStmt)
(function Seq (SStmt Stmt) )
reify reflect reify(Add(x,y)) > reify(x) + reify(y)
reflect(neutral) > term
THe letvar trick is kind of like reflect. var(Sem) is “syntax”
I need a concrete theorem to prove interior angles are silly It’s cool that is does saturate
echo ";re
(datatype Point)
(datatype Seg (seg Point Point))
; segments are undirected
(rewrite (seg a b) (seg b a))
; congruent segments
(datatype CongSeg (congseg Seg))
(datatype R (Q Rational))
(function length (Seg) R)
(function mid (Seg) Point)
;(rewrite (length (seg (mid (seg a b) a))) (Q (/ l 2))
; :when ((= (Q l) (length (seg a b)))))
(datatype Line (line Seg))
; DirectedSeg > Seg > Line > are refining notions of equality
; Line > Para shifted lines form parallel equivalence class
; CongSeg is shift invaraint and rotation quotient segment
(rule ((= (line (seg a b)) (line (seg b c)))) ((line (seg a c))))
(datatype Para (para line))
(function perp (Para) Para)
(rewrite (perp (perp l)) l)
;(relation para (Line Line))
;(relation perp (Line Line))
; symettry
;(rule ((para a b)) ((para b a)))
;(rule ((perp a b)) ((perp b a)))
;(rule ((para a b) (para b c)) ((para a c)))
;(rule ((para a b) (perp b c)) ((perp a c)))
;(rule ((para a b) (perp b c)) ((perp a c)))
(datatype Triangle (tri Point Point Point))
(datatype CongTri (cong Triangle))
(rewrite (cong (tri a b c)) (cong (tri b c a)))
(rewrite (cong (tri a b c)) (cong (tri b a c)))
; Refining equaities
; Tri > CongTri
(datatype Angle (angle line line))
;(rule )
; (datatype Circle (circle DSeg))
; generative rules
; intersection of lines. Not always defined. (rule ((not_perp a b)) (define l (intersect a b)))
; (function intersect (Line Line) Point)
; Generate a line perpendicular to a point
; (function perpline (Line Point) Line)
; (function arb (Line) Point)
; non degeneracy
; what is (line a a)? Arbitrary line
; (relation neq (Point Point))
; (relation neq (Line Line))
"  egglog
Clingo for extraction
%edge(1,2;2,3).
%path(X,Y) : edge(X,Y).
term(add(add(x,y),z)).
term(X) : term(add(X,Y)).
term(Y) : term(add(X,Y)).
term(X) : eq(X,_).
term(Y) : eq(_,Y).
eq(T,T) : term(T).
eq(X,Y) : eq(Y,X).
eq(X,Z) : eq(X,Y), eq(Y,Z).
eq(add(X,Y), add(X1,Y1)) : term(add(X,Y)),term(add(X1,Y1)), eq(X1,X), eq(Y1,Y).
eq(add(X,Y), add(Y,X)): term(add(X,Y)).
add(0,1,2).
add(2,3,4).
{eadd(X,Y,Z)} : add(X,Y,Z).
root(4).
: root(N), 1 { eadd(_,_,N) ; efoo(_,N) } 1. % root must extract one enode
: 0 {eadd(_,_,N) efoo(0,N) } 1 % each eclass extract at most one enode
% bottom up, if we pick a node, something wanted it.
{ eadd(N,_,_), eadd(_,N,_), root(N) } : eadd(_,_,N).
%top down
{ eadd( ,X); efoo(_, X) } = 1 : eadd(X,Y,_).
: min { eadd(_,_,_), efoo(_,_) }.
lit(a,1;b,2;c,3).
add(1,2,4).
lit(d,4).
root(4).
% Any no dpendnce term can be picked
{slit(N,E)} : lit(N,E).
% enode may be selected if it' arguments have been selected
{sadd(X,Y,E)} : eclass(X), eclass(Y), add(X,Y,E).
% eclass E is selected if an enode in it is selected
eclass(E) : slit(_,E).
eclass(E) : sadd(_,_,E).
% if selected (who cares if selected?)
{sadd(X,Y,E) : add(X,Y,E) } 1 : eclass(E).
% does this work?
: root(E), not eclass(E).
%minimize weighted sum of enodes selected.
#minimize {7,X,Y,Z : sadd(X,Y,Z);
1,L,E : slit(L,E)}.
% use cligraph to draw egraph.
% use clingraph to draw term.
from egglog.bindings import *
egraph = EGraph()
print(dir(egraph))
prog = egraph.parse_program("""
(datatype Math (Lit i64))
(let zero (Lit 0))
(print Lit)
""")
print(egraph.run_program())
echo "
;re
(datatype Math (Lit i64) (Add Math Math))
(let zero (Add (Lit 0) (Lit 0)))
(print Lit)
(print Add)
"  egglog > /tmp/egglog.out
echo "
;re
(datatype Math (Lit i64) (Add Math Math) (Var String))
(let zero (Add (Lit 0) (Lit 0)))
(rewrite (Add x y) (Add y x))
(birewrite (Add x (Add y z)) (Add (Add x y) z))
(rewrite (Add (Lit n) (Lit m)) (Lit (+ n m)))
(print Lit)
(print Add)
"  egglog > /tmp/egglog.out
Do horner style factorization
from lark import Lark, Transformer, v_args
grammar = """
sexp : "(" NAME sexp* ")" > apply
 NAME > ident
 NUMBER > number
 STRING > string
row : "(" NAME sexp* ")" ">" sexp
rows : row*
%import common.CNAME > NAME
%import common.ESCAPED_STRING > STRING
%import common.NUMBER
%import common.WS
%ignore WS
"""
import clingo
class MyTransformer(Transformer):
idents = {}
def apply(self, args):
name = args[0].lower()
args = ",".join(args[1:])
return f"{name}({args})"
def row(self, args):
name = args[0].lower()
assert name not in self.idents or self.idents[name] == len(args)  1
self.idents[name] = len(args)  1
args = ",".join(args[1:])
return f"{name}({args})."
def number(self,n):
return n[0].value
def rows(self,rows):
return "\n".join(rows), self.idents
parser = Lark(grammar, start="rows", parser='lalr', transformer=MyTransformer())
ex = """
(Lit 0) > (Lit 0)
(Add (Lit 0) (Lit 0)) > (Add (Lit 0) (Lit 0))
"""
print(parser.parse(ex))
import clingo
class MyTransformer(Transformer):
idents = {}
def apply(self, args):
name = args[0].lower()
return clingo.Function(name, args[1:])
def row(self, args):
name = args[0].lower()
assert name not in self.idents or self.idents[name] == len(args)  1
self.idents[name] = len(args)  1
return clingo.Function(name, args[1:])
def number(self,n):
return clingo.Number(int(n[0].value))
def rows(self,rows):
return rows, self.idents
parser = Lark(grammar, start="rows", parser='lalr', transformer=MyTransformer())
print(parser.parse(ex))
{a(1;2;3)}.
{b(3;4;5)}.
foo(1..5).
{ a(N) ; b(N) : foo(N) } = 1 .
#use "topfind";;
#require "ppx_jane sexplib core";;
(* open Sexplib.Std *)
open Core
(*
let compare_int = Int.compare
let equal_int = Int.equal
let compare_string = String.compare
let equal_string = String.equal
let compare_list = List.compare
let equal_list = List.equal
let compare_array f x y =
for i in (max (Array.length x) (Array.kength y)
let c = f ()
let equal_array f = Array.for_all2 f
*)
(* https://github.com/ztatlock/egotables/tree/main/ego_tables/lib *)
(* type value = .. *)
module Value = struct
type t = Eid of int  Int of int  Unit [@@deriving sexp, compare, equal]
end
type ident = string [@@deriving sexp, compare, equal]
type termpat = App of ident * termpat list  Var of ident [@@deriving sexp, compare, equal]
type term = App of ident * term list [@@deriving sexp, compare, equal]
type action =
 Union of term * term
 Rule of termpat list * termpat list
 Run of int
[@@deriving sexp]
module StringMap = Map.Make(String)
module Row = struct
open Array
type t = Value.t array [@@deriving compare, equal, hash]
end
module Table = Hashtbl.Make(Row)
type st = value Table.t StringMap.t
type valpat = Value of value  Var of ident
type flatpat = Table of ident * valpat list
let flatten pat : valpat * flatpat list =
match pat with
 App (n, args) > let x = fresh () in
vs, args = List.unzip List.map flatpat args
Var x, App (n, vs @ [x]) :: args
 Var i > Var i, []
(*
let rebuild tbl =
(Table.map (fun k v >
Array.map (find uf) k
))
*)
(* Hmm. I'm accidentally supporting variable arity *)
module Trie
type 'a t = More of t Value.Map.t  Done of 'a
let find
let mem
let union x y =
let inter x y =
end
type proj_trie = Trie.t * int list
(*
A projected trie has a a map from numbered variables where it does not care about intermiedtaes.
It is quite a bit like a BDD without sharing.
We could put the integers in the trie.
type 'a t = More of int * (t Value.Map.t Lazy.t)  Done of 'a
let join x y = match x,y with
 More n t, More (m, t') >
let (t,t') = if n < m then (t,t') else (t',t) in
if n = m then
Value.Map.merge ~conflict:() t t'
else
Value.Map.map (fun t > join t t') t
 Done x , Done y > merge x y
 More x, Done
type 'a bdd = ITE of int * bdd * bdd  Value 'a
*)
Look at spj discrimination trie
module IntMap = Map.Make(Int)
type varid = int
type 'a trie = More of varid * ('a trie IntMap.t)  Done of 'a  Nothing
(* partal functions *)
let empty = Nothing
let singleton n x y = More (n, (IntMap.singleton x (Done y)))
let complete a = Done a
let map f t =
let rec worker t =
match t with
 Nothing > Nothing
 Done x > f x
 More (n, t) > More (n, IntMap.map worker t )
in
worker t
(*
let merge f x y =
let rec worker x y =
match x,y with
 More (n, t), More (m, t') >
let (t,t') = if n < m then (t,t') else (t',t) in
if n = m then
IntMap.merge worker t t'
else
IntMap.map (fun t > worker t t') t
 Done x , Done y > f x y
 More (n,t), Done x  Done x, More (n,t) >
More (n, map (fun y > f x y) t)
in worker x y
*)
let union f x y =
let rec worker x y =
match x,y with
 More (n, t), More (m, t') when n = m >
More (n, IntMap.union (fun _key t t'> Some (worker t t') ) t t')
 More (n, t), More (m, t') when n < m >
More (n, IntMap.map (fun t > worker t y) t)
 More (n, t), More (m, t') when n > m >
More (m, IntMap.map (fun t > worker t x) t')
 Done x , Done y > f x y
 Nothing, x  x, Nothing> x
 More (n,t), Done x  Done x, More (n,t) >
More (n, map (fun y > f x y) t)
in worker x y
pto(x,y)
{owns(y,x)} : pto(y,x),
% two places can't own
: owns(y,x), owns(z,x), y != z.
tree(y) : tree(x),
flap yalow/ocamlflap
(* type sort = 'a array array *)
type 'a slice = {lo : int; size : int; arr : 'a array}
let slice i size (s : slice) : slice =
assert size <= s.size;
{s with lo = s.lo + i; size}
type 'a trie = Forced of 'a Table.t  Unforced of slice list
type 'a trie = More of 'a trie array lazy  Done of 'a
Array.fast_sort
type id = int
type 'a lazytrieinner = Forced of 'a sparsemap  Delay of id array *
and 'a sparsemap = 'a lazytrie Table.t
and 'a lazytrie = 'a lazytrieinner ref
interp(fact(N), Res) : interp(N,N1), interp(fact(N11), F), Res is N*F.
interp(X := Y, Res) : interp(X,X1), interp(Y,Y1), X1 = Y1, Res = true.
interp(lam(X,B), ) :
;re
(definesort BV64 () (_ BitVec 64))
(definesort BV8 () (_ BitVec 8))
(declaredatatype Flags (
(Flags
(cf (Bool))
; (zf Bool)
; (of Bool)
; (sf Bool)
)
))
(declaredatatype State (
(State (
; (rdi (BV64))
; (rsi (BV64))
; (rax (BV64))
; (rip (BV64))
; (mem (Array BV64 BV8))
)
)
))
(declaredatatype Reg
(
RDI
RSI
RAX
)
)
(definesort Insn () (Array State State))
;(definefun movrr ((dst Reg) (src Reg)) Insn)
;(definefun movmr ((dst BV64) (src Reg)) Insn)
; #define INSN(name, body) (definefun name ((dst BV64) (src Reg)) (lambda ((st State)) body))
;(definefun add ((dst BV64) (src Reg)) Insn)
;(definefun at ((addr BV64) (i Inns)
; (lambda ((s State))
; (select i st)
;
; )
;)
;)
;(definesort Prog () (Array ))
Mit paper day
smt mod fuzzing sadhak closed box function mst b functional. inputoutput interface available so what if we can dynlink in functions for example? colousus  “dfereed cncretization” paper by . unerappxomate . if underappxiatomion is unsa, use fuzzing AChar confixt driven fuzz looop add constraints to fuzzer? Huh. Fuzzer do probably support something like this. delphi  syntesis modulo oracles  reynolds
2ltt  kovacs two notions of defintion. runtime and compile time definition largely automatic inference of quote and splie via bidirectional typing canoy do everyhitin all constructions must best stable under obkect theoretic subsitution fully implcit scoping  related to hoas. mobius cocom
object inspection dependent types
3 stages obkect meta level +1 meta supports stage polymorphism
sizing universes vs staging invere levels. Orthoogonal. So universes have two indeices
probablistic circuits
particular x, we can track errors unknown. x + error. actual = compute + error
relational semantics???
Tracng code  crichton HCI on demand vs linear tracing working memor “information viualization” engineering cogsci Visual hinking design pattersn program slicing  reduce informayion content lean emacs vs drracker  show def use flowsitry  rust plugin
fuzzy interpreter to model humans
Accelerators  rachit
dahlia  affine type system
calyx
can memory acceses run concrurently?

sequental composition operator. renews affine resources
archtexts care about frequency and physical constraints
frequent backround polling on hared threads compiler interrupts  compiler inserts interrupts staticlly into the code. May need probes. It’s kind of automatic cooperative coroutinging. les overhead.
pipeline PDL

staging constructi
spec keyword + later verify. automstic cleanup
hazard locks
hardware, huh
fearless oncurrency rust is trees  strict uniueness domainetd referencs wasn’t there a popl talk? jules jacobs. not really tha releveant
you only liinearize once a linear type system to check that functions are algebraicaly linar does derivatve make sense in rust? replace wth clones? zippers ae derivative  bmcrbide. hmm.