Skip to content

Instantly share code, notes, and snippets.

@DaveCTurner
DaveCTurner / Blink.thy
Created Jun 11, 2021
Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/
View Blink.thy
@DaveCTurner
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"
begin
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
begin
(* https://twitter.com/Hillelogram/status/987432184217731073:
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. https://rise4fun.com/Dafny/S1WMn *)
(* The following merely asserts the time and space bounds. *)
(* Tail-recursive-modulo-cons calculation of running total - O(n) time and space *)
@DaveCTurner
DaveCTurner / tarsum
Last active Apr 8, 2020
SHA1 hashes of contents of TAR archive without extracting the archive first
View tarsum
#!/usr/bin/python
import sys
import tarfile
import hashlib
for filename in sys.argv[1:]:
print filename
with tarfile.open(filename, 'r') as tar:
for tarinfo in tar:
@DaveCTurner
DaveCTurner / escli.log
Last active Apr 9, 2019
Shape with hole
View escli.log
# see https://discuss.elastic.co/t/failed-to-create-valid-geo-shape/175975
# ========================================
# Request:
PUT /index
{
"mappings": {
"doc": {
"properties": {
"parcel": {
View Leftpad.thy
theory Leftpad
imports Main
begin
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 "./m328Pdef.inc"
.dseg
coltable:
.byte 64
View MinimumIndex.thy
theory MinimumIndex
imports Main
begin
(* 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
DaveCTurner / AllocationBenchmark.java
Created Mar 9, 2018
Benchmark of String.join vs stream reduction
View AllocationBenchmark.java
/*
* 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
*
* http://www.apache.org/licenses/LICENSE-2.0