interpreter: evaluate const-expr data/elem segment offsets at instantiation

interpreter/Interpreter/Runner.lean

@@ -256,6 +256,9 @@ def runOnce (a : Args) : IO UInt32 := do
   -- imported global is unreachable; the import pre-flight above
   -- rejects any module that would need one.
   let store0 := m.runConstGlobals a.fuel (m.initialStore (α := Unit)) {}
+  -- Data/elem segments whose offset is itself a const-expr are deferred
+  -- by `initialStore`; write them now that the globals are evaluated.
+  let store0 := m.runActiveSegments a.fuel store0 {}
   match Wasm.run a.fuel m idx store0 vs.reverse with
   | .Success results _ =>
     for v in results.reverse do

interpreter/Interpreter/Testsuite/Exec.lean

@@ -723,6 +723,10 @@ def runCommand
         -- then GC element-segment item initializers into their tables.
         let store0 := m.runConstGlobals fuel store0 env
         let store0 := m.runConstElems fuel store0 env
+        -- Data/elem segments whose offset is itself a const-expr
+        -- (`global.get`, extended-const) are deferred by `initialStore`;
+        -- write them now that the globals hold their real values.
+        let store0 := m.runActiveSegments fuel store0 env
         match m.startFunc with
         | none => pure (ModuleSlot.ok m store0 env)
         | some idx =>

interpreter/Interpreter/Wasm/Decoder/Wat.lean

@@ -2331,8 +2331,9 @@ private def parseMemDecl (xs : List Sexpr) : Except Err Wasm.MemDecl := do
 
 /-- Parse a `(data ...)` body. Active segments produce `offset := some n`;
 passive segments (no offset expression) produce `offset := none`. -/
-private def parseDataSegment (memNames : Std.HashMap String Nat)
+private def parseDataSegment (ctx : Ctx)
     (xs : List Sexpr) : Except Err Wasm.DataSegment := do
+  let memNames := ctx.memNames
   -- Strip an optional segment id ($name).
   let xs := match xs with
     | .atom a :: r => if a.startsWith "$" then r else xs
@@ -2347,39 +2348,49 @@ private def parseDataSegment (memNames : Std.HashMap String Nat)
       pure ((← resolveNamed memNames "memory" mref), r)
     | r => pure ((0 : Nat), r)
   -- Extract the offset constant; passive segments have no offset form.
-  -- Non-`i32.const` offset expressions (e.g. `(global.get N)` pointing
-  -- at an imported global) are accepted with a 0 placeholder so the
-  -- module still decodes; tests that depend on the actual offset will
-  -- fail at runtime rather than at decode time.
+  -- Non-literal offset expressions (`global.get`, extended-const
+  -- arithmetic) cannot be folded at decode time — the value depends on
+  -- the store — so they are kept as a const-expr program in
+  -- `offsetExpr` (with a `some 0` active-marker placeholder in
+  -- `offset`) and evaluated at instantiation by
+  -- `Module.runActiveSegments`.
   let parsed ← match xs with
     | .list [.atom "offset", .list [.atom "i32.const", .atom n]] :: r =>
-      do .ok ((some (← parseU32 n) : Option UInt32), r)
+      do .ok ((some (← parseU32 n) : Option UInt32), ([] : Wasm.Program), r)
     | .list [.atom "i32.const", .atom n] :: r =>
-      do .ok ((some (← parseU32 n) : Option UInt32), r)
+      do .ok ((some (← parseU32 n) : Option UInt32), ([] : Wasm.Program), r)
     -- memory64: active offsets in a 64-bit memory are i64 constants. The
     -- segment offset field is 32 bits; active 64-bit segments in practice
     -- are tiny, so a genuinely huge offset is a decode error.
     | .list [.atom "offset", .list [.atom "i64.const", .atom n]] :: r =>
       do
         let v ← parseI64 n
         if v.toNat ≥ 2 ^ 32 then .error "data offset out of range"
-        else .ok ((some v.toUInt32 : Option UInt32), r)
+        else .ok ((some v.toUInt32 : Option UInt32), ([] : Wasm.Program), r)
     | .list [.atom "i64.const", .atom n] :: r =>
       do
         let v ← parseI64 n
         if v.toNat ≥ 2 ^ 32 then .error "data offset out of range"
-        else .ok ((some v.toUInt32 : Option UInt32), r)
-    | .list [.atom "offset", .list (.atom "global.get" :: _)] :: r
-    | .list (.atom "global.get" :: _) :: r =>
-      .ok ((some (0 : UInt32) : Option UInt32), r)
-    | _ => .ok ((none : Option UInt32), xs)
-  let (offset, rest) := parsed
+        else .ok ((some v.toUInt32 : Option UInt32), ([] : Wasm.Program), r)
+    -- Non-literal offset expressions (`global.get`, extended-const
+    -- arithmetic): keep the const-expr program for evaluation at
+    -- instantiation; `some 0` marks the segment active.
+    | .list (.atom "offset" :: es) :: r =>
+      do .ok ((some (0 : UInt32) : Option UInt32), (← parseInstrSeq ctx es), r)
+    -- Bare (unwrapped) non-literal offset expression, e.g.
+    -- `(data (global.get $o) "…")`.
+    | e :: r =>
+      if initExprNeedsEval e then
+        do .ok ((some (0 : UInt32) : Option UInt32), (← parseInstrSeq ctx [e]), r)
+      else .ok ((none : Option UInt32), ([] : Wasm.Program), xs)
+    | _ => .ok ((none : Option UInt32), ([] : Wasm.Program), xs)
+  let (offset, offsetExpr, rest) := parsed
   let mut bytes : List UInt8 := []
   for tok in rest do
     match tok with
     | .atom s => bytes := bytes ++ (← parseWatString s)
     | _ => .error "data segment: expected string literal(s)"
-  .ok { offset, bytes, memIdx }
+  .ok { offset, bytes, memIdx, offsetExpr }
 
 /-- Collect names declared by `(table $name ...)` forms in source order.
 Same pattern as `collectFuncNames` / `collectGlobalNames`. -/
@@ -2586,19 +2597,32 @@ private def parseElemSegment (ctx : Ctx)
     tableIdx := some idx; rest := r
   | _ => pure ()
   let mut offset : Option Nat := none
+  let mut offsetExpr : Wasm.Program := []
   match rest with
   | .list [.atom "offset", .list [.atom "i32.const", .atom n]] :: r =>
     let v ← parseNat n; offset := some v; rest := r
   | .list [.atom "offset", .list [.atom "i64.const", .atom n]] :: r =>
     -- table64: active offsets in a 64-bit table are i64 constants.
     let v ← parseI64 n; offset := some v.toNat; rest := r
-  | .list (.atom "offset" :: _) :: r =>
-    -- Other offset expressions (constant globals etc.) — not modelled.
-    offset := some 0; rest := r
+  | .list (.atom "offset" :: es) :: r =>
+    -- Non-literal offset expressions (`global.get`, extended-const
+    -- arithmetic): keep the const-expr program for evaluation at
+    -- instantiation by `Module.runActiveSegments`; `some 0` marks the
+    -- segment active.
+    offset := some 0; offsetExpr := (← parseInstrSeq ctx es); rest := r
   | .list [.atom "i32.const", .atom n] :: r =>
     let v ← parseNat n; offset := some v; rest := r
   | .list [.atom "i64.const", .atom n] :: r =>
     let v ← parseI64 n; offset := some v.toNat; rest := r
+  -- Bare (unwrapped) non-literal offset expression, e.g.
+  -- `(elem (global.get $o) $f)`. Guard against `(item …)` heads so a
+  -- passive segment's first const-expr item is never taken for an offset.
+  | e :: r =>
+    match e with
+    | .list (.atom "item" :: _) => pure ()
+    | _ =>
+      if initExprNeedsEval e then
+        offset := some 0; offsetExpr := (← parseInstrSeq ctx [e]); rest := r
   | _ => pure ()
   match rest with
   | .atom "func"      :: r => rest := r
@@ -2617,7 +2641,7 @@ private def parseElemSegment (ctx : Ctx)
     if elemRefIsGc inner then isGc := true
     rest := r
   | _ => pure ()
-  if isDeclarative then offset := none
+  if isDeclarative then offset := none; offsetExpr := []
   if isGc then
     -- Each item is a `(item <const-expr>)` (or a bare const-expr) producing
     -- one reference value; keep the program for `runConstElems`.
@@ -2626,7 +2650,7 @@ private def parseElemSegment (ctx : Ctx)
       match it with
       | .list (.atom "item" :: inner) => exprs := exprs ++ [← parseInstrSeq ctx inner]
       | other                         => exprs := exprs ++ [← parseInstrSeq ctx [other]]
-    return { tableIdx, offset, exprs }
+    return { tableIdx, offset, exprs, offsetExpr }
   let mut funcs : List (Option Nat) := []
   for it in rest do
     match it with
@@ -2647,7 +2671,7 @@ private def parseElemSegment (ctx : Ctx)
       | [.list [.atom "ref.null", _]] => funcs := funcs ++ [none]
       | _ => .error "elem: unsupported (item ...) form"
     | _ => .error "elem: unsupported entry"
-  .ok { tableIdx, offset, funcs }
+  .ok { tableIdx, offset, funcs, offsetExpr }
 
 /-- Parse the `(param …)` / `(result …)` / `(type N)` forms inside the
 `(func …)` of an `(import …)` declaration, returning `(params, results)`.
@@ -2933,7 +2957,8 @@ def parseModule (xs : List Sexpr) : Except Err Wasm.Module := do
       | none   => memDecl := some (← parseMemDecl body)
       | some _ => extraMemDecls := extraMemDecls.push (← parseMemDecl body)
     | .list (.atom "data" :: body) =>
-      dataSegs := dataSegs.push (← parseDataSegment memNames body)
+      let dctx : Ctx := { Ctx.empty with funcIds := funcIds, globalIds := globalIds, types := types, tableNames := tableNames, elemNames := elemNames, memNames := memNames, tagNames := tagNames }
+      dataSegs := dataSegs.push (← parseDataSegment dctx body)
     | .list (.atom "table" :: body) =>
       for n in inlineExportsOf body do
         tableExports := tableExports.push (n, tblImps.length + tableDecls.size)

interpreter/Interpreter/Wasm/Examples/Basic.lean

@@ -33,6 +33,7 @@ import Interpreter.Wasm.Examples.FloatOps
 import Interpreter.Wasm.Examples.Gcd
 import Interpreter.Wasm.Examples.SelectAbs
 import Interpreter.Wasm.Examples.GlobalInitExpr
+import Interpreter.Wasm.Examples.SegmentOffsetExpr
 import Interpreter.Wasm.Examples.CallIndirectSubtype
 
 /-! # Wasm.Examples.Basic

interpreter/Interpreter/Wasm/Examples/SegmentOffsetExpr.lean

@@ -0,0 +1,81 @@
+import Interpreter.Wasm.Decoder.Wat
+import Interpreter.Wasm.Wp.Tactic
+import Interpreter.Wasm.Examples.Harness
+
+/-! ## Example: const-expr data/elem segment offsets
+
+    An active data or element segment's offset is a constant expression,
+    not just a literal: wasm 1.0 permits `global.get`, and the
+    extended-const proposal adds `i32.add`/`i32.sub`/`i32.mul` (i64
+    ditto). Talos keeps such offsets as a program in
+    `DataSegment.offsetExpr` / `ElementSegment.offsetExpr`; the segment
+    is skipped by `Module.initialStore` and written at instantiation by
+    `Module.runActiveSegments`, once `Module.runConstGlobals` has put
+    the globals in place.
+
+    This module is the regression test for issue #101, where such
+    segments landed at offset 0: the data below must end up at byte 4,
+    and the table entry at slot 2, or the theorems fail the build. -/
+
+namespace Wasm
+open Wasm.Examples
+namespace SegmentOffsetExpr
+
+/-- A module whose data segment lands at `global.get $o = 4` and whose
+element segment lands at `global.get $t = 2`. `readByte4` observes the
+data placement; `callAt2` observes the element placement (it traps if
+the funcref landed at slot 0 instead). -/
+def segmentOffsetWat : String := "
+(module
+  (global $o i32 (i32.const 4))
+  (global $t i32 (i32.const 2))
+  (memory 1)
+  (data (offset (global.get $o)) \"ABCD\")
+  (table 4 funcref)
+  (elem (offset (global.get $t)) $f42)
+  (type $ri (func (result i32)))
+  (func $f42 (type $ri) (i32.const 42))
+  (func $readByte4 (export \"readByte4\") (result i32)
+    (i32.load8_u (i32.const 4)))
+  (func $callAt2 (export \"callAt2\") (result i32)
+    (call_indirect (type $ri) (i32.const 2))))
+"
+
+private def decoded : Wasm.Module := decodeOrDefault segmentOffsetWat
+
+/-- The non-literal offsets are kept as programs rather than collapsed
+to a `0` placeholder: both segments carry a non-empty `offsetExpr`. -/
+theorem decoded_segments_keep_offsetExpr :
+    ((decoded.memory.bind (·.data[0]?)).map (·.offsetExpr.isEmpty)).getD true = false
+    ∧ (decoded.elements[0]?.map (·.offsetExpr.isEmpty)).getD true = false := by
+  constructor <;> native_decide
+
+/-- The instantiated store used by the theorems below: base store, then
+global initializers, then the deferred const-expr-offset segments. -/
+private def store0 : Store Unit :=
+  let m := decoded
+  m.runActiveSegments 64 (m.runConstGlobals 64 (m.initialStore (α := Unit)) {}) {}
+
+/-- `runActiveSegments` writes the data segment at the evaluated offset:
+byte 4 holds `'A' = 65`. The issue-#101 behaviour — the segment landing
+at offset 0 — would leave byte 4 zero. -/
+theorem readByte4_returns_65 :
+    runValues 64 decoded ((decoded.findExport "readByte4").getD 0) store0 []
+      = [.i32 65] := by
+  native_decide
+
+/-- Likewise the element segment: the funcref lands in table slot 2, so
+`call_indirect` at index 2 reaches `$f42`. With the segment at slot 0
+this call trapped on a null table entry. -/
+theorem callAt2_returns_42 :
+    runValues 64 decoded ((decoded.findExport "callAt2").getD 0) store0 []
+      = [.i32 42] := by
+  native_decide
+
+/-- And nothing leaked to the old placeholder location: byte 0 of the
+memory is still zero (the segment was *moved*, not duplicated). -/
+theorem byte0_still_zero : store0.mem.read8 0 = 0 := by
+  native_decide
+
+end SegmentOffsetExpr
+end Wasm

interpreter/Interpreter/Wasm/Semantics.lean

@@ -2277,7 +2277,9 @@ def Module.runConstElems (fuel : Nat) (m : Module) (st : Store α)
   for seg in m.elements do
     match seg.tableIdx, seg.offset with
     | some ti, some off =>
-      if !seg.exprs.isEmpty then
+      -- Segments whose offset is itself a pending const-expr are written
+      -- by `runActiveSegments` (which knows the real offset) instead.
+      if !seg.exprs.isEmpty && seg.offsetExpr.isEmpty then
         let mut i := 0
         for e in seg.exprs do
           match exec fuel m st {} e env with
@@ -2292,4 +2294,71 @@ def Module.runConstElems (fuel : Nat) (m : Module) (st : Store α)
     | _, _ => pure ()
   return st
 
+/-- Write the active data/element segments whose offset is a constant
+expression that could not be folded at decode time (`global.get` of an
+imported global, extended-const arithmetic). `Module.initialStore` skips
+these segments (their offset depends on the store); this pass evaluates
+each `offsetExpr` against the current store and writes the segment at
+the computed offset. Runs after `runConstGlobals` so the offsets see the
+evaluated (and imported) globals. -/
+def Module.runActiveSegments (fuel : Nat) (m : Module) (st : Store α)
+    (env : HostEnv α := {}) : Store α := Id.run do
+  let mut st := st
+  -- Evaluate one offset const-expr to a byte/element offset. `i64`
+  -- results come from memory64/table64 modules.
+  let evalOffset (st : Store α) (prog : Program) : Option Nat :=
+    match exec fuel m st {} prog env with
+    | .Fallthrough _ s' =>
+      match s'.values with
+      | .i32 v :: _ => some v.toNat
+      | .i64 v :: _ => some v.toNat
+      | _           => none
+    | _ => none
+  -- Active data segments with a pending offset expression. Segments live
+  -- in one global, source-ordered list (memory 0's `data`), routed to
+  -- their memory by `DataSegment.memIdx`.
+  let segs := match m.memory with
+    | some decl => decl.data
+    | none      => []
+  for seg in segs do
+    if seg.offset.isSome && !seg.offsetExpr.isEmpty then
+      match evalOffset st seg.offsetExpr with
+      | some off =>
+        if seg.memIdx = 0 then
+          st := { st with mem := st.mem.writeBytes off seg.bytes }
+        else
+          match st.extraMems[seg.memIdx - 1]? with
+          | some mem0 =>
+            let mems := st.extraMems.set (seg.memIdx - 1) (mem0.writeBytes off seg.bytes)
+            st := { st with extraMems := mems }
+          | none => pure ()
+      | none => pure ()
+  -- Active element segments with a pending offset expression.
+  for seg in m.elements do
+    match seg.tableIdx, seg.offset with
+    | some ti, some _ =>
+      if !seg.offsetExpr.isEmpty then
+        match evalOffset st seg.offsetExpr, st.tables[ti]? with
+        | some off, some tbl =>
+          if seg.exprs.isEmpty then
+            let tbls := st.tables.set ti (listWriteAt tbl off (seg.funcs.map Value.funcref))
+            st := { st with tables := tbls }
+          else
+            -- GC const-expr items, as in `runConstElems`, but at the
+            -- evaluated offset.
+            let mut i := 0
+            for e in seg.exprs do
+              match exec fuel m st {} e env with
+              | .Fallthrough st' s' =>
+                st := st'
+                match s'.values, st'.tables[ti]? with
+                | v :: _, some tbl' =>
+                  st := { st' with tables := st'.tables.set ti (tbl'.set (off + i) v) }
+                | _, _ => pure ()
+              | _ => pure ()
+              i := i + 1
+        | _, _ => pure ()
+    | _, _ => pure ()
+  return st
+
 end Wasm