SDK: host methods for most native statements

CLAUDE.md

@@ -162,12 +162,12 @@ The driver does not cache compiled modules between calls — every `Driver::exec
 
 - `var <ident> = <expr>` — declare a wildcard. Operations on it generate constraining statements.
 - `let <ident> = <expr>` — plain Rhai, literal known at both phases. No statements emitted.
-- `unsafe { <expr> }` — compute a wildcard value without emitting constraints. Pair with an explicit `action.st_*` call afterward, or a malicious prover can put anything there.
+- `unsafe { <expr> }` — compute a wildcard value without emitting constraints. Pair with an explicit `action.st_*` call afterward, or a malicious prover can put anything there. `+`, `-` and `*` on wildcards are only available inside such a block, so that a given expression always means the same thing (the flag covers the block's dynamic extent, script function calls included).
 
 **Host API** (registered via `register_fn` in `libs/sdk/src/lib.rs`):
 
-- 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>`.
+- On `action`: `input(class)`, `output(class)`, `mutate(class)`, `subaction(name)`, `random()`, `intro_vdf(iters, obj)`, `intro_lt_eq_u256(obj, target)`, `pow_obj_grind(obj, target)`, `top_limb_u256(n)`, plus one `st_*` per pod2 native predicate (`st_gt`, `st_sum`, `st_dict_contains`, `st_set_insert`, ... — the table in `libs/sdk/README.md` lists all of them; `SignedBy` and `PublicKey` have no host method).
+- On object handles: `set([[k,v],...])` (initializer for literals), `update(k,v)` (writes a witness-derived value), indexer `obj.<field>`. A `get(k)` method is registered but unimplemented; field reads go through the indexer.
 - 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.

libs/sdk/README.md

@@ -57,10 +57,58 @@ 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.
+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_product`,
+`action.st_gt`, ...) afterward, or a malicious prover can substitute any value.
+For `-` the pairing is a `Sum` with the operands rearranged (`a - b == r` is
+stated as `r + b == a`), since pod2 has no subtraction predicate.
+
+They stay `unsafe`-only on purpose rather than emitting their own statement
+outside a block. `unsafe` applies to the dynamic extent of its block, so it
+reaches into any script function called from inside one; an operator whose
+meaning depended on that would constrain its result or not according to the
+caller, and the unconstrained reading is the silent one.
+
+## Native statements
+
+`action.st_*` emits one pod2 native statement. Arguments are in the
+predicate's own order, so a call reads the same as the podlang it renders to,
+and each one takes a literal, a `var`, or a field read (`obj.field`). A
+whole-container argument naming an object is anchored to its record entry
+automatically.
+
+| Call | Holds when |
+| --- | --- |
+| `st_equal(a, b)`, `st_not_equal(a, b)` | the two values are (not) equal; any pod2 values |
+| `st_lt(a, b)`, `st_lt_eq(a, b)`, `st_gt(a, b)`, `st_gt_eq(a, b)` | integer comparison |
+| `st_sum(a, b, c)` | `a + b == c` |
+| `st_product(a, b, c)` | `a * b == c` |
+| `st_max(a, b, c)` | `max(a, b) == c` |
+| `st_hash(a, b, c)` | `c` is the pod2 hash of `a` and `b` |
+| `st_contains(c, k, v)`, `st_not_contains(c, k)` | any container (does not) hold `k` (mapped to `v`) |
+| `st_dict_contains(d, k, v)`, `st_dict_not_contains(d, k)` | same, and `d` is a dictionary |
+| `st_set_contains(s, v)`, `st_set_not_contains(s, v)` | `s` is a set that does (not) hold `v` |
+| `st_array_contains(a, i, v)` | array `a` holds `v` at index `i` |
+| `st_container_insert(old, k, v, new)` | `new` is `old` with `(k, v)` added |
+| `st_container_update(old, k, v, new)` | `new` is `old` with `k` remapped to `v` |
+| `st_container_delete(old, k, new)` | `new` is `old` with `k` removed |
+| `st_dict_insert`, `st_dict_update`, `st_dict_delete` | same three, pinning the container to a dictionary |
+| `st_set_insert(old, v, new)`, `st_set_delete(old, v, new)` | `new` is `old` with `v` added / removed |
+| `st_array_update(old, i, v, new)` | `new` is `old` with index `i` set to `v` |
+
+Two limits are worth knowing before reaching for these:
+
+- The transition statements (`st_*_insert` / `_update` / `_delete`) constrain
+  a relation between two container values. They do not compute the new
+  container, so it has to come from somewhere else: an object's entry, or a
+  witness from an `unsafe` block. Until the SDK can build container values
+  (see Missing features), the reachable use is relating two containers a
+  script already holds.
+- A field read of an object's whole-dict form is fine on inputs and mutates,
+  but reading a field of an *output* you just built (`out.durability`) is not
+  supported: the emitter renders it as `initials.out.durability`, a double
+  anchor podlang has no syntax for, and the module fails to compile.
 
 ## Type checking
 
@@ -153,35 +201,35 @@ as opaque entropy, not for byte-exact comparison with the L1 hash.
   - [ ] contains
   - [ ] insert
   - [ ] delete
-- [ ] Statements:
-  - [ ] Equal
-  - [ ] NotEqual
-  - [ ] LtEq
-  - [ ] Lt
-  - [ ] Contains
-  - [ ] NotContains
+- [x] Statements:
+  - [x] Equal
+  - [x] NotEqual
+  - [x] LtEq
+  - [x] Lt
+  - [x] Contains
+  - [x] NotContains
   - [x] Sum
-  - [ ] Product
-  - [ ] Max
-  - [ ] Hash
+  - [x] Product
+  - [x] Max
+  - [x] Hash
   - [ ] PublicKey
   - [ ] SignedBy
-  - [ ] ContainerInsert
-  - [ ] ContainerUpdate
-  - [ ] ContainerDelete
-  - [ ] DictContains
-  - [ ] DictNotContains
-  - [ ] SetContains
-  - [ ] SetNotContains
-  - [ ] ArrayContains
-  - [ ] GtEq
+  - [x] ContainerInsert
+  - [x] ContainerUpdate
+  - [x] ContainerDelete
+  - [x] DictContains
+  - [x] DictNotContains
+  - [x] SetContains
+  - [x] SetNotContains
+  - [x] ArrayContains
+  - [x] GtEq
   - [x] Gt
-  - [ ] DictInsert
-  - [ ] DictUpdate
-  - [ ] DictDelete
-  - [ ] SetInsert
-  - [ ] SetDelete
-  - [ ] ArrayUpdate
+  - [x] DictInsert
+  - [x] DictUpdate
+  - [x] DictDelete
+  - [x] SetInsert
+  - [x] SetDelete
+  - [x] ArrayUpdate
 - [ ] Execution time type checking without panics
 - [ ] operator+
 - [ ] operator\*
@@ -191,6 +239,7 @@ as opaque entropy, not for byte-exact comparison with the L1 hash.
 - [ ] error pretty print
 - [ ] forbid multiple Object::set operations on the same object
 - [ ] forbid Object::set after the objec thas been used in other operations
+- [ ] read a field of an output created in the same action (`out.field`)
 
 # Test example