lovely-error

-- import Mathlib.Logic.Equiv.Defs
import Mathlib.Tactic

def fiber (h:B->A)(a:A) := { b:B // h b = a }
def is_contr (T:Sort _) := (cc:T) ×' ∀ i, i = cc
def is_equiv (f:A->B) := ∀ i, is_contr (fiber f i)
def weq (A B) := (f:A->B) ×' is_equiv f

def id_weq : weq T T := by
  refine .mk id ?_

lovely-error

def heq_from (eq1:A=B)(k1:@HEq A a A (by subst eq1; exact b)): @HEq A a B b := by
  simp only [heq_eq_eq] at k1
  rw [@eqRec_eq_cast] at k1
  cases eq1
  simp only [cast_eq] at k1
  rw [<-heq_eq_eq] at k1
  exact k1

def heq_heq (eq1:A=B): (@HEq A a A (by subst eq1; exact b)) = (@HEq A a B b) := by
  apply propext

lovely-error

Dataflow description language

1. no global mem, every task and process can only access its local state
2. communication happen through pipes
   1. when targeting fpgas its size is the size of a single block ram
   2. customisation of lowering is possible in a separate constraint file
3. autoclocking
   1. we want to clock proc fsms at higher freqs to not keep seqvs starved most of the time
   2. still can be clocked with one main clock and each item has internal clock enable counter (???)

lovely-error

import Mathlib.Logic.Basic
import Mathlib.Logic.Function.Basic
import Mathlib.Tactic

def wmap (A:Sort _)(B:Sort _) : Sort _ := 
  { p: (A -> B) ×' (B -> A) // ∀ i, p.2 (p.1 i) = i }

def fiber (h:B->A)(a:A) := { b:B // h b = a }

def wtransp : (w:wmap A B) -> ∀ a:A , fiber w.val.snd a := by

lovely-error

macro if_nospec {
    ($cond:expr, $on_true:block, $on_false:block) => {
        {
            if core::hint::likely($cond) {
                core::sync::atomic::compiler_fence(core::sync::atomic::Ordering::SeqCst);
                #[allow(unused_unsafe)] unsafe {
                    core::arch::asm!("lfence");
                }
                $on_true 
            } else {

lovely-error

-- import Mathlib.Logic.Basic
-- import Mathlib.Tactic.GeneralizeProofs
-- import Mathlib.Logic.Function.Basic
-- import Mathlib.Tactic
-- import Aesop

inductive N where | z | s (_:N)

def plus (a b : N):N := 
  match a, b with

lovely-error

import Mathlib.Logic.Basic
import Mathlib.Logic.Function.Basic
import Mathlib.Tactic

def wmap (A:Sort _)(B:Sort _) : Sort _ := 
  { p: (A -> B) ×' (B -> A) // ∀ i, p.2 (p.1 i) = i }

def fiber (h:B->A)(a:A) := { b:B // h b = a }

def wtransp : (w:wmap A B) -> ∀ a:A , fiber w.val.snd a := by

lovely-error

// https://developer.arm.com/documentation/102336/0100/Load-Acquire-and-Store-Release-instructions
// https://developer.arm.com/documentation/ddi0602/2025-03/Base-Instructions/DMB--Data-memory-barrier-?lang=en


#[derive(Copy, Clone)]
enum Ordering {
    Unordered,
    Reads,
    Writes,
    ReadsWrites

lovely-error

homogenise the repr of generics / dyn Trait / (*mut/*const/&/&mut) dyn Trait
 
abstract value = (generic / dyn Trait / (*mut/*const/&/&mut) dyn Trait) value;
abstracted function = (takes at least one arg that is abstract or returns abstract value) and the fun is nonspecialisible;
at the 'lower level' abstract args are represented by wide pointers;
devise some opt passes to 'degeneralise' uses of abstracted funs at some sites;
specifically: 
1. uses within an 'inner world' (libs with visible impl)
2. cross bondry code must be generated to adhere to the wide pointer repr tho

lovely-error

inductive NatNum : Type | zero | succ (n:NatNum)


def add (a b:NatNum): NatNum := 
  match a with | .zero => b | .succ n => .succ (add n b)


#eval (add (.succ (.succ .zero)) (.succ (.succ .zero)))

#check add.induct