Hillel Wayne hwayne

Bsky spinner

Spins your avatar like a clock

Disclaimer: I set this up locally half a year ago and forgot all the steps, so the steps below may be wrong.

To run locally

For the newsletter at: FILL IN

Run with Dafny 4.6.0, with the flag --standard-libraries.

Pleased to announce a new #NFT offering: #eNdFT! We are minting one cause of death NFT for every person on earth, which is 100% guaranteed to reflect the way you do, in fact, actually die.

Unless you trade it!

Unhappy with your "car crash" #eNdFT? Exchange it for an "old age"! Of course, you better be prepared to pay through the nose for "old age". Due to the nature of our product, eNdFTs cannot be bought or sold, only be traded 1-1 for another #eNdFT (plus an optional eth price to cover value differences). There is no escaping death.

Please note that our prediction software isn't perfect. While every #eNdFT is accurate, it may be imprecise. For example, you could receive the "Most likely drowned" NFT, or "either cancer or a stabbing". Don't worry, eNdFTs are still an exciting speculation opportunity! We're improving our prediction software all the time, and that "cancer or stabbing" #eNdFT could one day become a super valuable "cancer"! Join the #eNdFT network today!

(Disclaimers: while we will confirm

	-- Drop this in /after or /after/plugin/
	-- explanation at commands (at end of file)

	vim.g.exo = "where you store your data files"
	local filelinks_file = vim.g.exo .. 'filelinks.json'

	local function get_filelinks()
	return vim.fn.json_decode(vim.fn.readfile(filelinks_file))
	end

	local function moduleline() -- can't be a global as line can move
	local lines = vim.api.nvim_buf_get_lines(0, 0, -1, false)
	for idx, line in ipairs(lines) do
	if string.match(line, "%-+ MODULE [%w_]+ %-") then
	return idx, line
	end
	end
	end

	local function fix_module_string()

	function template($t) {
	@"
	SPECIFICATION Spec

	CONSTANTS
	BuffLen = 2
	NumThreads = $t

	CHECK_DEADLOCK TRUE
	"@

	SPECIFICATION Spec
	\* Add statements after this line.
	CONSTANTS
	Threads = {t1}
	NULL = NULL
	Keys = {k1}
	MaxId = 1
	BUGMODE = TRUE

	PROPERTY LockProp

	import xml.etree.ElementTree as ET
	from xml.etree.ElementTree import Element
	from copy import deepcopy
	from argparse import ArgumentParser
	from dataclasses import dataclass
	from string import Template
	from pathlib import Path
	import typing as t

	#Common issue is that I need to have multiple slightly different versions of the same spec, this is a helper to do that.

	function Ask {
	Param (
	[PSDefaultValue(Help="*")]
	[switch]$Fast,
	[Parameter(Position=1)]
	[Alias("M")]
	[int]$Tokens=256,
	[Alias("n")]
	[int]$Results=1,
	[Parameter(Mandatory=$true, Position=0)]

	// dreidel model I wrote in 2023.
	// see https://buttondown.com/hillelwayne/archive/i-formally-modeled-dreidel-for-no-good-reason/
	dtmc

	const int M; //starting money
	formula Players = 4; //Players
	formula maxval = M*Players;
	formula done = (p1=0) \| (p2=0) \| (p3=0) \| (p4=0);
	formula halfpot = ceil(pot/2);