Skip to content

Instantly share code, notes, and snippets.


Cassie Jones porglezomp

View GitHub Profile
porglezomp / Leftpad.idr
Last active Aug 8, 2020
Taking on Hillel's challenge to formally verify leftpad (
View Leftpad.idr
import Data.Vect
-- `minus` is saturating subtraction, so this works like we want it to
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
eq_max Z (S _) = Refl
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl
-- The type here says "the result is" padded to (maximum k n), and is padding plus the original
leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a)
porglezomp / twitter-alt-to-title.js
Created Jun 19, 2020
Twitter Alt-Text to Title-Text
View twitter-alt-to-title.js
// ==UserScript==
// @name Twitter Alt-Text to Title-Text
// @description Copy the alt attribute of twitter images into the title attribute, so that I can see the alt text on hover.
// @version 1
// @grant none
// @include*
// ==/UserScript==
` .tweet .AdaptiveMedia-photoContainer img
porglezomp / example.c
Created Apr 7, 2020
Load unless there's a segfault
View example.c
// gcc example.c try_load.c
#include "try_load.h"
#include <stdio.h>
void try_to_load(const uint8_t *address) {
uint8_t value;
if (try_load_u8(address, &value)) {
printf("Successfully load from address %p: %d\n", address, value);
} else {
porglezomp / makefile
Created Jan 20, 2020
Convert the "Item Block Heights" video into a summary image
View makefile
# Convert the "Item Block Heights" video into a summary image
# Video:
# Image:
all: abcheight.png
youtube-dl -f mp4 'JteRFzrF6U4' -o input.mp4
frames: input.mp4
View GroupUniqueId.idr
-- This is a group with a set g, an operation *, and an identity e
record Group g ((*) : g -> g -> g) (e : g) where
constructor MkGroup
-- each of these fields provides a witness of one of the group laws
assoc : (a, b, c : g) -> (a * b) * c = a * (b * c)
ident : (a : g) -> (a * e = a, e * a = a)
inverse : (a : g) -> (b : g ** (a * b = e, b * a = e))
-- Given two groups g1 and g2, with identities e and e', e must be e'
uniquenessOfId : (g1 : Group g o e) -> (g2 : Group g o e') -> e = e'
porglezomp /
Last active Jan 11, 2020
Rust instructions for ROSE-8
// Thanks to Jordan Rose:
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Op1 {
porglezomp /
Last active Dec 25, 2019
Serializing Binary Data in Rust

Serializing Binary Data in Rust

The way I like to serialize data in Rust into binary formats is to let a data structure blit itself into a mutable buffer. This is a relatively composable, low level way to work that lends itself to having other abstractions built on top of it. I recently was serializing network packets, so let's make up a small packet format that illustrates how we can do this.

|  Tag (u16)  | Count (u16) |
|                           |
~        Entry (u32)        ~
porglezomp /
Created Oct 27, 2016
It's possible to have an extremely simple standard-conformant JSON parser!
# RFC 7159 § 9
# "An implementation may set limits on the size of texts that it accepts."
def parse_json(text):
if len(text) != 1:
raise ValueError("Only accepts single character JSON values")
return int(text[0])
porglezomp /
Last active Dec 3, 2019
Lets do some proofs about how transforms should behave
porglezomp /
Last active Oct 20, 2019
Creating a Rust hello world in 0x a presses.

This is a Rust "Hello World" program in 0x A presses.

$ vim
$ rustc --test
$ ./hello --quiet
Hello, World!

If you don't know, [the A Button Challenge] is a Mario 64 speedrun category in which runners attempt to use the A button (the jump button!) as few times as possible. Make sure you watch the classic [Watch for Rolling Rocks - 0.5x A Presses][A Button Challenge] video linked above in order to understand.

You can’t perform that action at this time.