Skip to main content

Crate weft_lang

Crate weft_lang 

Source
Expand description

§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: docs/spec/weft-v0.1.md.

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.