Skip to content

Instantly share code, notes, and snippets.

View DaveCTurner's full-sized avatar

David Turner DaveCTurner

76 followers · 4 following
View GitHub Profile
@DaveCTurner
DaveCTurner / Leftpad.thy
Last active June 19, 2023 07:26
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"
@DaveCTurner
DaveCTurner / Blink.thy
Created June 11, 2021 10:33
Isabelle model of example of dependent specs from https://www.hillelwayne.com/post/spec-composition/
@DaveCTurner
DaveCTurner / EWD840.thy
Last active March 10, 2021 04:37
Safety and liveness proof of Dijkstra's distributed termination detection algorithm
theory EWD840
imports "HOL-TLA.TLA"
begin
section Utilities
text ‹A handful of general lemmas that were useful along the way.›
lemma temp_impI:
assumes "sigma ⊨ P ⟹ sigma ⊨ Q"
@DaveCTurner
DaveCTurner / Fulcrum.thy
Last active March 6, 2021 07:07
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 April 8, 2020 16:38
SHA1 hashes of contents of TAR archive without extracting the archive first
#!/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 April 9, 2019 08:17
Shape with hole
# see https://discuss.elastic.co/t/failed-to-create-valid-geo-shape/175975
# ========================================
# Request:
PUT /index
{
"mappings": {
"doc": {
"properties": {
"parcel": {
@DaveCTurner
DaveCTurner / twinklies.asm
Created April 28, 2018 17:33
;
; twinklies.asm
;
.include "./m328Pdef.inc"
.dseg
coltable:
.byte 64
@DaveCTurner
DaveCTurner / MinimumIndex.thy
Last active April 22, 2018 20:15
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"
@DaveCTurner
DaveCTurner / shard-stats-excerpt.json
Created April 7, 2018 20:36
{
"0": [
{
"primary": false,
"translog": {
"operations": 1489983,
"size_in_bytes": 1722388686,
"uncommitted_operations": 577877,
"uncommitted_size_in_bytes": 648646336
},
@DaveCTurner
DaveCTurner / AllocationBenchmark.java
Created March 9, 2018 09:28
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
*
* http://www.apache.org/licenses/LICENSE-2.0