Update docs and fix gui

CLAUDE.md

@@ -154,12 +154,13 @@ The driver does not cache compiled modules between calls — every `Driver::exec
 
 - On `action`: `input(class)`, `output(class)`, `mutate(class)`, `subaction(name)`, `random()`, `st_gt(a,b)`, `st_sum(a,b,c)`, `intro_vdf(iters, obj)`, `intro_lt_eq_u256(obj, target)`, `pow_obj_grind(obj, target)`, `top_limb_u256(n)`.
 - On object handles: `set([[k,v],...])` (initializer for literals), `update(k,v)` (writes a witness-derived value), `get(k)`, indexer `obj.<field>`.
+- In scope as a constant: `state_header` — the grounding state root as a record (`block_number`, `block_timestamp`, `block_hash`, `created`, `nullifiers`, `prior_state_history`). Field reads (`state_header.block_timestamp`) emit anchored statements against the action's public `state_header` arg, which txlib pins from `TxFinalized` down through guards and bridges. Note it describes the (recent) grounding root, not the inclusion block — see `libs/sdk/README.md` for the timing caveat.
 
 **Constraint:** the event tree must be the same shape every run. Branching that emits _different events_ on different inputs is unsupported. Branching on wildcard values inside `unsafe { ... }` is fine.
 
-**Records-form rendering** (`libs/sdk/src/fmt_podlang.rs`): to keep predicate arity small, the formatter coalesces all same-role objects of an action into one record arg instead of N loose wildcards. The public records are `in <Action>In` / `out <Action>Out` (one entry per input/output object; a Mutate contributes to both); the private `<Action>Initials` record holds one entry per output object's pre-identity (script-final) dict. The related `chain_steps`/`<Action>Chain` packing does the same for intermediate chain states, but only past a threshold (`CHAIN_PACK_MIN_TS = 3`); the in/out/initials records have no threshold and are the canonical form.
+**Records-form rendering** (`libs/sdk/src/fmt_podlang.rs`): to keep predicate arity small, the formatter coalesces all of an action's objects into one record arg instead of N loose wildcards. The single public record is `io <Action>IO`, with one `in_<var>` entry per input followed by one `out_<var>` entry per output (a Mutate contributes one entry to each side); the private `<Action>Initials` record holds one entry per output object's pre-identity (script-final) dict. Every action signature also carries a public `state_header StateHeader` record arg, passed through sub-action calls and bridges. The related `chain_steps`/`<Action>Chain` packing does the same for intermediate chain states, but only past a threshold (`CHAIN_PACK_MIN_TS = 3`); the io/initials records have no threshold and are the canonical form.
 
-**`Side` vs `Collapse`** (same file): these are two distinct axes, do not conflate them. `Side { In, Out }` is the strictly-binary public I/O role — it drives `dispatch_side` and the public signature. `Collapse { Side(Side), Initials }` is the record namespace a _collapsed_ object dict pins to when rendered (`in.<name>` / `out.<name>` / `initials.<name>`) or anchored; it is what `collapsed_at` / `collapses_at` return. `Initials` lives only on `Collapse` (private-only, never a public record arg or a dispatch target) and is deliberately **not** a `Side`.
+**`Side` vs `Collapse`** (same file): these are two distinct axes, do not conflate them. `Side { In, Out }` is the strictly-binary I/O role — it drives `dispatch_side` and which half of the `io` record an entry sits in (`in_<name>` vs `out_<name>`). `Collapse { IO(Side), Initials }` is the record namespace a _collapsed_ object dict pins to when rendered (`io.in_<name>` / `io.out_<name>` / `initials.<name>`) or anchored; it is what `collapsed_at` / `collapses_at` return. `Initials` lives only on `Collapse` (private-only, never a public record arg or a dispatch target) and is deliberately **not** a `Side`.
 
 ## Coding style
 

interfaces/gui/src/shared/pod2utils.ts

@@ -9,7 +9,8 @@ function isPod2IntWrapper(value: unknown): value is { Int: string | number } {
 function parsePod2IntWrapper(value: unknown): number | null {
   if (!isPod2IntWrapper(value)) return null;
   const raw = value.Int;
-  const parsed = typeof raw === "number" ? raw : Number.parseInt(String(raw), 10);
+  const parsed =
+    typeof raw === "number" ? raw : Number.parseInt(String(raw), 10);
   return Number.isFinite(parsed) ? parsed : null;
 }
 
@@ -38,7 +39,10 @@ function normalizePod2ContainerInner(value: unknown): unknown {
     )
   ) {
     return Object.fromEntries(
-      tupleEntries.map(([key, entry]) => [key as string, normalizePod2Value(entry)]),
+      tupleEntries.map(([key, entry]) => [
+        key as string,
+        normalizePod2Value(entry),
+      ]),
     );
   }
 
@@ -48,10 +52,10 @@ function normalizePod2ContainerInner(value: unknown): unknown {
     )
   ) {
     return tupleEntries
-      .map(([index, entry]) => [
-        parsePod2IntWrapper(index) ?? 0,
-        normalizePod2Value(entry),
-      ] as const)
+      .map(
+        ([index, entry]) =>
+          [parsePod2IntWrapper(index) ?? 0, normalizePod2Value(entry)] as const,
+      )
       .sort((left, right) => left[0] - right[0])
       .map(([, entry]) => entry);
   }
@@ -61,6 +65,68 @@ function normalizePod2ContainerInner(value: unknown): unknown {
   );
 }
 
+const CONTAINER_KIND_PATTERN = /^[d-][s-][a-]$/;
+
+function isPod2Container(
+  value: Record<string, unknown>,
+): value is { kind: string; kvs: unknown[] } {
+  return (
+    Object.keys(value).length === 2 &&
+    typeof value.kind === "string" &&
+    CONTAINER_KIND_PATTERN.test(value.kind) &&
+    Array.isArray(value.kvs)
+  );
+}
+
+/**
+ * pod2 containers serialize as `{ kind, kvs }`: `kind` is a three-flag
+ * string ("d--" dictionary, "-s-" set, "--a" array; flags can combine when
+ * one root has been used as several types) and `kvs` holds `[key, value]`
+ * entries, collapsed to `[value]` when the key equals the value (always the
+ * case for sets). Unwrap by the claimed kind; a kvs whose entries do not
+ * match it falls back to the shape heuristics of
+ * `normalizePod2ContainerInner`.
+ */
+function normalizePod2Container(kind: string, kvs: unknown[]): unknown {
+  const entryPair = (entry: unknown): [unknown, unknown] | null => {
+    if (!Array.isArray(entry) || entry.length < 1 || entry.length > 2) {
+      return null;
+    }
+    return [entry[0], entry[entry.length - 1]];
+  };
+  const pairs = kvs.map(entryPair);
+
+  if (kind[0] === "d") {
+    if (pairs.every((pair) => pair !== null && typeof pair[0] === "string")) {
+      return Object.fromEntries(
+        (pairs as [string, unknown][]).map(([key, entry]) => [
+          key,
+          normalizePod2Value(entry),
+        ]),
+      );
+    }
+  } else if (kind[1] === "s") {
+    if (pairs.every((pair) => pair !== null)) {
+      return (pairs as [unknown, unknown][]).map(([, entry]) =>
+        normalizePod2Value(entry),
+      );
+    }
+  } else if (kind[2] === "a") {
+    const slots = pairs.map((pair) => {
+      if (!pair) return null;
+      const index = parsePod2IntWrapper(pair[0]);
+      if (index === null) return null;
+      return [index, normalizePod2Value(pair[1])] as const;
+    });
+    if (slots.every((slot) => slot !== null)) {
+      return (slots as (readonly [number, unknown])[])
+        .sort((left, right) => left[0] - right[0])
+        .map(([, entry]) => entry);
+    }
+  }
+  return normalizePod2ContainerInner(kvs);
+}
+
 function normalizePod2Value(value: unknown): unknown {
   if (typeof value === "string") {
     return value
@@ -86,6 +152,10 @@ function normalizePod2Value(value: unknown): unknown {
     return value;
   }
 
+  if (isPod2Container(value)) {
+    return normalizePod2Container(value.kind, value.kvs);
+  }
+
   const keys = Object.keys(value);
   if (keys.length === 1) {
     const key = keys[0];
@@ -122,7 +192,10 @@ function normalizePod2Value(value: unknown): unknown {
   }
 
   return Object.fromEntries(
-    Object.entries(value).map(([key, entry]) => [key, normalizePod2Value(entry)]),
+    Object.entries(value).map(([key, entry]) => [
+      key,
+      normalizePod2Value(entry),
+    ]),
   );
 }
 

libs/sdk/README.md

@@ -57,6 +57,11 @@ because we want to calculate the value of a `var` as a witness to some
 statement. The generation of constraining statements can be disabled by using
 an `unsafe` block.
 
+The integer operators `+` and `-` on `var` values are only available inside
+`unsafe` blocks: they compute a witness value and emit nothing. Pair the
+result with an explicit statement (`action.st_sum`, `action.st_gt`, ...)
+afterward, or a malicious prover can substitute any value.
+
 ## Type checking
 
 The scripting language has dynamic types so we do type checking at runtime.
@@ -85,6 +90,38 @@ action.intro_lt_eq_u256(wood, target);
 
 The emitted podlang embeds `target` as a hex `Raw(0x00…)` literal.
 
+## Reading the state header
+
+Every action scope has a `state_header` constant: the `StateHeader` record of
+the state root the transaction grounds against. Its entries are
+`block_number`, `block_timestamp`, `block_hash`, `created`, `nullifiers` and
+`prior_state_history`. A field access like `state_header.block_timestamp`
+behaves like a `var` entry ref: using it in a statement or an object write
+emits an anchored statement against the action's public `state_header`
+argument, which txlib pins to the grounded state root all the way up from
+`TxFinalized` — a prover cannot substitute its own values.
+
+```rhai
+fn Tick(action) {
+    var ticker = action.mutate("Ticker");
+    var min_ts = unsafe { ticker.ts + 3600 };
+    action.st_sum(ticker.ts, 3600, min_ts);
+    action.st_gt(state_header.block_timestamp, min_ts);
+    ticker.update("ts", state_header.block_timestamp);
+}
+```
+
+Timing caveat: the header describes the _grounding_ state root, not the block
+that will include the transaction. The synchronizer accepts grounding roots up
+to `MAX_STATE_ROOT_AGE_BLOCKS` (300 blocks, roughly an hour) old, so a prover
+may legitimately ground against the oldest accepted root: `block_timestamp`
+can trail wall-clock time by up to that window, and the transaction lands on
+chain later still. Treat time locks written against it as coarse-grained.
+
+`block_hash` is a lossy repacking of the execution block hash (each 8-byte
+limb reduced into a field element, see `pod2utils::b256_to_hash`) — suitable
+as opaque entropy, not for byte-exact comparison with the L1 hash.
+
 # Missing features
 
 - [ ] Literal Array

libs/sdk/src/fmt_podlang.rs

@@ -1,9 +1,11 @@
 //! Functions used to format to podlang source code.
 //!
 //! This is the records-form emitter. Every action becomes
-//! `Action(in <Action>In, out <Action>Out, chain0, chain, ...)` where the
-//! `in`/`out` typed wildcards are pod2 records carrying one entry per
-//! Object inst on that side. Each (action, object) tuple gets a bridge
+//! `Action(io <Action>IO, state_header StateHeader, chain0, chain, ...)`
+//! where `io` is a pod2 record carrying one `in_<var>` entry per Input
+//! and one `out_<var>` entry per Output (a Mutate contributes one of
+//! each) and `state_header` is the grounding state root record threaded
+//! down from `TxFinalized`. Each (action, object) tuple gets a bridge
 //! predicate that pins the focused entry via `ArrayContains` and defers
 //! to the action; the IsX OR is over those bridge predicates.
 
@@ -132,9 +134,9 @@ impl<'a> fmt::Display for VarNameFmt<'a> {
     }
 }
 
-/// Which public record an Object inst belongs to: `in <Action>In`
-/// and `out <Action>Out` each carry one entry per Object inst on that
-/// side (Mutate contributes to both).
+/// Which side of the `<Action>IO` record an Object inst's entry sits
+/// on: `in_<var>` entries come first, then `out_<var>` entries (Mutate
+/// contributes one entry to each side).
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
 pub(crate) enum Side {
     In,
@@ -307,11 +309,11 @@ fn collect_sub_action_calls(action: &ActionContext) -> Vec<SubActionCall> {
 /// Emit one action predicate. For each Object inst, sides whose
 /// `needs_wildcard` is set get a leading `ArrayContains` clause + a
 /// private wildcard; collapsed sides drop both and let body refs render
-/// as `in.<entry>` / `out.<entry>` anchored refs. Witness vars (e.g.,
-/// values passed to `obj.update(k, v)`) appear as plain private
-/// wildcards. Sub-action calls are emitted with synthesized typed-
-/// private wildcards `_<Sub>_in_<n>` / `_<Sub>_out_<n>` matching the
-/// sub's record schemas.
+/// as `io.in_<entry>` / `io.out_<entry>` anchored refs. Witness vars
+/// (e.g., values passed to `obj.update(k, v)`) appear as plain private
+/// wildcards. Sub-action calls are emitted with a synthesized typed-
+/// private wildcard `_<Sub>_io_<n>` matching the sub's record schema,
+/// and pass the parent's `state_header` through.
 fn fmt_action(action: &ActionContext, loader: &Loader, w: &mut dyn fmt::Write) -> fmt::Result {
     let meta = loader
         .actions_meta
@@ -390,7 +392,7 @@ fn fmt_action(action: &ActionContext, loader: &Loader, w: &mut dyn fmt::Write) -
 
     // Per-var rendering state for body emission. Each var holds a
     // back-reference to `meta` so `VarNameFmt::collapses_at` can
-    // resolve whether it renders as `in.<name>` / `out.<name>` /
+    // resolve whether it renders as `io.in_<name>` / `io.out_<name>` /
     // `initials.<name>` at a given ts.
     let mut vars: HashMap<&str, VarNameFmt> = action
         .vars
@@ -519,7 +521,7 @@ fn fmt_action(action: &ActionContext, loader: &Loader, w: &mut dyn fmt::Write) -
     // extra ts that `output_max_ts` reserves) is the post-identity `new`
     // dict TxInsert produces. The post-identity form is the object's
     // output state: it is what the transaction inserts, and it collapses
-    // to `out.<name>` to bind the `<Action>Out` record entry.
+    // to `io.out_<name>` to bind the `<Action>IO` record entry.
     for o in &meta.object_refs {
         let chain = vars["chain"];
         let chain_next = chain.next();
@@ -577,7 +579,7 @@ fn fmt_bridges(loader: &Loader, w: &mut dyn fmt::Write) -> fmt::Result {
             let bridge_name = bridge_predicate_name(&o.class, &meta.name, &o.varname, multi);
 
             // Bridge predicate signature: state, state_header, chain0, chain (public);
-            // in <ActionIn>, out <ActionOut> private as needed.
+            // io <ActionIO> private when the action has any entries.
             write!(w, "{bridge_name}(state, state_header, chain0, chain")?;
             let mut priv_parts: Vec<String> = Vec::new();
             if !meta.in_entries.is_empty() || !meta.out_entries.is_empty() {

libs/sdk/src/lib.rs

@@ -1559,21 +1559,21 @@ fn try_value_from_dynamic(v: Dynamic) -> RuntimeResult<Value> {
 /// One object reference in an action, in declaration order. Only
 /// `class` is exposed; `io` is internal, used by the
 /// `local_inputs()` / `local_outputs()` filters. `varname` is the
-/// script-side variable name; it doubles as the entry name in the
-/// records-form `<Action>In` / `<Action>Out` schemas.
+/// script-side variable name; side-prefixed (`in_<var>` / `out_<var>`)
+/// it forms the entry names in the records-form `<Action>IO` schema.
 #[derive(Debug, Clone)]
 pub struct ActionObjectRef {
     pub(crate) io: ObjectIO,
     pub class: String,
     pub(crate) varname: String,
 }
 
-/// One slot in an action's `<Action>In` or `<Action>Out` record. A
-/// Mutate Object contributes one `EntryShape` to each side; Input/
-/// Output Objects contribute one to their side only. `needs_wildcard`
-/// drives whether the slot is referenced directly (collapsed to
-/// `<side>.<entry>` anchored refs) or via a private wildcard pinned
-/// by an `ArrayContains` clause.
+/// One slot in an action's `<Action>IO` record (in-entries first,
+/// then out-entries). A Mutate Object contributes one `EntryShape` to
+/// each side; Input/Output Objects contribute one to their side only.
+/// `needs_wildcard` drives whether the slot is referenced directly
+/// (collapsed to `io.<side>_<entry>` anchored refs) or via a private
+/// wildcard pinned by an `ArrayContains` clause.
 #[derive(Debug, Clone)]
 pub(crate) struct EntryShape {
     pub varname: String,
@@ -1651,15 +1651,18 @@ impl ActionMeta {
             .position(|name| name == varname)
     }
 
-    /// Find this Object's `in` entry. Returns its slot in the
-    /// `<Action>In` record and the entry shape.
+    /// Find this Object's in-side entry. Returns its slot in the
+    /// `<Action>IO` record and the entry shape.
     pub(crate) fn in_entry(&self, varname: &str) -> Option<(usize, &EntryShape)> {
         self.in_entries
             .iter()
             .enumerate()
             .find(|(_, e)| e.varname == varname)
     }
 
+    /// Find this Object's out-side entry. Returns its slot in the
+    /// `<Action>IO` record (offset past the in-entries) and the entry
+    /// shape.
     pub(crate) fn out_entry(&self, varname: &str) -> Option<(usize, &EntryShape)> {
         self.out_entries
             .iter()