andres-erbsen’s gists

andres-erbsen / pmsa0003.py

Created January 10, 2022 03:27

	#!/usr/bin/env python3
	import collections, datetime, json, serial, sys

	Sample = collections.namedtuple('Sample', ['t', 'pm1_ug_m3', 'pm2_5_ug_m3', 'pm10_ug_m3', 'pm1atm_ug_m3', 'pm2_5atm_ug_m3', 'pm_atm_ug_m3', 'pd300nm_dl', 'pd500nm_dl', 'pd1um_dl', 'pd2_5um_dl', 'pd5um_dl', 'pd10um_dl', 'data13_reserved', 'checksum'])

	def pmsa003_read_passive(uart):
	while not (uart.read(1) == b'B' and uart.read(1) == b'M'):
	pass
	assert 28 == (uart.read(1)[0] << 8) + uart.read(1)[0] # frame length in bytes
	return Sample(datetime.datetime.now(), *[(uart.read(1)[0] << 8) + uart.read(1)[0] for i in range(14)])

andres-erbsen / rotate_by_reversing.v

Created October 7, 2021 04:29

	Require Import Coq.Lists.List. Import ListNotations.
	Require Import Lia.

	Lemma skipn_skipn {A} n m (xs : list A) : skipn n (skipn m xs) = skipn (n+m) xs. Admitted.

	Section __.
	Context {A : Type}. Implicit Types xs : list A.

	Definition rot' n xs := skipn n xs ++ firstn n xs.
	Lemma rot'_0 xs : rot' 0 xs = xs.

andres-erbsen / genimg.sh

Created September 29, 2021 20:46

	#!/bin/sh -eux
	img="arch-$(date '+%Y-%m-%d').img.qcow2"
	mnt="${img}-root"

	cleanup() {
	umount -lRf "$mnt/var/cache/pacman/pkg" \|\| true
	umount -lRf "$mnt/run" \|\| true
	umount -lRf "$mnt" \|\| true
	umount -Rf "$mnt" \|\| true
	qemu-nbd --disconnect /dev/nbd0 \|\| true

andres-erbsen / rfc8439.v

Created September 18, 2021 00:07

rfc8439.v with tests

	Require Coq.Init.Byte Coq.Strings.String. Import Init.Byte(byte(..)) String.
	Require Import coqutil.Datatypes.List. Import Lists.List List.ListNotations.
	Require Import Coq.ZArith.BinInt. Import Zdiv. Local Open Scope Z_scope.
	Require Import coqutil.Byte coqutil.Word.LittleEndianList.

	(* reference: https://datatracker.ietf.org/doc/html/rfc8439 *)
	(* perl -ne 'BEGIN{$/=""} print unless /^Example /' < rfc8439.v *)

	Definition poly1305 (p:=2^130-5) (k : list byte) (m : list byte) : list byte :=
	let r := Z.land (le_combine (firstn 16 k)) 0x0ffffffc0ffffffc0ffffffc0fffffff in

andres-erbsen / rfc8439.v

Last active September 18, 2021 00:01

	Require Coq.Init.Byte Coq.Strings.String. Import Init.Byte(byte(..)) String.
	Require Import coqutil.Datatypes.List. Import Lists.List List.ListNotations.
	Require Import Coq.ZArith.BinInt. Import Zdiv. Local Open Scope Z_scope.
	Require Import coqutil.Byte coqutil.Word.LittleEndianList.

	(* reference: https://datatracker.ietf.org/doc/html/rfc8439 *)

	Definition poly1305 (p:=2^130-5) (k : list byte) (m : list byte) : list byte :=
	let r := Z.land (le_combine (firstn 16 k)) 0x0ffffffc0ffffffc0ffffffc0fffffff in
	let t := fold_left (fun a n => (a+le_combine(n++[x01]))*r mod p) (chunk 16 m) 0 in

andres-erbsen / genimg.sh

Created March 5, 2021 05:33

	#!/bin/sh -eux
	# Adapted from builds.sr.ht, AGPL license at the end of the file
	root=root
	arch=x86_64

	cleanup() {
	# The order here is important if you don't want to hose your mounts
	umount -lRf "$root"/var/cache/pacman/pkg \|\| true
	umount -lRf "$root"/run \|\| true
	umount -lRf "$root"/boot \|\| true

andres-erbsen / coroutine.cpp

Last active December 7, 2019 00:08

generic C++ coroutine template

	// dependency: libc++experimental
	// clang++ -std=c++2a -fcoroutines-ts -lc++ coro.cpp
	#include <cstdio>
	#include <cassert>
	#include <variant>
	#include <experimental/coroutine>
	using unit = std::monostate;

	template <typename input, typename output>
	struct interactive {

andres-erbsen / gist:6419251ded8da2fcc5bb7e2ab249ff69

Created June 12, 2019 19:17

goal inclusion matching from jason

	Definition tmp {T} (x : T) := x.

	Ltac first_goal_occurs_in_other_goal :=
	unshelve (
	repeat (let y := multimatch goal with
	\| [ \|- context[?y] ] => y
	\| [ H : context[?y] \|- _ ] => y
	\| [ H := context[?y] \|- _ ] => y
	end in
	is_evar y;

andres-erbsen / fork.v

Created December 6, 2018 04:17

andres-erbsen / tryeach.v

Created December 5, 2018 21:05

	#!/bin/sh -eux
	img="arch-$(date '+%Y-%m-%d').img.qcow2"
	mnt="${img}-root"

	cleanup() {
	umount -lRf "$mnt/var/cache/pacman/pkg" \|\| true
	umount -lRf "$mnt/run" \|\| true
	umount -lRf "$mnt" \|\| true
	umount -Rf "$mnt" \|\| true
	qemu-nbd --disconnect /dev/nbd0 \|\| true

Andres Erbsen andres-erbsen