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.

video

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://egg-smol-python.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

slides

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.

slides

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/magic-terms.html https://effect.systems/blog/ta-completion.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/issue-2/write-a-sql-optimizer-using-egg/

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/egraphs-2023-papers/3/Improving-Term-Extraction-with-Acyclic-Constraints slides

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/pldi-2023-tutorials/7/Neurosymbolic-Programming-in-Scallop Scallop is a neurosymbolic datalog
Flux refinement types keynote

Everyone is all over sparse computation

PLARCH

https://pldi23.sigplan.org/details/plarch-2023-papers/9/Goals-for-a-modern-ISA-specification 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/plarch-2023-papers/7/Generate-Compilers-from-Hardware-Models- The hardware lottery sara hooker https://arxiv.org/abs/2009.06489 syntehsizing lakeroad

Timing channels anish chronitron “Chroniton is a tool for verifying constant-time 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 Jean-Baptiste 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/tutorial-web-page/ 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 + n-1 +… = 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/ARRAY-2023-papers/4/OptiTrust-an-Interactive-Optimization-Framework

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/pldi-2023-pldi/17/Mosaic-An-Interoperable-Compiler-for-Tensor-Algebra 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

Morphic-lang.org

Asp for egglog rule synthesis

2011 jean xaiver student canonicalizing egraph? Jean-Baptiste Tristan Evaluating Value-Graph 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/optimal-oblivious-reconfigurable-networks 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 let-var 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/ego-tables/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/ocaml-flap

(* 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(N1-1), F), Res is N*F.
interp(X := Y, Res) :- interp(X,X1), interp(Y,Y1), X1 = Y1, Res = true.
interp(lam(X,B), ) :-  

;re
(define-sort BV64 () (_ BitVec 64))
(define-sort BV8 () (_ BitVec 8))
(declare-datatype Flags (
    (Flags
        (cf (Bool))
       ; (zf Bool)
       ; (of Bool)
       ; (sf Bool)
    )
))
(declare-datatype State (
    (State (
      ;  (rdi (BV64))
     ;   (rsi (BV64))
     ;   (rax (BV64))
     ;   (rip (BV64))
     ;   (mem (Array BV64 BV8))
        )
    )
))

(declare-datatype Reg
    (
        RDI
        RSI
        RAX
    )
)

(define-sort Insn () (Array State State))

;(define-fun movrr ((dst Reg) (src Reg)) Insn)
;(define-fun movmr ((dst BV64) (src Reg)) Insn)  

; #define INSN(name, body) (define-fun name ((dst BV64) (src Reg)) (lambda ((st State)) body))

;(define-fun add ((dst BV64) (src Reg)) Insn)

;(define-fun at ((addr BV64) (i Inns)
;   (lambda ((s State))
;       (select i st)
;
;   )   
;)
;)

;(define-sort Prog () (Array ))

Mit paper day

smt mod fuzzing sadhak closed box function mst b functional. input-output 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.