Skip to content

Add array_copy to heap_lang

Tej Chajed requested to merge tchajed/iris-coq:add-array-copy into master

Implements a function similar to C memcpy. The heap_lang spec and proof are inspired by https://gitlab.mpi-sws.org/iris/lambda-rust/blob/3b4ae69fa3be1344245245bf05e5e80e790e064d/theories/lang/lib/memcpy.v.

Fixes #293 (closed).

Merge request reports