Skip to content

Instantly share code, notes, and snippets.

View lovely-error's full-sized avatar
😆
Don't forget that you will die some day

Enigma Lav lovely-error

😆
Don't forget that you will die some day
View GitHub Profile
@lovely-error
lovely-error / dyn.rs
Created October 29, 2024 14:07
(Almost) How to desugar dynsized values in rust
#![feature(ptr_metadata)]
// use libc; // 0.2.159
use std::alloc::Layout;
use std::ptr::copy_nonoverlapping;
use std::mem::forget;
use std::ptr::metadata;
use std::ptr::DynMetadata;
fn main() {
@lovely-error
lovely-error / matmul.rs
Created October 1, 2024 15:10
naive matrix multiplication
#![feature(debug_closure_helpers)]
use core::{alloc::Layout, mem::{align_of, size_of}};
#[derive(Debug, Clone, Copy)]
struct MatrixDims {
rows: u8,
cols: u8
}
@lovely-error
lovely-error / quot.lean
Last active September 17, 2024 19:41
Injectivity of quotient constructor would lead to proof of false
def zmod : Nat -> Type | n => Quot (fun a b => a % n = b % n)
theorem prop_true_or_false : (p:Prop) -> p = False ∨ p = True := by
exact fun p => Or.symm (Classical.propComplete p)
theorem quot_ctor_inj : Quot.mk f a = Quot.mk f b -> a = b := by
intro k
-- injection k
admit
example {x:Rat} : 3 * x / 0.2 = (2 + 1/2) / (3 + 1/3) -> x = 1/20 := by
let is1 : (0.2:Rat) = 1/5 := by rfl
rw [is1]
let is2 : 3 * x / (1/5) = 3 * x * 5 := by
simp_all only [one_div, div_inv_eq_mul]
rw [is2]
let is3 : 3 * x * 5 = 15 * x := by
calc
3 * x * 5 = 3 * 5 * x := mul_right_comm 3 x 5
3 * 5 * _ = 15 * x := by
@lovely-error
lovely-error / ln.lean
Last active October 23, 2024 09:18
what the hell..
def wmap : Type _ -> Type _ -> Type _ :=
fun A B => @Subtype (Prod (A -> B) (B -> A)) fun ⟨ f , h ⟩ => ∀ i, h (f i) = i
def p1 : (w:wmap A B) -> let ⟨ ⟨ _ , h ⟩ , _ ⟩ := w; ∀ a:A , @Subtype B fun b => h b = a := by
intro w
let ⟨ ⟨ f , h ⟩ , p ⟩ := w
simp at p
simp
intro a
@lovely-error
lovely-error / vect_as_vv.agda
Last active May 29, 2024 00:25
Vect as W type
{-# OPTIONS --type-in-type #-}
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
data Prod (L R : Set) : Set where
pair : L -> R -> Prod L R
data Unit : Set where
pt : Unit
@lovely-error
lovely-error / mod_eqn_solver.rs
Last active May 23, 2024 10:43
Solve (N * K) mod 2^64 = 1
// for given number N, this function finds another number K such that
// (N * K) mod 2^64 = 1
fn mult_mod_inv(n: u64) -> u64 {
assert!(n & 1 == 1, "Doesnt work for even numbers");
assert!(n != 0, "Equation 0 mod N == 1 does not have a solution");
let mut k = 1u64;
let mut i = 1u64;
for _ in 0 .. 64 {
i <<= 1;
let c = k.wrapping_mul(n);
@lovely-error
lovely-error / ocl_enable.md
Last active May 17, 2024 17:35
Get OpenCL working on RX580 amdgpu using APT
  1. Create this file sudo touch /etc/apt/sources.list.d/rocm.list
  2. put this line in there deb [arch=amd64] https://repo.radeon.com/rocm/apt/3.5.1/ xenial main
  3. sudo apt update
  4. install ocl sudo apt install rocm-opencl3.5.0
  5. this script doesnt write icd path to /etc/OpenCL/vendors/ so that's on us
  6. touch /etc/OpenCL/vendors/amdocl64.icd
  7. echo "/opt/rocm-3.5.1/opencl/lib/libamdocl64.so" > /etc/OpenCL/vendors/amdocl64.icd
  8. done. run clinfo. thing should work at this point
@lovely-error
lovely-error / kern.cl
Last active March 6, 2024 07:52
Conditional execution without branches on gpu
// this kernel writes a value only if invoaction index is even *_*
// when _flag is true, the store adress gets computed to be beyound (1 << 48) byte location .
// apparently stores beyound valid adress space on gpu... just become noops!
#define store_if_true(Ty, addr, val, flag) \
*((__global Ty*)(((unsigned long)addr) + (((unsigned long)(flag == 0)) * ((1LU << 48) - ((unsigned long)addr))))) = val;
__kernel void kern(__global unsigned int* buffer) {