david415

package main

import (
	"bytes"
	"fmt"
)

func isAlmost(x, y []byte) bool {
	skipped := false

david415

package main

import (
	"bufio"
	"flag"
	"fmt"
	"io"
	"os"
	"sort"
	"strconv"

david415

Rebuttal of "[36C3] The ecosystem is moving"
============================================


abstract
--------

Moxie is wrong about a lot of things in this talk. Here I'll discuss

david415

NOTE that in order to use this you'll have to tell your TLA+ model checker about the
values of DirAuthNodes and Relays, for example:

DirAuthNodes <- {"n1","n2","n3","n4","n5"}
Relays <- {"r1", "r2", "r3", "r4", "r5"}

------------------------------ MODULE dirauth ------------------------------

EXTENDS Naturals, Sequences, TLC, FiniteSets

david415

int counter = 0;

typedef RWLock {
  chan writeComplete = [0] of {bit};
  chan allowWrite = [0] of {bit};
  int readers;
  bit writing;
  int writeWaiters;
  int readWaiters
}

david415

partial def grep (stream : IO.FS.Stream) (expected : String) : IO Unit := do
  let line ← stream.getLine
  if line.isEmpty then
    pure ()
  else
    let words := line.splitOn " "
    if words.contains expected then
      IO.print line
    grep stream expected

david415

@[extern "add_one"]
opaque addOne : UInt32 → UInt32

def specialAddOne : (x : Nat) → Nat :=
  fun x => (addOne (UInt32.ofNat x)).toNat

axiom specialAddOne_eq_add_one : ∀ x : Nat, specialAddOne x = x + 1

variable (a b c d e : Nat)
variable (h1 : a = b)