Skip to content

Instantly share code, notes, and snippets.

View Scratch.thy
theory Scratch
imports Main
begin
lemma
shows "∀x. P x"
proof -
{
fix t
have "P t" sorry
View Scratch.thy
theory Scratch
imports Main
begin
fun plus1 :: "nat ⇒ nat" where
"plus1 n = n + 1"
theorem plus1E:
assumes "plus1 x = y"
obtains "y = x + 1"
@Cryolite
Cryolite / client
Created Feb 7, 2019
https://qiita.com/nwtgck/items/78309fc529da7776cba0 のプロトコル上に証明書による安全な鍵交換を実装する PoC コード
View client
#!/usr/bin/env bash
set -euo pipefail
if [[ -v VERBOSE ]]; then
set -x
PS4='+$LINENO: '
fi
function print-error-message ()
{
@Cryolite
Cryolite / config.txt
Created Sep 24, 2018
ルータ B の WAN 側インタフェイス (LAN2) における不正アクセス検知機能の設定例
View config.txt
# ip lan2 intrusion detection in on
# ip lan2 intrustion detection out on
@Cryolite
Cryolite / config.txt
Created Sep 24, 2018
ルータ B の IP マスカレイド適用時における DF ビットの扱いの設定
View config.txt
# nat descriptor masquerade remove df-bit off
@Cryolite
Cryolite / config.txt
Last active Sep 24, 2018
ルータ B の WAN 側インタフェイス (LAN2) に対する IP フィルタ設定の例
View config.txt
# ip filter 1 pass 192.168.2.0/24 * icmp 0
# ip filter dynamic 1 * * ping
# ip lan2 filter 1 dynamic 1
# ip filter 2 pass * 192.168.2.0/24 icmp-error
# ip lan2 filter 2
@Cryolite
Cryolite / network1.txt
Created Sep 24, 2018
ネットワーク構成
View network1.txt
The Internet
~~~~~~~~~~~~
|
|
|
|LAN2
+--------------------------+
| Router B (YAMAHA RTX810) |
+--------------------------+
|LAN1
View gist:d7a27ec349fce83c2245ab8bb1e4ad0f
observer = startObservingAsynchronousEvent(timeout=one_minute);
while (true) {
if (observer.eventOccurs()) break;
if (observer.eventOccursOrTimeout()) {
// if (observer.eventOccurs()) break;
throw TimeoutException();
}
sleep(one_second);
}
View wandbox-sponsors-en.md

We Are Soliciting Private and Company Sponsors

Wandbox is an online service with which source code snippets in many programming languages compile and run.
This service has been made and maintained by @melponn and @kikairoya.

Currently, it is running on three Sakura VPS 2G Plan servers. It takes JPY56,310 a year as the running cost.

It is a hard way to cope with the operating expenses by ourselves.
Therefore, we are soliciting private and company sponsors who support Wandbox.
We ask for cooperation from individuals and companies who usually use Wandbox.

@Cryolite
Cryolite / gist:3269831
Created Aug 6, 2012
A test case for nanahan::Map
View gist:3269831
#include <map/map.hpp>
#include <boost/functional/hash.hpp>
#include <boost/unordered_map.hpp>
#include <boost/random/mersenne_twister.hpp>
#include <boost/random/uniform_smallint.hpp>
#include <boost/random/uniform_real.hpp>
#include <ext/throw_allocator.h>
#include <cstddef>
#include <ctime>
#include <utility>