larsr

# Lars.Rasmusson@gmail.com, 2019-01-12

from numpy import *

def gcd(n, m):
    n, m = min(n, m), max(n, m)
    while n != 0: n, m = m % n, n
    return m

def experiment(N):

larsr

I have a cheap DVB USB dongle.

After plugging it in to linux lsusb shows me

Bus 001 Device 004: ID 15a4:1001 Afatech Technologies, Inc. AF9015/AF9035 DVB-T stick
Bus 001 Device 001: ID 1d6b:0002 Linux Foundation 2.0 root hub
Bus 002 Device 001: ID 1d6b:0001 Linux Foundation 1.1 root hub

so it is an Afatech dongle model AF9035.

larsr

#!/usr/bin/python2.5
# Copyright (c) 2007 Brandon Sterne
# Licensed under the MIT license.
# http://brandon.sternefamily.net/files/mit-license.txt
# Python AES implementation

import sys, hashlib, string, getpass
from copy import copy
from random import randint

larsr

Creating a .so dynamic library of a haskell program and calling it from C

TLDR:

• Export a haskell function with foreign export.
• Create a C wrapper that calls hs_init when the library is loaded.
• Compile the .hs and .c wrapper with ghc, linking with lHSrts-ghc8.6.5
• Use it from C by linking as usual.

(For more details, see here.)

larsr

(*  Proof that you can build foldR out of foldL *)


Require Import Arith List. Import ListNotations.


Fixpoint foldR {A : Type} {B : Type} (f : A -> B -> B) (v : B) (l : list A) : B :=
  match l with
  | nil => v
  | x :: xs => f x (foldR f v xs)

larsr

Disable Device Enrollment Program (DEP) notification on macOS Catalina.md

With full reinstall (recommended)

   a. Boot into recovery using command-R during reboot, wipe the harddrive using Disk Utility, and select reinstall macOS

   b. Initial installation will run for approximately 1 hour, and reboot once

   c. It will then show a remaining time of about 10-15 minutes

larsr

type formula =
  | Var of string
  | Not of formula
  | Or of formula * formula
  | And of formula * formula

let rec str = function
  | Var s -> s
  | Not f -> "(not " ^ (str f) ^ ")"
  | Or (f, g) -> "(" ^ (str f) ^ " or " ^ (str g) ^ ")"

larsr

# docker build -t coq .
# coqtop() (docker run --rm -v "$HOME:$HOME" -ti coq sh -c "cd $HOME ; "'coqtop $(cat ~/src/VST/_CoqProject-export)'" $@")

#FROM coqorg/coq:dev
FROM coqorg/coq:8.11.0

RUN opam init -y; \
    opam repo --set-default add coq-released https://coq.inria.fr/opam/released; \
    opam install -y -b coq-mathcomp-algebra coq-mathcomp-analysis coq-coquelicot coq-compcert
    

larsr

#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#ifdef _MSC_VER
#include <intrin.h> /* for rdtscp and clflush */
#pragma optimize("gt",on)
#else
#include <x86intrin.h> /* for rdtscp and clflush */
#endif

larsr

Haskell

import Crypto.Cipher.AES
import Data.ByteString.UTF8 (fromString, toString)
import Data.ByteString.Base16 (encode)


main = do