AppBundle V3 State IR

State, reducer, shell, and proof from one agent-authored app contract.

Agents write bounded AppBundle JSON. ViewSpec validates interactive_state_v0, emits a pure TypeScript reducer at state_reducer.ts, checks state_replay_assertions, renders the static shell, and proves it with viewspec prove-app --with-shell.

State replaypassed

Reducergenerated

Manifestchecked

Shell hashmatched

Runtime LLMnone

Compiler-owned output

AppBundle V3 is the current flagship proof path because it binds UI and interaction together without asking an agent to hand-wire state transitions.

viewspec compile-app viewspec.app.json \
  --out app-dist \
  --target html-tailwind-app --json

viewspec prove-app --app viewspec.app.json \
  --out .viewspec-app-proof \
  --with-shell --json

Evidence Tabs

These tabs are static evidence, not a live simulator. They show the contract surface ViewSpec proves: AppBundle JSON, generated reducer, replay assertion, rendered shell, and proof report facts.

{
  "schema_version": 3,
  "resource_binding": "fixture_readonly_v0",
  "state": {
    "profile": "interactive_state_v0",
    "entries": [
      { "id": "incident_filter", "type": "string", "initial": "open" },
      { "id": "selected_incident_ids", "type": "string_list", "initial": [] }
    ],
    "mutations": [
      {
        "id": "set_filter",
        "kind": "set_value",
        "state_ref": "incident_filter",
        "payload_path": "filter"
      }
    ],
    "selectors": [
      { "id": "visible_incidents", "source": "resource_view:incidents", "where_state": "incident_filter" }
    ],
    "state_replay_assertions": [
      { "id": "filter_changes_visible_rows", "mutation_ref": "set_filter", "expect_selector_ref": "visible_incidents" }
    ]
  }
}

export type ViewSpecState = {
  incident_filter: string
  selected_incident_ids: string[]
}

export type ViewSpecAction =
  | { type: "set_filter"; payload: { filter: string } }
  | { type: "select_incident"; payload: { id: string } }

export function reduceViewSpecState(
  state: ViewSpecState,
  action: ViewSpecAction
): ViewSpecState {
  switch (action.type) {
    case "set_filter":
      return { ...state, incident_filter: action.payload.filter }
    case "select_incident":
      return { ...state, selected_incident_ids: [action.payload.id] }
    default:
      return state
  }
}

{
  "assertion_id": "filter_changes_visible_rows",
  "artifact": "state_reducer.ts",
  "reducer_export": "reduceViewSpecState",
  "initial_state": { "incident_filter": "open", "selected_incident_ids": [] },
  "action": { "type": "set_filter", "payload": { "filter": "critical" } },
  "expected_state": { "incident_filter": "critical", "selected_incident_ids": [] },
  "status": "passed"
}

target: html-tailwind-app
route_navigation: static_shell_v0
policy.network_calls: none
state_reducer_hash and state_manifest_hash: present for V3.
shell_artifact_hash: matched between compile-app output and prove-app --with-shell shell proof.
state_replay_assertions: all passed for the generated reduceViewSpecState reducer.

What this proves

State is part of the contract.

V3 proves that a bounded app contract can compile screens, local interactive state, reducer code, shell metadata, and replay results into files a reviewer can inspect.

Explicit caveats

Bounded by design.

AppBundle is local and proof-oriented. State IR is not Redux, not Zustand, not CRDT, not persistence, not backend generation, not browser-history proof, and not a deployable framework app.

State, reducer, shell, and proof from one agent-authored app contract.

Evidence Tabs

Operations Queue

Incident Detail

State is part of the contract.

Bounded by design.