Skip to content

Instantly share code, notes, and snippets.

View cppio's full-sized avatar

Parth Shastri cppio

27 followers · 0 following
View GitHub Profile
@cppio
cppio / Void.lean
Last active October 2, 2024 19:36
Example showing that definition equality in Lean is not transitive. This means that preservation (subject reduction) does not hold.
inductive Void : Prop
| void (v : Void) : Void
/-
def inf : Void → Nat
| .void v => .succ (inf v)
-/
noncomputable def inf : Void → Nat := @Void.rec _ fun _ => .succ
example (v : Void) : inf v = inf (.void v) := rfl
@cppio
cppio / Markov.lean
Created October 1, 2024 17:20
import Batteries.WF
abbrev ExistsAfter (P : Nat → Prop) := Acc fun y x => y = x.succ ∧ ¬P x
inductive Nat.ge (n : Nat) : Nat → Prop
| refl : ge n n
| step : ge n m.succ → ge n m
theorem Nat.ge_succ : ge n m → ge n.succ m
| .refl => .step .refl
@cppio
cppio / drop_box.rs
Last active August 3, 2024 15:19
Rust technique to allow a recursive type to be destructured while having an optimized drop implementation.
use std::{
mem::ManuallyDrop,
ops::{Deref, DerefMut},
};
pub trait BoxDrop {
fn drop(self: Box<Self>);
}
#[repr(transparent)]
@cppio
cppio / binary_tree.rs
Last active August 3, 2024 17:44
Binary tree in Rust with O(1) memory destructor.
#[repr(usize)]
pub enum Tree<T> {
Leaf(T),
Node(DropBox<Self>, DropBox<Self>),
}
impl<T> BoxDrop for Tree<T> {
fn drop(self: Box<Self>) {
#[repr(usize)]
enum RawTree<T> {
@cppio
cppio / gdb.sh
Created April 20, 2024 23:55
An example of using gdb inside of Docker on macOS
docker run -it --rm alpine
# inside
apk add gdb-multiarch
wget https://gist.githubusercontent.com/cppio/6576572073a424b01b9d0c9a2e4bade5/raw/42aa93d2be602e343792a59587d7a8ad7152a7d8/hello.x86_64
chmod +x hello.x86_64
ROSETTA_DEBUGSERVER_PORT=12345 ./hello.x86_64 &
gdb-multiarch hello.x86_64 -ex 'tar rem :12345'
@cppio
cppio / hello.aarch64
Last active December 18, 2023 16:41
Minimal Linux hello world binaries
@cppio
cppio / bsearch.py
Last active September 18, 2023 23:11
Many ways to write binary search
def bsearch0(l, x):
assert all(i < j for i, j in zip(l, l[1:]))
lo, hi = 0, len(l)
while lo < hi:
# l[:lo] < x < l[hi:]
mid = hi - (hi - lo) // 2 - 1
assert lo <= mid < hi
if x > l[mid]:
lo = mid + 1
elif x < l[mid]:
@cppio
cppio / Rewriting.agda
Last active November 22, 2025 14:14
Enabling rewriting in Agda allows proving funext and K
{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
import Agda.Builtin.Equality.Rewrite
private module _ {a} {A : Set a} where
Path⇒≡ : (p : .Bool → A) → p false ≡ p true
Path⇒≡ _ = refl
@cppio
cppio / Markov.agda
Created September 7, 2023 15:14
{-# OPTIONS --cubical-compatible #-}
open import Data.Nat.Base
open import Data.Product
open import Relation.Nullary
open import Relation.Unary
module Markov {p} (P : ℕ → Set p) (dec : Decidable P) .(h : Σ ℕ P) where
{-# TERMINATING #-}
@cppio
cppio / float_bin.py
Created July 16, 2023 16:01
import struct
def float32_bin(x):
x, = struct.unpack("=I", struct.pack("=f", x))
sign, exponent, mantissa = x >> 31, x >> 23 & 0xff, x & 0x7fffff
if exponent != 255:
return f"{['', '-'][sign]}0b{int(exponent != 0)}.{mantissa:023b}p{max(exponent, 1) - 127}"
elif mantissa:
return "nan"
else: