Commit 6b43b5a5 authored by Michael Sammler's avatar Michael Sammler

Initial commit

parents
*.vo
*.vio
*.v.d
.coqdeps.d
*.glob
*.cache
*.aux
\#*\#
.\#*
*~
*.bak
.coq-native/
build-dep/
Makefile.coq
Makefile.coq.conf
_opam
image: ralfjung/opam-ci:opam2
stages:
- build
variables:
CPU_CORES: "10"
.template: &template
stage: build
script:
- git clone https://gitlab.mpi-sws.org/FP/iris-ci.git ci -b opam2
- ci/buildjob
cache:
key: "$CI_JOB_NAME"
paths:
- opamroot/
only:
- master
- /^ci/
except:
- triggers
- schedules
## Build jobs
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
# build-coq.8.8.0:
# <<: *template
# variables:
# OPAM_PINS: "coq version 8.8.0"
# build-coq.8.7.2:
# <<: *template
# variables:
# OPAM_PINS: "coq version 8.7.2"
All files in this development are distributed under the terms of the
BSD license, included below.
------------------------------------------------------------------------------
BSD LICENCE
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
* Neither the name of the <organization> nor the
names of its contributors may be used to endorse or promote products
derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq
+@make -f Makefile.coq all
.PHONY: all
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories $$(test -d tests && echo tests) \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete
rm -f Makefile.coq
.PHONY: clean
# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile awk.Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
# Install build-dependencies
build-dep/opam: opam Makefile
@echo "# Creating build-dep package."
@mkdir -p build-dep
@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
build-dep: build-dep/opam phony
@# We want opam to not just instal the build-deps now, but to also keep satisfying these
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything.
@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
@# package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
((! opam --version | grep "^1\." > /dev/null) || ( \
echo "# Reinstalling build-dep package." && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \
))
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
_CoqProject: ;
awk.Makefile: ;
opam: ;
# Phony wildcard targets
phony: ;
.PHONY: phony
# Coq development for "The High-Level Benefits of Low-Level Sandboxing"
This is the Coq development accompanying "The High-Level Benefits of Low-Level Sandboxing".
## Prerequisites
This version is known to compile with Coq 8.9.0 and 8.9.1 but should
also work with other versions supported by Iris.
## Building from source
When building from source, we recommend to use opam (1.2.2 or newer) for
installing the dependencies. This requires the following two repositories:
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
Once you got opam set up, run `make build-dep` to install the right versions
of the dependencies.
Run `make -jN` to build the full development, where `N` is the number of your
CPU cores.
## Structure
The proofs of the main theorems can be found in the following files:
| Theorem | file | name in Coq |
|--------------------------------------|-------------------------------|----------------|
| Theorem 2 (Soundness of the sandbox) | theories/lang/adversary.v | type_adv_expr' |
| Theorem 3 (Robust Safety) | theories/lang/robust_safety.v | robust_safety |
- The main proofs are in the folder [lang](theories/lang).
- [lang.v](theories/lang/lang.v): Definition of the language
lambda-sandbox and its operational semantics.
- [syscall_policies.v](theories/lang/syscall_policies.v): Definition
of system call policies.
- [heap.v](theories/lang/heap.v) and
[lifting.v](theories/lang/lifting.v): Instantiation of Iris and
lifting lemmata for working with WP.
The stronger version of P-syscall mentioned in the paper is
`wp_syscall` in [lifting.v](theories/lang/lifting.v).
- [type.v](theories/lang/type.v): Definition of the semantic type
system, basic types like functions and products and typing rules.
It contains the following typing rules from the paper (the first
column is always the name from the paper and the second column the
name in this Coq development):
| Rule | Definition/Lemma |
|-------------|------------------|
| T-val | type_val |
| T-stuck | type_stuck |
| T-let | type_let |
| T-seq | type_seq |
| T-any | any |
| T-int | int |
| T-any-copy | any_copy |
| T-int-copy | int_copy |
| T-add | type_plus |
| T-alloc | type_new |
| T-write | type_write |
| T-read-copy | type_read_copy |
| T-read | type_read |
| T-fn-copy | fn_copy |
| T-fn | type_fn |
| T-call | type_fn_call |
| T-low-ptr | lowptr |
| T-low-copy | lowptr_copy |
| T-alloc-low | type_new_low |
| T-free-low | type_delete_low |
| T-write-low | type_write_low |
| T-read-low | type_read_low |
Note that functions in the Coq development have a privilege
parameter, which is implicitly always High in the rules presented
in the paper.
- [adversary.v](theories/lang/adversary.v): Proof of Theorem 2
(Soundness of the sandbox) as `type_adv_expr'` and T-gated-call
as `type_gated_call`.
- [robust_safety.v](theories/lang/robust_safety.v): Proof of Theorem
3 (Robust Safety) as `robust_safety`. It also contains a comment
explaining the statement of the theorem.
- [wrapper.v](theories/lang/wrapper.v): Definition of import and
export wrappers and implementation of the wrappers for the basic
types.
| Wrapper | Definition |
|-----------------|----------------|
| any.import | import_any |
| any.export | export_any |
| int.import | import_int |
| int.export | export_int |
| LowPtr.import | import_lowptr |
| LowPtr.export | export_lowptr |
| product.import | import_product |
| product.export | export_product |
- [interface.v](theories/lang/interface.v): Definition of
`wrap_import` and `wrap_export` and corresponding typing rules.
| Definition/Rule | Definition/Lemma |
|-------------------|--------------------------------------|
| wrap_import | wrap_import |
| T-wrap-import | type_wrap_import |
| wrap_export | wrap_export |
| T-wrap-export | type_wrap_export |
| main_file | untrusted_main / type_untrusted_main |
- [lib](theories/lang/lib) contains additional libraries.
- [file.v](theories/lang/lib/file.v): Definition of the file system call
policy, the file related functions and the associated typing rules.
| Definition/Rule | Definition/Lemma |
|-----------------|--------------------------|
| fileSP | fileSP |
| A_file | file_axioms |
| I_fileSP | fileSPG |
| T-file-open | type_file_open |
| T-file-read | type_file_read |
| T-file-close | type_file_close |
| do_open | do_open / type_do_open |
| do_read | do_read / type_do_read |
| do_close | do_close / type_do_close |
- [sum.v](theories/lang/lib/sum.v): Sum types and `option`.
| Definition | Definition/Lemma |
|-----------------|----------------------|
| option | option |
| unwrap | unwrap / type_unwrap |
- [mutex.v](theories/lang/lib/mutex.v): Mutex implementation.
| Definition/Rule | Definition/Lemma |
|-----------------|------------------------|
| mutex | mutex |
| mutex copy | mutex_copy |
| guard | mutexguard |
| acquire | acquire / type_acquire |
| release | release / type_release |
- [int_map.v](theories/lang/lib/int_map.v): Integer map and associated operations.
| Definition | Definition/Lemma |
|------------|----------------------------------|
| map | int_map |
| map_put | int_map_put / type_int_map_put |
| map_take | int_map_take / type_int_map_take |
- [sealing.v](theories/lang/lib/sealing.v): Wrappers for dynamic sealing.
| Definition/Rule | Definition/Lemma |
|---------------------------------|------------------|
| T-sealed | sealed |
| sealed.import / T-sealed-import | import_sealed |
| sealed.export / T-sealed-export | export_sealed |
- The folder [examples](theories/examples) contains examples.
- The `unsafe_print` example can be found in [unsafe_print.v](theories/examples/unsafe_print.v).
| Definition/Rule | Definition/Lemma |
|-----------------------|--------------------|
| printSP | printSP |
| main_sandbox | main |
| T-lessthan1000 | less_than_1000 |
| T-print | type_unsafe_print |
| print | print / type_print |
| robust safety theorem | print_safe |
- The file system example can be found in [sealing.v](theories/examples/sealing.v).
| Definition/Rule | Definition/Lemma |
|-----------------------|--------------------|
| robust safety theorem | expose_file_safe |
## Presentational differences to the paper
- This Coq development does not define typing contexts explicitly, but
directly works with the semantic interpretation of typing contexts.
This means that
```
v1 ◁ int, v2 ◁ int |=_p e : bool | v1 ◁ int, v2 ◁ int
```
is represented as
```
v1 ◁ int -∗ v2 ◁ int -∗ typed_expr p bool (v1 ◁ int ∗ v2 ◁ int) e
```
This makes working with the typing judgment a lot more pleasant
since the type assignments can be manipulated with the standard Iris
tactics. This also means that the T-weaken and T-copy typing
rules are not explicitly formalized in this Coq development since
they are implicitly provided by Iris.
- For presentation purposes the paper glosses over some of the details
of the handling of surface values. More concretely, in the paper
types are defined as a function from `SurfaceVal` to `iProp` to make
the definition of types cleaner and easier to follow. However, such
a function is very cumbersome to use in Coq as one would always need
to prove that a value is a surface value to be able to state that it
is well-typed. Thus, in this formalization each type is defined via
a function from `Val` to `iProp` with the additional requirement
that each well-typed value is actually a surface value (see `type`
in [type.v](theories/lang/type.v)). This means the obligation to
show that `v` in `v ◁ ty` is a surface value can be handled once in
the typing rules for `ty` instead of everytime `v ◁ ty` is
used.
## Extensions to the paper
- This Coq development provides a mechanism to merge different system
call policies (`mergeSP` and `mergeSPG` in
[syscall_policies.v](theories/lang/syscall_policies.v)), which
allows to link functions that are verfied with regard to different
system call policies as long as the system call policies talk about
different system calls. See `use_file_assert_safe` in
[file.v](theories/examples/file.v) for an example.
- This Coq development includes additional typing rules like
`type_case` in [type.v](theories/lang/type.v) which are not
discussed in the paper.
-Q theories sandbox
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/lang/base.v
theories/lang/lang.v
theories/lang/robust_safety.v
theories/lang/syscall_policies.v
theories/lang/notation.v
theories/lang/substitution.v
theories/lang/tactics.v
theories/lang/lifting.v
theories/lang/heap.v
theories/lang/type.v
theories/lang/proofmode.v
theories/lang/macro_helper.v
theories/lang/wrapper.v
theories/lang/interface.v
theories/lang/adversary.v
theories/lang/unfold.v
theories/lang/lib/memcpy.v
theories/lang/lib/assert.v
theories/lang/lib/file.v
theories/lang/lib/product.v
theories/lang/lib/sum.v
theories/lang/lib/mutex.v
theories/lang/lib/int_map.v
theories/lang/lib/sealing.v
theories/examples/heap.v
theories/examples/type.v
theories/examples/const_int.v
theories/examples/file.v
theories/examples/sealing.v
theories/examples/small_int.v
theories/examples/unsafe_print.v
A formal model of a sandbox.
opam-version: "1.2"
name: "coq-sandbox"
version: "dev"
maintainer: "Michael Sammler <msammler@mpi-sws.org>"
description: "Coq development for The High-Level Benefits of Low-Level Sandboxing"
license: "BSD"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/sandbox'" ]
depends: [
"coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
]
((nil . ((eval . (flycheck-mode 0)))))
From sandbox.lang Require Import lang notation proofmode type wrapper adversary robust_safety interface unfold.
From sandbox.lang.lib Require Import assert product.
Section const_int.
Context `{sandboxG Σ}.
Definition use_2 : val :=
λ: ["v"], let: "cmp" := "v" = #2 in assert ["cmp"].
Lemma type_use_2 :
use_2 fn High [# const_int 2] any.
Proof.
iApply type_fn => //. solve_surface_expr. do 2 iModIntro. iIntros (xl).
inv_vec xl => v /=. iIntros "[Hv _]". simpl_subst.
iApply (type_let with "[Hv]"). by iApply (type_eq with "Hv").
iIntros (cmp) "Hcmp _". case_bool_decide => //=. simpl_subst.
iApply type_fn_call => //. by iApply type_assert.
by iSplitL.
Qed.
Definition use_2_call : val :=
λ: [], let: "v" := wrap_import (nroot.@"use_2_call") [] (const_int 2) [] in
use_2 ["v"].
Lemma type_use_2_call :
use_2_call fn High [# ] any.
Proof.
Local Opaque use_2.
iApply type_fn => //. do 2 iModIntro. iIntros (xl).
inv_vec xl. iIntros "_". simpl_subst.
iApply type_let. {
iApply type_fn_call => //. iApply (type_wrap_import _ []) => //=. done.
}
iIntros (v) "? _". simpl_subst.
iApply type_fn_call => //. by iApply type_use_2. by iFrame.
Qed.
Local Transparent wrap_import wrap_export import_const_int import_int export_lowptr export_int import_any export_product import_product export_any.
Definition use_2_export : val := wrap_export use_2 [const_int 2] any.
Definition use_2_export_val : val.
Proof using.
let t:= eval unfold use_2_export, wrap_export in use_2_export in solve_unfold t.
Unshelve. apply _.
Defined.
Lemma use_2_export_val_eq : use_2_export_val = use_2_export.
Proof. by apply: recv_f_equal. Qed.
Definition use_2_call_export : val := wrap_export use_2_call [] any.
Definition use_2_call_export_val : val.
Proof using.
let t:= eval unfold use_2_call_export, wrap_export in use_2_call_export in solve_unfold t.
Unshelve. apply _.
Defined.
Lemma use_2_call_export_val_eq : use_2_call_export_val = use_2_call_export.
Proof. by apply: recv_f_equal. Qed.
End const_int.
Definition interface (u : interface_map) := λ p, match p with
| Low => u
| High =>
<[ nroot.@ "1" := use_2_export_val]> $
<[ nroot.@ "2" := use_2_call_export_val]>
end.
Lemma use_2_interface_safe u t2 σ2 :
let _ := SyscallG (λ _, True) in
map_Forall (λ _ v, surface_val v) u
rtc erased_step ([(untrusted_main_val [] at High)%E], initial_state (interface u)) (t2, σ2)
is_good abortSP σ2.
Proof.
set Σ : gFunctors := #[sandboxΣ]. move=>???.
eapply (robust_safety Σ _ abortSP ) => //.
move => ?. exists (liftSPG Σ abortSP). split => //. split => //???.
rewrite untrusted_main_val_eq use_2_export_val_eq use_2_call_export_val_eq.
iIntros "_ !#". iSplit; last by iApply type_untrusted_main.
rewrite !big_sepM_insert => //. 2:{
rewrite lookup_insert_None; split => //.
by intros [??]%ndot_inj.
}
do ! iSplit => //.
- iExists _. iApply (type_wrap_export _ [const_int 2] _ _ type_use_2) => //=.
- iExists _. iApply (type_wrap_export _ [] _ _ type_use_2_call) => //=.
Qed.
Print Assumptions use_2_interface_safe.
From sandbox.lang Require Import lang notation proofmode type robust_safety.
From sandbox.lang.lib Require Import file assert.
Section file.
Context `{sandboxG Σ} `{fileG Σ} `{inSP Σ fileSPG}.
Definition use_file : val :=
λ: [], let: "f" := do_open [ #1 ] in
let: "p" := do_read ["f"] in
let: "f" := ! ("p" + #0) in
do_close ["f"].
Lemma type_use_file:
use_file fn High [# ] any.
Proof.
Local Opaque do_open do_read do_close.
iApply type_fn => //. do 2 iModIntro.
iIntros (xl). inv_vec xl => /=. iIntros "_". simpl_subst.
iApply (type_let with "[]"). {
iApply (type_fn_call $! type_do_open with "[]") => //.
by iSplit. }
iIntros (f) "Hf _". simpl_subst.
iApply (type_let with "[Hf]"). {
iApply (type_fn_call $! type_do_read with "[Hf]") => //.
by iFrame. }
iIntros (f2) "Hf _". simpl_subst.
iApply (type_let with "[Hf]"). {
by iApply type_read => //.
}
iIntros (?) "Hv _". simpl_subst.
iApply (type_fn_call $! type_do_close) => //.
by iFrame.
Qed.
Definition use_file_assert : val :=
λ: [], use_file [ ];; assert [ #1 ].
Lemma type_use_file_assert:
use_file_assert fn High [# ] any.
Proof.
Local Opaque use_file.
iApply type_fn => //. do 2 iModIntro. iIntros (xl).
inv_vec xl => /=. iIntros "_". simpl_subst.
iApply (type_let with "[]"). {
by iApply (type_fn_call $! type_use_file with "[]"). }
iIntros (?) "_ _". simpl_subst.
iApply (typed_expr_mono any True%I) => //. iIntros (?). by iApply ty_surface.
iApply (type_fn_call $! (type_assert _)) => //. by iSplitL.
Qed.
End file.
Definition interface (u : interface_map) := λ p, match p with
| Low => u
| High =>
end.
Lemma use_file_safe u t2 σ2 :
let _ := SyscallG file_axioms in
map_Forall (λ _ v, surface_val v) u
rtc erased_step ([(use_file [] at High)%E], initial_state (interface u)) (t2, σ2)
is_good fileSP σ2.
Proof.
set Σ : gFunctors := #[sandboxΣ; fileΣ].
eapply (robust_safety Σ _ _ ) => // Hpre.
exists fileSPG. split_and? => //? HSP HPre.
iIntros "_ !#". iSplit => //.
iApply @type_use_file. rewrite HSP HPre. by apply insp_reflexive.
Qed.
Lemma use_file_assert_safe u t2 σ2 :
let _ := SyscallG file_axioms in
map_Forall (λ _ v, surface_val v) u
rtc erased_step ([(use_file_assert [] at High)%E], initial_state (interface u)) (t2, σ2)
is_good (mergeSP fileSP abortSP) σ2.
Proof.
set Σ : gFunctors := #[sandboxΣ; fileΣ].
eapply (robust_safety Σ _ (mergeSP fileSP abortSP) ) => // ?.
exists (mergeSPG Σ fileSPG (liftSPG Σ abortSP)).
split => //. split => // ?. by rewrite /= right_id. move => HSP HP.
iIntros "_ !#". iSplit => //.
iApply @type_use_file_assert. rewrite HSP HP. by apply _.
Qed.
Print Assumptions use_file_safe.
Print Assumptions use_file_assert_safe.
From sandbox.lang Require Import lang notation proofmode.
Section examples.
Context `{sandboxG Σ}.
Definition assert_int : val :=
λ: ["x"], "x" + #1;; #.
Lemma assert_int_wp p E v:
{{{ True }}}
assert_int [ v ] at p @ E ?
{{{(n : Z), RET # at p; v = #n }}}.
Proof.
iIntros (Φ) "_ HΦ".
wp_rec.
wp_bind (BinOp _ _ _).
move: v => [|*]; last by solve_stuck.
move => [|?|n]; [solve_stuck..|].
wp_op. wp_seq.
by iApply "HΦ".
Qed.
Definition read_write_high : expr :=
let: "l" := Alloc High #1 in
"l" <- #0;;
let: "v" := !"l" in
Free #1 "l";;
"v".
Example read_write_high_wp :
{{{ True }}}
read_write_high at High ?
{{{ RET #0 at High; True }}}.
Proof.
rewrite /read_write_high. iIntros (Φ) "_ HΦ".
wp_alloc_high l as "Hl" "Hlfree". rewrite heap_mapsto_vec_singleton.
wp_let.
wp_write_high.
wp_read_high.
wp_let.
rewrite -heap_mapsto_vec_singleton.
wp_free_high => //.
by iApply "HΦ".
Qed.
Definition read_write_low : expr :=
let: "l" := Alloc Low #1 in
"l" <- #0;;
let: "v" := !"l" in
"l" <- "v";;
assert_int [ "v" ];;
withcont: "end" :
if: "v" = #0 then "end" [ "v" ] else "end" [ #0 ]
cont: "end" ["v"] :=
Free #1 "l";;
"v".
Example read_write_low_wp :
{{{ True }}}
read_write_low at Low
? {{{ RET #0 at Low; True }}}.
Proof.
rewrite /read_write_low. iIntros (Φ) "_ HΦ".
wp_alloc_low l => Hl.
wp_let.
wp_write_low.
wp_read_low v => ?. wp_let.
wp_write_low.
wp_apply assert_int_wp => //. iIntros (n ->). wp_seq.
wp_rec.
wp_op.
case_bool_decide as Hn; wp_case;
wp_rec; wp_free_low; rewrite ? Hn;
by iApply "HΦ".
Qed.
End examples.
From sandbox.lang Require Import lang notation proofmode type syscall_policies robust_safety wrapper interface unfold.
From sandbox.lang.lib Require Import file assert sealing product.
Definition seal_name : namespace := nroot .@ "file".
Section sealing.
Context `{sandboxG Σ} `{fileG Σ} `{inSP Σ fileSPG}.
Lemma type_do_open_sealed : do_open fn High [# int] (sealed seal_name file).
Proof. iApply type_do_open. Qed.
Lemma type_do_read_sealed : do_read fn High [# (sealed seal_name file)] (product [sealed seal_name file; any]).
Proof. iApply type_do_read. Qed.
Lemma type_do_close_sealed : do_close fn High [# (sealed seal_name file)] any.
Proof. iApply type_do_close. Qed.
Definition do_open_export : val := wrap_export do_open [# int] (sealed seal_name file).
Definition do_read_export : val := wrap_export do_read [# (sealed seal_name file)] (product [sealed seal_name file; any]).
Definition do_close_export : val := wrap_export do_close [# (sealed seal_name file)] any.
(* we now have the wrapped functions but we cannot use them directly
in expose_file_safe as they depend on sandboxG, which is not
available where we want to use these functions in expose_file_safe.
So we need this hack of defining do_open_export_val which is the
same as do_open_export as do_open_export_val_eq shows, but it does
not depend on sandboxG. *)
Local Transparent wrap_import wrap_export import_const_int import_int export_lowptr export_int import_any export_product import_product export_any export_sealed import_sealed.
Definition do_open_export_val : val.
Proof using.
let t:= eval unfold do_open_export, wrap_export in do_open_export in solve_unfold t.
Unshelve. apply _.