Skip to content

Instantly share code, notes, and snippets.

Avatar

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
philzook58 / z3kanren.py
Created May 22, 2021
A Kanren abusing Z3 to full extent
View z3kanren.py
import operator
from z3 import *
def lift(z3assert):
def res(s):
s.push()
s.add(z3assert)
if s.is_good():
yield
s.pop()
View unionfind.v
(*|
A data structure that I've been more and more interested in recently is the disjoint set datastructure or union-find.
https://en.wikipedia.org/wiki/Disjoint-set_data_structure 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. https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
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
philzook58 / IntDisjointMap.jl
Created Mar 30, 2021
disjoint set map in julia
View IntDisjointMap.jl
struct IntDisjointMap
parents::Vector{Int64}
values::Vector{Any}
merge_fun
end
IntDisjointMap(merge_fun) = IntDisjointMap(Vector{Int64}[], [], merge_fun)
Base.length(x::IntDisjointMap) = length(x.parents)
@philzook58
philzook58 / cat.rs
Created Mar 14, 2021
Egg categories
View cat.rs
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
philzook58 / Instructions.md
Last active Mar 7, 2021
Generate Egg programs from Metatheory.jl
View Instructions.md
@philzook58
philzook58 / cat.jl
Last active Mar 7, 2021
type tagged Category theor in metatheory.,jly
View cat.jl
using Pkg
Pkg.activate("metatheory")
Pkg.add(url="https://github.com/0x0f0f0f/Metatheory.jl.git")
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
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) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-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. https://arxiv.org/abs/1804.02452 See Appendix A
% Difference from unison model.mzn: Try not using integers. Try to use better minizinc syntax. Much simplified
include "globals.mzn";
%% ---------------------------------------
%% PARAMETERS
%% ---------------------------------------
% 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.