cppio

docker run -it --rm alpine
# inside
apk add gdb-multiarch
wget https://gist.githubusercontent.com/cppio/6576572073a424b01b9d0c9a2e4bade5/raw/42aa93d2be602e343792a59587d7a8ad7152a7d8/hello.x86_64
chmod +x hello.x86_64
ROSETTA_DEBUGSERVER_PORT=12345 ./hello.x86_64 &
gdb-multiarch hello.x86_64 -ex 'tar rem :12345'

cppio

cppio

def bsearch0(l, x):
    assert all(i < j for i, j in zip(l, l[1:]))
    lo, hi = 0, len(l)
    while lo < hi:
        # l[:lo] < x < l[hi:]
        mid = hi - (hi - lo) // 2 - 1
        assert lo <= mid < hi
        if x > l[mid]:
            lo = mid + 1
        elif x < l[mid]:

cppio

{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
import Agda.Builtin.Equality.Rewrite

private module _ {a} {A : Set a} where
  Path⇒≡ : (p : .Bool → A) → p false ≡ p true
  Path⇒≡ _ = refl

cppio

{-# OPTIONS --cubical-compatible #-}

open import Data.Nat.Base
open import Data.Product
open import Relation.Nullary
open import Relation.Unary

module Markov {p} (P : ℕ → Set p) (dec : Decidable P) .(h : Σ ℕ P) where

{-# TERMINATING #-}

cppio

import struct

def float32_bin(x):
    x, = struct.unpack("=I", struct.pack("=f", x))
    sign, exponent, mantissa = x >> 31, x >> 23 & 0xff, x & 0x7fffff
    if exponent != 255:
        return f"{['', '-'][sign]}0b{int(exponent != 0)}.{mantissa:023b}p{max(exponent, 1) - 127}"
    elif mantissa:
        return "nan"
    else:

cppio

macro_rules! for_ {
    ($dollar:tt $ident:ident:$spec:tt in [$($tt:tt),+ $(,)?] $($item:tt)*) => {
        macro_rules! __for_body {
            ($dollar($dollar $ident:$spec),+) => {
                $dollar($($item)*)*
            }
        }
        __for_body! { $($tt),+ }
    }
}

cppio

//type F = f32;
//type U = u32;
type F = f64;
type U = u64;

pub fn sample_a(i: U) -> F {
    let d = 2.0 / F::EPSILON;
    (i % d as U) as F / d
}

cppio

def beq_of_eq {α : Type u} [BEq α] [LawfulBEq α] {a b : α} : a = b → a == b := (· ▸ LawfulBEq.rfl)

instance [BEq α] [LawfulBEq α] : DecidableEq α
  | x, y => if h : x == y then isTrue (eq_of_beq h) else isFalse (h ∘ beq_of_eq)

cppio

variable {α : Sort u} {β : α → Sort v} (f g : (x : α) → β x)

def eqv := ∀ x, f x = g x

theorem eq_of_eqv (h : eqv f g) : f = g :=
  congrArg (λ x => ·.lift (· x) (λ _ _ => (· x))) (Quot.sound h)