Commit 743e313b authored by Michael Sammler's avatar Michael Sammler

add missing proofs

parent a7e4f15b
From refinedc.typing Require Import typing.
From refinedc.tutorial.t06_struct Require Import generated_code.
From refinedc.tutorial.t06_struct Require Import generated_spec.
Set Default Proof Using "Type".
(* Generated from [tutorial/t06_struct.c]. *)
Section proof_argtest.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [argtest]. *)
Lemma type_argtest (blue getblue : loc) :
blue ◁ᵥ blue @ function_ptr type_of_blue -
getblue ◁ᵥ getblue @ function_ptr type_of_getblue -
typed_function (impl_argtest blue getblue) type_of_argtest.
Proof.
start_function "argtest" ([]).
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "argtest" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "argtest".
Qed.
End proof_argtest.
From refinedc.typing Require Import typing.
From refinedc.tutorial.t06_struct Require Import generated_code.
From refinedc.tutorial.t06_struct Require Import generated_spec.
Set Default Proof Using "Type".
(* Generated from [tutorial/t06_struct.c]. *)
Section proof_getblue.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [getblue]. *)
Lemma type_getblue :
typed_function impl_getblue type_of_getblue.
Proof.
start_function "getblue" ([[r g] b]) => arg_b.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "getblue" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "getblue".
Qed.
End proof_getblue.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment