diff --git a/README.md b/README.md index 5acc019a..bce9796b 100644 --- a/README.md +++ b/README.md @@ -71,7 +71,7 @@ Then, run: ```bash make run_wast ``` -The interpreter is expected to pass all the other core tests (last tested on 17th Aug 2025): +The interpreter is expected to pass all the other core tests (last tested on 11th Dec 2025): ```bash Total passed: 54004/54004 (100.00%) ``` diff --git a/changelogs/v2.2.1.md b/changelogs/v2.2.1.md new file mode 100644 index 00000000..1fc9ce31 --- /dev/null +++ b/changelogs/v2.2.1.md @@ -0,0 +1,10 @@ +# Release 2.2.1 + +## New Features +- Extended the persistent array interfaces to allow bulk update by byte generators. This avoids creating redundant historic versions of memories and should result in a slight speedup in memory update operations. + +## Refactorings +- Removed dependency on the Uint63 module. The persistent array module now uses OCaml's `int` instead, which is 63-bit on 64-bit OCaml. + +## Bugfixes +- Corrected an errorneous type alias used in simd vector operations. diff --git a/coq-wasm.opam b/coq-wasm.opam index eec85a23..09597fb4 100644 --- a/coq-wasm.opam +++ b/coq-wasm.opam @@ -22,6 +22,7 @@ depends: [ "linenoise" {>= "1.4.0"} "mdx" {>= "1.9.0"} "wasm" {>= "2.0.2" & <= "2.0.2"} + "zarith" {>= "1.11"} "odoc" {with-doc} ] build: [ diff --git a/dune-project b/dune-project index 0f8bdbfe..389d8e54 100644 --- a/dune-project +++ b/dune-project @@ -24,6 +24,7 @@ (linenoise (>= 1.4.0)) (mdx (>= 1.9.0)) (wasm (and (>= 2.0.2) (<= 2.0.2))) + (zarith (>= 1.11)) ) (maintainers "Xiaojia Rao" diff --git a/src/Parray/Parray.ml b/src/Parray/Parray.ml index a62fcddf..f6bba2a2 100644 --- a/src/Parray/Parray.ml +++ b/src/Parray/Parray.ml @@ -9,237 +9,289 @@ (************************************************************************) (* Modified by Xiaojia Rao *) (* Summary of changes: *) -(* - Maximum array length changed to 2^32 to comply with Wasm's limit (may not work on 32-bit OCaml) *) -(* - Added a different make function `make_copy` that uses an initialiser array *) +(* - Added a separate node type for block updates *) +(* - Maximum array length changed to max_int to comply with Wasm's limit (requires 64-bit OCaml) *) +(* - Added a different make function `make_copy` that uses an initialiser array and deep copy *) (*******************************************************************************************************) (** Uniform Arrays: non-flat arrays (even floats are boxed, i.e., doesn't use {!Obj.double_array_tag}) *) - module UArray : - sig - type 'a t - val empty : 'a t - val unsafe_get : 'a t -> int -> 'a - val unsafe_set : 'a t -> int -> 'a -> unit - val length : 'a t -> int - val make : int -> 'a -> 'a t - val copy : 'a t -> 'a t - val of_array : 'a array -> 'a t - val to_array : 'a t -> 'a array - (* 'a should not be float (no Obj.double_tag) *) - val unsafe_of_obj : Obj.t -> 'a t - end = - struct - type 'a t = Obj.t array - (** Guaranteed to be a non-flat array and no funny business with write - barriers because of the opacity of Obj.t. *) - - let empty = [||] - - let length (v : 'a t) = Array.length v - - let of_array v = - if (Obj.tag (Obj.repr v) == Obj.double_array_tag) then begin - let n = Array.length v in - (* Ensure that we initialize it with a non-float *) - let ans = Array.make n (Obj.repr ()) in - for i = 0 to n - 1 do - Array.unsafe_set ans i (Obj.repr (Array.unsafe_get v i)) - done; - ans - end else - (Obj.magic (Array.copy v)) - - let obj_is_float x = Obj.tag x == Obj.double_tag - - let to_array (type a) (v : a t) : a array = - let () = assert (not (Array.exists obj_is_float v)) in - Obj.magic (Array.copy v) - - let unsafe_of_obj (type a) (v : Obj.t) = - let () = assert (Obj.tag v == 0) in - (Obj.obj v : a t) - - let unsafe_get = Obj.magic Array.unsafe_get - let unsafe_set = Obj.magic Array.unsafe_set - - let make (type a) n (x : a) : a t = - (* Ensure that we initialize it with a non-float *) - let ans = Array.make n (Obj.repr ()) in - let () = Array.fill ans 0 n (Obj.repr x) in - ans - - let copy = Array.copy - - end - - (* Changed to full 32 bit to match Wasm's memory limit *) - let max_array_length = 4294967296 - - let max_length = Uint63.of_int max_array_length - - let to_int i = snd (Uint63.to_int2 i) - - let trunc_size n = - if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int max_array_length) then - to_int n - else max_array_length - - type 'a t = ('a kind) ref - and 'a kind = - | Array of 'a UArray.t * 'a - | Updated of int * 'a * 'a t - - let unsafe_of_obj t def = ref (Array (UArray.unsafe_of_obj t, def)) - let of_array t def = ref (Array (UArray.of_array t, def)) - - let rec rerootk t k = - match !t with - | Array (a, _) -> k a - | Updated (i, v, p) -> - let k' a = - let v' = UArray.unsafe_get a i in - UArray.unsafe_set a i v; - t := !p; (* i.e., Array (a, def) *) - p := Updated (i, v', t); - k a in - rerootk p k' - - let reroot t = rerootk t (fun a -> a) - - let length_int p = - UArray.length (reroot p) - - let length p = Uint63.of_int @@ length_int p - - let get p n = - let t = reroot p in - let l = UArray.length t in - if Uint63.le Uint63.zero n && Uint63.lt n (Uint63.of_int l) then - UArray.unsafe_get t (to_int n) - else - match !p with - | Array (_, def) -> def - | Updated _ -> assert false - - let set p n e = - let a = reroot p in - let l = Uint63.of_int (UArray.length a) in - if Uint63.le Uint63.zero n && Uint63.lt n l then - let i = to_int n in +module UArray : +sig + type 'a t + val empty : 'a t + val unsafe_get : 'a t -> int -> 'a + val unsafe_set : 'a t -> int -> 'a -> unit + val length : 'a t -> int + val make : int -> 'a -> 'a t + val copy : 'a t -> 'a t + val of_array : 'a array -> 'a t + val to_array : 'a t -> 'a array + (* 'a should not be float (no Obj.double_tag) *) + val unsafe_of_obj : Obj.t -> 'a t +end = +struct + type 'a t = Obj.t array + (** Guaranteed to be a non-flat array and no funny business with write + barriers because of the opacity of Obj.t. *) + + let empty = [||] + + let length (v : 'a t) = Array.length v + + let of_array v = + if (Obj.tag (Obj.repr v) == Obj.double_array_tag) then begin + let n = Array.length v in + (* Ensure that we initialize it with a non-float *) + let ans = Array.make n (Obj.repr ()) in + for i = 0 to n - 1 do + Array.unsafe_set ans i (Obj.repr (Array.unsafe_get v i)) + done; + ans + end else + (Obj.magic (Array.copy v)) + + let obj_is_float x = Obj.tag x == Obj.double_tag + + let to_array (type a) (v : a t) : a array = + let () = assert (not (Array.exists obj_is_float v)) in + Obj.magic (Array.copy v) + + let unsafe_of_obj (type a) (v : Obj.t) = + let () = assert (Obj.tag v == 0) in + (Obj.obj v : a t) + + let unsafe_get = Obj.magic Array.unsafe_get + let unsafe_set = Obj.magic Array.unsafe_set + + let make (type a) n (x : a) : a t = + (* Ensure that we initialize it with a non-float *) + let ans = Array.make n (Obj.repr ()) in + let () = Array.fill ans 0 n (Obj.repr x) in + ans + + let copy = Array.copy + +end + +(* Changed to max_int to allow for Wasm's memory limit. This needs 64-bit OCaml to work *) +let max_array_length = max_int + +let max_length = max_array_length + +let to_int i = i + +let trunc_size n = + if 0<=n && n < max_array_length then + to_int n + else max_array_length + +let uarray_get_range a i len = + let res = Array.make len (UArray.unsafe_get a i) in + for j = 1 to len - 1 do + Array.unsafe_set res j (UArray.unsafe_get a (i + j)) + done; + res + +let uarray_set_range a i block = + let len = Array.length block in + for j = 0 to len - 1 do + UArray.unsafe_set a (i + j) (Array.unsafe_get block j) + done + +(* -------------------------------------------------- *) + +type 'a t = ('a kind) ref +and 'a kind = + | Array of 'a UArray.t * 'a + | Updated of int * 'a * 'a t + | BlockUpdated of int * 'a array * 'a t + +let unsafe_of_obj t def = ref (Array (UArray.unsafe_of_obj t, def)) +let of_array t def = ref (Array (UArray.of_array t, def)) + +let rec rerootk t k = + match !t with + | Array (a, _) -> k a + | Updated (i, v, p) -> + let k' a = let v' = UArray.unsafe_get a i in - UArray.unsafe_set a i e; - let t = ref !p in (* i.e., Array (a, def) *) + UArray.unsafe_set a i v; + t := !p; (* i.e., Array (a, def) *) p := Updated (i, v', t); - t - else p - - let default p = - let _ = reroot p in - match !p with - | Array (_,def) -> def - | Updated _ -> assert false - - let make_int n def = - ref (Array (UArray.make n def, def)) - - let make n def = make_int (trunc_size n) def - - (* An addition to the kernel Parray extraction that initialises with another array acting as an initialiser *) - let make_copy n init arr initlen = - if Uint63.le initlen (length arr) then - let trunc_n = trunc_size n in - if Uint63.le (length arr) (Uint63.of_int trunc_n) then - let marr = UArray.make trunc_n init in - let initlen_int = to_int initlen in - for i = 0 to initlen_int - 1 do - UArray.unsafe_set marr i (get arr (Uint63.of_int i)) - done; - ref (Array (marr, init)) - else assert false - else assert false - - let uinit n f = - if Int.equal n 0 then UArray.empty - else begin - let t = UArray.make n (f 0) in - for i = 1 to n - 1 do - UArray.unsafe_set t i (f i) - done; - t - end - - let init n f def = - let n = trunc_size n in - let t = uinit n f in - ref (Array (t, def)) - - let to_array p = - let _ = reroot p in - match !p with - | Array (t,def) -> UArray.to_array t, def - | Updated _ -> assert false - - let copy p = - let _ = reroot p in - match !p with - | Array (t, def) -> ref (Array (UArray.copy t, def)) - | Updated _ -> assert false - - (* Higher order combinators: the callback may update the underlying - array requiring a reroot between each call. To avoid doing n - reroots (-> O(n^2)), we copy if we have to reroot again. *) - - let is_rooted p = match !p with - | Array _ -> true - | Updated _ -> false - - type 'a cache = { - orig : 'a t; - mutable self : 'a UArray.t; - mutable rerooted_again : bool; - } - - let make_cache p = { - orig = p; - self = reroot p; - rerooted_again = false; - } - - let uget_cache cache i = - let () = if not cache.rerooted_again && not (is_rooted cache.orig) - then begin - cache.self <- UArray.copy (reroot cache.orig); - cache.rerooted_again <- true - end - in - UArray.unsafe_get cache.self i - - let map f p = - let t = make_cache p in - let len = UArray.length t.self in - let res = uinit len (fun i -> f (uget_cache t i)) in - let def = f (default p) in - ref (Array (res, def)) - - let fold_left f x p = - let r = ref x in - let t = make_cache p in - let len = UArray.length t.self in - for i = 0 to len - 1 do - r := f !r (uget_cache t i) + k a in + rerootk p k' + | BlockUpdated (i, old_vals, p) -> + let k' a = + let len = Array.length old_vals in + let v' = uarray_get_range a i len in + uarray_set_range a i old_vals; + t := !p; + p := BlockUpdated (i, v', t); + k a in + rerootk p k' + +let reroot t = rerootk t (fun a -> a) + +let length_int p = + UArray.length (reroot p) + +let length p = length_int p + +let get p n = + let t = reroot p in + let l = UArray.length t in + if 0 <= n && n < l then + UArray.unsafe_get t (to_int n) + else + match !p with + | Array (_, def) -> def + | Updated _ -> assert false + | BlockUpdated _ -> assert false + +let set p n e = + let a = reroot p in + let l = (UArray.length a) in + if 0 <= n && n < l then + let i = to_int n in + let v' = UArray.unsafe_get a i in + UArray.unsafe_set a i e; + let t = ref !p in (* i.e., Array (a, def) *) + p := Updated (i, v', t); + t + else p + +(* --- new function for block set by a generator --- *) + +let set_gen p start_pos block_len generator = + let a = reroot p in + let i = to_int start_pos in + let len = to_int block_len in + let total_len = UArray.length a in + (* Check bounds and block size *) + if 0 <= start_pos && (start_pos + block_len) <= (total_len) then + let old_vals = uarray_get_range a i len in + for j = 0 to len - 1 do + let new_val = generator (j) in + UArray.unsafe_set a (i + j) new_val + done; + let t = ref !p in + p := BlockUpdated (i, old_vals, t); + t + else p +(* ------------------------------ *) + +let default p = + let _ = reroot p in + match !p with + | Array (_,def) -> def + | Updated _ -> assert false + | BlockUpdated _ -> assert false + +let make_int n def = + ref (Array (UArray.make n def, def)) + +let make n def = make_int (trunc_size n) def + +(* An addition to the kernel Parray extraction that initialises with another array acting as an initialiser *) +let make_copy n init arr initlen = + if initlen <= (length arr) then + let trunc_n = trunc_size n in + if (length arr) <= (trunc_n) then + let marr = UArray.make trunc_n init in + let initlen_int = to_int initlen in + for i = 0 to initlen_int - 1 do + UArray.unsafe_set marr i (get arr (i)) done; - f !r (default p) + ref (Array (marr, init)) + else assert false + else assert false + +let uinit n f = + if Int.equal n 0 then UArray.empty + else begin + let t = UArray.make n (f 0) in + for i = 1 to n - 1 do + UArray.unsafe_set t i (f i) + done; +t + end + +let init n f def = + let n = trunc_size n in + let t = uinit n f in + ref (Array (t, def)) + +let to_array p = + let _ = reroot p in + match !p with + | Array (t,def) -> UArray.to_array t, def + | Updated _ -> assert false + | BlockUpdated _ -> assert false + +let copy p = + let _ = reroot p in + match !p with + | Array (t, def) -> ref (Array (UArray.copy t, def)) + | Updated _ -> assert false + | BlockUpdated _ -> assert false + +(* Higher order combinators: the callback may update the underlying + array requiring a reroot between each call. To avoid doing n + reroots (-> O(n^2)), we copy if we have to reroot again. *) + +let is_rooted p = match !p with + | Array _ -> true + | Updated _ -> false + | BlockUpdated _ -> false + +type 'a cache = { + orig : 'a t; +mutable self : 'a UArray.t; + mutable rerooted_again : bool; +} + +let make_cache p = { + orig = p; +self = reroot p; + rerooted_again = false; +} + +let uget_cache cache i = + let () = if not cache.rerooted_again && not (is_rooted cache.orig) + then begin + cache.self <- UArray.copy (reroot cache.orig); +cache.rerooted_again <- true + end + in + UArray.unsafe_get cache.self i + +let map f p = + let t = make_cache p in + let len = UArray.length t.self in + let res = uinit len (fun i -> f (uget_cache t i)) in + let def = f (default p) in + ref (Array (res, def)) + +let fold_left f x p = + let r = ref x in + let t = make_cache p in + let len = UArray.length t.self in + for i = 0 to len - 1 do + r := f !r (uget_cache t i) + done; + f !r (default p) + +let fold_left2 f a p1 p2 = + let r = ref a in + let t1 = make_cache p1 in + let len = UArray.length t1.self in + let t2 = make_cache p2 in + if UArray.length t2.self <> len then invalid_arg "Parray.fold_left2"; +for i = 0 to len - 1 do + let v1 = uget_cache t1 i in + let v2 = uget_cache t2 i in + r := f !r v1 v2 + done; +f !r (default p1) (default p2) - let fold_left2 f a p1 p2 = - let r = ref a in - let t1 = make_cache p1 in - let len = UArray.length t1.self in - let t2 = make_cache p2 in - if UArray.length t2.self <> len then invalid_arg "Parray.fold_left2"; - for i = 0 to len - 1 do - let v1 = uget_cache t1 i in - let v2 = uget_cache t2 i in - r := f !r v1 v2 - done; - f !r (default p1) (default p2) \ No newline at end of file diff --git a/src/Parray/Parray.mli b/src/Parray/Parray.mli index d401a828..fad13f5d 100644 --- a/src/Parray/Parray.mli +++ b/src/Parray/Parray.mli @@ -9,21 +9,28 @@ (************************************************************************) (* Modified by Xiaojia Rao *) (* Summary of changes: *) -(* - Maximum array length changed to 2^32 to comply with Wasm's limit (may not work on 32-bit OCaml) *) +(* - Maximum array length changed to max_int to comply with Wasm's limit (requires 64-bit OCaml) *) (* - Added a different make function `make_copy` that uses an initialiser array *) (*******************************************************************************************************) -val max_length : Uint63.t +val max_length : int type 'a t -val length : 'a t -> Uint63.t +val length : 'a t -> int val length_int : 'a t -> int -val get : 'a t -> Uint63.t -> 'a -val set : 'a t -> Uint63.t -> 'a -> 'a t +val get : 'a t -> int -> 'a +val set : 'a t -> int -> 'a -> 'a t + +val set_gen : 'a t -> int -> int -> (int -> 'a) -> 'a t +(** [set_gen p start_pos block_len generator] returns a new persistent array + based on [p] where the range of length [block_len] starting at [start_pos] + is updated by calling [generator] for each index 0 to [block_len - 1]. + [block_len] must be greater than 0. *) + val default : 'a t -> 'a -val make : Uint63.t -> 'a -> 'a t -val make_copy : Uint63.t -> 'a -> 'a t -> Uint63.t -> 'a t -val init : Uint63.t -> (int -> 'a) -> 'a -> 'a t +val make : int -> 'a -> 'a t +val make_copy : int -> 'a -> 'a t -> int -> 'a t +val init : int -> (int -> 'a) -> 'a -> 'a t val copy : 'a t -> 'a t val map : ('a -> 'b) -> 'a t -> 'b t diff --git a/src/Parray/Parray_shim.ml b/src/Parray/Parray_shim.ml new file mode 100644 index 00000000..b83ae7fe --- /dev/null +++ b/src/Parray/Parray_shim.ml @@ -0,0 +1,32 @@ +(* A wrapper file for the custom Parray module to take arguments of type `Z.t` instead of OCaml's `int`. + Note that this does not magically allow the 31st bit to be used on 32-bit OCaml distributions. + It is rather for connecting the unbounded integer types in the extracted code to the `int` + length parameter requried by OCaml's `Array.make`. +*) + +type 'a t = 'a Parray.t + +let z_of_int x = + Big_int_Z.big_int_of_int x + +let int_of_z z = + if Big_int_Z.is_int_big_int z then + Big_int_Z.int_of_big_int z +else invalid_arg "int_of_z overflow" + +let length a = z_of_int (Parray.length a) +let make z a = Parray.make (int_of_z z) a + +let copy = Parray.copy + +let make_copy n init arr initlen = + Parray.make_copy (int_of_z n) init arr (int_of_z initlen) + +let get a z = Parray.get a (int_of_z z) + +let set a z v = Parray.set a (int_of_z z) v + +let set_gen a z len gen = + Parray.set_gen a (int_of_z z) (int_of_z len) (fun id -> gen (z_of_int id)) + +let default = Parray.default \ No newline at end of file diff --git a/src/Parray/Parray_shim.mli b/src/Parray/Parray_shim.mli new file mode 100644 index 00000000..05ce9aba --- /dev/null +++ b/src/Parray/Parray_shim.mli @@ -0,0 +1,15 @@ +type 'a t +val length : 'a t -> Big_int_Z.big_int +val get : 'a t -> Big_int_Z.big_int -> 'a +val set : 'a t -> Big_int_Z.big_int -> 'a -> 'a t + +val set_gen : 'a t -> Big_int_Z.big_int -> Big_int_Z.big_int -> (Big_int_Z.big_int -> 'a) -> 'a t +(** [set_gen p start_pos block_len generator] returns a new persistent array + based on [p] where the range of length [block_len] starting at [start_pos] + is updated by calling [generator] for each index 0 to [block_len - 1]. + [block_len] must be greater than 0. *) + +val default : 'a t -> 'a +val make : Big_int_Z.big_int -> 'a -> 'a t +val make_copy : Big_int_Z.big_int -> 'a -> 'a t -> Big_int_Z.big_int -> 'a t +val copy : 'a t -> 'a t \ No newline at end of file diff --git a/src/Parray/Uint63.ml b/src/Parray/Uint63.ml deleted file mode 100644 index c33ef522..00000000 --- a/src/Parray/Uint63.ml +++ /dev/null @@ -1,248 +0,0 @@ -(************************************************************************) -(* * The Rocq Prover / The Rocq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* = 0 then - begin q := !q lor 1; nh := Int64.sub !nh y; end - done; - !q, Int64.to_int !nh - -let div21 xh xl y = - let xh = to_uint64 xh in - let y = to_uint64 y in - if Int64.compare y xh <= 0 then 0, 0 else div21 xh xl y - - (* exact multiplication *) -(* TODO: check that none of these additions could be a logical or *) - - -(* size = 32 + 31 - (hx << 31 + lx) * (hy << 31 + ly) = - hxhy << 62 + (hxly + lxhy) << 31 + lxly -*) - -(* precondition : (x lsr 62 = 0 || y lsr 62 = 0) *) -let mulc_aux x y = - let lx = x land maxuint31 in - let ly = y land maxuint31 in - let hx = x lsr 31 in - let hy = y lsr 31 in - (* hx and hy are 32 bits value but at most one is 32 *) - let hxy = hx * hy in (* 63 bits *) - let hxly = hx * ly in (* 63 bits *) - let lxhy = lx * hy in (* 63 bits *) - let lxy = lx * ly in (* 62 bits *) - let l = lxy lor (hxy lsl 62) (* 63 bits *) in - let h = hxy lsr 1 in (* 62 bits *) - let hl = hxly + lxhy in (* We can have a carry *) - let h = if lt hl hxly then h + (1 lsl 31) else h in - let hl'= hl lsl 31 in - let l = l + hl' in - let h = if lt l hl' then h + 1 else h in - let h = h + (hl lsr 32) in - (h,l) - -let mulc x y = - if (x lsr 62 = 0 || y lsr 62 = 0) then mulc_aux x y - else - let yl = y lxor (1 lsl 62) in - let (h,l) = mulc_aux x yl in - (* h << 63 + l = x * yl - x * y = x * (1 << 62 + yl) = - x << 62 + x*yl = x << 62 + h << 63 + l *) - let l' = l + (x lsl 62) in - let h = if lt l' l then h + 1 else h in - (h + (x lsr 1), l') - -let equal (x : int) (y : int) = x = y -[@@ocaml.inline always] - -let compare (x:int) (y:int) = - let x = x lxor 0x4000000000000000 in - let y = y lxor 0x4000000000000000 in - Int.compare x y - -let compares (x : int) (y : int) = - Int.compare x y - - (* head tail *) - -let head0 x = - let r = ref 0 in - let x = ref x in - if !x land 0x7FFFFFFF00000000 = 0 then r := !r + 31 - else x := !x lsr 31; - if !x land 0xFFFF0000 = 0 then (x := !x lsl 16; r := !r + 16); - if !x land 0xFF000000 = 0 then (x := !x lsl 8; r := !r + 8); - if !x land 0xF0000000 = 0 then (x := !x lsl 4; r := !r + 4); - if !x land 0xC0000000 = 0 then (x := !x lsl 2; r := !r + 2); - if !x land 0x80000000 = 0 then (x := !x lsl 1; r := !r + 1); - if !x land 0x80000000 = 0 then ( r := !r + 1); - !r;; - -let tail0 x = - let r = ref 0 in - let x = ref x in - if !x land 0xFFFFFFFF = 0 then (x := !x lsr 32; r := !r + 32); - if !x land 0xFFFF = 0 then (x := !x lsr 16; r := !r + 16); - if !x land 0xFF = 0 then (x := !x lsr 8; r := !r + 8); - if !x land 0xF = 0 then (x := !x lsr 4; r := !r + 4); - if !x land 0x3 = 0 then (x := !x lsr 2; r := !r + 2); - if !x land 0x1 = 0 then ( r := !r + 1); - !r - -let is_uint63 t = - Obj.is_int t -[@@ocaml.inline always] - -(* Arithmetic with explicit carries *) - -(* Analog of Numbers.Abstract.Cyclic.carry *) -type 'a carry = C0 of 'a | C1 of 'a - -let addc x y = - let r = x + y in - if lt r x then C1 r else C0 r - -let addcarryc x y = - let r = x + y + 1 in - if le r x then C1 r else C0 r - -let subc x y = - let r = x - y in - if le y x then C0 r else C1 r - -let subcarryc x y = - let r = x - y - 1 in - if lt y x then C0 r else C1 r \ No newline at end of file diff --git a/src/Parray/Uint63.mli b/src/Parray/Uint63.mli deleted file mode 100644 index 8780f46c..00000000 --- a/src/Parray/Uint63.mli +++ /dev/null @@ -1,98 +0,0 @@ -(************************************************************************) -(* * The Rocq Prover / The Rocq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* t -val to_int2 : t -> int * int (* msb, lsb *) -val of_int64 : Int64.t -> t -val to_int64 : t -> Int64.t -(* -val of_uint : int -> t - *) -(** [int_min n m] returns the minimum of [n] and [m], - [m] must be in [0, 2^30-1]. *) -val to_int_min : t -> int -> int - - (* conversion to float *) -val of_float : float -> t - -val hash : t -> int - - (* conversion to a string *) -val to_string : t -> string - -val compile : t -> string - -(* constants *) -val zero : t -val one : t - - (* logical operations *) -val l_sl : t -> t -> t -val l_sr : t -> t -> t -val l_and : t -> t -> t -val l_xor : t -> t -> t -val l_or : t -> t -> t - - (* Arithmetic operations *) -val a_sr : t -> t -> t -val add : t -> t -> t -val sub : t -> t -> t -val mul : t -> t -> t -val div : t -> t -> t -val rem : t -> t -> t - -val diveucl : t -> t -> t * t - - (* Signed arithmetic opeartions *) -val divs : t -> t -> t -val rems : t -> t -> t - - (* Specific arithmetic operations *) -val mulc : t -> t -> t * t -val addmuldiv : t -> t -> t -> t - -(** [div21 xh xl y] returns [q % 2^63, r] - s.t. [xh * 2^63 + xl = q * y + r] and [r < y]. - When [y] is [0], returns [0, 0]. *) -val div21 : t -> t -> t -> t * t - - (* comparison *) -val lt : t -> t -> bool -val equal : t -> t -> bool -val le : t -> t -> bool -val compare : t -> t -> int - - (* signed comparision *) -val lts : t -> t -> bool -val les : t -> t -> bool -val compares : t -> t -> int - - (* head and tail *) -val head0 : t -> t -val tail0 : t -> t - -val is_uint63 : Obj.t -> bool - -(* Arithmetic with explicit carries *) - -(* Analog of Numbers.Abstract.Cyclic.carry *) -type 'a carry = C0 of 'a | C1 of 'a - -val addc : t -> t -> t carry -val addcarryc : t -> t -> t carry -val subc : t -> t -> t carry -val subcarryc : t -> t -> t carry \ No newline at end of file diff --git a/src/Parray/dune b/src/Parray/dune index 899e26fd..06c96038 100644 --- a/src/Parray/dune +++ b/src/Parray/dune @@ -2,4 +2,5 @@ (name parray) (modules :standard) (wrapped false) + (libraries zarith) ) \ No newline at end of file diff --git a/src/convert.ml b/src/convert.ml index a53a2b9a..7d3749e9 100644 --- a/src/convert.ml +++ b/src/convert.ml @@ -5,4 +5,4 @@ let rec to_nat = function let rec from_nat = function | Extract.O -> 0 - | Extract.S n -> 1 + from_nat n + | Extract.S n -> 1 + from_nat n \ No newline at end of file diff --git a/src/convert.mli b/src/convert.mli index 87d4d0be..1e75203f 100644 --- a/src/convert.mli +++ b/src/convert.mli @@ -2,4 +2,4 @@ val to_nat : int -> Extract.nat (** Convert [Extract.nat] to [int]. **) -val from_nat : Extract.nat -> int +val from_nat : Extract.nat -> int \ No newline at end of file diff --git a/src/execute.ml b/src/execute.ml index 673d6e1b..fd25642a 100644 --- a/src/execute.ml +++ b/src/execute.ml @@ -64,7 +64,7 @@ let rec eval_interp_cfg verbosity gen max_call_depth cfg d = match cfg_res with | RSC_normal (_hs', cfg', d') -> let d_int = Utils.int_of_z d' in - if (d_int > max_call_depth) && (max_call_depth != -1) then begin + if (d_int > max_call_depth) && (max_call_depth != (-1)) then begin debug_info verbosity stage ~style:red (fun _ -> "Call stack exhaustion\n"); Cfg_exhaustion end diff --git a/src/extraction.v b/src/extraction.v index b8d7eeaf..7945e139 100644 --- a/src/extraction.v +++ b/src/extraction.v @@ -1,14 +1,6 @@ (** Extraction to OCaml. **) From Coq Require Extraction. -From Coq Require PArray. -From Coq Require Import - extraction.ExtrOcamlBasic - extraction.ExtrOcamlNativeString - extraction.ExtrOcamlZBigInt - ExtrOCamlInt63 -. - From Wasm Require Import efficient_extraction datatypes_properties @@ -24,21 +16,32 @@ From Wasm Require Import . Require Import compcert.lib.Integers. +Require Import ZArith NArith. + +From Coq Require PArray. +From Coq Require Import + extraction.ExtrOcamlBasic + extraction.ExtrOcamlNativeString + extraction.ExtrOcamlZBigInt +. Extraction Language OCaml. Extract Constant lookup_N => "EfficientExtraction.lookup_N_safe". -Extract Constant memory_vec.array "'a" => "Parray.t". +Extract Constant memory_vec.array "'a" => "Parray_shim.t". Extraction Inline memory_vec.array. -Extract Constant memory_vec.arr_make => "Parray.make". -Extract Constant memory_vec.arr_make_copy => "Parray.make_copy". -Extract Constant memory_vec.arr_get => "Parray.get". -Extract Constant memory_vec.arr_default => "Parray.default". -Extract Constant memory_vec.arr_set => "Parray.set". -Extract Constant memory_vec.arr_length => "Parray.length". -Extract Constant memory_vec.arr_copy => "Parray.copy". +(* Requires some custom rerouting *) + +Extract Constant memory_vec.arr_make => "Parray_shim.make". +Extract Constant memory_vec.arr_make_copy => "Parray_shim.make_copy". +Extract Constant memory_vec.arr_get => "Parray_shim.get". +Extract Constant memory_vec.arr_default => "Parray_shim.default". +Extract Constant memory_vec.arr_set => "Parray_shim.set". +Extract Constant memory_vec.arr_set_gen => "Parray_shim.set_gen". +Extract Constant memory_vec.arr_length => "Parray_shim.length". +Extract Constant memory_vec.arr_copy => "Parray_shim.copy". Extract Constant SIMD_ops.app_vunop_str => "SIMD_ops.app_vunop_str". Extract Constant SIMD_ops.app_vbinop_str => "SIMD_ops.app_vbinop_str". diff --git a/src/shim.ml b/src/shim.ml index ead6529e..b197cb12 100644 --- a/src/shim.ml +++ b/src/shim.ml @@ -98,6 +98,7 @@ end module Interpreter = functor (EH : Host) -> struct + module Host = EH include Host diff --git a/theories/common.v b/theories/common.v index 5c027af7..257e625d 100644 --- a/theories/common.v +++ b/theories/common.v @@ -1037,3 +1037,29 @@ Definition induction3 (P : nat -> Prop) := @rect3 P. Definition induction4 (P : nat -> Prop) := @rect4 P. Definition induction5 (P : nat -> Prop) := @rect5 P. Definition induction6 (P : nat -> Prop) := @rect6 P. + +(* Tactic for dealing with dependent type simplifications *) +Ltac simplify_dependent_case := + match goal with + | |- context [(match ?match_expr as b in bool return (?match_expr = b -> _) with + | true => _ + | false => _ + end) Logic.eq_refl] => + generalize (Logic.eq_refl match_expr); + generalize match_expr at 2 3; + let Hdep_case := fresh "Hdep_case" in + case => Hdep_case => //= + end. + +Ltac simplify_dependent_case_hyp H := + match type of H with + | context [(match ?match_expr as b in bool return (?match_expr = b -> _) with + | true => _ + | false => _ + end) Logic.eq_refl] => + move: H; + generalize (Logic.eq_refl match_expr); + generalize match_expr at 2 3; + let Hdep_case := fresh "Hdep_case" in + case => Hdep_case => //= + end. diff --git a/theories/host.v b/theories/host.v index 02762160..60fa9806 100644 --- a/theories/host.v +++ b/theories/host.v @@ -24,7 +24,7 @@ Set Implicit Arguments. Section Predicate. -Context `{hfc: host_function_class} `{memory: Memory}. +Context `{hfc: host_function_class} `{memory: BlockUpdateMemory}. (** We assume a set of host functions. **) (** The application of a host function either: diff --git a/theories/instantiation_spec.v b/theories/instantiation_spec.v index a3966d4f..c7bbfe62 100644 --- a/theories/instantiation_spec.v +++ b/theories/instantiation_spec.v @@ -92,7 +92,7 @@ Definition alloc_tabs (s : store_record) (ts : list table_type) : store_record * Definition gen_mem_instance (lim : limits) : meminst := let len := BinNatDef.N.mul page_size lim.(lim_min) in - {| meminst_data := mem_make Integers.Byte.zero len; + {| meminst_data := mem_make len; meminst_type := lim; |}. diff --git a/theories/memory.v b/theories/memory.v index 57dc8102..b1f2090a 100644 --- a/theories/memory.v +++ b/theories/memory.v @@ -3,7 +3,7 @@ From Coq Require Import BinNat. From Wasm Require Import bytes common. From HB Require Import structures. -From mathcomp Require Import ssrbool eqtype. +From mathcomp Require Import ssreflect ssrbool eqtype. Set Implicit Arguments. Unset Strict Implicit. @@ -18,9 +18,11 @@ Section Memory. Definition byte_limit : N := N.mul page_size page_limit. + Definition wasm_memory_default_byte : byte := #00. + Class Memory := { mem_t : Type; - mem_make : byte -> N -> mem_t; + mem_make : N -> mem_t; (* Doesn't take an init, as Wasm forces it to zero *) mem_length : mem_t -> N; mem_lookup : N -> mem_t -> option byte; (* Doesn't have to succeed *) @@ -38,13 +40,13 @@ Section Memory. mem_lookup i mem = None; mem_make_length : - forall b len, - mem_length (mem_make b len) = N.min len byte_limit; + forall len, + mem_length (mem_make len) = N.min len byte_limit; mem_make_lookup : - forall i len b, + forall i len, N.lt i (N.min len byte_limit) -> - mem_lookup i (mem_make b len) = Some b; + mem_lookup i (mem_make len) = Some wasm_memory_default_byte; mem_update_lookup : forall mem mem' i b, @@ -56,11 +58,6 @@ Section Memory. i <> i' -> mem_update i' b mem = Some mem' -> mem_lookup i mem' = mem_lookup i mem; - - mem_update_length : - forall i b mem mem', - mem_update i b mem = Some mem' -> - mem_length mem' = mem_length mem; mem_update_ib : forall mem i b, @@ -82,8 +79,231 @@ Section Memory. forall n mem mem', mem_grow n mem = Some mem' -> mem_length mem' = N.add (mem_length mem) n; + + mem_grow_default: + forall n len mem mem' i, + N.lt i n -> + mem_grow n mem = Some mem' -> + mem_length mem = len -> + mem_lookup (len + i) mem' = Some #00 + }. -Context `{Memory}. + Context `{Memory}. + + Lemma mem_lookup_some_length: forall m i, + mem_lookup i m <> None -> + N.lt i (mem_length m). + Proof. + move => m i Hlookup. + destruct (N.ltb i (mem_length m)) eqn:Hlt; first by lias. + exfalso. + move/N.ltb_spec0 in Hlt. + by apply mem_lookup_oob in Hlt. + Qed. + + Lemma mem_lookup_some_length': forall m i b, + mem_lookup i m = Some b -> + N.lt i (mem_length m). + Proof. + move => m i b Hlookup. + apply mem_lookup_some_length. + by rewrite Hlookup. + Qed. + Lemma mem_lookup_none_length: forall m i, + mem_lookup i m = None -> + N.ge i (mem_length m). + Proof. + move => m i Hlookup. + destruct (N.ltb i (mem_length m)) eqn:Hlt; move/N.ltb_spec0 in Hlt; last done. + by apply mem_lookup_ib in Hlt. + Qed. + + Lemma mem_update_some_length: forall m i b, + mem_update i b m <> None -> + N.lt i (mem_length m). + Proof. + move => m i b Hupdate. + destruct (N.ltb i (mem_length m)) eqn:Hlt; first by lias. + exfalso. + move/N.ltb_spec0 in Hlt. + by apply mem_update_oob with (b := b) in Hlt. + Qed. + + Lemma mem_update_some_length': forall m i b m', + mem_update i b m = Some m' -> + N.lt i (mem_length m). + Proof. + move => m i b m' Hupdate. + by apply mem_update_some_length with (b := b); rewrite Hupdate. + Qed. + + Lemma mem_update_none_length: forall m i b, + mem_update i b m = None -> + N.ge i (mem_length m). + Proof. + move => m i b Hlookup. + destruct (N.ltb i (mem_length m)) eqn:Hlt; move/N.ltb_spec0 in Hlt; last done. + by apply mem_update_ib with (b := b) in Hlt. + Qed. + + Lemma mem_length_boundary : forall m i, + mem_lookup i m <> None -> + mem_lookup (N.succ i) m = None -> + mem_length m = N.succ i. + Proof. + move => m i Hlookup1 Hlookup2. + apply mem_lookup_some_length in Hlookup1. + apply mem_lookup_none_length in Hlookup2. + apply N.le_succ_l in Hlookup1. + by lias. + Qed. + + Lemma mem_length_extensional_aux: forall m m', + (forall i, (mem_lookup i m == None) = (mem_lookup i m' == None)) -> + ~ (mem_length m < mem_length m')%N. + Proof. + move => m m' Heq Hlt. + specialize (Heq (mem_length m)). + rewrite mem_lookup_oob in Heq; last by lias. + rewrite eq_refl in Heq; symmetry in Heq; move/eqP in Heq. + by specialize (mem_lookup_ib Hlt). + Qed. + + Lemma mem_length_extensional : forall m m', + (forall i, (mem_lookup i m == None) = (mem_lookup i m' == None)) -> + mem_length m = mem_length m'. + Proof. + move => m m' Heq. + specialize (mem_length_extensional_aux Heq) as Hbound1. + assert (~ (mem_length m' < mem_length m)%N) as Hbound2. + { apply mem_length_extensional_aux. + by move => i; specialize (Heq i). + } + by lias. + Qed. + + Lemma mem_update_length : forall i b mem mem', + mem_update i b mem = Some mem' -> + mem_length mem' = mem_length mem. + Proof. + move => i b mem mem' Hupdate. + apply mem_length_extensional; move => j. + destruct (mem_lookup j mem) eqn:Hlookup. + - destruct (N.eqb i j) eqn:Hid; move/N.eqb_spec in Hid; subst. + + apply mem_update_lookup in Hupdate. + by rewrite Hupdate. + + apply mem_update_lookup_ne with (i := j) in Hupdate; last by lias. + by rewrite Hupdate Hlookup. + - specialize (mem_lookup_none_length Hlookup) as Hbound1. + specialize (mem_update_some_length' Hupdate) as Hbound2. + assert (i <> j) as Hneq; first by lias. + rewrite -> mem_update_lookup_ne with (mem := mem) (i := j) (i' := i) (b := b); by lias. + Qed. + End Memory. + +Section BlockUpdateMemory. + + Class BlockUpdateMemory := { + m: Memory; + mem_update_gen: N -> N -> (N -> byte) -> mem_t -> option mem_t; + + mem_update_gen_ib: + forall n len gen m, + N.le (N.add n len) (mem_length m) -> + mem_update_gen n len gen m <> None; + + mem_update_gen_oob: + forall n len gen m, + N.gt (N.add n len) (mem_length m) -> + mem_update_gen n len gen m = None; + + mem_update_gen_lookup: + forall n len gen m m' i, + mem_update_gen n len gen m = Some m' -> + N.lt i len -> + mem_lookup (N.add n i) m' = Some (gen i); + + mem_update_gen_lookup_lt: + forall n len gen m m' i, + mem_update_gen n len gen m = Some m' -> + N.lt i n -> + mem_lookup i m' = mem_lookup i m; + + mem_update_gen_lookup_ge: + forall n len gen m m' i, + mem_update_gen n len gen m = Some m' -> + N.ge i (N.add n len) -> + mem_lookup i m' = mem_lookup i m; + }. + + #[global] + Instance memory_from_bum `{bum: BlockUpdateMemory} : Memory := m. + + Hint Resolve memory_from_bum : typeclass_instances. + + Context `{BlockUpdateMemory}. + + Lemma mem_update_gen_some_length: forall n len gen m, + mem_update_gen n len gen m <> None -> + N.le (N.add n len) (mem_length m). + Proof. + move => n len gen m Hupdate. + destruct (N.leb (N.add n len) (mem_length m)) eqn:Hle; move/N.leb_spec0 in Hle => //. + exfalso. + apply Hupdate, mem_update_gen_oob. + by lias. + Qed. + + Lemma mem_update_gen_some_length': forall n len gen m b, + mem_update_gen n len gen m = Some b -> + N.le (N.add n len) (mem_length m). + Proof. + move => n len gen m b Hupdate. + apply mem_update_gen_some_length with (gen := gen); eauto. + by rewrite Hupdate. + Qed. + + Lemma mem_update_gen_lookup_ex: forall n len gen m m' i, + mem_update_gen n len gen m = Some m' -> + (mem_lookup i m == None) = (mem_lookup i m' == None). + Proof. + move => n len gen m m' i Hupdate. + destruct (N.ltb i n) eqn:Hlt; move/N.ltb_spec0 in Hlt. + - specialize (mem_update_gen_lookup_lt Hupdate Hlt) as Heq. + by rewrite Heq. + - destruct (N.ltb i (N.add n len)) eqn:Hlt2; move/N.ltb_spec0 in Hlt2. + + assert (N.lt (N.sub i n) len) as Hlt3; first by lias. + specialize (mem_update_gen_lookup Hupdate Hlt3) as Hlookupgen. + replace (n+(i-n)%N)%N with i in Hlookupgen; last by lias. + rewrite Hlookupgen. + assert (mem_lookup i m <> None) as Hlookup. + { apply mem_lookup_ib. + apply mem_update_gen_some_length' in Hupdate. + by lias. + } + by lias. + + specialize (mem_update_gen_lookup_ge Hupdate Hlt2) as Heq. + by rewrite Heq. + Qed. + + Lemma mem_update_gen_length : forall n len gen m m', + mem_update_gen n len gen m = Some m' -> + mem_length m = mem_length m'. + Proof. + move => n len gen m m' Hupdate. + apply mem_length_extensional. + move => i. + destruct (mem_lookup i m) eqn:Hlookup1; + destruct (mem_lookup i m') eqn:Hlookup2 => //=; exfalso. + - move/eqP in Hlookup2. + erewrite <- mem_update_gen_lookup_ex in Hlookup2; eauto. + by rewrite Hlookup1 in Hlookup2. + - move/eqP in Hlookup1. + erewrite -> mem_update_gen_lookup_ex in Hlookup1; eauto. + by rewrite Hlookup2 in Hlookup1. + Qed. + +End BlockUpdateMemory. diff --git a/theories/memory_list.v b/theories/memory_list.v index 8fbc714f..87cfd0f4 100644 --- a/theories/memory_list.v +++ b/theories/memory_list.v @@ -10,15 +10,17 @@ Unset Printing Implicit Defensive. Section MemoryList. + Context `{def_byte: byte}. + Record memory_list : Type := { - ml_init : byte; + ml_init : byte := def_byte; ml_data : list byte; }. Definition ml_make := - fun v len => + fun len => let capped_len := N.min len byte_limit in - {| ml_init := v; ml_data := mkseq (fun _ => v) (N.to_nat capped_len) |}. + {| ml_data := mkseq (fun _ => def_byte) (N.to_nat capped_len) |}. Definition ml_length := fun ml => N.of_nat (size ml.(ml_data)). @@ -28,7 +30,6 @@ Section MemoryList. let new_length := N.add len_delta (N.of_nat (length ml.(ml_data))) in if new_length <=? byte_limit then Some {| - ml_init := ml.(ml_init); ml_data := ml.(ml_data) ++ mkseq (fun _ => ml.(ml_init)) (N.to_nat len_delta) |} else None. @@ -42,8 +43,7 @@ Section MemoryList. Definition ml_update := fun i v ml => if N.ltb i (ml_length ml) - then Some {| ml_init := ml.(ml_init); - ml_data := set_nth ml.(ml_init) ml.(ml_data) (N.to_nat i) v + then Some {| ml_data := set_nth ml.(ml_init) ml.(ml_data) (N.to_nat i) v |} else None. @@ -74,21 +74,21 @@ Section MemoryList. Qed. Lemma ml_make_length: - forall b len, - ml_length (ml_make b len) = N.min len byte_limit. + forall len, + ml_length (ml_make len) = N.min len byte_limit. Proof. - move => b len => /=. + move => len => /=. unfold ml_length, ml_make. rewrite size_mkseq. by rewrite N2Nat.id. Qed. Lemma ml_make_lookup: - forall i len b, + forall i len, (i < N.min len byte_limit)%N -> - ml_lookup i (ml_make b len) = Some b. + ml_lookup i (ml_make len) = Some def_byte. Proof. - move => i len b Hlen /=. + move => i len Hlen /=. unfold ml_lookup. erewrite ml_make_length; eauto. move/N.ltb_spec0 in Hlen; rewrite Hlen => /=. @@ -207,22 +207,47 @@ Proof. unfold ml_length in Hlen. replace (N.to_nat i < size (ml_data mem)) with true; by lias. Qed. - + +Lemma ml_grow_default: + forall (n len : N) (mem mem' : memory_list) (i : N), + (i < n)%N -> + ml_grow n mem = Some mem' -> + ml_length mem = len -> + ml_lookup (len + i) mem' = Some mem.(ml_init). +Proof. + move => n len mem mem' i Hlt Hgrow Hlen. + unfold ml_grow in Hgrow; remove_bools_options. + unfold ml_lookup, ml_length => /=. + rewrite size_cat Nat2N.inj_add size_mkseq N2Nat.id. + replace (_ Type. -Parameter arr_make : PrimInt63.int -> A -> array A. +Parameter arr_make : N -> A -> array A. (* The same as make but initialises its prefix with values from the prefix of another array. Does not overflow if the length exceeds the make length. This is used in the vector_grow function. *) -Parameter arr_make_copy: PrimInt63.int -> A -> array A -> PrimInt63.int -> array A. -Parameter arr_get : array A -> PrimInt63.int -> A. +Parameter arr_make_copy: N -> A -> array A -> N -> array A. +Parameter arr_get : array A -> N -> A. Parameter arr_default : array A -> A. -Parameter arr_set : array A -> PrimInt63.int -> A -> array A. -Parameter arr_length : array A -> PrimInt63.int. +Parameter arr_set : array A -> N -> A -> array A. +(* Takes the length and the generator for the block *) +Parameter arr_set_gen : array A -> N -> N -> (N -> A) -> array A. +Parameter arr_length : array A -> N. Parameter arr_copy : array A -> array A. -Definition max_arr_length : PrimInt63.int := Uint63.of_Z (Z.of_N byte_limit). +Definition max_arr_length : N := byte_limit. Notation " t .[ i ] " := (arr_get t i) (at level 5). Notation " t .[ i <- a ] " := (arr_set t i a) (at level 5). Parameter get_out_of_bounds : - forall (t : array A) (i : PrimInt63.int), - PrimInt63.ltb i (arr_length t) = false -> t.[i] = arr_default t. + forall (t : array A) (i : N), + N.ltb i (arr_length t) = false -> t.[i] = arr_default t. Parameter get_set_same : - forall (t : array A) (i : PrimInt63.int) (a : A), - PrimInt63.ltb i (arr_length t) = true -> t.[i<-a].[i] = a. + forall (t : array A) (i : N) (a : A), + N.ltb i (arr_length t) = true -> t.[i<-a].[i] = a. Parameter get_set_other : - forall (t : array A) (i j : PrimInt63.int) (a : A), + forall (t : array A) (i j : N) (a : A), i <> j -> t.[i<-a].[j] = t.[j]. Parameter default_set : - forall (t : array A) (i : PrimInt63.int) (a : A), + forall (t : array A) (i : N) (a : A), arr_default t.[i<-a] = arr_default t. Parameter get_make : - forall (a : A) (size i : PrimInt63.int), + forall (a : A) (size i : N), (arr_make size a).[i] = a. Parameter get_make_copy: - forall (a: A) (size i: PrimInt63.int) (t: array A) (initlen: PrimInt63.int), - PrimInt63.ltb i size -> - PrimInt63.leb initlen (arr_length t) -> - PrimInt63.ltb i (arr_length t) -> + forall (a: A) (size i: N) (t: array A) (initlen: N), + N.ltb i size -> + N.leb initlen (arr_length t) -> + N.ltb i (arr_length t) -> (arr_make_copy size a t initlen).[i] = t.[i]. Parameter get_make_copy_default: - forall (a: A) (size i: PrimInt63.int) (t: array A) (initlen: PrimInt63.int), - PrimInt63.ltb i size -> - PrimInt63.leb initlen (arr_length t) -> - PrimInt63.leb initlen i -> + forall (a: A) (size i: N) (t: array A) (initlen: N), + N.ltb i size -> + N.leb initlen (arr_length t) -> + N.leb initlen i -> (arr_make_copy size a t initlen).[i] = a. Parameter leb_length : forall (t : array A), - PrimInt63.leb (arr_length t) max_arr_length = true. + N.leb (arr_length t) max_arr_length = true. Parameter length_make : - forall (size : PrimInt63.int) (a : A), + forall (size : N) (a : A), arr_length (arr_make size a) = - Uint63.min size max_arr_length. + N.min size max_arr_length. Parameter length_make_copy : - forall (size : PrimInt63.int) (a : A) (t: array A) (initlen: PrimInt63.int), + forall (size : N) (a : A) (t: array A) (initlen: N), arr_length (arr_make_copy size a t initlen) = - Uint63.min size max_arr_length. + N.min size max_arr_length. Parameter length_set : - forall (t : array A) (i : PrimInt63.int) (a : A), + forall (t : array A) (i : N) (a : A), arr_length t.[i<-a] = arr_length t. + +(* Some added axioms for set_gen *) +Parameter length_set_gen : + forall (t : array A) (i : N) (len: N) (gen: N -> A), + arr_length (arr_set_gen t i len gen) = arr_length t. + +Parameter arr_set_gen_lookup: + forall n len gen m i, + N.ltb i len -> + arr_get (arr_set_gen m n len gen) (N.add n i) = (gen i). + +Parameter arr_set_gen_lt: + forall n len gen m i, + N.ltb i n -> + arr_get (arr_set_gen m n len gen) i = arr_get m i. + +Parameter arr_set_gen_ge: + forall n len gen m i, + N.leb (N.add n len) i -> + arr_get (arr_set_gen m n len gen) i = arr_get m i. + Parameter get_copy : - forall (t : array A) (i : PrimInt63.int), + forall (t : array A) (i : N), (arr_copy t).[i] = t.[i]. Parameter length_copy : forall (t : array A), arr_length (arr_copy t) = arr_length t. Parameter array_ext : forall (t1 t2 : array A), arr_length t1 = arr_length t2 -> - (forall i : PrimInt63.int, - PrimInt63.ltb i (arr_length t1) = true -> t1.[i] = t2.[i]) -> + (forall i : N, + N.ltb i (arr_length t1) = true -> t1.[i] = t2.[i]) -> arr_default t1 = arr_default t2 -> t1 = t2. Parameter default_copy : forall (t : array A), arr_default (arr_copy t) = arr_default t. Parameter default_make : - forall (a : A) (size : PrimInt63.int), + forall (a : A) (size : N), arr_default (arr_make size a) = a. Parameter get_set_same_default : - forall (t : array A) (i : PrimInt63.int), + forall (t : array A) (i : N), t.[i<-arr_default t].[i] = arr_default t. Parameter get_not_default_lt : - forall (t : array A) (x : PrimInt63.int), - t.[x] <> arr_default t -> PrimInt63.ltb x (arr_length t) = true. + forall (t : array A) (x : N), + t.[x] <> arr_default t -> N.ltb x (arr_length t) = true. End Array. @@ -115,53 +138,68 @@ Section vector. Context {T: Type}. Implicit Types x : T. - - Definition Uint63_of_N n : PrimInt63.int := Uint63.of_Z (Z.of_N n). - Definition Uint63_to_N z : N := Z.to_N (Uint63.to_Z z). - Definition Uint63_of_positive p : PrimInt63.int := Uint63.of_Z (Zpos p). - Definition Uint63_to_positive z : positive := Z.to_pos (Uint63.to_Z z). + Context `{def_val: T}. Record vector := { v_data: array T; v_size: N; v_capacity: N; - v_init: T; + v_init: T := def_val; v_size_valid: v_size <= v_capacity; - v_capacity_eq: v_capacity = Uint63_to_N (arr_length v_data); + v_capacity_eq: v_capacity = (arr_length v_data); + v_uninitialised: + forall (i : N), + v_size <= i -> + i < v_capacity -> + arr_get v_data i = v_init; }. Definition vector_length vec : N := vec.(v_size). - Definition vector_make (len: N) x : vector. + Definition vector_make (len: N) : vector. Proof. remember (N.min len byte_limit) as capped_len. - refine (@Build_vector (arr_make (Uint63_of_N capped_len) x) capped_len capped_len x _ _). + refine (@Build_vector (arr_make capped_len def_val) capped_len capped_len _ _ _). - by lias. - rewrite length_make; subst. - unfold max_arr_length, Uint63_to_N, Uint63_of_N. - rewrite Uint63.min_spec Znat.Z2N.inj_min. - repeat rewrite of_Z_spec. - repeat rewrite Znat.Z2N.inj_mod => //; try by lias. - repeat rewrite Znat.N2Z.id. - rewrite N.mod_small; cbn; by lias. + unfold max_arr_length. + by lias. + - move => ???; by lias. Defined. Definition vector_lookup vec n : option T := - if n i Hlb Hub. + rewrite get_set_other => //; first by apply v_uninitialised. + unfold vector_length in Hn. + by lias. + - exact None. + Defined. + + Definition vector_update_gen (vec: vector) (n: N) (len: N) (gen: N -> T) : option vector. + Proof. + destruct (N.leb (N.add n len) (vector_length vec)) eqn:Hn. + - refine (Some (@Build_vector (arr_set_gen vec.(v_data) n len (fun offset => gen offset)) vec.(v_size) vec.(v_capacity) _ _ _)). + + by apply v_size_valid. + + rewrite length_set_gen. + by apply v_capacity_eq. + + move => i Hlb Hub. + rewrite arr_set_gen_ge => //; first by apply v_uninitialised. + unfold vector_length in Hn. + by lias. + - exact None. Defined. Lemma N_min_idem_r : forall n m, @@ -176,12 +214,11 @@ Section vector. | true => (fun _ => match newsize <=? vec.(v_capacity) as p2 return (newsize <=? vec.(v_capacity) = p2) -> _ with | true => - (fun _ => Some (@Build_vector vec.(v_data) newsize vec.(v_capacity) vec.(v_init) _ _)) + (fun _ => Some (@Build_vector vec.(v_data) newsize vec.(v_capacity) _ _ _)) | false => let new_capacity := (N.min (N.max newsize (vec.(v_capacity) * 2%N)) byte_limit) in - let x := vec.(v_init) in - let new_vd := arr_make_copy (Uint63_of_N new_capacity) x vec.(v_data) (Uint63_of_N vec.(v_size)) in - (fun _ => Some (@Build_vector new_vd newsize new_capacity x _ _)) + let new_vd := arr_make_copy new_capacity def_val vec.(v_data) vec.(v_size) in + (fun _ => Some (@Build_vector new_vd newsize new_capacity _ _ _)) end (Logic.eq_refl (newsize <=? vec.(v_capacity)))) | false => (fun _ => None) end (Logic.eq_refl (newsize <=? byte_limit)). @@ -191,17 +228,25 @@ Section vector. Next Obligation. by apply v_capacity_eq. Qed. + Next Obligation. + unfold vector_length in *. + apply v_uninitialised; by lias. + Qed. Next Obligation. move/N.leb_spec0 in e0. by lias. Qed. Next Obligation. rewrite length_make_copy. - unfold Uint63_to_N, Uint63_of_N. - rewrite min_spec Znat.Z2N.inj_min of_Z_spec. - rewrite Znat.Z2N.inj_mod; try by lias. - rewrite Znat.N2Z.id. - rewrite N.mod_small; cbn; by lias. + unfold max_arr_length. + by lias. + Qed. + Next Obligation. + unfold vector_length in *. + rewrite get_make_copy_default => //; try by lias. + rewrite - v_capacity_eq. + apply/N.leb_spec0. + by apply v_size_valid. Qed. Lemma vector_size_bound: forall vec, @@ -210,9 +255,8 @@ Section vector. move => vec. specialize (@v_size_valid vec) as Hvalid. specialize (v_capacity_eq vec) as Hcap. - unfold Uint63_to_N in Hcap. rewrite Hcap in Hvalid. - specialize (leb_length (v_data vec)) as Hlenub; move/Uint63.lebP in Hlenub. + specialize (leb_length (v_data vec)) as Hlenub; move/N.leb_spec0 in Hlenub. unfold max_arr_length in Hlenub. clear Hcap. cbn in *; by lias. @@ -222,12 +266,13 @@ End vector. Section MemoryVec. - Definition memory_vec : Type := @vector byte. - Definition mv_length := @vector_length byte. - Definition mv_make n b := @vector_make byte b n. - Definition mv_lookup i v := @vector_lookup byte v i. - Definition mv_update i b v:= @vector_update byte v i b. - Definition mv_grow n v:= @vector_grow byte v n. + Definition memory_vec : Type := @vector byte wasm_memory_default_byte. + Definition mv_length := @vector_length byte wasm_memory_default_byte. + Definition mv_make n := @vector_make byte wasm_memory_default_byte n. + Definition mv_lookup i v := @vector_lookup byte wasm_memory_default_byte v i. + Definition mv_update i b v := @vector_update byte wasm_memory_default_byte v i b. + Definition mv_update_gen i n gen m := @vector_update_gen byte wasm_memory_default_byte m i n gen. + Definition mv_grow n v:= @vector_grow byte wasm_memory_default_byte v n. Lemma mv_lookup_ib: forall mem i, @@ -256,17 +301,17 @@ Section MemoryVec. Qed. Lemma mv_make_length: - forall b len, mv_length (mv_make b len) = N.min len byte_limit. + forall len, mv_length (mv_make len) = N.min len byte_limit. Proof. done. Qed. Lemma mv_make_lookup: - forall i len b, + forall i len, (i < N.min len byte_limit) -> - mv_lookup i (mv_make b len) = Some b. + mv_lookup i (mv_make len) = Some wasm_memory_default_byte. Proof. - move => i len b Hlen /=. + move => i len Hlen /=. unfold mv_lookup, vector_lookup. setoid_rewrite mv_make_length. move/N.ltb_spec0 in Hlen; rewrite Hlen => /=. @@ -279,67 +324,46 @@ Lemma mv_update_length : mv_update i b mem = Some mem' -> mv_length mem' = mv_length mem. Proof. - move => mem mem' i b Hupdate. - unfold mv_update, vector_update in Hupdate. - by remove_bools_options. + move => mem mem' i b. + rewrite /mv_update /vector_update. + simplify_dependent_case. + by move => [<-] /=. Qed. - Lemma mv_update_lookup : - forall mem mem' i b, - mv_update i b mem = Some mem' -> - mv_lookup i mem' = Some b. - Proof. - move => mem mem' i b Hupdate. - unfold mv_lookup, vector_lookup. - erewrite mv_update_length; eauto. - unfold mv_update, vector_update in *. - remove_bools_options => /=. - rewrite Hif. - rewrite get_set_same => //. - unfold vector_length in Hif. - specialize (v_capacity_eq mem) as Hcap. - specialize (@v_size_valid _ mem) as Hsize. - move/N.ltb_spec0 in Hif. - apply/ltbP. - unfold Uint63_of_N. - unfold Uint63_to_N in Hcap. - rewrite of_Z_spec. - apply (f_equal Z.of_N) in Hcap. - rewrite Znat.Z2N.id in Hcap. - - rewrite - Hcap. - assert (Z.of_N i mod wB <= Z.of_N i)%Z as Hbound. - { apply Z.mod_le; by lias. } - (* lots of transitivity *) - by lias. - - specialize (to_Z_bounded (arr_length (v_data mem))). - by lias. - Qed. +Lemma mv_update_lookup : + forall mem mem' i b, + mv_update i b mem = Some mem' -> + mv_lookup i mem' = Some b. +Proof. + move => mem mem' i b. + rewrite /mv_lookup /vector_lookup. + move => Hupdate. + erewrite mv_update_length; eauto. + unfold mv_update, vector_update in Hupdate. + simplify_dependent_case_hyp Hupdate. + move => [<-] /=. + rewrite Hdep_case get_set_same => //. + unfold vector_length in Hdep_case. + specialize (v_capacity_eq mem) as Hcap. + specialize (@v_size_valid _ _ mem) as Hsize. + by lias. +Qed. + Lemma mv_update_lookup_ne: forall mem mem' i j b, i <> j -> mv_update j b mem = Some mem' -> mv_lookup i mem' = mv_lookup i mem. Proof. - move => mem mem' i j b Hneq Hupdate. + move => mem mem' i j b Hneq. unfold mv_lookup, vector_lookup. - unfold mv_update, vector_update in Hupdate. - remove_bools_options => /=. - move/N.ltb_spec0 in Hif. + unfold mv_update, vector_update. + simplify_dependent_case. + move => [<-] /=. unfold vector_length. destruct (i //. rewrite get_set_other => //. - unfold Uint63_of_N. - move => Hinjeq. - unfold vector_length in Hif. - move/N.ltb_spec0 in Hindex. - specialize (@vector_size_bound _ mem) as Hsizebound. - assert (i < byte_limit) as Hiub; first by lias. - assert (j < byte_limit) as Hjub; first by lias. - apply (f_equal to_Z) in Hinjeq. - do 2 (rewrite of_Z_spec in Hinjeq). - cbn in *. - do 2 (rewrite Z.mod_small in Hinjeq => //; last by lias). by lias. Qed. @@ -350,12 +374,7 @@ Lemma mv_grow_length : Proof. move => n mem mem'. unfold mv_grow, vector_grow. - generalize (Logic.eq_refl ((vector_length mem + n) <=? byte_limit)). - generalize ((vector_length mem + n) <=? byte_limit) at 2 3. - case => Hub => //=. - generalize (Logic.eq_refl ((vector_length mem + n) <=? v_capacity mem)). - generalize ((vector_length mem + n) <=? v_capacity mem) at 2 3. - case => Hgrow //=; move => [<-] => /=; done. + do 2 simplify_dependent_case => //; move => [<-] => /=; done. Qed. Lemma mv_update_ib: @@ -363,11 +382,12 @@ Lemma mv_update_ib: (i < mv_length mem)%N -> mv_update i b mem <> None. Proof. - move => mem i b => /=. - rewrite /mv_length /mv_update /vector_update. - move => H. - apply N.ltb_lt in H. - by rewrite H. + move => mem i b Hlt => /=. + rewrite /mv_update /vector_update. + simplify_dependent_case. + unfold mv_length in Hlt. + apply N.ltb_lt in Hlt. + by lias. Qed. Lemma mv_update_oob: @@ -375,15 +395,80 @@ Lemma mv_update_oob: (i >= mv_length mem)%N -> mv_update i b mem = None. Proof. - move => mem i b => /=. - rewrite /mv_length /mv_update /vector_update. - move => H. - apply N.ge_le in H; move/N.leb_spec0 in H. - rewrite N.leb_antisym in H. - move/negPf in H. - by rewrite H. + move => mem i b Hge => /=. + rewrite /mv_update /vector_update. + simplify_dependent_case. + exfalso. + unfold mv_length in Hge. + by lias. Qed. +Lemma mv_update_gen_ib: + forall (n len : N) (gen : N -> byte) (m : vector), + n + len <= mv_length m -> mv_update_gen n len gen m <> None. +Proof. + move => n len gen m Hlt. + rewrite /mv_update_gen /vector_update_gen. + simplify_dependent_case. + unfold mv_length in Hlt. + apply N.leb_le in Hlt. + by lias. +Qed. + +Lemma mv_update_gen_oob: + forall (n len : N) (gen : N -> byte) (m : vector), + n + len > mv_length m -> mv_update_gen n len gen m = None. +Proof. + move => n len gen m Hgt. + rewrite /mv_update_gen /vector_update_gen. + simplify_dependent_case; exfalso. + move/N.leb_spec0 in Hgt. + by lias. +Qed. + +Lemma mv_update_gen_lookup: + forall n len gen m m' i, + mv_update_gen n len gen m = Some m' -> + N.lt i len -> + mv_lookup (N.add n i) m' = Some (gen i). +Proof. + move => n len gen m m' i Hupdate Hlt. + rewrite /mv_update_gen /vector_update_gen /vector_length in Hupdate. + simplify_dependent_case_hyp Hupdate. + move => [<-] => /=. + rewrite /mv_lookup /vector_lookup => /=. + replace (n + i + N.lt i n -> + mv_lookup i m' = mv_lookup i m. +Proof. + move => n len gen m m' i Hupdate Hlt. + rewrite /mv_update_gen /vector_update_gen /vector_length in Hupdate. + simplify_dependent_case_hyp Hupdate. + move => [<-] => /=. + rewrite /mv_lookup /vector_lookup => /=. + rewrite arr_set_gen_lt; by lias. +Qed. + +Lemma mv_update_gen_lookup_ge: + forall n len gen m m' i, + mv_update_gen n len gen m = Some m' -> + N.ge i (N.add n len) -> + mv_lookup i m' = mv_lookup i m. +Proof. + move => n len gen m m' i Hupdate Hlt. + rewrite /mv_update_gen /vector_update_gen /vector_length in Hupdate. + simplify_dependent_case_hyp Hupdate. + move => [<-] => /=. + rewrite /mv_lookup /vector_lookup => /=. + by rewrite arr_set_gen_ge; lias. +Qed. + Lemma mv_grow_lookup : forall i n mem mem', (i < mv_length mem)%N -> @@ -395,56 +480,70 @@ Proof. move/N.ltb_spec0 in Hlen. move/N.ltb_spec0 in Hlengrow. unfold mv_grow, vector_grow. - generalize (Logic.eq_refl ((vector_length mem + n) <=? byte_limit)). - generalize ((vector_length mem + n) <=? byte_limit) at 2 3. - case => Hub => //=. - generalize (Logic.eq_refl ((vector_length mem + n) <=? v_capacity mem)). - generalize ((vector_length mem + n) <=? v_capacity mem) at 2 3. - case => Hgrow //=; move => [<-] => /=; unfold mv_lookup, vector_lookup => /=; rewrite Hlen Hlengrow. + do 2 simplify_dependent_case; move => [<-] => /=; unfold mv_lookup, vector_lookup => /=; rewrite Hlen Hlengrow. - done. - - move/N.leb_spec0 in Hub. - move/N.leb_spec0 in Hgrow. - unfold mv_length in *. + - unfold mv_length, vector_length in *. + move/N.leb_spec0 in Hdep_case. + move/N.leb_spec0 in Hdep_case0. move/N.ltb_spec0 in Hlen. move/N.ltb_spec0 in Hlengrow. assert (i < byte_limit) as Hibound; first by lias. - specialize (@v_size_valid _ mem) as Hsize. + specialize (@v_size_valid _ _ mem) as Hsize. specialize (v_capacity_eq mem) as Hcap. - unfold Uint63_to_N in Hcap. rewrite Hcap in Hsize. - apply Znat.N2Z.inj_le in Hsize. - specialize (to_Z_bounded (arr_length (v_data mem))) as HZbound. - rewrite Znat.Z2N.id in Hsize => //; last by lias. - rewrite get_make_copy => //; unfold Uint63_of_N. - + apply/Uint63.ltbP. - repeat rewrite of_Z_spec. - do 2 (rewrite Z.mod_small; last by cbn; cbn in Hub; lias). - by lias. - + apply/Uint63.lebP. - rewrite of_Z_spec. - rewrite Z.mod_small; by lias. - + apply/Uint63.ltbP. - rewrite of_Z_spec. - rewrite Z.mod_small; last by cbn; cbn in Hibound; lias. - unfold vector_length in Hlen. + unfold vector_length in Hlen. + rewrite get_make_copy => //; by lias. +Qed. + +Lemma mv_grow_default: + forall (n len : N) (mem mem' : memory_vec) (i : N), + i < n -> + mv_grow n mem = Some mem' -> + mv_length mem = len -> + mv_lookup (len + i) mem' = Some wasm_memory_default_byte. +Proof. + move => n len mem mem' i Hlt Hgrow Hlen. + unfold mv_grow, vector_grow in *. + simplify_dependent_case_hyp Hgrow. + simplify_dependent_case; move => [<-] => /=; unfold mv_lookup, vector_lookup => /=; subst; unfold mv_length. + - replace (_ Some m - | b :: bs' => - match mem_update start_idx b m with - | Some m' => write_bytes m' (N.add start_idx 1%N) bs' - | None => None - end +(** write bytes to `m` starting at `start_idx` using a generator. More efficient than writing individual bytes and should almost always be used when applicable. *) +Definition write_bytes_gen (m : mem_t) (start_idx : N) (len: N) (gen: N -> byte) : option mem_t := + mem_update_gen start_idx len gen m. + +(** write bytes `bs` to `m` starting at `start_idx`. *) +Definition write_bytes (m : mem_t) (start_idx : N) (bs : bytes) : option mem_t := + write_bytes_gen m start_idx (N.of_nat (length bs)) + (fun n => + match lookup_N bs n with + | Some b => b + | None => #00 + end). + +Definition write_bytes_gen_meminst (m: meminst) (start_idx : N) (len: N) (gen: N -> byte) : option meminst := + match write_bytes_gen m.(meminst_data) start_idx len gen with + | Some md' => + Some (Build_meminst m.(meminst_type) md') + | None => None end. Definition write_bytes_meminst (m: meminst) (start_idx : N) (bs: bytes) : option meminst := @@ -59,7 +68,7 @@ Definition serialise_num (v : value_num) : bytes := #[deprecated(since="wasmcert-coq-v2.2", note="Use serialise_num instead.")] Definition bits := serialise_num. - + Definition ml_valid (m: mem_t) : Prop := N.modulo (mem_length m) page_size = 0%N. @@ -135,12 +144,17 @@ Definition vec_get_v128 (v: value_vec) : v128 := | VAL_vec128 vv => vv end. - Definition store (m : meminst) (n : N) (off : static_offset) (bs : bytes) (l : nat) : option meminst := if N.leb (n + off + N.of_nat l) (mem_length m) then write_bytes_meminst m (n + off) (bytes_takefill #00 l bs) else None. +Definition store_gen (m : meminst) (n : N) (off : static_offset) (l : N) (gen: N -> byte) : option meminst := + if N.leb (n + off + l) (mem_length m) + then + write_bytes_gen_meminst m (n + off) l gen + else None. + (* The first argument of wrap doesn't affect the opsem at all, so this is fine. Might need a change in the future if this behaviour changes. *) Definition store_packed := store. diff --git a/theories/properties.v b/theories/properties.v index 961d67c7..21aaf200 100644 --- a/theories/properties.v +++ b/theories/properties.v @@ -1289,7 +1289,7 @@ Ltac extract_listn := Section Host. -Context `{hfc: host_function_class} `{memory: Memory}. +Context `{hfc: host_function_class} `{memory: BlockUpdateMemory}. Lemma values_typing_size: forall s vs ts, values_typing s vs ts -> diff --git a/theories/subtyping_properties.v b/theories/subtyping_properties.v index 31f8c74b..a8af12ba 100644 --- a/theories/subtyping_properties.v +++ b/theories/subtyping_properties.v @@ -780,7 +780,7 @@ Ltac unify_principal := Section Host. -Context {hfc: host_function_class} `{memory: Memory}. +Context {hfc: host_function_class} `{memory: BlockUpdateMemory}. Lemma value_typing_ref_impl: forall s v t, value_typing s (VAL_ref v) t -> diff --git a/theories/type_preservation.v b/theories/type_preservation.v index 89a901d2..642c5f14 100644 --- a/theories/type_preservation.v +++ b/theories/type_preservation.v @@ -672,29 +672,24 @@ Proof. + by eapply IHn; eauto. Qed. -Lemma write_bytes_preserve_length: forall m pos str m', - write_bytes m pos str = Some m' -> +Lemma write_bytes_gen_preserve_length: forall m pos len gen m', + write_bytes_gen m pos len gen = Some m' -> memory.mem_length m = memory.mem_length m'. Proof. - move => m pos str. - move: m pos. - induction str; move => m pos m' Hwrite; simpl in *. - - by injection Hwrite as <-. - - remove_bools_options. - apply IHstr in Hwrite. - apply mem_update_length in Hoption. - by lias. + move => m pos len gen m' Hwrite. + unfold write_bytes_gen in Hwrite. + by apply mem_update_gen_length in Hwrite. Qed. -Lemma write_bytes_meminst_preserve_type: forall m pos str m', - write_bytes_meminst m pos str = Some m' -> +Lemma write_bytes_meminst_preserve_type: forall m pos len gen m', + write_bytes_gen_meminst m pos len gen = Some m' -> meminst_type m = meminst_type m' /\ mem_length m = mem_length m'. Proof. - move => m pos str m' Hwrite. - unfold write_bytes_meminst in Hwrite. + move => m pos len gen m' Hwrite. + unfold write_bytes_gen_meminst in Hwrite. remove_bools_options; split => //=. - by eapply write_bytes_preserve_length; eauto. + by eapply write_bytes_gen_preserve_length; eauto. Qed. Lemma reduce_inst_unchanged: forall hs s f es hs' s' f' es', diff --git a/theories/typing.v b/theories/typing.v index 2aa5b19d..05cbda9e 100644 --- a/theories/typing.v +++ b/theories/typing.v @@ -10,7 +10,7 @@ Unset Printing Implicit Defensive. Section Host. -Context `{hfc: host_function_class} `{memory: Memory}. +Context `{hfc: host_function_class} `{memory: BlockUpdateMemory}. (** std-doc: For the purpose of checking external values against imports, such values are classified by external types. The following auxiliary typing rules specify this typing relation relative to a store S in which the referenced instances live. diff --git a/theories/typing_inversion.v b/theories/typing_inversion.v index 54689771..05df865b 100644 --- a/theories/typing_inversion.v +++ b/theories/typing_inversion.v @@ -10,7 +10,7 @@ Unset Printing Implicit Defensive. Section Typing_inversion_be. -Context `{memory: Memory}. +Context `{memory: BlockUpdateMemory}. (* Some quality of life lemmas *) (* Upd: these lemmas are deprecated; it is encouraged to directly use subtyping rule. *) @@ -470,7 +470,7 @@ Ltac e_typing_ind HType := Section Typing_inversion_e. -Context `{hfc: host_function_class} `{memory: Memory}. +Context `{hfc: host_function_class} `{memory: BlockUpdateMemory}. (** Typing lemmas **) @@ -852,7 +852,7 @@ Ltac invert_e_typing := (* Some more complicated lemmas *) Section Typing_inversion_e. -Context `{hfc: host_function_class} `{memory: Memory}. +Context `{hfc: host_function_class} `{memory: BlockUpdateMemory}. (* inst_typing inversion *) Lemma inst_t_context_local_empty: forall s i C,