lovely-error

#![feature(decl_macro)]
macro d($ptr:expr) { unsafe { *$ptr } }
macro p($val:expr) { &raw mut $val }
macro pc($val:expr) { &raw const $val }

lovely-error

import Batteries


def NModB251CC8 := Vector (Fin 251) 4
def MAX_VAL := (250 * 251^0) + (250 * 251^1) + (250 * (251 ^ 2)) + (250 * (251 ^ 3))
def NModSC := Fin (MAX_VAL + 1)

def from_NModB251CC8_to_Nat : NModB251CC8 -> Nat | i => (i.zipWithIndex.map (fun ⟨ a , i ⟩ => a * ((251:Nat) ^ i))).foldl Nat.add 0

example : from_NModB251CC8_to_Nat (Vector.mk #[250,250,250,250] (by decide)) < MAX_VAL + 1 := by trivial

lovely-error

#include <stdio.h>
#include <stdbool.h>

void lmao (bool cond) {
  void* jmp_addr ;
  __asm__ goto volatile (
    "mov %[true_label], %[jmp_addr]\n\t"
    "mov %[false_label], %%rbx\n\t"
    "test %[cond], %[cond]\n\t"
    "cmovz %%rbx, %[jmp_addr]\n\t"

lovely-error

AMD

Internals [https://www.youtube.com/watch?v=KN_i-ay0y1A&list=PLB1fSi1mbw6IKbZSPz9a2r2DbnHWnLbF-&index=32] Dispatch [https://llvm.org/docs/AMDGPUUsage.html#kernel-dispatch] HSA API [https://rocm.docs.amd.com/projects/ROCR-Runtime/en/docs-6.2.4/api-reference/api.html] HSA SPEC [https://hsafoundation.com/wp-content/uploads/2021/02/HSA-SysArch-1.2.pdf] CLC [https://github.com/HSAFoundation/CLOC]

NVDA

lovely-error

#![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

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 

lovely-error

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

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

{-# 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

// 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);