Skip to content

Instantly share code, notes, and snippets.

GitHub seems like the wrong place to put a status?

Cassie Jones porglezomp

GitHub seems like the wrong place to put a status?
Block or report user

Report or block porglezomp

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
porglezomp / 00 add baseline
Created Dec 14, 2018
Eggman Scheme Bytecode Examples
View 00 add baseline
function (+ a b) entry=bb0
v0 = lookup 'assert
v1 = typeof v0
v2 = Binop.SYM_EQ v1 'function
brn v2 non_function
v3 = arity v0
v4 = Binop.NUM_EQ v3 1
brn v4 wrong_arity
v5 = lookup 'number?

An Allocator

This is a working memory allocator for C++! It was written as test code for an operating systems class project, we were implementing a virtual memroy system, and so I built an allocator on top of that. To work, it needs access to a vm_map call which will return a fresh 4KB page, and it needs to return consecutive addresses for consecutive calls (at least most of the time, or else we can't allocate large blocks).

It is based on a linear search through a free list, with a best-fit allocation scheme.

View SketchSystems.spec
# Memory Eviction
swap page -> NoRW
file page -> NoRW
read -> Read
write -> ReadWrite
queue -> Start
porglezomp / bowser.txt
Last active Oct 3, 2018
pictures of bowser and others
View bowser.txt
porglezomp /
Last active Sep 7, 2018
View LLVM optimizer pass diffs, inspired by John Regehr's blog post
import sys
import subprocess
import tempfile
if len(sys.argv) < 2:
print(f"Usage: {sys.argv[0]} <llvm args...>")
script = sys.argv[1:]
result =
porglezomp /
Last active Aug 30, 2018
Proving reverse correct with Idris, following the challenge at

Proving About reverse in Idris

I saw a challenge on Twitter from @arntzenius, in response to some discussion about the limits of dependent types.

Hey Agda fans! In the spirit of @Hillelogram's verification challenges: How would you prove that reversing an ascending list produces a descending one?

(Also accepting answers in other languages/systems.)

porglezomp / Turing.idr
Last active Aug 14, 2018
A constructive proof that Idris is Turing complete.
View Turing.idr
%default total
data Direction = L | R
record Machine state halt alphabet where
constructor MkMachine
initial : state
transition : state -> Maybe alphabet -> Maybe (Either halt state, Maybe alphabet, Direction)
data Tape : (a : Type) -> Type where
View animalcrossing.js
// ==UserScript==
// @name Animal Crossing Twitter Rating
// @description Display the rating of tweets using the Animal Crossing letter rating system
// @version 1
// @grant none
// @include*
// ==/UserScript==
// Notes via
porglezomp /
Created Jul 19, 2018
Sin/Cos error ULPs
// Sin functions
const S1: f64 = -0.166666666416265235595; /* -0x15555554cbac77.0p-55 */
const S2: f64 = 0.0083333293858894631756; /* 0x111110896efbb2.0p-59 */
const S3: f64 = -0.000198393348360966317347; /* -0x1a00f9e2cae774.0p-65 */
const S4: f64 = 0.0000027183114939898219064; /* 0x16cd878c3b46a7.0p-71 */
pub fn k_sinf(x: f64) -> f32 {
let z = x * x;

Making the same joke, over and over.

  • lattice minimum/maximum elements
  • function domains
  • secondary headings/titles
  • html subscripts
  • nintendo's newest console
  • nontermination
  • FRC 2018 field elements
  • compiler control flow graph analysis
You can’t perform that action at this time.