Crate weft_lang 

Weft — the Thread’s native code format (reference implementation)

Ship intent, not instructions. A Weft program is a typed, total, effect-explicit term graph, identified by the hash of its canonical encoding. What crosses the wire is the same object that gets verified; execution backends (this crate’s reference interpreter first) compile or interpret it locally. Spec: weft-v0.1.

v0.1 scope — deliberately austere:

• First-order and non-recursive. Definitions call other definitions by content hash; since a definition’s hash doesn’t exist until it is built, cycles are unconstructible and every program terminates by construction. (fold over finite data arrives in v0.2.)
• No local names. Variables are de Bruijn indices, so alpha-equivalent programs are identical programs — same bytes, same hash. Names live outside the code, as metadata.
• Deterministic core: integers, booleans, text. Division by zero is defined (= 0), so no arithmetic traps exist. No floats.
• Effects are values. Constructing an [Action] performs nothing; the host (the browser) receives the returned actions and decides. A definition’s declared effect row must cover everything it (and its callees, transitively) can construct — the row IS the permission.
• Cost is static. The verifier computes a fuel bound per definition; the interpreter meters actual fuel. Verified code cannot run away.

Modules

draft_lib

weft-draft — level design as a verified program

model_lib

weft-model — the Thread’s modeling library

pack

weft-pack — packages for a content-addressed language

project

Projection — the human-readable rendering of a Weft module.

Structs

Def

One verified unit of Weft: typed parameters, result type, declared effect row, optional contracts, and the body. Its hash is its name.

Evaluated

Evaluate entry-style: call a definition with argument values, metering fuel and enforcing contracts. Deterministic: same module + args → same value + same fuel spent, on every host.

Module

A set of definitions keyed by hash — the unit of distribution. entry names the behavior’s event handler.

Verified

The verifier’s certificate for one definition: its checked effect row and the static fuel bound (an upper bound on interpreter steps per call).

WeftHash

A definition’s identity: the SHA-256 of its canonical encoding. Rendered — including on the wire — as weft:<hex>. To know the hash is to know the thing entire.

Enums

EffectKind

The effect vocabulary — the Behavior ABI’s Actions plus the declarative interaction effects, as types. Constructing one is pure; only the browser performs it. A behavior whose row lacks CommerceBuy cannot spend a traveler’s gold — not “shouldn’t”: the verifier rejects it.

PrimOp

Pure operations on the deterministic core.

Term

The term graph. Variables are de Bruijn indices (0 = innermost binder); a definition’s parameters are the outermost binders, in order.

Ty

The v0.1 type language.

Value

A runtime value.

WeftError

Constants

FIX_PI

π in Fix micros — the reference constant every host shares.

FIX_SCALE

One whole unit in Ty::Fix’s scale: fixed-point values count millionths.

FIX_TAU

τ (2π) in Fix micros.

MAX_LIST

The longest list a program may build with PrimOp::ListCat. Bounded like everything else: a model of ten thousand parts is a mistake, not an ambition, and the bound is what lets list growth exist at all without breaking the totality guarantee.

Functions

callees_of

Public view of a term’s call targets (pack’s closure trim uses it).

canonical_bytes

The canonical bytes of a definition — what the hash is over.

eval_call

hash_def

A definition’s identity.

verify_module

Verify every definition in a module: types, effect rows (transitive), contract typing, call closure — and compute static fuel bounds. Verification is per-hash cacheable: same hash, same verdict, forever.