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)

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

int counter = 0;

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

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

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


abstract
--------

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

david415

package main

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

david415

package main

import (
	"bytes"
	"fmt"
)

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

david415

[UpstreamProxy]
  Type = "socks5"
  Network = "tcp"
  Address = "127.0.0.1:9050"

[Logging]
  Disable = false
  Level = "DEBUG"
  File = "/home/user/catshadow_testnet/bob/catshadow.log"

david415

extern crate hyper;
extern crate hyperlocal;

use std::os::unix::net::UnixListener;
use hyper::{Response, rt::{Future, Stream}, service::service_fn};
use hyperlocal::server::{Http, Incoming};

fn main () {
    if let Err(err) =  std::fs::remove_file("hyperlocal_test_echo_server_2.sock") {

david415

use std::thread;
use std::os::unix::net::{UnixStream, UnixListener};


fn handle_client(stream: UnixStream) {
    // ...
}