Skip to content

Instantly share code, notes, and snippets.

DaveCTurner / Blink.thy
Created Jun 11, 2021
Isabelle model of example of dependent specs from
View Blink.thy
DaveCTurner / EWD840.thy
Last active Mar 10, 2021
Safety and liveness proof of Dijkstra's distributed termination detection algorithm
View EWD840.thy
theory EWD840
imports "HOL-TLA.TLA"
section Utilities
textA handful of general lemmas that were useful along the way.
lemma temp_impI:
assumes "sigma ⊨ P ⟹ sigma ⊨ Q"
View Fulcrum.thy
theory Fulcrum
imports Main
Fulcrum. Given a sequence of integers, returns the index i that minimizes |sum(seq[..i]) - sum(seq[i..])|. Does this in O(n) time and O(n) memory. *)
(* The following merely asserts the time and space bounds. *)
(* Tail-recursive-modulo-cons calculation of running total - O(n) time and space *)
DaveCTurner / tarsum
Last active Apr 8, 2020
SHA1 hashes of contents of TAR archive without extracting the archive first
View tarsum
import sys
import tarfile
import hashlib
for filename in sys.argv[1:]:
print filename
with, 'r') as tar:
for tarinfo in tar:
DaveCTurner / escli.log
Last active Apr 9, 2019
Shape with hole
View escli.log
# see
# ========================================
# Request:
PUT /index
"mappings": {
"doc": {
"properties": {
"parcel": {
View Leftpad.thy
theory Leftpad
imports Main
definition leftPad :: "'a ⇒ nat ⇒ 'a list ⇒ 'a list"
where "leftPad padChar targetLength s ≡ replicate (targetLength - length s) padChar @ s"
definition isPadded :: "'a ⇒ 'a list ⇒ 'a list ⇒ bool"
where "isPadded padChar unpadded padded ≡ ∃ n. set (take n padded) ⊆ { padChar } ∧ drop n padded = unpadded"
View twinklies.asm
; twinklies.asm
.include "./"
.byte 64
View MinimumIndex.thy
theory MinimumIndex
imports Main
(* A theory about functions that return the index of a minimum element in a list *)
(* Correctness properties: any valid implementation instantiates this locale: *)
locale minimumIndex =
fixes minimumIndex :: "int list ⇒ nat"
View shard-stats-excerpt.json
"0": [
"primary": false,
"translog": {
"operations": 1489983,
"size_in_bytes": 1722388686,
"uncommitted_operations": 577877,
"uncommitted_size_in_bytes": 648646336
DaveCTurner /
Created Mar 9, 2018
Benchmark of String.join vs stream reduction
* Licensed to Elasticsearch under one or more contributor
* license agreements. See the NOTICE file distributed with
* this work for additional information regarding copyright
* ownership. Elasticsearch licenses this file to you under
* the Apache License, Version 2.0 (the "License"); you may
* not use this file except in compliance with the License.
* You may obtain a copy of the License at