Skip to content

Instantly share code, notes, and snippets.

View siraben's full-sized avatar

Ben Siraphob siraben

289 followers · 140 following
View GitHub Profile
@siraben
siraben / endian-test.sh
Created April 3, 2026 19:41
Big-endian testing, reproducibly
#!/usr/bin/env nix-shell
#! nix-shell -i bash --pure
#! nix-shell -p qemu gcc "pkgsCross.mips-linux-gnu.stdenv.cc" "pkgsCross.mips-linux-gnu.stdenv.cc.libc.static" "pkgsCross.s390x.stdenv.cc" "pkgsCross.s390x.stdenv.cc.libc.static"
#! nix-shell -I nixpkgs=https://github.com/NixOS/nixpkgs/archive/ac62194c3917d5f474c1a844b6fd6da2db95077d.tar.gz
# Big-endian testing with QEMU user-mode emulation and Nix cross-compilers.
# Reproduces: https://www.hanshq.net/big-endian-qemu.html
set -euo pipefail
@siraben
siraben / rk4.nix
Last active April 7, 2023 21:11
Implementation of sine function in Nix using fourth-order Runge-Kutta
{ lib ? (import <nixpkgs> {}).lib }:
with lib;
let
# Fourth-order Runge-Kutta method
rk4 = f: x0: y0: z0: h:
let
k1_y = z0;
k1_z = f x0 y0 z0;
@siraben
siraben / owner.sol
Created November 6, 2022 22:54
Example Solidity contract with an owner field
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.7.0 <0.9.0;
/**
* @title Owner
* @dev Set & change owner
*/
contract Owner {
@siraben
siraben / factorial.txt
Last active September 25, 2022 18:32
Recursive descent parsing in Cool
((\f. (\x. (f \v. ((x x) v)) \x. (f \v. ((x x) v))) \r. \n. i(n,o,m(n,(r d(n))))) x)
@siraben
siraben / cbv.cl
Created September 8, 2022 18:52
Call-by-value λ-calculus interpreter in Cool
-- Call-by-value lambda calculus in cool
(*
data Expr = Var Str
| Abs Str Expr
| App Expr Expr
| Sub1 Expr
| Mul Expr Expr
| Add Expr Expr
| Ifz Expr Expr Expr
*)
@siraben
siraben / Proving insertion sort in Coq.pdf
Last active July 13, 2022 01:50
Proving insertion sort correct easily in Coq
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@siraben
siraben / free-monads.hs
Created February 27, 2022 09:28
Free monads example accompanying https://siraben.dev/2020/02/20/free-monads.html
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE TypeOperators #-}
module ExtALaCarte where
@siraben
siraben / vandy_covid.ipynb
Last active February 22, 2022 16:25
Web scraping Vanderbilt's COVID-19 dashboard
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
@siraben
siraben / no_surject_12.v
Last active December 17, 2021 23:20
Constructive proof that there are no surjections from {1} to {1,2}
(* There are no surjections from {1} to {1,2} *)
Definition surjective {A B} (f : A -> B) := forall (b : B), exists (a : A), b = f a.
Definition One := unit.
Definition Two := bool.
Theorem no_surject_one_two : ~ exists (f : One -> Two), surjective f.
Proof.
@siraben
siraben / countable_choice_wikipedia.v
Created August 2, 2021 17:10
"countable choice" according to wikipedia
(* P is a family of nat-indexed sets of nat such that:
H: for all n, there is an m such that m ∈ P n
-----------
Then we show that there is a choice function f
*)
Theorem countable_choice_wikipedia
(P : nat -> (nat -> Prop)) (H : forall n, { m | P n m }) : { f | forall n, (exists m, P n m /\ f n = m)}.
Proof.
set (f := fun (n : nat) => let (m, Hm) := H n in m).
exists f.