(* * Copyright (c) 2017-present, * Programming Research Laboratory (ROPAS), Seoul National University, Korea * This software is distributed under the term of the BSD-3 clause license. *) (** * Type of user's proof obligation *) (** The module type defined in this file presents user's responsibility for correctness proof of the validator. *) Set Implicit Arguments. Require Import Morphisms. Require Import UserInputType VocabA. Require GenFunc. Require DomCon SemCon. Require Import vgtac. Require Import Monad. Module Type PINPUT. Include INPUT. Include GenFunc.Make. Parameter Loc_g : DomCon.Loc.t -> Loc.t. Parameter Val_g : DomCon.val_t -> Val.t -> Prop. (** Abstraction of Proc.t in DomCon.stack1. *) Parameter SProc_g : DomCon.Proc.t -> Loc.t. Parameter val_g_monotone : monotone Val.le Val_g. Parameter prop_approx_one_loc : forall g l (Hl: approx_one_loc g l = true) m (Hm : SemCon.wf_non_rec_mem g m) l1 (Hl1: Loc.eq (Loc_g l1) l) (Hml1 : DomCon.M.In l1 m) l2 (Hl2: Loc.eq (Loc_g l2) l) (Hml2 : DomCon.M.In l2 m), DomCon.Loc.eq l1 l2. Load MemGCommon. Parameter correct_run : forall g step cn cmd con_s con_s' abs_m abs_m' (Hmem_g : Mem_g con_s abs_m) (HCon : SemCon.Run g step cn cmd con_s con_s') (HAbs : abs_m' = run_only Strong g cn cmd abs_m), Mem_g con_s' abs_m'. (* Property 1: The functions collecting access information return the same values. *) Load VeqCommon. Parameter run_only_access_same : forall g cn cmd m, veq (run_only Strong g cn cmd m) (run_access Strong g cn cmd m). Parameter run_access_sound : forall g cn cmd, aeqm1 (run_access Strong g cn cmd). End PINPUT.