andres-erbsen

#!/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

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

#!/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

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

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

#!/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

// 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

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

Ltac fork :=
  multimatch constr:(Set) with
  | _ => true
  | _ => false
  end.
Goal True.
  let x := fork in
  idtac x;
  unify x false.
  (* true *)

andres-erbsen

Definition bag := nat.
Existing Class bag.
Instance : bag := 5.
Instance : bag := 6.
Instance : bag := 7.
Instance : bag := 8.
Instance : bag := 9.

Ltac tryeach cls t :=
  let picked := fresh "picked" in