std.world_model

Generated by sema doc from crates/sema-runtime/assets/stdlib/sema/world_model.sema. Import with from std.world_model import …. For a narrative introduction see std.world_model.

world_model

std.world_model — bounded deterministic and seeded transition systems.

The contract keeps model-private state separate from agent-visible observations, threads immutable clock/RNG identities through every transition, bounds steps, branches, retained trajectory records, and shrink attempts, and provides exact replay plus deterministic greedy counterexample shrinking. A model supplies two pure functions: step(State, Action) -> Transition and invariant(State) -> bool. Model calls remain explicit effects inside that supplied step function.

struct HiddenState

Fields

field	type	descriptor
identity	str
value	any

struct State

Fields

field	type	descriptor
visible	any
hidden	HiddenState
clock_id	str
rng_id	str
tick	int

struct Action

Fields

field	type	descriptor
kind	str
payload	any

struct Observation

Fields

field	type	descriptor
value	any
tick	int
clock_id	str
rng_id	str

struct Reward

Fields

field	type	descriptor
value	f64
reason	str

struct Terminal

Fields

field	type	descriptor
done	bool
reason	str

struct Transition

Fields

field	type	descriptor
before_tick	int
action	Action
state	State
observation	Observation
reward	Reward
terminal	Terminal
accepted	bool

struct Bounds

Fields

field	type	descriptor
max_steps	int
max_branches	int
max_retained_steps	int
max_shrink_attempts	int

struct Trajectory

Fields

field	type	descriptor
initial	State
state	State
transitions	list[Transition]
bounds	Bounds
exhausted	bool

struct Branch

Fields

field	type	descriptor
id	str
parent_id	str
fork_step	int
trajectory	Trajectory

struct World

Fields

field	type	descriptor
root	Trajectory
branches	list[Branch]
bounds	Bounds
exhausted	bool

struct ShrinkResult

Fields

field	type	descriptor
trajectory	Trajectory
attempts	int
minimal	bool
exhausted	bool

def bounds

def bounds(max_steps: int, max_branches: int, max_retained_steps: int, max_shrink_attempts: int) -> Bounds !{}

Parameters

name	type
max_steps	int
max_branches	int
max_retained_steps	int
max_shrink_attempts	int

Returns Bounds

Effects !{}

def state

def state(visible: any, hidden: any, hidden_id: str, clock_id: str, rng_id: str) -> State !{}

Parameters

name	type
visible	any
hidden	any
hidden_id	str
clock_id	str
rng_id	str

Returns State

Effects !{}

def action

def action(kind: str, payload: any) -> Action !{}

Parameters

name	type
kind	str
payload	any

Returns Action

Effects !{}

def reward

def reward(value: f64, reason: str) -> Reward !{}

Parameters

name	type
value	f64
reason	str

Returns Reward

Effects !{}

def terminal

def terminal(done: bool, reason: str) -> Terminal !{}

Parameters

name	type
done	bool
reason	str

Returns Terminal

Effects !{}

def public_state

def public_state(item: State)

Parameters

name	type
item	State

def next_state

def next_state(before: State, visible: any, hidden: any)

Parameters

name	type
before	State
visible	any
hidden	any

def observation

def observation(item: State, value: any)

Parameters

name	type
item	State
value	any

def leaks_hidden

def leaks_hidden(item: State, observed: Observation)

Parameters

name	type
item	State
observed	Observation

def transition

def transition(before: State, selected: Action, visible: any, hidden: any, observed: any, scored: Reward, stopped: Terminal, accepted: bool) -> Transition !{}

Parameters

name	type
before	State
selected	Action
visible	any
hidden	any
observed	any
scored	Reward
stopped	Terminal
accepted	bool

Returns Transition

Effects !{}

def stable_transition

def stable_transition(before: State, selected: Action, observed: any, scored: Reward, stopped: Terminal, accepted: bool)

Parameters

name	type
before	State
selected	Action
observed	any
scored	Reward
stopped	Terminal
accepted	bool

def same_value

def same_value(left: any, right: any)

Parameters

name	type
left	any
right	any

def validate_transition

def validate_transition(before: State, selected: Action, outcome: Transition, invariant: fn) !{}

Parameters

name	type
before	State
selected	Action
outcome	Transition
invariant	fn

Effects !{}

def start

def start(initial: State, limits: Bounds, invariant: fn) -> Trajectory !{}

Parameters

name	type
initial	State
limits	Bounds
invariant	fn

Returns Trajectory

Effects !{}

def is_terminal

def is_terminal(trace: Trajectory)

Parameters

name	type
trace	Trajectory

def copy_transitions

def copy_transitions(values: list[Transition])

Parameters

name	type
values	list[Transition]

def exhausted

def exhausted(trace: Trajectory)

Parameters

name	type
trace	Trajectory

def advance

def advance(trace: Trajectory, selected: Action, step: fn, invariant: fn) -> Trajectory !{}

Parameters

name	type
trace	Trajectory
selected	Action
step	fn
invariant	fn

Returns Trajectory

Effects !{}

def continue_actions

def continue_actions(trace: Trajectory, actions: list[Action], step: fn, invariant: fn)

Parameters

name	type
trace	Trajectory
actions	list[Action]
step	fn
invariant	fn

def run

def run(initial: State, actions: list[Action], limits: Bounds, step: fn, invariant: fn)

Parameters

name	type
initial	State
actions	list[Action]
limits	Bounds
step	fn
invariant	fn

def same_transition

def same_transition(left: Transition, right: Transition)

Parameters

name	type
left	Transition
right	Transition

def replay

def replay(trace: Trajectory, step: fn, invariant: fn) -> Trajectory !{}

Parameters

name	type
trace	Trajectory
step	fn
invariant	fn

Returns Trajectory

Effects !{}

def replay_prefix

def replay_prefix(trace: Trajectory, steps: int, step: fn, invariant: fn)

Parameters

name	type
trace	Trajectory
steps	int
step	fn
invariant	fn

def actions

def actions(trace: Trajectory)

Parameters

name	type
trace	Trajectory

def without_action

def without_action(values: list[Action], removed: int)

Parameters

name	type
values	list[Action]
removed	int

def shrink

def shrink(trace: Trajectory, step: fn, invariant: fn, fails: fn) -> ShrinkResult !{}

Parameters

name	type
trace	Trajectory
step	fn
invariant	fn
fails	fn

Returns ShrinkResult

Effects !{}

def world

def world(root: Trajectory)

Parameters

name	type
root	Trajectory

def world_tree

def world_tree(root: Trajectory) -> World !{}

Parameters

name	type
root	Trajectory

Returns World

Effects !{}

def copy_branches

def copy_branches(values: list[Branch])

Parameters

name	type
values	list[Branch]

def retained_steps

def retained_steps(item: World)

Parameters

name	type
item	World

def has_branch

def has_branch(item: World, branch_id: str)

Parameters

name	type
item	World
branch_id	str

def branch_trajectory

def branch_trajectory(item: World, branch_id: str)

Parameters

name	type
item	World
branch_id	str

def fork

def fork(item: World, parent_id: str, branch_id: str, fork_step: int, alternate: list[Action], step: fn, invariant: fn) -> World !{}

Parameters

name	type
item	World
parent_id	str
branch_id	str
fork_step	int
alternate	list[Action]
step	fn
invariant	fn

Returns World

Effects !{}

def transition_view

def transition_view(item: Transition)

Parameters

name	type
item	Transition

def trajectory_view

def trajectory_view(trace: Trajectory)

Parameters

name	type
trace	Trajectory

def project_transition

def project_transition(item: Transition) !{observe.record}

Parameters

name	type
item	Transition

Effects !{observe.record}

def project_trajectory

def project_trajectory(trace: Trajectory) -> None !{observe.record}

Parameters

name	type
trace	Trajectory

Returns None

Effects !{observe.record}

def project_replay

def project_replay(original: Trajectory, replayed: Trajectory) -> None !{observe.record}

Parameters

name	type
original	Trajectory
replayed	Trajectory

Returns None

Effects !{observe.record}

def project_world

def project_world(item: World) -> None !{observe.record}

Parameters

name	type
item	World

Returns None

Effects !{observe.record}

def project_shrink

def project_shrink(item: ShrinkResult) -> None !{observe.record}

Parameters

name	type
item	ShrinkResult

Returns None

Effects !{observe.record}