andres-erbsen

Section __.
  Context (A : Type).
  Inductive list := cons (_:A) (_:list) | nil.
  Check list_ind : forall P : _ -> Prop,
      (forall a l, P l -> P (cons a l)) ->
      P nil ->
      forall l : list, P l.

  Inductive btree := branch (_:A) (_:btree) (_:btree) | leaf.
  Check btree_ind : forall P : btree -> Prop,

andres-erbsen

Module Import Interval.
  Unset Elimination Schemes.
  (** An [interval] is the quotient of [bool] under the trivial
      relation, that [true = false].  Based on the real interval, we
      call the left endpoint [zero], the right endpoint [one], and the
      proof of equality [seg : zero = one]. *)
  Private Inductive interval := zero | one.
  Axiom seg : zero = one.

  (** The eliminator for the interval says that if you send [zero]

andres-erbsen

;; coq
(require 'proof-site "/usr/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
(setq coq-mode-abbrev-table '())
(add-hook 'coq-mode-hook #'(lambda () (modify-syntax-entry ?_ "w")))
(add-hook 'coq-mode-hook #'(lambda () (modify-syntax-entry ?' "w")))

;; vim-style shortcuts
(require 'undo-tree)
(require 'evil)
  (evil-mode 1)

andres-erbsen

R.<Px,Py,Qx,Qy,Rx,Ry,a,b> = PolynomialRing(QQ,8)
A=(Px,Py); B=(Qx,Qy); C=(Rx,Ry)

I=R.ideal(Py^2-Px^3-a*Px-b,
          Qy^2-Qx^3-a*Qx-b,
          Ry^2-Rx^3-a*Rx-b)

def add((x1, y1), (x2,y2)): # incomplete (this is the common case)
    return ((y2-y1)^2/(x2-x1)^2-x1-x2,(y2-y1)/(x2-x1)*(x1-(y2-y1)^2/(x2-x1)^2+x1+x2)-y1)

andres-erbsen

package main

import (
	"net"
	"sort"
	"strconv"
	"strings"
)

func rfc1918private(ip net.IP) bool {

andres-erbsen

# Rooming people into double rooms and single rooms while considering both
# (lack of) roommate preference and room choice preference.

# Written in GNU MathProg by Andres Erbsen <andreser@mit.edu> in Nov 2015.
# Released to public domain (or licensed under CC0 by user's choice).

# USAGE: glpsol --math singledouble.mod | tr ';' '\n'

set people;
set rooms;

andres-erbsen

[consensus]
SignaturesRequired = 2

[freshness]
SignaturesRequired = 2
 
[verifier "mit"]
PublicKey = CiCheFqDmJ0Pg+j+lypkmmiHrFmRn50rlDi5X0l4+lJRFA==
[verifier "alokat"]
PublicKey = CiD6CFKBpG54dG3OMx6PJ58z5rlNFK24Dx2HMpR7urHIVA==

andres-erbsen

[consensus]
SignaturesRequired = 2
[freshness]
SignaturesRequired = 2

[verifier "dename@mit.edu"]
PublicKey = CiCheFqDmJ0Pg+j+lypkmmiHrFmRn50rlDi5X0l4+lJRFA==
[verifier "alokat"]
PublicKey = CiD6CFKBpG54dG3OMx6PJ58z5rlNFK24Dx2HMpR7urHIVA==

andres-erbsen

from charm.toolbox.ecgroup import ECGroup
from charm.toolbox.PKSig import PKSig
from charm.toolbox.ecgroup import G

"""
LWW Linkable Spontaneous Anonymous Group Signature for Ad Hoc Groups (LSAGS)

| From: "Linkable Spontaneous Anonymous Group Signature for Ad Hoc Groups"
| Published in:
| Available from: http://eprint.iacr.org/2004/027.pdf

andres-erbsen

# PKGBUILD Maintainer: Andres Erbsen <andres@krutt.org>
pkgname=mininet-git
pkgver=2.0
pkgrel=0
pkgdesc="Mininet network emulator"
url="https://github.com/mininet/mininet/"
arch=('x86_64' 'i686')
license=('custom')
makedepends=('help2man')
depends=('bash' 'python2' 'python2-networkx' 'net-tools' 'iputils' 'iperf')