lovely-error

def Bool.nor a b := Bool.not (.or a b)

example : Bool.or a b = .not (.nor a b) := by
  decide +revert

example : Bool.and a b = .nor (.not a) (.not b) := by
  decide +revert

example : Bool.not a = .nor a a := by

lovely-error

use core::fmt::Write;

fn mk_iter(ulim:u32) -> impl Iterator<Item=u32> {
    (0 .. ulim).map(move |i| ulim - 1 - i)
}
fn zpad(n:u32, bw:u32) -> u32 {
    bw - (32 - n.leading_zeros())
}
fn mk_lines(out:&mut String, max_bits:u32, enum_name:&str, entry_pad:&str, entries:&[&str]) {
    let max_entries = 2u32.pow(max_bits);

lovely-error

#![feature(coroutines)]
#![feature(coroutine_trait)]
#![feature(decl_macro)]

// ideal iface
// struct ConFun<R, Y>(fn (*mut (), R) -> Option<(ConFun<R, Y>, Y)>);
// struct StartFun<R, Y>(fn (*mut ()) -> Option<(ConFun<R, Y>, *mut ())>);


trait Coroutine2<R>: core::ops::Coroutine<R> {

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

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
import Mathlib.Logic.Equiv.Basic



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

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