Skip to content

Instantly share code, notes, and snippets.


Philip Zucker philzook58

View GitHub Profile
View exmaple.c
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <time.h>
#define FLAG_BUFFER 128
#define MAX_SYM_LEN 4
typedef struct Stonks {
int shares;
philzook58 /
Created May 22, 2021
A Kanren abusing Z3 to full extent
import operator
from z3 import *
def lift(z3assert):
def res(s):
if s.is_good():
View unionfind.v
A data structure that I've been more and more interested in recently is the disjoint set datastructure or union-find. It's used in egraphs, unification, prolog, and graph connectivity.
I realized a cute representation that is easy to use and prover stuff about, although very inefficient compared to the usual version of disjoint set. It uses a simple functional representation based off the observation that the preimages of a function form disjoint sets. This representation is somewhat analogous to using functions to represent Maps in Coq like in Software Foundations.
The nice thing about this is that it really avoids any termination stickiness. Termination of the `find_root` operation of a union find in an explicit array or tree is not at all obvious and requires side proof or a refined type.
The termination ultimately comes from the fact that you used a finite number of unions to cons
philzook58 / IntDisjointMap.jl
Created Mar 30, 2021
disjoint set map in julia
View IntDisjointMap.jl
struct IntDisjointMap
IntDisjointMap(merge_fun) = IntDisjointMap(Vector{Int64}[], [], merge_fun)
Base.length(x::IntDisjointMap) = length(x.parents)
philzook58 /
Created Mar 14, 2021
Egg categories
use egg::{*, rewrite as rw};
use wasm_bindgen::prelude::*;
use std::time::Duration;
define_language! {
enum CatLanguage {
// string variant with no children
"id" = IdMorph(Id),
"om" = OTimesM([Id; 2]),
"oo" = OTimesO([Id; 2]),
philzook58 /
Last active Mar 7, 2021
Generate Egg programs from Metatheory.jl
philzook58 / cat.jl
Last active Mar 7, 2021
type tagged Category theor in metatheory.,jly
View cat.jl
using Pkg
using Metatheory
using Metatheory.EGraphs
cat_theory = @theory begin
hom(hom(f, ob(a), ob(b)) hom(id(ob(b)), ob(b), ob(b)), ob(a), ob(b)) == hom(f, ob(a), ob(b))
hom(hom(id(ob(a)), ob(a), ob(a)) hom(f, ob(a), ob(b)), ob(a), ob(b)) == hom(f, ob(a), ob(b))
hom(hom(f, ob(a), ob(b)) hom(hom(g, ob(b), ob(c)) hom(h, ob(c), ob(d)), ob(b), ob(d)), ob(a), ob(d)) == hom(hom(hom(f, ob(a), ob(b)) hom(g, ob(b), ob(c)), ob(a), ob(c)) hom(h, ob(c), ob(d)), ob(a), ob(d))
philzook58 / z3_tut.v
Created Feb 27, 2021
Z3 Tutorial to Coq
View z3_tut.v
I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial , while at times it felt a bit like Cody's Coq tutorial was trying to feed the kids their vegetables. He knew it was going to be like this from the outset and had a fun little analogy of me downhill skiing while he was about to go on a cross country slog.
There are a number of factors to this.
* I could use Z3's python bindings giving an air of familiarity, whereas everything was incredibly foreign in Coq.
* Z3 can actually be used to declaratively state problems and automatically calculate solutions to them with very little user help, which gives it a lot more "Wow" factor.
* Coq is a tool that requires significantly more background to even comprehend what the hell it is. I still think many aspects of it are tota
View model.mzn
% Follow paper exactly. See Appendix A
% Difference from unison model.mzn: Try not using integers. Try to use better minizinc syntax. Much simplified
include "globals.mzn";
%% ---------------------------------------
%% ---------------------------------------
% Type definitions
View cybercat.ipynb
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.