From a3cf42c37336009a9aa7cd2c3c9fafad7d86bffb Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 8 May 2026 04:02:41 +0000 Subject: [PATCH] soft-agent: switch deploy specs to lex 0.3 record quantifiers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Retires the flat-scalar binding workaround now that lex-lang 0.3 (#208) supports spec quantifiers over user-defined ADTs and structural records. agents/{depot,vehicle}.spec: rewritten to quantify over record-typed `s` (state) and, for depot, `a` (action.payload) bindings, with field access in the body: spec depot_grid_budget { forall s :: { current_kw :: Float, budget_kw :: Float, pv_kw :: Float }, a :: { power_kw :: Float }: s.current_kw + a.power_kw <= s.budget_kw + s.pv_kw } Same invariant, stronger contract: state and action provenance are visible in the spec body, no more name-collision risk between state and payload fields. soft-agent::bindings: new `record_bindings(state, action)` forwards the agent's state JSON and the action's payload (SendA2a) or args (CallMcp) as two `LexValue::Record` bindings. Numbers map to Float (or Int if not f64-representable), strings to Str, bools to Bool; nested objects recurse. LLM actions get an empty action record. `default_float_bindings` (the 0.2-era flattening helper from PR #6) is kept exported as the legacy path so anyone with flat-scalar specs keeps working. soft-runner: now installs `record_bindings` instead of `default_float_bindings` when an agent declares specs. Tests: - 5 new unit tests for `record_bindings` (state forwarding, payload forwarding, args forwarding, LLM-action empty-record, non-object state → Unit) on top of the 2 retained legacy tests. - `deploy_specs.rs` updated: integration tests use the new helper; `depot_spec_evaluates_directly_with_record_bindings` verifies the on-disk depot.spec accepts record-shaped bindings of the exact shape `record_bindings` produces. cargo fmt clean, cargo clippy --workspace --all-targets -- -D warnings clean, full workspace test suite: 88 passed / 0 failed. Verified end-to-end via deploy/run-local.sh: vehicle proposed=2 allowed=2, depot proposed=1 allowed=1, pv ungated as expected, no violations. Discovery note: spec-checker 0.3 surfaces a useful "unbound spec var ``" reason when a quantifier name has no matching binding — made debugging the binding-shape mismatch trivial during this work. --- agents/depot.spec | 38 ++-- agents/vehicle.spec | 20 +-- crates/soft-agent/src/bindings.rs | 223 +++++++++++++++++------- crates/soft-agent/src/lib.rs | 2 +- crates/soft-agent/tests/deploy_specs.rs | 58 +++--- crates/soft-runner/src/main.rs | 6 +- 6 files changed, 225 insertions(+), 122 deletions(-) diff --git a/agents/depot.spec b/agents/depot.spec index d5df6f5..6e62f19 100644 --- a/agents/depot.spec +++ b/agents/depot.spec @@ -1,27 +1,23 @@ # depot.spec — grid-budget gate for the depot agent. # -# Quantifies over a mix of state and action data: -# - current_kw : load already on the grid (from state) -# - budget_kw : depot's hard contract limit (from state) -# - pv_kw : current photovoltaic offset (from state) -# - power_kw : power the outgoing GrantSession is committing to -# (from the -# SendA2a -# payload) +# Quantifies over two record-typed bindings: +# - `s` :: { current_kw, budget_kw, pv_kw } — projected from the +# depot's state record at gate time. +# - `a` :: { power_kw } — projected from the *outgoing* +# SendA2a.payload (e.g. the GrantSession the depot is committing +# to). The lex handler embeds power_kw in every GrantSession so +# the spec can audit the commitment, not the internal request. # -# This is a stronger invariant than reading `requested_kw` from state: -# it audits the *commitment depot is making*, not the request as -# recorded internally. If depot's handler ever produces a GrantSession -# whose `power_kw` exceeds available headroom — even by a bug in the -# handler — the gate denies the action. +# Lex-lang 0.3 (#208) shipped record-typed quantifiers and field +# access, so the spec body destructures the records directly — no +# flattening helper required (cf. soft-agent's `bindings::record_bindings`, +# which simply forwards state and action.payload as `Record` values). # -# soft-runner's `default_float_bindings` extracts `power_kw` from the -# SendA2a action's payload and merges it with state floats; that's -# what makes this spec body resolvable at gate time. +# This is the same invariant as 0.2's flat-binding form +# (current_kw + power_kw ≤ budget_kw + pv_kw); the only change is +# binding shape. spec depot_grid_budget { - forall current_kw :: Float, - power_kw :: Float, - budget_kw :: Float, - pv_kw :: Float: - current_kw + power_kw <= budget_kw + pv_kw + forall s :: { current_kw :: Float, budget_kw :: Float, pv_kw :: Float }, + a :: { power_kw :: Float }: + s.current_kw + a.power_kw <= s.budget_kw + s.pv_kw } diff --git a/agents/vehicle.spec b/agents/vehicle.spec index 648b910..a20e2e4 100644 --- a/agents/vehicle.spec +++ b/agents/vehicle.spec @@ -1,16 +1,14 @@ # vehicle.spec — state-of-charge reserve gate for the vehicle agent. # -# Quantifies over scalar floats in the vehicle's state: -# - soc : current state of charge (0.0..1.0) -# - energy_needed : energy this delivery will consume -# - reserve : floor SOC must stay above +# Quantifies over a record-typed `s` binding projected from the +# vehicle's state. The action shape isn't relevant for this +# invariant — vehicle's outgoing actions don't carry SOC data — so +# the gate doesn't need a record-typed `a` binding here. # -# Invariant: any outbound action must preserve the post-delivery -# reserve (soc - energy_needed >= reserve). Phase 1 spec from -# tests/phase1_specs.rs, lifted into the deploy fleet. +# Lex-lang 0.3 (#208) shipped record-typed quantifiers and field +# access; soft-agent's `bindings::record_bindings` forwards the +# state JSON straight through as a `LexValue::Record`. spec vehicle_soc_reserve { - forall soc :: Float, - energy_needed :: Float, - reserve :: Float: - soc - energy_needed >= reserve + forall s :: { soc :: Float, reserve :: Float, energy_needed :: Float }: + s.soc - s.energy_needed >= s.reserve } diff --git a/crates/soft-agent/src/bindings.rs b/crates/soft-agent/src/bindings.rs index 78d90f6..4217acb 100644 --- a/crates/soft-agent/src/bindings.rs +++ b/crates/soft-agent/src/bindings.rs @@ -1,22 +1,27 @@ -//! Default `BindingsFn` for spec gates. +//! Default `BindingsFn`s for spec gates. //! -//! [`default_float_bindings`] walks an agent's state plus the action -//! being evaluated and emits one `LexValue::Float` binding per -//! top-level numeric field. Action-derived bindings override -//! state-derived bindings on collision so a spec can reason about a -//! field both agents might carry under the same name (e.g. `power_kw` -//! in state vs in an outgoing GrantSession payload — the latter is -//! the value the gate should validate, since it's what the agent is -//! committing to). +//! [`record_bindings`] is the recommended default for soft-agent on +//! lex-lang 0.3+: it forwards an agent's state and the action's +//! payload (or args) as two record-typed bindings — `s` and `a` — +//! that a spec can destructure directly via field access. This +//! relies on lex-lang #208 (spec-checker quantifiers over user-defined +//! ADTs and structural records). //! -//! Action sources by variant: -//! - [`Action::SendA2a`]: walks the `payload` object. -//! - [`Action::CallMcp`]: walks the `args` object. -//! - [`Action::LocalLlm`] / [`Action::CloudLlm`]: no numeric scalars. +//! Spec authors write: //! -//! Only top-level fields are extracted; nested objects are ignored. -//! Use a custom [`BindingsFn`](crate::BindingsFn) when a spec needs -//! deeper structure or non-Float types. +//! ```text +//! spec my_invariant { +//! forall s :: { current_kw :: Float, budget_kw :: Float }, +//! a :: { power_kw :: Float }: +//! s.current_kw + a.power_kw <= s.budget_kw +//! } +//! ``` +//! +//! [`default_float_bindings`] is the legacy flattening helper kept +//! for backward compatibility — specs that still quantify over flat +//! scalar bindings (`forall current_kw :: Float, ...`) continue to +//! work. New specs should prefer [`record_bindings`] for the stronger +//! type contract and clearer scoping. use indexmap::IndexMap; use lex_bytecode::Value as LexValue; @@ -24,8 +29,76 @@ use serde_json::Value; use crate::Action; -/// Default `BindingsFn` for soft-runner-style deployments. See module -/// docs for semantics. +/// Forwards `state` and the action's payload/args as two record-typed +/// bindings — `s` and `a` — for use with lex-lang 0.3+ specs that +/// quantify over records. +/// +/// Action sources by variant: +/// - [`Action::SendA2a`]: forwards `payload`. +/// - [`Action::CallMcp`]: forwards `args`. +/// - [`Action::LocalLlm`] / [`Action::CloudLlm`]: forwards an empty +/// record (the spec body's field accesses on `a` will be +/// undefined; specs that intentionally apply only to a/2a or MCP +/// should add an explicit guard, or omit `a` from the quantifier). +/// +/// Non-object JSON values (null, scalar, array) are forwarded as +/// `LexValue::Unit`; the spec evaluator treats field access on Unit +/// as Inconclusive (soft-Deny under the runner's policy). +pub fn record_bindings(state: &Value, action: &Action) -> IndexMap { + let mut out = IndexMap::new(); + out.insert("s".to_string(), json_to_record_value(state)); + + let action_obj = match action { + Action::SendA2a { payload, .. } => payload.clone(), + Action::CallMcp { args, .. } => args.clone(), + Action::LocalLlm { .. } | Action::CloudLlm { .. } => Value::Object(Default::default()), + }; + out.insert("a".to_string(), json_to_record_value(&action_obj)); + out +} + +fn json_to_record_value(v: &Value) -> LexValue { + match v { + Value::Object(map) => { + let mut fields = IndexMap::new(); + for (k, val) in map { + fields.insert(k.clone(), json_scalar_to_lex(val)); + } + LexValue::Record(fields) + } + _ => LexValue::Unit, + } +} + +fn json_scalar_to_lex(v: &Value) -> LexValue { + match v { + Value::Number(n) => { + if let Some(f) = n.as_f64() { + LexValue::Float(f) + } else if let Some(i) = n.as_i64() { + LexValue::Int(i) + } else { + LexValue::Unit + } + } + Value::Bool(b) => LexValue::Bool(*b), + Value::String(s) => LexValue::Str(s.clone()), + Value::Object(_) => json_to_record_value(v), + // Lists/null/etc. — not currently consumed by any deploy spec. + // If a future spec needs them, extend here (LexValue::List, Unit). + _ => LexValue::Unit, + } +} + +/// Legacy flat-scalar `BindingsFn` for soft-agent on lex-lang 0.2 and +/// for specs that prefer explicit scalar quantifiers. Walks state's +/// top-level Float fields, then merges in floats from the action +/// source: SendA2a payload, CallMcp args. Action bindings override +/// state bindings on key collision. +/// +/// New specs should prefer [`record_bindings`] paired with +/// record-typed quantifiers — same contract, fewer name collisions, +/// clearer state-vs-action provenance. pub fn default_float_bindings(state: &Value, action: &Action) -> IndexMap { let mut out = IndexMap::new(); if let Some(obj) = state.as_object() { @@ -63,81 +136,107 @@ mod tests { } } - #[test] - fn pulls_top_level_floats_from_state() { - let state = json!({"current_kw": 30.0, "budget_kw": 100.0, "name": "depot"}); - let action = Action::LocalLlm { - prompt: "irrelevant".into(), + fn record_field(b: &IndexMap, rec: &str, field: &str) -> Option { + let LexValue::Record(map) = b.get(rec)? else { + return None; }; - let b = default_float_bindings(&state, &action); - assert_eq!(float(&b, "current_kw"), Some(30.0)); - assert_eq!(float(&b, "budget_kw"), Some(100.0)); - assert!(b.get("name").is_none(), "non-numeric fields skipped"); + map.get(field).cloned() } + // ---------- record_bindings ---------- + #[test] - fn pulls_top_level_floats_from_send_a2a_payload() { - let state = json!({"current_kw": 30.0}); + fn record_bindings_forwards_state_as_s() { + let state = json!({"current_kw": 30.0, "budget_kw": 100.0}); + let action = Action::LocalLlm { prompt: "p".into() }; + let b = record_bindings(&state, &action); + assert_eq!( + record_field(&b, "s", "current_kw"), + Some(LexValue::Float(30.0)) + ); + assert_eq!( + record_field(&b, "s", "budget_kw"), + Some(LexValue::Float(100.0)) + ); + } + + #[test] + fn record_bindings_forwards_send_a2a_payload_as_a() { + let state = json!({}); let action = Action::SendA2a { peer: "vehicle".into(), topic: "GrantSession".into(), payload: json!({"power_kw": 50, "charger_id": "c-1"}), }; - let b = default_float_bindings(&state, &action); - assert_eq!(float(&b, "current_kw"), Some(30.0)); - assert_eq!(float(&b, "power_kw"), Some(50.0)); - assert!(b.get("charger_id").is_none()); + let b = record_bindings(&state, &action); + assert_eq!( + record_field(&b, "a", "power_kw"), + Some(LexValue::Float(50.0)) + ); + assert_eq!( + record_field(&b, "a", "charger_id"), + Some(LexValue::Str("c-1".into())) + ); } #[test] - fn pulls_top_level_floats_from_call_mcp_args() { - let state = json!({"soc": 0.85}); + fn record_bindings_forwards_call_mcp_args_as_a() { + let state = json!({}); let action = Action::CallMcp { server: "telemetry".into(), tool: "report".into(), - args: json!({"voltage": 240.0, "label": "main"}), + args: json!({"voltage": 240}), }; - let b = default_float_bindings(&state, &action); - assert_eq!(float(&b, "soc"), Some(0.85)); - assert_eq!(float(&b, "voltage"), Some(240.0)); - assert!(b.get("label").is_none()); + let b = record_bindings(&state, &action); + assert_eq!( + record_field(&b, "a", "voltage"), + Some(LexValue::Float(240.0)) + ); } #[test] - fn action_overrides_state_on_key_collision() { - let state = json!({"power_kw": 10.0, "budget_kw": 100.0}); + fn record_bindings_for_llm_action_yields_empty_a() { + let state = json!({"k": 1.0}); + let action = Action::LocalLlm { prompt: "p".into() }; + let b = record_bindings(&state, &action); + let LexValue::Record(map) = b.get("a").unwrap() else { + panic!("expected Record for `a`"); + }; + assert!(map.is_empty(), "LLM actions carry no record-shaped data"); + } + + #[test] + fn record_bindings_non_object_state_yields_unit_s() { + let state = json!("not an object"); + let action = Action::LocalLlm { prompt: "p".into() }; + let b = record_bindings(&state, &action); + assert!(matches!(b.get("s"), Some(LexValue::Unit))); + } + + // ---------- default_float_bindings (regression) ---------- + + #[test] + fn legacy_default_float_bindings_still_works() { + let state = json!({"current_kw": 30.0}); let action = Action::SendA2a { peer: "v".into(), topic: "Grant".into(), payload: json!({"power_kw": 50.0}), }; let b = default_float_bindings(&state, &action); - // Action's power_kw shadows state's. + assert_eq!(float(&b, "current_kw"), Some(30.0)); assert_eq!(float(&b, "power_kw"), Some(50.0)); - // State-only fields still come through. - assert_eq!(float(&b, "budget_kw"), Some(100.0)); } #[test] - fn empty_state_and_non_numeric_action_yields_empty_bindings() { - let state = json!({}); + fn legacy_action_overrides_state_on_collision() { + let state = json!({"power_kw": 10.0}); let action = Action::SendA2a { - peer: "x".into(), - topic: "Y".into(), - payload: json!({"only": "strings"}), + peer: "v".into(), + topic: "G".into(), + payload: json!({"power_kw": 50.0}), }; let b = default_float_bindings(&state, &action); - assert!(b.is_empty()); - } - - #[test] - fn local_and_cloud_llm_actions_contribute_no_bindings() { - let state = json!({"k": 1.0}); - let local = Action::LocalLlm { prompt: "p".into() }; - let cloud = Action::CloudLlm { prompt: "p".into() }; - let bl = default_float_bindings(&state, &local); - let bc = default_float_bindings(&state, &cloud); - assert_eq!(bl.len(), 1); - assert_eq!(bc.len(), 1); + assert_eq!(float(&b, "power_kw"), Some(50.0)); } } diff --git a/crates/soft-agent/src/lib.rs b/crates/soft-agent/src/lib.rs index a19fd65..3dd3455 100644 --- a/crates/soft-agent/src/lib.rs +++ b/crates/soft-agent/src/lib.rs @@ -34,7 +34,7 @@ pub mod trace; pub use action::Action; pub use agent::{Agent, AgentConfig, AgentId}; -pub use bindings::default_float_bindings; +pub use bindings::{default_float_bindings, record_bindings}; pub use effect::{Effect, EffectSet}; pub use error::Error; pub use executor::{ActionExecutor, ExecError, MockExecutor}; diff --git a/crates/soft-agent/tests/deploy_specs.rs b/crates/soft-agent/tests/deploy_specs.rs index df6b722..138682f 100644 --- a/crates/soft-agent/tests/deploy_specs.rs +++ b/crates/soft-agent/tests/deploy_specs.rs @@ -2,7 +2,7 @@ //! //! Loads `agents/depot.lex` + `agents/depot.spec` straight from the //! repo (and `agents/vehicle.lex` + `agents/vehicle.spec`), wires up -//! `default_float_bindings` (the `BindingsFn` that `soft-runner` +//! `record_bindings` (the `BindingsFn` that `soft-runner` //! installs), and asserts: //! //! - the depot grants when (current + power_kw) ≤ (budget + pv); @@ -25,7 +25,7 @@ use std::path::PathBuf; use indexmap::IndexMap; use lex_bytecode::Value as LexValue; use serde_json::json; -use soft_agent::{default_float_bindings, A2aMessage, Gate, Mailbox, Runner, StepReport, Verdict}; +use soft_agent::{record_bindings, A2aMessage, Gate, Mailbox, Runner, StepReport, Verdict}; fn agents_dir() -> PathBuf { PathBuf::from(env!("CARGO_MANIFEST_DIR")) @@ -78,7 +78,7 @@ fn depot_grants_when_within_budget() { "requested_kw": 50.0, })) .gate(gate) - .bindings_fn(Box::new(default_float_bindings)) + .bindings_fn(Box::new(record_bindings)) .build() .expect("runner builds"); @@ -116,7 +116,7 @@ fn depot_denies_when_over_budget() { "requested_kw": 50.0, })) .gate(gate) - .bindings_fn(Box::new(default_float_bindings)) + .bindings_fn(Box::new(record_bindings)) .build() .expect("runner builds"); @@ -157,7 +157,7 @@ fn vehicle_dispatch_allowed_when_above_reserve() { "tried": 0, })) .gate(gate) - .bindings_fn(Box::new(default_float_bindings)) + .bindings_fn(Box::new(record_bindings)) .build() .expect("runner builds"); @@ -198,7 +198,7 @@ fn vehicle_dispatch_denied_when_below_reserve() { "tried": 0, })) .gate(gate) - .bindings_fn(Box::new(default_float_bindings)) + .bindings_fn(Box::new(record_bindings)) .build() .expect("runner builds"); @@ -223,33 +223,45 @@ fn vehicle_dispatch_denied_when_below_reserve() { } #[test] -fn depot_spec_evaluates_directly() { - // Sanity: the spec body compiles and the bindings the runner - // would build evaluate to the expected verdicts. `power_kw` is - // populated from the action's payload at gate time; here we plug - // it in manually. +fn depot_spec_evaluates_directly_with_record_bindings() { + // Sanity: the on-disk depot.spec compiles and accepts record-shaped + // `s` and `a` bindings of the kind `record_bindings` produces. Unit- + // level proof that the lex-lang 0.3 record-quantifier path works + // against our actual deploy-fleet spec. let spec_src = read_spec("depot"); let gate = Gate::from_sources(&[&spec_src], "fn _host() -> Int { 0 }").unwrap(); - let mut allow_b = IndexMap::new(); - allow_b.insert("current_kw".into(), LexValue::Float(30.0)); - allow_b.insert("power_kw".into(), LexValue::Float(50.0)); - allow_b.insert("budget_kw".into(), LexValue::Float(100.0)); - allow_b.insert("pv_kw".into(), LexValue::Float(0.0)); + let allow_b = build_depot_record_bindings(30.0, 100.0, 0.0, 50.0); assert!(matches!(gate.evaluate(&allow_b), Verdict::Allow)); - let mut deny_b = IndexMap::new(); - deny_b.insert("current_kw".into(), LexValue::Float(80.0)); - deny_b.insert("power_kw".into(), LexValue::Float(50.0)); - deny_b.insert("budget_kw".into(), LexValue::Float(100.0)); - deny_b.insert("pv_kw".into(), LexValue::Float(0.0)); + let deny_b = build_depot_record_bindings(80.0, 100.0, 0.0, 50.0); assert!(matches!(gate.evaluate(&deny_b), Verdict::Deny { .. })); } +fn build_depot_record_bindings( + current_kw: f64, + budget_kw: f64, + pv_kw: f64, + power_kw: f64, +) -> IndexMap { + let mut s = IndexMap::new(); + s.insert("current_kw".into(), LexValue::Float(current_kw)); + s.insert("budget_kw".into(), LexValue::Float(budget_kw)); + s.insert("pv_kw".into(), LexValue::Float(pv_kw)); + + let mut a = IndexMap::new(); + a.insert("power_kw".into(), LexValue::Float(power_kw)); + + let mut b = IndexMap::new(); + b.insert("s".into(), LexValue::Record(s)); + b.insert("a".into(), LexValue::Record(a)); + b +} + #[test] fn depot_grant_carries_power_kw_in_payload() { // The depot's GrantSession action embeds `power_kw` so the spec - // can check it. Without that field, `default_float_bindings` + // can check it. Without that field, `record_bindings` // wouldn't bind `power_kw` and the spec would be Inconclusive (a // soft-Deny under the runner's fail-safe policy). This test pins // the contract by exercising the gate path end-to-end and @@ -269,7 +281,7 @@ fn depot_grant_carries_power_kw_in_payload() { "requested_kw": 50.0, })) .gate(gate) - .bindings_fn(Box::new(default_float_bindings)) + .bindings_fn(Box::new(record_bindings)) .build() .expect("runner builds"); diff --git a/crates/soft-runner/src/main.rs b/crates/soft-runner/src/main.rs index b24fafe..20ceab8 100644 --- a/crates/soft-runner/src/main.rs +++ b/crates/soft-runner/src/main.rs @@ -36,7 +36,7 @@ use lex_runtime::Policy; use serde_json::Value; use soft_a2a::{A2aRoutedExecutor, A2aServer, AgentCard}; use soft_agent::{ - default_float_bindings, Gate, LexHost, Mailbox, Metrics, Runner, StepReport, DSL_PREAMBLE, + record_bindings, Gate, LexHost, Mailbox, Metrics, Runner, StepReport, DSL_PREAMBLE, }; use crate::anthropic::AnthropicCloudHandler; @@ -284,9 +284,7 @@ fn main() -> ExitCode { gate.spec_count(), spec_paths.join(", ") ); - builder = builder - .gate(gate) - .bindings_fn(Box::new(default_float_bindings)); + builder = builder.gate(gate).bindings_fn(Box::new(record_bindings)); } let metrics = Arc::new(Metrics::new(&agent_name));