diff --git a/CLAUDE.md b/CLAUDE.md index 168d12a4..f4c2a080 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -162,12 +162,12 @@ The driver does not cache compiled modules between calls — every `Driver::exec - `var = ` — declare a wildcard. Operations on it generate constraining statements. - `let = ` — plain Rhai, literal known at both phases. No statements emitted. -- `unsafe { }` — compute a wildcard value without emitting constraints. Pair with an explicit `action.st_*` call afterward, or a malicious prover can put anything there. +- `unsafe { }` — 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.`. +- 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.`. 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. diff --git a/libs/sdk/README.md b/libs/sdk/README.md index e98d03fa..00f26fd9 100644 --- a/libs/sdk/README.md +++ b/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 diff --git a/libs/sdk/src/lib.rs b/libs/sdk/src/lib.rs index 915a3159..42dfa3ef 100644 --- a/libs/sdk/src/lib.rs +++ b/libs/sdk/src/lib.rs @@ -389,6 +389,30 @@ fn validate_args(args_types: [(Dynamic, Type); N]) -> RuntimeRes Ok(rs.try_into().expect("len = N")) } +/// Declare the host methods that emit one native statement each, and +/// the one function that registers them. Each row gives the script-side +/// name, the pod2 predicate, and one argument per statement arg with the +/// type it is checked against at Load time (`Type::Unk` where any pod2 +/// value goes). Argument order is the predicate's own, so a call reads +/// like the podlang it renders to. Generating both halves from one table +/// is what keeps a method from existing in Rust but not in Rhai. +macro_rules! st_methods { + ($($name:ident, $pred:ident, [$($arg:ident: $typ:expr),+ $(,)?]);+ $(;)?) => { + impl ActionHandle { + $( + fn $name(self, $($arg: Dynamic),+) -> RuntimeResult<()> { + let args = validate_args([$(($arg, $typ)),+])?; + self.native_st(NativePredicate::$pred, args.into()) + } + )+ + } + + fn register_st_methods(engine: &mut Engine) { + $( engine.register_fn(stringify!($name), ActionHandle::$name); )+ + } + }; +} + /// Used to track how many updates from mutations a variable takes. #[derive(Default, Debug)] struct VarState { @@ -1024,6 +1048,28 @@ impl ActionHandle { .iter() .map(|o| (o.varname.clone(), 0usize)) .collect(); + + // The anchored form of each arg of a body statement, in arg + // order, or None where the arg stays as proved. A whole-dict arg + // naming an Object collapsed at this ts lifts to its record slot; + // a dict-field arg (`var.key`) lifts to its entry, but only for + // callers whose statement was proved with every arg literal + // (`lift_keys`) -- ops built from `as_op_arg` already carry the + // entry form. + // The anchored form the compiled podlang gives this arg, or None + // when it renders as a literal or a loose wildcard. A dict-field + // ref (`var.key`) resolves to its entry; a whole-container ref + // resolves to the record slot its Object collapses to at this ts. + let arg_anchor = |arg: &Ref, current_ts: &HashMap| -> Option { + let arg = arg.borrow(); + match &*arg { + VarOrValue::Var(Var { key: Some(_), .. }) => Some(arg.as_op_arg()), + VarOrValue::Var(Var { + key: None, name, .. + }) => current_ts.get(name).and_then(|ts| anchor_at(name, *ts)), + VarOrValue::Value(_) => None, + } + }; { let mut exe_ctx = exe_rc.borrow_mut(); let exe_ctx = &mut *exe_ctx; @@ -1032,14 +1078,22 @@ impl ActionHandle { match inst { Inst::Object { .. } => {} Inst::Statement { pred, args } => { - let op = native_pred_to_op(*pred); - let op_type = OperationType::Native(op); - let op_args = args.iter().map(|v| v.borrow().as_op_arg()).collect(); + let op_type = OperationType::Native(native_pred_to_op(*pred)); + // Built with each arg already in the form the + // rendered podlang names it, so the statement + // needs no lifting afterwards. + let op_args = args + .iter() + .map(|arg| { + arg_anchor(arg, ¤t_ts) + .unwrap_or_else(|| arg.borrow().as_op_arg()) + }) + .collect(); let st = exe_ctx .bld .builder .priv_op(Operation(op_type, op_args, OperationAux::None)) - .unwrap(); + .map_err(|err| format!("{pred} statement failed: {err}"))?; body_sts.push(st); } Inst::Intro { @@ -1047,27 +1101,12 @@ impl ActionHandle { } => { let st_literal = statement.clone().expect("Intro statement captured at Rhai"); - // The intro pod's cached Statement carries only - // literal values, while the compiled podlang - // anchors two arg forms: a dict-field arg - // (`var.key`) is lifted to its entry, and a - // whole-dict arg of an Object collapsed at this - // ts is lifted to its record slot. Loose-wildcard - // and literal args stay literal. + // The pod proved its statement over literal + // values, so unlike a body statement this one + // cannot be built anchored and has to be lifted. let replacements: Vec> = args .iter() - .map(|arg| { - let arg = arg.borrow(); - match &*arg { - VarOrValue::Var(Var { key: Some(_), .. }) => { - Some(arg.as_op_arg()) - } - VarOrValue::Var(Var { - key: None, name, .. - }) => current_ts.get(name).and_then(|ts| anchor_at(name, *ts)), - VarOrValue::Value(_) => None, - } - }) + .map(|arg| arg_anchor(arg, ¤t_ts)) .collect(); let st = if replacements.iter().any(|r| r.is_some()) { exe_ctx @@ -1371,14 +1410,6 @@ impl ActionHandle { let raw = RawValue([F(0), F(0), F(0), F(n_int as u64)]); Ok(ArgHandle::literal(self.clone(), Value::from(raw))) } - fn st_gt(self, v0: Dynamic, v1: Dynamic) -> RuntimeResult<()> { - let [v0, v1] = validate_args([(v0, Type::Int), (v1, Type::Int)])?; - self.native_st(NativePredicate::Gt, vec![v0, v1]) - } - fn st_sum(self, v0: Dynamic, v1: Dynamic, v2: Dynamic) -> RuntimeResult<()> { - let [v0, v1, v2] = validate_args([(v0, Type::Int), (v1, Type::Int), (v2, Type::Int)])?; - self.native_st(NativePredicate::Sum, vec![v0, v1, v2]) - } fn intro_vdf(self, n_iters: Dynamic, input: Dynamic) -> RuntimeResult { let [n_iters, input] = validate_args([(n_iters, Type::Int), (input, Type::Raw)])?; @@ -1434,6 +1465,38 @@ impl ActionHandle { } } +// `SignedBy` and `PublicKey` are absent on purpose: both need key +// material, which an action script has no way to name, and `SignedBy` +// additionally needs a signature passed as operation aux data. +st_methods! { + st_equal, Equal, [v0: Type::Unk, v1: Type::Unk]; + st_not_equal, NotEqual, [v0: Type::Unk, v1: Type::Unk]; + st_lt, Lt, [v0: Type::Int, v1: Type::Int]; + st_lt_eq, LtEq, [v0: Type::Int, v1: Type::Int]; + st_gt, Gt, [v0: Type::Int, v1: Type::Int]; + st_gt_eq, GtEq, [v0: Type::Int, v1: Type::Int]; + st_sum, Sum, [v0: Type::Int, v1: Type::Int, v2: Type::Int]; + st_product, Product, [v0: Type::Int, v1: Type::Int, v2: Type::Int]; + st_max, Max, [v0: Type::Int, v1: Type::Int, v2: Type::Int]; + st_hash, Hash, [v0: Type::Unk, v1: Type::Unk, v2: Type::Unk]; + st_contains, Contains, [c: Type::Unk, k: Type::Unk, v: Type::Unk]; + st_not_contains, NotContains, [c: Type::Unk, k: Type::Unk]; + st_dict_contains, DictContains, [d: Type::Dict, k: Type::Unk, v: Type::Unk]; + st_dict_not_contains, DictNotContains, [d: Type::Dict, k: Type::Unk]; + st_set_contains, SetContains, [s: Type::Unk, v: Type::Unk]; + st_set_not_contains, SetNotContains, [s: Type::Unk, v: Type::Unk]; + st_array_contains, ArrayContains, [a: Type::Unk, i: Type::Int, v: Type::Unk]; + st_container_insert, ContainerInsert, [old: Type::Unk, k: Type::Unk, v: Type::Unk, new: Type::Unk]; + st_container_update, ContainerUpdate, [old: Type::Unk, k: Type::Unk, v: Type::Unk, new: Type::Unk]; + st_container_delete, ContainerDelete, [old: Type::Unk, k: Type::Unk, new: Type::Unk]; + st_dict_insert, DictInsert, [old: Type::Dict, k: Type::Unk, v: Type::Unk, new: Type::Dict]; + st_dict_update, DictUpdate, [old: Type::Dict, k: Type::Unk, v: Type::Unk, new: Type::Dict]; + st_dict_delete, DictDelete, [old: Type::Dict, k: Type::Unk, new: Type::Dict]; + st_set_insert, SetInsert, [old: Type::Unk, v: Type::Unk, new: Type::Unk]; + st_set_delete, SetDelete, [old: Type::Unk, v: Type::Unk, new: Type::Unk]; + st_array_update, ArrayUpdate, [old: Type::Unk, i: Type::Int, v: Type::Unk, new: Type::Unk]; +} + fn rt_err_from_anyhow(err: anyhow::Error) -> Box { Box::new(EvalAltResult::ErrorRuntime( Dynamic::from(Rc::new(err)), @@ -1581,33 +1644,61 @@ impl ArgHandle { } } -/// operator- for maybe-var types -fn arg_sub(a: ArgHandle, b: ArgHandle) -> RuntimeResult { - type_check_args([(&a, Type::Int), (&b, Type::Int)])?; - // TODO: Handle the case where a and b are not var - let value = Rc::new(RefCell::new(VarOrValue::var(Type::Int))); - let ctx = a.ctx.0.borrow(); - ctx.assert_unsafe(true)?; - if ctx.exe_ctx.is_some() { - let a = a.arg.borrow().as_value().as_int().expect("int"); - let b = b.arg.borrow().as_value().as_int().expect("int"); - let result = a.checked_sub(b).expect("no overflow"); - value.borrow_mut().set_value(Value::from(result)); +/// Integer operator on maybe-var operands, with the native statement +/// that constrains its result. +#[derive(Clone, Copy)] +enum ArithOp { + Add, + Sub, + Mul, +} + +impl ArithOp { + fn symbol(&self) -> &'static str { + match self { + Self::Add => "+", + Self::Sub => "-", + Self::Mul => "*", + } + } + fn apply(&self, a: i64, b: i64) -> Option { + match self { + Self::Add => a.checked_add(b), + Self::Sub => a.checked_sub(b), + Self::Mul => a.checked_mul(b), + } } - Ok(ArgHandle::new(a.ctx.clone(), value)) } -/// operator+ for maybe-var types -fn arg_add(a: ArgHandle, b: ArgHandle) -> RuntimeResult { +/// operator+, operator- and operator* for maybe-var types. Only +/// available inside an `unsafe` block: the result is a bare witness and +/// nothing constrains it until the script pairs it with an explicit +/// statement (`action.st_sum`, `action.st_product`, ...). +/// +/// Emitting the paired statement here instead would make the operator +/// mean two different things: `unsafe` is set for the dynamic extent of +/// its block, so the same expression inside a script function would +/// constrain its result or not depending on the caller. +fn arg_arith(op: ArithOp, a: ArgHandle, b: ArgHandle) -> RuntimeResult { type_check_args([(&a, Type::Int), (&b, Type::Int)])?; - // TODO: Handle the case where a and b are not var let value = Rc::new(RefCell::new(VarOrValue::var(Type::Int))); - let ctx = a.ctx.0.borrow(); - ctx.assert_unsafe(true)?; - if ctx.exe_ctx.is_some() { - let a = a.arg.borrow().as_value().as_int().expect("int"); - let b = b.arg.borrow().as_value().as_int().expect("int"); - let result = a.checked_add(b).expect("no overflow"); + let is_exe = { + let ctx = a.ctx.0.borrow(); + ctx.assert_unsafe(true)?; + ctx.exe_ctx.is_some() + }; + if is_exe { + let int = |arg: &Ref| -> RuntimeResult { + arg.borrow() + .as_value() + .as_int() + .ok_or_else(|| format!("operator{}: operand is not an int", op.symbol()).into()) + }; + let (x, y) = (int(&a.arg)?, int(&b.arg)?); + let result = op.apply(x, y).ok_or_else(|| -> Box { + let sym = op.symbol(); + format!("operator{sym}: integer overflow on {x} {sym} {y}").into() + })?; value.borrow_mut().set_value(Value::from(result)); } Ok(ArgHandle::new(a.ctx.clone(), value)) @@ -2647,8 +2738,6 @@ fn new_engine() -> Engine { .register_fn("mutate", ActionHandle::mutate) .register_fn("subaction", ActionHandle::subaction) .register_fn("random", ActionHandle::random) - .register_fn("st_gt", ActionHandle::st_gt) - .register_fn("st_sum", ActionHandle::st_sum) .register_fn("intro_vdf", ActionHandle::intro_vdf) .register_fn("intro_lt_eq_u256", ActionHandle::intro_lt_eq_u256) .register_fn("pow_obj_grind", ActionHandle::pow_obj_grind) @@ -2668,27 +2757,36 @@ fn new_engine() -> Engine { Ok(()) }, ) - .register_fn("-", arg_sub) - .register_fn("-", |a: ArgHandle, b: i64| -> RuntimeResult { - let ctx = a.ctx.clone(); - arg_sub(a, ArgHandle::literal(ctx, Value::from(b))) - }) - .register_fn("-", |a: i64, b: ArgHandle| -> RuntimeResult { - let ctx = b.ctx.clone(); - arg_sub(ArgHandle::literal(ctx, Value::from(a)), b) + .register_indexer_get(ArgHandle::entry); + + register_st_methods(&mut engine); + for (symbol, op) in [ + ("+", ArithOp::Add), + ("-", ArithOp::Sub), + ("*", ArithOp::Mul), + ] { + register_arith(&mut engine, symbol, op); + } + + engine +} + +/// Register one integer operator over every operand pairing a script can +/// write: two wildcards, or a wildcard and an integer literal either way +/// round. +fn register_arith(engine: &mut Engine, symbol: &'static str, op: ArithOp) { + engine + .register_fn(symbol, move |a: ArgHandle, b: ArgHandle| { + arg_arith(op, a, b) }) - .register_fn("+", arg_add) - .register_fn("+", |a: ArgHandle, b: i64| -> RuntimeResult { + .register_fn(symbol, move |a: ArgHandle, b: i64| { let ctx = a.ctx.clone(); - arg_add(a, ArgHandle::literal(ctx, Value::from(b))) + arg_arith(op, a, ArgHandle::literal(ctx, Value::from(b))) }) - .register_fn("+", |a: i64, b: ArgHandle| -> RuntimeResult { + .register_fn(symbol, move |a: i64, b: ArgHandle| { let ctx = b.ctx.clone(); - arg_add(ArgHandle::literal(ctx, Value::from(a)), b) - }) - .register_indexer_get(ArgHandle::entry); - - engine + arg_arith(op, ArgHandle::literal(ctx, Value::from(a)), b) + }); } impl Default for Sdk { diff --git a/libs/sdk/src/tests.rs b/libs/sdk/src/tests.rs index dcbd8740..c919be98 100644 --- a/libs/sdk/src/tests.rs +++ b/libs/sdk/src/tests.rs @@ -10,6 +10,16 @@ fn apply_tx(state: &mut TestState, tx: &Tx) { ); } +fn assert_renders(module: &SdkModule, expected: &[&str]) { + for fragment in expected { + assert!( + module.podlang_src.contains(fragment), + "missing {fragment}\nactual:\n{}", + module.podlang_src + ); + } +} + fn grounding_witness(state: &TestState, input_commitments: &[Hash]) -> Arc { state.build_grounding_witness( input_commitments, @@ -926,3 +936,260 @@ fn test_sdk_state_header() { let [_ticker1] = res.objs(); apply_tx(&mut state, &ticker1_tx); } + +/// A whole-container statement arg renders anchored (`io.in_ore`) when +/// its Object's side collapses into the io record, so execution has to +/// lift the proved statement to the record entry the same way an intro +/// pod's is lifted. +#[allow(clippy::cloned_ref_to_slice_refs)] +#[test] +fn test_statement_whole_dict_arg() { + let _ = env_logger::builder().is_test(true).try_init(); + let craft_src = r#" + fn FindOre(action) { + var ore = action.output("Ore"); + ore.set([["grade", 7], ["floor", 3]]); + } + + fn AssertOre(action) { + var ore = action.input("Ore"); + var metal = action.output("Metal"); + action.st_dict_contains(ore, "grade", 7); + action.st_contains(ore, "floor", 3); + } +"#; + let sdk = Sdk::default(); + let module = sdk + .load_module_from_src_actions(craft_src, &["FindOre", "AssertOre"]) + .unwrap(); + assert_renders( + &module, + &[ + r#"DictContains(io.in_ore, "grade", 7)"#, + r#"Contains(io.in_ore, "floor", 3)"#, + ], + ); + + let mut state = TestState::default(); + + let executor = module.executor(true, grounding_witness(&state, &[])); + let res = executor.action("FindOre", vec![]).unwrap(); + let ore_tx = res.tx.clone(); + let [ore] = res.objs(); + apply_tx(&mut state, &ore_tx); + + let executor = module.executor(true, grounding_witness(&state, &[ore.obj.commitment()])); + let res = executor.action("AssertOre", vec![ore]).unwrap(); + let metal_tx = res.tx.clone(); + apply_tx(&mut state, &metal_tx); +} + +/// `*` computes a witness inside an `unsafe` block and emits nothing; +/// `st_product` is what constrains it. Proving the pair end to end is +/// what shows the new operator and its statement agree. +#[allow(clippy::cloned_ref_to_slice_refs)] +#[test] +fn test_unsafe_product_paired_with_statement() { + let _ = env_logger::builder().is_test(true).try_init(); + let craft_src = r#" + fn FindOre(action) { + var ore = action.output("Ore"); + ore.set([["grade", 7]]); + } + + fn MixAlloy(action) { + var ore = action.mutate("Ore"); + var doubled = unsafe { ore.grade * 2 }; + action.st_product(ore.grade, 2, doubled); + ore.update("work", doubled); + } +"#; + let sdk = Sdk::default(); + let module = sdk + .load_module_from_src_actions(craft_src, &["FindOre", "MixAlloy"]) + .unwrap(); + assert_renders(&module, &["Product(ore0.grade, 2, doubled)"]); + + let mut state = TestState::default(); + + let executor = module.executor(true, grounding_witness(&state, &[])); + let res = executor.action("FindOre", vec![]).unwrap(); + let ore_tx = res.tx.clone(); + let [ore] = res.objs(); + apply_tx(&mut state, &ore_tx); + + let executor = module.executor(true, grounding_witness(&state, &[ore.obj.commitment()])); + let res = executor.action("MixAlloy", vec![ore]).unwrap(); + let mixed_tx = res.tx.clone(); + let [mixed] = res.objs(); + apply_tx(&mut state, &mixed_tx); + assert_eq!( + mixed.obj.get(&StrKey::from("work")).unwrap().unwrap(), + Value::from(14) + ); +} + +/// The operators emit nothing on their own, and are rejected outside an +/// `unsafe` block rather than quietly constraining their result. That +/// keeps one meaning per spelling: `unsafe` covers the dynamic extent of +/// its block, so a context-dependent operator would mean different things +/// in a script function depending on its caller. +#[test] +fn test_arithmetic_is_unsafe_only() { + let craft_src = r#" + fn UnsafeMix(action) { + var ore = action.input("Ore"); + var alloy = action.output("Alloy"); + var lowered = unsafe { ore.grade - 1 }; + alloy.update("work", lowered); + } +"#; + let sdk = Sdk::default(); + let module = sdk + .load_module_from_src_actions(craft_src, &["UnsafeMix"]) + .unwrap(); + assert!( + !module.podlang_src.contains("Sum("), + "unsafe subtraction should emit no statement:\n{}", + module.podlang_src + ); + + for (action, src) in [ + ( + "BareSub", + r#" + fn BareSub(action) { + var ore = action.input("Ore"); + var alloy = action.output("Alloy"); + var lowered = ore.grade - 1; + alloy.update("work", lowered); + } +"#, + ), + ( + "BareMul", + r#" + fn BareMul(action) { + var ore = action.input("Ore"); + var alloy = action.output("Alloy"); + var doubled = ore.grade * 2; + alloy.update("work", doubled); + } +"#, + ), + ] { + let err = match Sdk::default().load_module_from_src_actions(src, &[action]) { + Ok(_) => panic!("expected {action} to require an unsafe block"), + Err(err) => err.to_string(), + }; + assert!(err.contains("expected unsafe block"), "{action}: {err}"); + } +} + +/// Every native statement the host API exposes has to survive the round +/// trip through rendered podlang, which `load_module_from_src_actions` +/// parses and compiles. Grouped a few per action to stay inside pod2's +/// per-predicate statement budget. +#[test] +fn test_statement_surface_round_trips() { + let craft_src = r#" + fn Compare(action) { + var crate_in = action.input("Crate"); + action.st_equal(crate_in.size, 2); + action.st_not_equal(crate_in.size, 3); + } + + fn Order(action) { + var crate_in = action.input("Crate"); + action.st_lt(1, crate_in.size); + action.st_lt_eq(2, 2); + action.st_gt_eq(3, 2); + } + + fn Arith(action) { + var crate_in = action.input("Crate"); + action.st_product(2, 3, 6); + action.st_max(2, 3, 3); + action.st_hash(1, 2, crate_in.digest); + } + + fn Reads(action) { + var crate_in = action.input("Crate"); + action.st_not_contains(crate_in, "missing"); + action.st_dict_not_contains(crate_in, "absent"); + } + + fn SetReads(action) { + var crate_in = action.input("Crate"); + action.st_set_contains(crate_in.tags, 1); + action.st_set_not_contains(crate_in.tags, 2); + action.st_array_contains(crate_in.items, 0, 1); + } + + fn ContainerTransitions(action) { + var crate_in = action.input("Crate"); + var crate_out = action.output("Crate"); + action.st_container_insert(crate_in, "k", 1, crate_out); + action.st_container_update(crate_in, "k", 1, crate_out); + action.st_container_delete(crate_in, "k", crate_out); + } + + fn DictTransitions(action) { + var crate_in = action.input("Crate"); + var crate_out = action.output("Crate"); + action.st_dict_insert(crate_in, "k", 1, crate_out); + action.st_dict_update(crate_in, "k", 1, crate_out); + action.st_dict_delete(crate_in, "k", crate_out); + } + + // Entry args on both sides come from inputs: a keyed read of an + // output's script-final form renders as `initials..`, + // a double anchor podlang has no syntax for. + fn SetTransitions(action) { + var crate_a = action.input("Crate"); + var crate_b = action.input("Crate"); + action.st_set_insert(crate_a.tags, 1, crate_b.tags); + action.st_set_delete(crate_a.tags, 1, crate_b.tags); + action.st_array_update(crate_a.items, 0, 1, crate_b.items); + } +"#; + let sdk = Sdk::default(); + let module = sdk + .load_module_from_src_actions( + craft_src, + &[ + "Compare", + "Order", + "Arith", + "Reads", + "SetReads", + "ContainerTransitions", + "DictTransitions", + "SetTransitions", + ], + ) + .unwrap(); + assert_renders( + &module, + &[ + "Equal(crate_in.size, 2)", + "NotEqual(crate_in.size, 3)", + "Lt(1, crate_in.size)", + "LtEq(2, 2)", + "GtEq(3, 2)", + "Product(2, 3, 6)", + "Max(2, 3, 3)", + "Hash(1, 2, crate_in.digest)", + r#"NotContains(io.in_crate_in, "missing")"#, + r#"DictNotContains(io.in_crate_in, "absent")"#, + "SetContains(crate_in.tags, 1)", + "SetNotContains(crate_in.tags, 2)", + "ArrayContains(crate_in.items, 0, 1)", + r#"ContainerDelete(io.in_crate_in, "k", initials.crate_out)"#, + r#"DictInsert(io.in_crate_in, "k", 1, initials.crate_out)"#, + "SetInsert(crate_a.tags, 1, crate_b.tags)", + "SetDelete(crate_a.tags, 1, crate_b.tags)", + "ArrayUpdate(crate_a.items, 0, 1, crate_b.items)", + ], + ); +}