lovely-error

open import Agda.Primitive

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

cong : {a b : Level} {A : Set a} {B : Set b} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

lovely-error

-- https://www.falstad.com/circuit/circuitjs.html?ctz=DwYwlgTgBAZgvAIgIwKgFwM6IAwDpsEECsqYIiSeATAVQOx0DM2AHFQGwCcndqIARoiLZUAB0EIALI1QA3CENQBbTEICmAWiQoAfACgoUYAHcoAD0R0WkqEU5UoVm5MktU8BCID0+w8DTmluwstlQhLEjsoW6wOGIAdohaqPxqFATKAPaIACZqMACGAK4ANmhyqUl47JRWdJxEHHQcSES8ULL85Aga1WF0kTT0LCzY7IwkPgZGAEqBCBFRkuw2LCtQy5LucVDGHiJQSgVmsopTfnMWCCvY0bZ0UY0x+6h7iFTuCtcHRydnvkYAlcnLZ7FBFqCPrFPAkKCk0sgModsgg8oVSuUOpVPLgaJErCtGJIxs1lhVutRsFQkCxOBE6NhGMFGBwEOcjKYrpwkA4iC5wZFbC5tjD2cBLoh2EQliyoOxWBsWSKDm8YYdjqcEJMAcBoMDrBtXI4aIbnjsvpQMmKAMrzZq3FwhKVLVzKsRwqAlMA7NAAC3ebJ1AHN5s6Nut2FRnCs3WLOZLiXcbnLibGdfHrom1jZkzx2Gnprq7cEoHnjbc826oF9hFbg-MnuCCBtOFFRgcXjaG2CQY2nFXRB6vT7-QgPmK9ZYDSD7Y5rFWLYRA4WJVqwo4S65bg8zWrVT8Nf9CxnuQ4RrcIeeC34gVObPZwoKHwPEsh4ekfii0cUyhUEZT8WzIkSSoPkYk6ClcSpGk6SQBkmRYRgiV4ONQ0TMtZ0raFvB1VdL2bbMmw7HZ92UQ8tWXG9ixCMsISwl4oFEV8UCgbFLSyXJ8h-TFOgRDROFweorGwOkWGaODxnJJJJFwbg5O4YRQLsIgUDFW8EB3cF1kvGNsNhHoWLYpElC-LiMT-KpcBqbA6gaJoWjaKSej6MTBipKxRhWLYxRDK46LBCFLV3HDj3mS9RgFKJT2vDk7QNB85xsfs9NQq4eW0wUeVlRYYpMeYkBZEI6EaKA

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