inspect-wasm-artifact and the WABT provider

You wrote capture/fixtures/wasm/ledger.wat by hand, with the same four functions as ledger.c, and assembled it to ledger.wasm with wat2wasm. You ask rea 6.7.0 to inspect the module, on the CLI and over MCP, and both entry points return the same Evidence record. When you finish this section, you can set up the WABT provider and read the record. You can also say what the record does not prove.

Setup

WebAssembly is not a native target. open_binary on a module returns target_unavailable with the constraint wasm_requires_static_inspection, and the error names the inspect_wasm_artifact call to make. The tool needs three WABT programs that you install yourself. Set REA_WABT_BIN_DIRECTORY to the absolute directory that holds wasm-validate, wasm-objdump, and wasm2wat. The tool is available only when that variable is absolute, and binary_session reports that availability.

REA_WABT_BIN_DIRECTORY=/opt/homebrew/bin
$ /opt/homebrew/bin/wasm-validate --version
1.0.42
[exit 0]
$ /opt/homebrew/bin/wasm-objdump --version
1.0.42
[exit 0]
$ /opt/homebrew/bin/wasm2wat --version
1.0.42
[exit 0]

The command and the record

The CLI command is rea inspect-wasm-artifact PATH. In the capture it exited 0 after about two seconds and printed one Evidence record.

$ rea inspect-wasm-artifact fixtures/wasm/ledger.wasm --format json
[exit 0] (… s) -> 16-inspect-wasm-artifact.json

{
  "evidence_id": "ev_3a09e4b0…",
  "subject": {
    "name": "ledger.wasm",
    "digest": {
      "sha256": "699f6ff7…"
    },
    "local_path": "$CAPTURE/fixtures/wasm/ledger.wasm",
    "format": "file",
    "architecture": null
  },
  "provider": {
    "id": "wabt-artifact",
    "name": "REA WABT artifact adapter",
    "version": "wabt@1.0.42"
  },
  "analysis_profile": null,
  "predicate_type": "rea.analysis",
  "operation": "inspect_wasm_artifact",
  "parameters": {
    "path": "$CAPTURE/fixtures/wasm/ledger.wasm",
    "glue_paths": [],
    "candidate_paths": []
  },

The subject format is file and the architecture is null, because no native format applies. The provider version names the WABT release. The record is observed, with shipped-artifact as its authority, because the bytes on disk are the source. The two empty arrays are optional inputs. glue_paths names JavaScript files whose .wasm string literals rea links to candidate modules, and candidate_paths names those modules.

What rea ran

rea copies the module into a private workspace as a read-only module.wasm. It then runs three programs from the directory that REA_WABT_BIN_DIRECTORY names. Each program must print exactly 1.0.42 as its version. If one does not, rea does not run it. The tool_profile records what ran.

"tool_profile": {
  "source": "https://github.com/WebAssembly/wabt",
  "release": "1.0.42",
  …
  "commands": [
    {
      "tool": "wasm-validate",
      "path": "/opt/homebrew/Cellar/wabt/1.0.42_1/bin/wasm-validate",
      "sha256": "99a52c78…",
      "version_banner": "1.0.42\n",
      "arguments": [
        "--enable-all",
        "module.wasm"
      ]
    },
    …
  ],
  "timeout_ms": 30000,
  "output_budget_bytes": 33554432
},

The limits are 8 MiB of input, 30 s for each program, and 32 MiB of output.

rea checks the digest of the copy before and after each program. It also checks the digest of each program again after the command. A digest identifies the bytes of a program. It does not prove who published the program.

Sections

The sections array holds the seven sections with their byte ranges and the count of entries in each.

"artifact": {
  "path": "$CAPTURE/fixtures/wasm/ledger.wasm",
  "sha256": "699f6ff7…",
  "bytes": 290
},
"validation": "valid",
"sections": [
  {
    "kind": "Type",
    "start": 10,
    "end": 26,
    "bytes": 16,
    "description": "count: 3"
  },
  {
    "kind": "Import",
    "start": 28,
    "end": 39,
    "bytes": 11,
    "description": "count: 1"
  },
  …
  {
    "kind": "Data",
    "start": 273,
    "end": 290,
    "bytes": 17,
    "description": "count: 1"
  }
],

The file is 290 bytes. Eight bytes of magic and version come first. Each section starts with a one-byte id and a length, and the payload follows. The Type payload therefore starts at offset 0x0a, which is 10. The data segment holds the five grade labels at address 1024, two bytes apart.

The typed interface

The record holds the imports and exports two times. The imports and exports arrays keep the exact WAT forms. The interface entries add the direction, the index, and a resolved signature for each one.

"interface": {
  "state": "complete",
  "entries": [
    {
      "direction": "import",
      "module": "env",
      "name": "log",
      "kind": "func",
      "index": 0,
      "signature": {
        "kind": "func",
        "params": [
          "i32"
        ],
        "results": []
      },
      "wat_form": "(import \"env\" \"log\" (func (;0;) (type 0)))",
      "issue": null
    },
    …
    {
      "direction": "export",
      "module": null,
      "name": "percent_change",
      "kind": "func",
      "index": 1,
      "signature": {
        "kind": "func",
        "params": [
          "i32",
          "i32"
        ],
        "results": [
          "i32"
        ]
      },
      "wat_form": "(export \"percent_change\" (func 1))",
      "issue": null
    },
    …

percent_change takes two i32 values and returns one, the same shape as the C function. The import env.log is function 0, so the four functions of the module are 1 to 4. A second tool, compare_wasm_interfaces, reads two of these records and reports each import and export as added, removed, changed, or unchanged. It reads no files and runs no WABT program.

The WAT

The wat field holds the text that wasm2wat printed, its SHA-256 37eab56a…, and the representation decoded-wat. The body of percent_change is the C function in stack form. It tests the first parameter for zero. It then pushes 0, or it computes the subtraction, the multiplication by 100, and the signed division.

  (func (;1;) (type 1) (param i32 i32) (result i32)
    local.get 0
    i32.eqz
    if (result i32)  ;; label = @1
      i32.const 0
    else
      local.get 1
      local.get 0
      i32.sub
      i32.const 100
      i32.mul
      local.get 0
      i32.div_s
    end)

Two things in the text form echo Part 4. The grade body is a br_table with twelve targets, the WebAssembly form of the jump table that clang built for the same switch in ledger-x86_64-O1.o. The grade_label body calls function 2, then function 0, which is the imported env.log. It then adds twice the grade to 1024, the address of the data segment, two bytes per label. You can read that from the WAT without a decompiler, because the module has no stripped symbols and no relocations.

Limitations

The record has everything Part 5 described: an evidence_id, a confidence, an authority, and five limitations. The record does not decompile the functions. It gives the WAT text, and the reading of that text is your work.

"limitations": [
  "WAT is a decoded representation, not original source or proof of runtime behavior. Custom annotations may retain payloads, but WAT does not establish original binary layout or round-trip byte identity. Original bytes and objdump output remain authoritative.",
  "Imports and exports retain exact top-level WABT WAT forms. Names remain escaped producer text; unescaped objdump display names are not parsed as unambiguous identifiers.",
  "JavaScript references are AST-observed static literals only. Candidate matches are associations, not proven data flow, URL-to-file identity or runtime loading. Computed references and aliases are not resolved.",
  "No target execution or implicit fetch. WABT tools are trusted caller-supplied executables; SHA-256 identifies their bytes, not publisher authenticity. No OS memory sandbox is claimed.",
  "Each subprocess has a 30-second deadline and 32 MiB combined output budget. Oversized output fails instead of producing truncated success."
],

The first limitation says that the WAT is a decoded representation. The WAT does not show the original source, and it does not prove runtime behaviour. The record is observed for the bytes and the tool output only. The fields runtime_execution and network_fetch both read not-performed, because rea never runs the module.

Over MCP

Over MCP the tool is inspect_wasm_artifact with the same path. Step 24 of the session returned ok after 404 ms. The reply is a tool result. Its structuredContent is the same Evidence record, with the same id ev_3a09e4b0…. Its _meta carries the untrusted-content marker of Section 8.1.

"result": {
  "_meta": {
    "provenance": {
      "untrusted_content": true,
      "source": "analysis_target"
    }
  },
  …
  "structuredContent": {
    "evidence_id": "ev_3a09e4b0…",

The session retains the record, so export_evidence_bundle writes it to a bundle with the other records. For a large module, pass detail: "summary" on the first call. rea then keeps the complete record. It returns counts, the validation result, and the WAT identity, without the WAT text. You read pages of the full record with inspect_analysis_view.

A cross-check with wabt

The capture also ran wasm-objdump -h -x on the module without rea, in 16-wabt.txt. The section table there has the same seven rows as the headers text in the record. Type starts at 0x0000000a, and Data ends at 0x00000122, which is 290. The offsets agree with sections. Figure 6.2 draws the path from the two entry points to the one record.