hanki

23. Working in Hanki as an agent: the loop

The tooling below is one loop and no set of disconnected flags. Sketch the program with typed holes and let hanki check dictate each gap. Learn the surfaces you call from hanki doc --format=json and hanki query in place of reading source into context. Close diagnostics with explain, --fix, re-run, in place of re-deriving edits. Test with hanki test --format=json, property tests for universally-quantified claims and --deterministic for actor code. Run just-written code under the allowance hanki effects reports, through --allow and --deny. And before landing a change to a module others consume, let hanki api-diff classify the contract delta. HANKI-CARD.md §22 gives the same loop in compact form, the version every scaffolded project's agent reads. The bullets below are the per-tool depth:

error: internal compiler error - this is a bug in hanki, not in your program
  <the panic message>
  at <file:line:col>
  hanki 0.0.1 while running: check
  Please report it with the source and the command that triggered it.
  Re-run with RUST_BACKTRACE=1 for a backtrace to include.

The exit code is 70 (EX_SOFTWARE), outside the 250-254 block §22 reserves for a program's language faults: the toolchain failing and the program failing are different events. RUST_BACKTRACE=1 still produces a backtrace, printed under the report in place of a bare panic. An actor handler that panics is not this: the scheduler catches it and reports it through the death protocol (§15) as a HostPanic death, which is a fact about the running program.

main.hk:2:3: error[H0201]: type mismatch: expected int, found string
   2 |   "not an int"
     |   ^^^^^^^^^^^^

The caret counts Unicode scalars, matching the column the first line reports, and clips to the line's own length. A synthetic span, a @derive or where-expansion node with no source position, prints the header line alone. --format=json is unchanged: its rendered field gives the one line, which is what an agent parses.

The allowance also travels into the runtime. Every module.load! and module.reload! re-enforces it against the loaded file's declared surface, on the same declaration-level semantics as the launch gate, and refuses a widening load with a catchable ModuleLoadError, and runtime-loaded code therefore cannot escape the sandbox. Loaded code is default-deny. Even with no --allow or --deny, a program that loads modules at runtime pins its load-boundary allowance to its own declared capability surface, and a loaded module may therefore perform only what the host itself advertised; a dependency understating its manifest cannot execute the undeclared effect, capability denied: arriving in the caught ModuleLoadError. A host charges the effects of every Module<T> action it calls (§14), and the host's surface is therefore the ceiling it grants loaded code: to let a plugin do net, the host declares net on the trait method it calls, which also means --deny net on the host stops the whole composition, with no capability-leak hole. This bites only at the load boundary. A program with no module.load! site is left with the unconstrained fast paths, cache and unbounded fuel, untouched, and an explicit --allow is the user's own allowance replacing the derived baseline. Both tiers gate the load boundary. An AOT binary has no launch flags, and hanki build therefore bakes the host's declared surface into it, for a program that can load at all, and the embed loader enforces that baseline at every load! and reload!, the same default the bytecode scheduler derives, from the same declarations. A deployer tightens it without rebuilding through HANKI_ALLOW and HANKI_DENY in the environment, the form HANKI_DETERMINISTIC takes (§22): an allow list retains only the atoms it names that the baseline already grants, and the environment therefore narrows the baseline and never widens it; fs expands as on the CLI; deny wins; and an atom no capability names refuses the run with the CLI's own message, exit 1, in place of tightening nothing. They are read at the first load!, a program that never loads having nothing for the knobs to gate.

Capabilities bound what a run may do, and a companion bound caps how much. hanki run --max-steps N faults the run, exit 250, once N bytecode steps total across every actor are spent, and the run can never execute more than N. Steps are metered in small per-actor grants, and with several actors running at once the fault may therefore fire marginally early, while a single-actor or --deterministic run trips at N. A sandboxed run, any --deny or --allow, applies a generous default budget where --max-steps is unset, and untrusted code can therefore neither perform an undeclared capability nor spin forever. hanki run --max-bytes N is the memory companion, capping total heap allocation, collections, tuples, closures, and the string, bytes and bignum backing bytes those objects hold, at N bytes across the run, faulting the same way, exit 250, with the same sandbox default, and CPU and memory are therefore both bounded. The byte count is a conservative over-approximation, an Arc-shared payload held by several objects being charged once per holder, a security ceiling having to fail early and never late. hanki test takes both --max-steps and --max-bytes too, bounding each test, and a test that exceeds a budget fails, reported directly and never shrunk into a counterexample as a logic failure is. This is the bytecode tier's fuel-sandboxable mode (§22), and the AOT throughput tier omits it.

Where those flags bound a whole run from the CLI, with_budget(bytes, steps) BODY end bounds a nested scope from within the language. It carves a sub-quota from the parent's remaining step and byte budgets, a child never exceeding the parent and its spend debiting the parent, runs BODY under it, and evaluates to Result<T, sys.BudgetExceeded>, where T is BODY's type: Ok(v) on completion, and Err(Exceeded) the moment the sub-quota is spent. Unlike the whole-run ceiling, which faults the run at exit 250, a with_budget overrun is catchable, the host survives an over-budget child and recovers by matching the result, and it is therefore the in-language primitive for running untrusted or unbounded nested work, an embedded interpreter or a user-supplied predicate, under a bounded, recoverable ceiling. It nests: an inner with_budget sub-quotas the outer one, and a normal throw inside the body still propagates through it, budget exhaustion alone being intercepted. It is bytecode tier only, like the flags it scopes, and the AOT lowering rejects it, that tier having no resource metering.