VSU_main2linking with stdlib2 instead of with stdlib
#include <stddef.h> #include "stdlib.h" #include "stack2.h" #include "triang2.h" int main(void) { return triang(10); }and the only difference would be in the Makefile, the Unix ld or cc command would link the programs together with stdlib2.o instead of stdlib.o.
The VSU for main
Require Import VST.floyd.proofauto.
Require Import VST.floyd.VSU.
Require Import VC.main2.
Require VC.stdlib2 VC.stack2 VC.triang2.
Require VC.Spec_stdlib VC.Spec_stack VC.Spec_triang.
Require VC.VSU_stdlib2 VC.VSU_stack VC.VSU_triang.
#[export] Instance Compspecs: compspecs. make_compspecs VC.main2.prog. Defined.
Definition M : Spec_stdlib.MallocFreeAPD := VSU_stdlib2.M.
Definition STACK : Spec_stack.StackAPD := VSU_stack.STACK M.
Time Definition stacktriangVSU1 := ltac:(linkVSUs
(VSU_stack.StackVSU M) (VSU_triang.TriangVSU M STACK)).
(* 1.98 seconds to 6 seconds *)
Require Import VST.floyd.VSU.
Require Import VC.main2.
Require VC.stdlib2 VC.stack2 VC.triang2.
Require VC.Spec_stdlib VC.Spec_stack VC.Spec_triang.
Require VC.VSU_stdlib2 VC.VSU_stack VC.VSU_triang.
#[export] Instance Compspecs: compspecs. make_compspecs VC.main2.prog. Defined.
Definition M : Spec_stdlib.MallocFreeAPD := VSU_stdlib2.M.
Definition STACK : Spec_stack.StackAPD := VSU_stack.STACK M.
Time Definition stacktriangVSU1 := ltac:(linkVSUs
(VSU_stack.StackVSU M) (VSU_triang.TriangVSU M STACK)).
(* 1.98 seconds to 6 seconds *)
An alternate way to adjust the Exports of a VSU
Check restrictExports. (* : VSU E Imports p Exports GP -> funspecs -> Type *)
Check prove_restrictExports. (*
: forall (v: VSU ?E ?Imports ?p ?Exports ?GP )
(Exports': funspecs),
list_norepet (map fst Exports') ->
Forall (funspec_sub_in ?Exports) Exports' ->
restrictExports v Exports' *)
Check prove_restrictExports. (*
: forall (v: VSU ?E ?Imports ?p ?Exports ?GP )
(Exports': funspecs),
list_norepet (map fst Exports') ->
Forall (funspec_sub_in ?Exports) Exports' ->
restrictExports v Exports' *)
Given a VSU v, restrictExports v Exports' is the type of a new VSU
whose Exports list has been replaced by Exports'.
The lemma prove_restrictExports says,
We will now use this to build stacktriangVSU.
- if Exports' does not have any repeated identifiers, and
- if for every (id,fspec') in Exports', there is an (id,fspec) in Exports such that funspec_sub (fspec,fspec'),
- then there is a new VSU whose exports is Exports'.
Eval simpl in VSU_Exports stacktriangVSU1. (* newstack, push, pop, triang *)
Lemma stacktriangVSU:
restrictExports stacktriangVSU1
(Spec_triang.TriangASI M).
Proof.
prove_restrictExports.
Lemma stacktriangVSU:
restrictExports stacktriangVSU1
(Spec_triang.TriangASI M).
Proof.
prove_restrictExports.
At this point, we must prove funspec_sub for every (id,fspec') in
the TriangASI. There is just one, namely triang_spec. So just
one bulleted subgoal. And because (in this use of restrictExports)
we did not change the funspec between Exports and Exports',
we can use funspec_sub_refl to prove it.
- apply funspec_sub_refl.
Qed.
Eval hnf in VSU_Exports stacktriangVSU. (* newstack, push, pop, triang *)
Qed.
Eval hnf in VSU_Exports stacktriangVSU. (* newstack, push, pop, triang *)
For more significant uses of funspec_sub to adapt and abstract VSUs, see:
"Verified Software Units", by Lennart Beringer, ESOP'21.
End of digression about restrictExports
Time Definition coreVSU :=
privatizeExports
ltac:(linkVSUs stacktriangVSU VSU_stdlib2.MallocFreeVSU)
[stdlib._malloc; stdlib._free; stdlib._exit] .
Time Definition whole_prog := ltac:(QPlink_progs (QPprog prog) (VSU_prog coreVSU)).
privatizeExports
ltac:(linkVSUs stacktriangVSU VSU_stdlib2.MallocFreeVSU)
[stdlib._malloc; stdlib._free; stdlib._exit] .
Time Definition whole_prog := ltac:(QPlink_progs (QPprog prog) (VSU_prog coreVSU)).
The funspec for main is just as it was in VSU_main.
Definition main_spec :=
DECLARE _main
WITH gv: globals
PRE [ ] main_pre whole_prog tt gv
POST[ tint ]
PROP()
RETURN (Vint (Int.repr 55))
SEP(TT).
Definition Vprog: varspecs := QPvarspecs whole_prog.
Definition Main_imports: funspecs := Spec_triang.TriangASI M.
Definition Main_Gprog : funspecs := main_spec :: Main_imports.
Lemma body_main: semax_body Vprog Main_Gprog f_main main_spec.
DECLARE _main
WITH gv: globals
PRE [ ] main_pre whole_prog tt gv
POST[ tint ]
PROP()
RETURN (Vint (Int.repr 55))
SEP(TT).
Definition Vprog: varspecs := QPvarspecs whole_prog.
Definition Main_imports: funspecs := Spec_triang.TriangASI M.
Definition Main_Gprog : funspecs := main_spec :: Main_imports.
Lemma body_main: semax_body Vprog Main_Gprog f_main main_spec.
Identical to the proof of body_main in VSU_main.
(* FILL IN HERE *) Admitted.
Definition MainComp: MainCompType nil ltac:(QPprog prog) coreVSU whole_prog (snd main_spec) emp.
Proof.
mkComponent prog.
solve_SF_internal body_main.
Qed.
Lemma WholeComp: WholeCompType coreVSU MainComp.
Proof. proveWholeComponent. Qed.
Lemma WholeProgSafe: WholeProgSafeType WholeComp tt.
Proof. proveWholeProgSafe. Qed.
Eval red in WholeProgSafeType WholeComp tt.
(* 2023-03-25 11:30 *)
Definition MainComp: MainCompType nil ltac:(QPprog prog) coreVSU whole_prog (snd main_spec) emp.
Proof.
mkComponent prog.
solve_SF_internal body_main.
Qed.
Lemma WholeComp: WholeCompType coreVSU MainComp.
Proof. proveWholeComponent. Qed.
Lemma WholeProgSafe: WholeProgSafeType WholeComp tt.
Proof. proveWholeProgSafe. Qed.
Eval red in WholeProgSafeType WholeComp tt.
(* 2023-03-25 11:30 *)