diff --git a/src/concolic/concolic.ml b/src/concolic/concolic.ml
index 3889fc3dd..1be1265d7 100644
--- a/src/concolic/concolic.ml
+++ b/src/concolic/concolic.ml
@@ -122,14 +122,14 @@ module P = struct
       let open Choice in
       let+ a = Choice.select_i32 a in
       { concrete = f_c m.concrete a
-      ; symbolic = f_s m.symbolic (Symbolic_value.const_i32 a)
+      ; symbolic = f_s m.symbolic (S.address_i32 a)
       }
 
     let with_concrete_store m a f_c f_s v =
       let open Choice in
       let+ addr = Choice.select_i32 a in
       f_c m.concrete ~addr v.concrete;
-      f_s m.symbolic ~addr:(Symbolic_value.const_i32 addr) v.symbolic
+      f_s m.symbolic ~addr:(S.address_i32 addr) v.symbolic
 
     let load_8_s m a = with_concrete m a C.load_8_s S.load_8_s
 
diff --git a/src/dune b/src/dune
index 4fa1fca25..ec98f73e5 100644
--- a/src/dune
+++ b/src/dune
@@ -64,6 +64,9 @@
   symbolic_choice_minimalist
   symbolic_global
   symbolic_memory
+  symbolic_memory_backend
+  symbolic_memory_choice
+  symbolic_memory_intf
   symbolic_table
   symbolic_value
   symbolic_wasm_ffi
diff --git a/src/symbolic/symbolic.ml b/src/symbolic/symbolic.ml
index 8b64f67e9..875e3bb46 100644
--- a/src/symbolic/symbolic.ml
+++ b/src/symbolic/symbolic.ml
@@ -73,7 +73,7 @@ struct
         Symbolic_value.const_i32 v
 
     let check_within_bounds m a =
-      match check_within_bounds m a with
+      match is_within_bounds m a with
       | Error t -> Choice.trap t
       | Ok (cond, ptr) ->
         let open Choice in
diff --git a/src/symbolic/symbolic_memory.ml b/src/symbolic/symbolic_memory.ml
index dca85d11c..c5f51e6a3 100644
--- a/src/symbolic/symbolic_memory.ml
+++ b/src/symbolic/symbolic_memory.ml
@@ -2,202 +2,119 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-module Value = Symbolic_value
 module Expr = Smtml.Expr
-module Ty = Smtml.Ty
+module Value = Symbolic_value
 open Expr
 
 let page_size = Symbolic_value.const_i32 65_536l
 
-type t =
-  { data : (Int32.t, Value.int32) Hashtbl.t
-  ; parent : t option
-  ; mutable size : Value.int32
-  ; chunks : (Int32.t, Value.int32) Hashtbl.t
-  }
-
-let create size =
-  { data = Hashtbl.create 128
-  ; parent = None
-  ; size = Value.const_i32 size
-  ; chunks = Hashtbl.create 16
-  }
-
-let i32 v =
-  match view v with
-  | Val (Num (I32 i)) -> i
-  | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v
-
-let grow m delta =
-  let old_size = Value.I32.mul m.size page_size in
-  let new_size = Value.I32.(div (add old_size delta) page_size) in
-  m.size <-
-    Value.Bool.select_expr
-      (Value.I32.gt new_size m.size)
-      ~if_true:new_size ~if_false:m.size
-
-let size { size; _ } = Value.I32.mul size page_size
-
-let size_in_pages { size; _ } = size
-
-let fill _ = assert false
-
-let blit _ = assert false
-
-let blit_string m str ~src ~dst ~len =
-  (* This function is only used in memory init so everything will be concrete *)
-  let str_len = String.length str in
-  let mem_len = Int32.(to_int (i32 m.size) * to_int (i32 page_size)) in
-  let src = Int32.to_int @@ i32 src in
-  let dst = Int32.to_int @@ i32 dst in
-  let len = Int32.to_int @@ i32 len in
-  if src < 0 || dst < 0 || len < 0 || src + len > str_len || dst + len > mem_len
-  then Value.Bool.const true
-  else begin
-    for i = 0 to len - 1 do
-      let byte = Char.code @@ String.get str (src + i) in
-      let dst = Int32.of_int (dst + i) in
-      Hashtbl.replace m.data dst (make (Val (Num (I8 byte))))
-    done;
-    Value.Bool.const false
-  end
-
-let clone m =
-  { data = Hashtbl.create 16
-  ; parent = Some m
-  ; size = m.size
-  ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *)
-  }
-
-let rec load_byte { parent; data; _ } a =
-  try Hashtbl.find data a
-  with Not_found -> (
-    match parent with
-    | None -> make (Val (Num (I8 0)))
-    | Some parent -> load_byte parent a )
-
-(* TODO: don't rebuild so many values it generates unecessary hc lookups *)
-let merge_extracts (e1, h, m1) (e2, m2, l) =
-  let ty = Expr.ty e1 in
-  if m1 = m2 && Expr.equal e1 e2 then
-    if h - l = Ty.size ty then e1 else make (Extract (e1, h, l))
-  else make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l))))
-
-let concat ~msb ~lsb offset =
-  assert (offset > 0 && offset <= 8);
-  match (view msb, view lsb) with
-  | Val (Num (I8 i1)), Val (Num (I8 i2)) ->
-    Value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
-  | Val (Num (I8 i1)), Val (Num (I32 i2)) ->
-    let offset = offset * 8 in
-    if offset < 32 then
-      Value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2)
-    else
-      let i1' = Int64.of_int i1 in
-      let i2' = Int64.of_int32 i2 in
-      Value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
-  | Val (Num (I8 i1)), Val (Num (I64 i2)) ->
-    let offset = Int64.of_int (offset * 8) in
-    Value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
-  | Extract (e1, h, m1), Extract (e2, m2, l) ->
-    merge_extracts (e1, h, m1) (e2, m2, l)
-  | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) ->
-    make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))
-  | _ -> make (Concat (msb, lsb))
-
-let loadn m a n =
-  let rec loop addr size i acc =
-    if i = size then acc
-    else
-      let addr' = Int32.(add addr (of_int i)) in
-      let byte = load_byte m addr' in
-      loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
-  in
-  let v0 = load_byte m a in
-  loop a n 1 v0
-
-let load_8_s m a =
-  let v = loadn m (i32 a) 1 in
-  match view v with
-  | Val (Num (I8 i8)) -> Value.const_i32 (Int32.extend_s 8 (Int32.of_int i8))
-  | _ -> cvtop (Ty_bitv 32) (Sign_extend 24) v
-
-let load_8_u m a =
-  let v = loadn m (i32 a) 1 in
-  match view v with
-  | Val (Num (I8 i)) -> Value.const_i32 (Int32.of_int i)
-  | _ -> cvtop (Ty_bitv 32) (Zero_extend 24) v
-
-let load_16_s m a =
-  let v = loadn m (i32 a) 2 in
-  match view v with
-  | Val (Num (I32 i16)) -> Value.const_i32 (Int32.extend_s 16 i16)
-  | _ -> cvtop (Ty_bitv 32) (Sign_extend 16) v
-
-let load_16_u m a =
-  let v = loadn m (i32 a) 2 in
-  match view v with
-  | Val (Num (I32 _)) -> v
-  | _ -> cvtop (Ty_bitv 32) (Zero_extend 16) v
-
-let load_32 m a = loadn m (i32 a) 4
-
-let load_64 m a = loadn m (i32 a) 8
-
-let extract v pos =
-  match view v with
-  | Val (Num (I32 i)) ->
-    let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
-    value (Num (I8 i'))
-  | Val (Num (I64 i)) ->
-    let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
-    value (Num (I8 i'))
-  | Cvtop (_, Zero_extend 24, ({ node = Symbol _; _ } as sym))
-  | Cvtop (_, Sign_extend 24, ({ node = Symbol _; _ } as sym))
-    when Smtml.Ty.equal (Ty_bitv 8) (ty sym) ->
-    sym
-  | _ -> make (Extract (v, pos + 1, pos))
-
-let storen m ~addr v n =
-  let a0 = i32 addr in
-  for i = 0 to n - 1 do
-    let addr' = Int32.add a0 (Int32.of_int i) in
-    let v' = extract v i in
-    Hashtbl.replace m.data addr' v'
-  done
-
-let store_8 m ~addr v = storen m ~addr v 1
-
-let store_16 m ~addr v = storen m ~addr v 2
-
-let store_32 m ~addr v = storen m ~addr v 4
-
-let store_64 m ~addr v = storen m ~addr v 8
-
-let get_limit_max _m = None (* TODO *)
-
-let check_within_bounds m a =
-  match view a with
-  | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a)
-  | Ptr { base; offset } -> (
-    match Hashtbl.find m.chunks base with
-    | exception Not_found -> Error Trap.Memory_leak_use_after_free
-    | size ->
-      let ptr = Int32.add base (i32 offset) in
-      let upper_bound =
-        Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size))
-      in
-      Ok
-        ( Value.Bool.(or_ (const (Int32.lt ptr base)) upper_bound)
-        , Value.const_i32 ptr ) )
-  | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a
-
-let free m base =
-  if not @@ Hashtbl.mem m.chunks base then
-    Fmt.failwith "Memory leak double free";
-  Hashtbl.remove m.chunks base
-
-let replace_size m base size = Hashtbl.replace m.chunks base size
+module Make (Backend : Symbolic_memory_intf.M) = struct
+  type t =
+    { data : Backend.t
+    ; mutable size : Value.int32
+    }
+
+  type address = Backend.address
+
+  let create size = { data = Backend.create (); size = Value.const_i32 size }
+
+  let ptr p = Backend.ptr p
+
+  let address a = Backend.address a
+
+  let address_i32 a = Backend.address_i32 a
+
+  let i32 v =
+    match view v with
+    | Val (Num (I32 i)) -> i
+    | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v
+
+  let grow m delta =
+    let old_size = Value.I32.mul m.size page_size in
+    let new_size = Value.I32.(div (add old_size delta) page_size) in
+    m.size <-
+      Value.Bool.select_expr
+        (Value.I32.gt new_size m.size)
+        ~if_true:new_size ~if_false:m.size
+
+  let size { size; _ } = Value.I32.mul size page_size
+
+  let size_in_pages { size; _ } = size
+
+  let fill _ = assert false
+
+  let blit _ = assert false
+
+  let blit_string m str ~src ~dst ~len =
+    (* This function is only used in memory init so everything will be concrete *)
+    let str_len = String.length str in
+    let mem_len = Int32.(to_int (i32 m.size) * to_int (i32 page_size)) in
+    let src = Int32.to_int @@ i32 src in
+    let dst = Int32.to_int @@ i32 dst in
+    let len = Int32.to_int @@ i32 len in
+    if
+      src < 0 || dst < 0 || len < 0
+      || src + len > str_len
+      || dst + len > mem_len
+    then Value.Bool.const true
+    else begin
+      for i = 0 to len - 1 do
+        let byte = Char.code @@ String.get str (src + i) in
+        let dst = Backend.address_i32 (Int32.of_int (dst + i)) in
+        Backend.storen m.data dst (value (Num (I8 byte))) 1
+      done;
+      Value.Bool.const false
+    end
+
+  let clone m = { data = Backend.clone m.data; size = m.size }
+
+  let load_8_s m a =
+    let v = Backend.loadn m.data a 1 in
+    match view v with
+    | Val (Num (I8 i8)) -> Value.const_i32 (Int32.extend_s 8 (Int32.of_int i8))
+    | _ -> cvtop (Ty_bitv 32) (Sign_extend 24) v
+
+  let load_8_u m a =
+    let v = Backend.loadn m.data a 1 in
+    match view v with
+    | Val (Num (I8 i)) -> Value.const_i32 (Int32.of_int i)
+    | _ -> cvtop (Ty_bitv 32) (Zero_extend 24) v
+
+  let load_16_s m a =
+    let v = Backend.loadn m.data a 2 in
+    match view v with
+    | Val (Num (I32 i16)) -> Value.const_i32 (Int32.extend_s 16 i16)
+    | _ -> cvtop (Ty_bitv 32) (Sign_extend 16) v
+
+  let load_16_u m a =
+    let v = Backend.loadn m.data a 2 in
+    match view v with
+    | Val (Num (I32 _)) -> v
+    | _ -> cvtop (Ty_bitv 32) (Zero_extend 16) v
+
+  let load_32 m a = Backend.loadn m.data a 4
+
+  let load_64 m a = Backend.loadn m.data a 8
+
+  let store_8 m ~addr v = Backend.storen m.data addr v 1
+
+  let store_16 m ~addr v = Backend.storen m.data addr v 2
+
+  let store_32 m ~addr v = Backend.storen m.data addr v 4
+
+  let store_64 m ~addr v = Backend.storen m.data addr v 8
+
+  let get_limit_max _m = None (* TODO *)
+
+  let is_within_bounds m a = Backend.is_within_bounds m.data a
+
+  let free m ptr = Backend.free m.data ptr
+
+  let realloc m ptr size = Backend.realloc m.data ptr size
+end
+
+module Backend = Symbolic_memory_backend.Make (Symbolic_memory_choice)
+include Make (Backend)
 
 module ITbl = Hashtbl.Make (struct
   include Int
diff --git a/src/symbolic/symbolic_memory.mli b/src/symbolic/symbolic_memory.mli
index 276272885..629a8dd9f 100644
--- a/src/symbolic/symbolic_memory.mli
+++ b/src/symbolic/symbolic_memory.mli
@@ -2,70 +2,5 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-type t
-
-type collection
-
-val init : unit -> collection
-
-val clone : collection -> collection
-
-val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
-
-val check_within_bounds :
-  t -> Smtml.Expr.t -> (Smtml.Expr.t * Symbolic_value.int32, Trap.t) result
-
-val replace_size : t -> Int32.t -> Smtml.Expr.t -> unit
-
-val free : t -> Int32.t -> unit
-
-val load_8_s : t -> Smtml.Expr.t -> Symbolic_value.int32
-
-val load_8_u : t -> Smtml.Expr.t -> Symbolic_value.int32
-
-val load_16_s : t -> Smtml.Expr.t -> Symbolic_value.int32
-
-val load_16_u : t -> Smtml.Expr.t -> Symbolic_value.int32
-
-val load_32 : t -> Smtml.Expr.t -> Symbolic_value.int32
-
-val load_64 : t -> Smtml.Expr.t -> Symbolic_value.int32
-
-val store_8 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit
-
-val store_16 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit
-
-val store_32 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit
-
-val store_64 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit
-
-val grow : t -> Smtml.Expr.t -> unit
-
-val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
-
-val blit :
-  t -> src:Smtml.Expr.t -> dst:Smtml.Expr.t -> len:Smtml.Expr.t -> Smtml.Expr.t
-
-val blit_string :
-     t
-  -> string
-  -> src:Smtml.Expr.t
-  -> dst:Smtml.Expr.t
-  -> len:Smtml.Expr.t
-  -> Smtml.Expr.t
-
-val size : t -> Smtml.Expr.t
-
-val size_in_pages : t -> Smtml.Expr.t
-
-val get_limit_max : t -> Smtml.Expr.t option
-
-module ITbl : sig
-  type 'a t
-
-  type key
-
-  val iter : (key -> 'a -> unit) -> 'a t -> unit
-end
-
-val iter : (t ITbl.t -> unit) -> collection -> unit
+(** @inline *)
+include Symbolic_memory_intf.S
diff --git a/src/symbolic/symbolic_memory_backend.ml b/src/symbolic/symbolic_memory_backend.ml
new file mode 100644
index 000000000..220cdae78
--- /dev/null
+++ b/src/symbolic/symbolic_memory_backend.ml
@@ -0,0 +1,127 @@
+open Smtml.Expr
+module Expr = Smtml.Expr
+module Value = Symbolic_value
+
+module Make (_ : Choice_intf.Base) : Symbolic_memory_intf.M = struct
+  type address = Int32.t
+
+  type t =
+    { data : (address, Value.int32) Hashtbl.t
+    ; parent : t option
+    ; chunks : (address, Value.int32) Hashtbl.t
+    }
+
+  let create () =
+    { data = Hashtbl.create 128; parent = None; chunks = Hashtbl.create 16 }
+
+  let clone m =
+    { data = Hashtbl.create 16
+    ; parent = Some m
+    ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *)
+    }
+
+  let address v =
+    match view v with
+    | Val (Num (I32 i)) -> i
+    | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v
+
+  let ptr v =
+    match view v with
+    | Ptr { base; _ } -> base
+    | _ -> Log.err {|free: cannot fetch pointer base of "%a"|} Expr.pp v
+
+  let address_i32 i = i
+
+  let rec load_byte { parent; data; _ } a =
+    try Hashtbl.find data a
+    with Not_found -> (
+      match parent with
+      | None -> make (Val (Num (I8 0)))
+      | Some parent -> load_byte parent a )
+
+  (* TODO: don't rebuild so many values it generates unecessary hc lookups *)
+  let merge_extracts (e1, h, m1) (e2, m2, l) =
+    let ty = Expr.ty e1 in
+    if m1 = m2 && Expr.equal e1 e2 then
+      if h - l = Smtml.Ty.size ty then e1 else make (Extract (e1, h, l))
+    else make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l))))
+
+  let concat ~msb ~lsb offset =
+    assert (offset > 0 && offset <= 8);
+    match (view msb, view lsb) with
+    | Val (Num (I8 i1)), Val (Num (I8 i2)) ->
+      Value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
+    | Val (Num (I8 i1)), Val (Num (I32 i2)) ->
+      let offset = offset * 8 in
+      if offset < 32 then
+        Value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2)
+      else
+        let i1' = Int64.of_int i1 in
+        let i2' = Int64.of_int32 i2 in
+        Value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2')
+    | Val (Num (I8 i1)), Val (Num (I64 i2)) ->
+      let offset = Int64.of_int (offset * 8) in
+      Value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
+    | Extract (e1, h, m1), Extract (e2, m2, l) ->
+      merge_extracts (e1, h, m1) (e2, m2, l)
+    | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) ->
+      make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))
+    | _ -> make (Concat (msb, lsb))
+
+  let loadn m a n =
+    let rec loop addr size i acc =
+      if i = size then acc
+      else
+        let addr' = Int32.(add addr (of_int i)) in
+        let byte = load_byte m addr' in
+        loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc)
+    in
+    let v0 = load_byte m a in
+    loop a n 1 v0
+
+  let extract v pos =
+    match view v with
+    | Val (Num (I8 _)) -> v
+    | Val (Num (I32 i)) ->
+      let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
+      value (Num (I8 i'))
+    | Val (Num (I64 i)) ->
+      let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
+      value (Num (I8 i'))
+    | Cvtop (_, Zero_extend 24, ({ node = Symbol _; _ } as sym))
+    | Cvtop (_, Sign_extend 24, ({ node = Symbol _; _ } as sym))
+      when Smtml.Ty.equal (Ty_bitv 8) (ty sym) ->
+      sym
+    | _ -> make (Extract (v, pos + 1, pos))
+
+  let storen m addr v n =
+    for i = 0 to n - 1 do
+      let addr' = Int32.add addr (Int32.of_int i) in
+      let v' = extract v i in
+      Hashtbl.replace m.data addr' v'
+    done
+
+  let is_within_bounds m a =
+    match view a with
+    | Val (Num (I32 a)) -> Ok (Value.Bool.const false, a)
+    | Ptr { base; offset } -> (
+      match Hashtbl.find m.chunks base with
+      | exception Not_found -> Error Trap.Memory_leak_use_after_free
+      | size ->
+        let ptr = Int32.add base (address offset) in
+        let upper_bound =
+          Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size))
+        in
+        Ok (Value.Bool.(or_ (const (Int32.lt ptr base)) upper_bound), ptr) )
+    | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a
+
+  let free m ptr =
+    if not @@ Hashtbl.mem m.chunks ptr then
+      Error Trap.Memory_leak_use_after_free
+      (* failwith "Memory leak double free"; *)
+    else Ok (Hashtbl.remove m.chunks ptr)
+
+  let realloc m ptr size =
+    Hashtbl.replace m.chunks ptr size;
+    Expr.ptr ptr (Symbolic_value.const_i32 0l)
+end
diff --git a/src/symbolic/symbolic_memory_choice.ml b/src/symbolic/symbolic_memory_choice.ml
new file mode 100644
index 000000000..9df22e676
--- /dev/null
+++ b/src/symbolic/symbolic_memory_choice.ml
@@ -0,0 +1,19 @@
+module V = Symbolic_value
+
+type 'a t = 'a
+
+let return a = a
+
+let bind a k = k a
+
+let ( let* ) = bind
+
+let map a k = k a
+
+let ( let+ ) = map
+
+let select _ = assert false
+
+let select_i32 _ = assert false
+
+let trap _ = assert false
diff --git a/src/symbolic/symbolic_memory_intf.ml b/src/symbolic/symbolic_memory_intf.ml
new file mode 100644
index 000000000..3bc79bbb8
--- /dev/null
+++ b/src/symbolic/symbolic_memory_intf.ml
@@ -0,0 +1,108 @@
+module type M = sig
+  type t
+
+  type address
+
+  val create : unit -> t
+
+  val clone : t -> t
+
+  val ptr : Smtml.Expr.t -> address
+
+  val address : Smtml.Expr.t -> address
+
+  val address_i32 : Int32.t -> address
+
+  val loadn : t -> address -> int -> Smtml.Expr.t
+
+  val storen : t -> address -> Smtml.Expr.t -> int -> unit
+
+  val is_within_bounds :
+    t -> Smtml.Expr.t -> (Smtml.Expr.t * address, Trap.t) result
+
+  val free : t -> address -> (unit, Trap.t) result
+
+  val realloc : t -> address -> Smtml.Expr.t -> Smtml.Expr.t
+end
+
+module type S = sig
+  type t
+
+  type address
+
+  type collection
+
+  val init : unit -> collection
+
+  val clone : collection -> collection
+
+  val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
+
+  val is_within_bounds :
+    t -> Smtml.Expr.t -> (Smtml.Expr.t * address, Trap.t) result
+
+  val ptr : Smtml.Expr.t -> address
+
+  val address : Smtml.Expr.t -> address
+
+  val address_i32 : Int32.t -> address
+
+  val free : t -> address -> (unit, Trap.t) result
+
+  val realloc : t -> address -> Smtml.Expr.t -> Smtml.Expr.t
+
+  val load_8_s : t -> address -> Symbolic_value.int32
+
+  val load_8_u : t -> address -> Symbolic_value.int32
+
+  val load_16_s : t -> address -> Symbolic_value.int32
+
+  val load_16_u : t -> address -> Symbolic_value.int32
+
+  val load_32 : t -> address -> Symbolic_value.int32
+
+  val load_64 : t -> address -> Symbolic_value.int32
+
+  val store_8 : t -> addr:address -> Smtml.Expr.t -> unit
+
+  val store_16 : t -> addr:address -> Smtml.Expr.t -> unit
+
+  val store_32 : t -> addr:address -> Smtml.Expr.t -> unit
+
+  val store_64 : t -> addr:address -> Smtml.Expr.t -> unit
+
+  val grow : t -> Smtml.Expr.t -> unit
+
+  val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
+
+  val blit :
+       t
+    -> src:Smtml.Expr.t
+    -> dst:Smtml.Expr.t
+    -> len:Smtml.Expr.t
+    -> Smtml.Expr.t
+
+  val blit_string :
+       t
+    -> string
+    -> src:Smtml.Expr.t
+    -> dst:Smtml.Expr.t
+    -> len:Smtml.Expr.t
+    -> Smtml.Expr.t
+
+  val size : t -> Smtml.Expr.t
+
+  val size_in_pages : t -> Smtml.Expr.t
+
+  val get_limit_max : t -> Smtml.Expr.t option
+
+  module ITbl : sig
+    type 'a t
+
+    type key
+
+    val iter : (key -> 'a -> unit) -> 'a t -> unit
+  end
+
+  val iter : (t ITbl.t -> unit) -> collection -> unit
+end
diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml
index 962dec31c..46ebd626b 100644
--- a/src/symbolic/symbolic_wasm_ffi.ml
+++ b/src/symbolic/symbolic_wasm_ffi.ml
@@ -39,34 +39,15 @@ module M :
 
   let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol
 
-  open Expr
-
   let abort () : unit Choice.t = Choice.add_pc @@ Value.Bool.const false
 
-  let i32 v : int32 Choice.t =
-    match view v with
-    | Val (Num (I32 v)) -> Choice.return v
-    | _ ->
-      Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v;
-      Choice.bind (abort ()) (fun () -> assert false)
-
-  let ptr v : int32 Choice.t =
-    match view v with
-    | Ptr { base; _ } -> Choice.return base
-    | _ ->
-      Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v;
-      Choice.bind (abort ()) (fun () -> assert false)
-
   let alloc m (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
-    let open Choice in
-    let+ base = i32 base in
-    Memory.replace_size m base size;
-    Expr.ptr base (Value.const_i32 0l)
+    Choice.return (Memory.realloc m (Memory.address base) size)
 
   let free m (p : Value.int32) : unit Choice.t =
-    let open Choice in
-    let+ base = ptr p in
-    Memory.free m base
+    match Memory.free m (Memory.ptr p) with
+    | Error t -> Choice.trap t
+    | Ok () -> Choice.return ()
 
   let exit (_p : Value.int32) : unit Choice.t = abort ()
 end