Semantic Closure — WASM Demo (`add1`)

← index

This page runs a tiny, proof-traceable C artifact fully in the browser (no backend). The WebAssembly module is compiled from RESEARCHER_BUNDLE/artifacts/compiler/c/add1_wasm.c, derived from the Lean→LambdaIR→MiniC→C extraction demo (closing_the_loop_bundle_demo).

Run

Input (signed 64-bit):

Output: loading…

Note: WASM i64 values are exposed to JS as BigInt.

Proof Mapping

The demo’s semantics-level justification lives in the ClosingTheLoop “λ-calculus bridge”:

HeytingLean.ClosingTheLoop.Semantics.LambdaIRBridge
LambdaIRBridge.eval_beta (β-law for evaluation)

theorem eval_beta … :
  eval ((lam body) · arg) ρ =
    eval body (extendEnv ρ (eval arg ρ)) := by
  rfl

Extraction artifacts (same function across stages):

add1.lambdair.txt
add1.minic.txt
add1.c (native demo with main)
add1_wasm.c (WASM-export-only)

WASM Payload

For offline viewing, the WASM bytes are embedded as base64 in: wasm/add1_wasm_b64.js.

Exports:
  - add1(i64) → i64

Semantic Closure — WASM Demo (add1)

Run

Proof Mapping

WASM Payload

Semantic Closure — WASM Demo (`add1`)