Sunny Gonnabathula sunny-g

`urwasm`: WebAssembly interpreter suite on Urbit

WebAssembly is a low-level language for a portable virtual machine. Wasm is designed to be a compilation target for a variety of programming languages and its design is hardware independent and relatively simple, making its support ubiquitous in modern browsers. Its simple design made it a perfect first candidate for a first emulator of an conventional computational system on a novel functional computer: Urbit. In this paper I discuss the current state of urwasm project and some technical details, as well as describe the strategy to jet the interpreter of a state machine in a functional environment.

Introduction

Solving SAT via interaction net superpositions

I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite

Interpreter in Hoon

Change memory model: random access via (map page-number=@ page-array=@)
Revisit the model of block/loop/if and call/call_indirect execution: it appears that the current model causes unnecessary copies of the entire membuffer, slowing down the computation. So instead of cloning the core, interpreting an expression and back-propagating changes in the global state, I need to call an evaluating arm that will edit the global state in-place
Cache function fetching:
- Have a gate fetch-operation within apply-instruction that takes term of an instruction as an argument and returns a number of operands to be consumed and a gate to be applied to the immediate arguments and consumed operands
- Cache that gate
- Fetching gate and operation gates must be defined outside of hwasm core
- Use four letters for operators (shoudld speed things up since 4 letter term is a direct atom)
Floating point: verify roundings and such (iirc they are different in Wasm spec an

The target audience is people who are familiar with Urbit's architecture, though not necessarily much of its code.

Plunder and Urbit

As some of you already know, i recently left my job as a core dev for the Urbit Foundation to work on a similar system called Plunder. Plunder was created in 2020 by two former Tlon employees, after their proposal for a new version of Nock was rejected. They have since reworked that significantly and built a reference implementation of their own system. You can follow its continued development on its mailing list.

I've known about Plunder for quite some time now, but their recently released demo -- in which the system is used to serve a 70 GB dataset, complete with metadata and searchable -- made me feel the need to explore it again and in greater detail. Doing this with my personal server doesn't feel like a big ask, but there is currentl

info 9-3-23 Added 4bit LLaMA install instructions for cards as small as 6GB VRAM! (See "BONUS 4" at the bottom of the guide)

warning 9-3-23 Added Torrent for HFv2 Model Weights, required for ooga's webUI, Kobold, Tavern and 4bit (+4bit model)! Update ASAP!

danger 11-3-23 There's a new torrent version of the 4bit weights called "LLaMA-HFv2-4bit". The old "LLaMA-4bit" torrent may be fine. But if you have any issues with it, it's recommended to update to the new 4bit torrent or use the decapoda-research versions off of HuggingFace or produce your own 4bit weights. Newer Torrent Link or [Newer Magnet Link](magnet:?xt=urn:btih:36945b5958b907b3ab69e963ba0de1abdf48c16c&dn=LLaMA-HFv2-4bit&tr=http%3a%2f%2fbt1.archive.org%3a6969%2fannounce&tr=http%3a%2f%2fbt2.archive.org%3a696

This Gist provides a solution to periodically capture screenshots of your Mac, and create therefrom a searchable PDF archive so that you can always get an answer to the “what, when, and where” questions about your usages.

To use these scripts:

Download the shell script rewind, then:
1. put it under ~/bin (or other fixed path you prefer);
2. execute

	// A nano dependent type-checker featuring inductive types via self encodings.
	// All computation rules are justified by interaction combinator semantics,
	// resulting in major simplifications and improvements over old Kind-Core.
	// Specifically, computable annotations (ANNs) and their counterpart (ANN
	// binders) and a new self encoding based on equality (rather than dependent
	// motives) greatly reduce code size. A more complete file, including
	// superpositions (for optimal unification) is available on the
	// Interaction-Type-Theory repository.
	// Credits also to Franchu and T6 for insights.

	=>
	\|%
	+$ ulam
	$~ [%coin *coin]
	:: leaves
	::
	$% [%coin =coin] :: atom, noun, or compound coin
	[%path =pith] :: hoon path syntax
	[%page =mark noun=*] :: %foo\|bar, bar is coin blob
	::

	import time
	from contextlib import suppress

	import torch
	import torch.nn as nn
	import torch.optim as optim
	import torch.nn.functional as F
	import torch.backends.cuda as cuda
	from torch.utils.data import DataLoader, IterableDataset

	type term =
	\| Lam of (term -> term)
	\| Pi of term * (term -> term)
	\| Appl of term * term
	\| Ann of term * term
	\| FreeVar of int
	\| Star
	\| Box

	let unfurl lvl f = f (FreeVar lvl)