diff --git a/src/Makefile b/src/Makefile index 6c891412..25db23d1 100644 --- a/src/Makefile +++ b/src/Makefile @@ -20,7 +20,7 @@ MLDIR = ml EXTRACTDIR = ml/extracted COQINCLUDES=$(foreach d, $(COQDIR), -R $(d) Vellvm) -R $(EXTRACTDIR) Extract -COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) +COQC="$(COQBIN)coqc" -time-file "./profiling" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQEXEC="$(COQBIN)coqtop" -q -w none $(COQINCLUDES) -batch -load-vernac-source COQMAKEFILE="$(COQBIN)coq_makefile" diff --git a/src/_CoqProject b/src/_CoqProject index 2f6f192e..06f047bc 100644 --- a/src/_CoqProject +++ b/src/_CoqProject @@ -12,68 +12,28 @@ ./coq/Analysis/Iteration.v ./coq/Analysis/Kildall.v ./coq/Analysis/ssa.v -./coq/Handlers/Concretization.v -./coq/Handlers/Global.v -./coq/Handlers/Handlers.v -./coq/Handlers/Intrinsics.v -./coq/Handlers/Local.v -./coq/Handlers/MemPropT.v -./coq/Handlers/MemoryInterpreters.v -./coq/Handlers/MemoryModel.v -./coq/Handlers/MemoryModelImplementation.v -./coq/Handlers/MemoryModules/FiniteAddresses.v -./coq/Handlers/MemoryModules/FiniteExecPrimitives.v -./coq/Handlers/MemoryModules/FiniteIntptr.v -./coq/Handlers/MemoryModules/FiniteSizeof.v -./coq/Handlers/MemoryModules/FiniteSpecPrimitives.v -./coq/Handlers/MemoryModules/InfiniteAddresses.v -./coq/Handlers/MemoryModules/Within.v -./coq/Handlers/OOM.v -./coq/Handlers/Pick.v -./coq/Handlers/SerializationTheory.v -./coq/Handlers/Stack.v -./coq/Handlers/UndefinedBehaviour.v ./coq/Numeric/Archi.v ./coq/Numeric/Coqlib.v ./coq/Numeric/Floats.v ./coq/Numeric/IEEE754_extra.v ./coq/Numeric/Integers.v ./coq/Numeric/Zbits.v -./coq/QC/GenAST.v -./coq/QC/GenAlive2.v -./coq/QC/Generators.v ./coq/QC/ReprAST.v ./coq/QC/ShowAST.v ./coq/QC/Utils.v ./coq/QC/DList.v ./coq/Semantics.v -./coq/Semantics/ConcretizationParams.v ./coq/Semantics/Denotation.v ./coq/Semantics/DynamicValues.v ./coq/Semantics/GepM.v +./coq/Semantics/Memory/DvalueBytes.v ./coq/Semantics/StoreId.v -./coq/Semantics/InfiniteToFinite/Conversions/BaseConversions.v -./coq/Semantics/InfiniteToFinite/Conversions/DvalueConversions.v -./coq/Semantics/InfiniteToFinite/Conversions/EventConversions.v -./coq/Semantics/InfiniteToFinite/Conversions/TreeConversions.v -./coq/Semantics/InfiniteToFinite/R2Injective.v -./coq/Semantics/InterpretationStack.v ./coq/Semantics/IntrinsicsDefinitions.v ./coq/Semantics/ItreeRaiseMReturns.v ./coq/Semantics/LLVMEvents.v ./coq/Semantics/LLVMParams.v -./coq/Semantics/Lang.v -./coq/Semantics/Memory/ErrSID.v -./coq/Semantics/Memory/FiniteProvenance.v -./coq/Semantics/Memory/MemBytes.v -./coq/Semantics/Memory/DvalueBytes.v -./coq/Semantics/Memory/Overlaps.v ./coq/Semantics/Memory/Sizeof.v -./coq/Semantics/Memory/StoreId.v ./coq/Semantics/MemoryAddress.v -./coq/Semantics/MemoryParams.v -./coq/Semantics/RuttProps.v -./coq/Semantics/TopLevel.v ./coq/Semantics/VellvmIntegers.v ./coq/Syntax.v ./coq/Syntax/AstLib.v @@ -88,23 +48,10 @@ ./coq/Syntax/TypToDtyp.v ./coq/Syntax/TypeUtil.v ./coq/Theory.v -./coq/Theory/ContainsUB.v -./coq/Theory/ContainsUBExtra.v -./coq/Theory/ContainsUBOriginal.v ./coq/Theory/DenotationTheory.v -./coq/Theory/ExpLemmas.v -./coq/Theory/InstrLemmas.v -./coq/Theory/InterpreterCFG.v -./coq/Theory/InterpreterMCFG.v -./coq/Theory/LocalFrame.v -./coq/Theory/OOMRefinementExamples.v -./coq/Theory/Refinement.v -./coq/Theory/StatePredicates.v ./coq/Theory/SymbolicInterpreter.v -./coq/Theory/TopLevelRefinements.v ./coq/Transformations/BlockFusion.v ./coq/Transformations/DeadCodeElimination.v -./coq/Transformations/EquivExpr.v ./coq/Transformations/Peephole.v ./coq/Transformations/Transform.v ./coq/Utilities.v diff --git a/src/backfile b/src/backfile new file mode 100644 index 00000000..ad5309d8 --- /dev/null +++ b/src/backfile @@ -0,0 +1,55 @@ +./coq/QC/GenAST.v +./coq/QC/GenAlive2.v +./coq/QC/Generators.v +./coq/Handlers/Concretization.v +./coq/Handlers/Global.v +./coq/Handlers/Handlers.v +./coq/Handlers/Intrinsics.v +./coq/Handlers/Local.v +./coq/Handlers/MemPropT.v +./coq/Handlers/MemoryInterpreters.v +./coq/Handlers/MemoryModel.v +./coq/Handlers/MemoryModelImplementation.v +./coq/Handlers/MemoryModules/FiniteAddresses.v +./coq/Handlers/MemoryModules/FiniteExecPrimitives.v +./coq/Handlers/MemoryModules/FiniteIntptr.v +./coq/Handlers/MemoryModules/FiniteSizeof.v +./coq/Handlers/MemoryModules/FiniteSpecPrimitives.v +./coq/Handlers/MemoryModules/InfiniteAddresses.v +./coq/Handlers/MemoryModules/Within.v +./coq/Handlers/OOM.v +./coq/Handlers/Pick.v +./coq/Handlers/SerializationTheory.v +./coq/Handlers/Stack.v +./coq/Handlers/UndefinedBehaviour.v +./coq/Semantics/InfiniteToFinite/Conversions/BaseConversions.v +./coq/Semantics/InfiniteToFinite/Conversions/DvalueConversions.v +./coq/Semantics/InfiniteToFinite/Conversions/EventConversions.v +./coq/Semantics/InfiniteToFinite/Conversions/TreeConversions.v +./coq/Semantics/InfiniteToFinite/R2Injective.v +./coq/Semantics/InterpretationStack.v +./coq/Semantics/Memory/ErrSID.v +./coq/Semantics/Memory/FiniteProvenance.v +./coq/Semantics/Memory/Overlaps.v +./coq/Semantics/Memory/StoreId.v +./coq/Semantics/Memory/MemBytes.v +./coq/Semantics/ConcretizationParams.v +./coq/Semantics/MemoryParams.v +../coq/Semantics/Lang.v +./coq/Semantics/RuttProps.v +./coq/Semantics/TopLevel.v +./coq/Theory/ContainsUB.v +./coq/Theory/ContainsUBExtra.v +./coq/Theory/ContainsUBOriginal.v +./coq/Theory/ExpLemmas.v +./coq/Theory/InstrLemmas.v +./coq/Theory/InterpreterCFG.v +./coq/Theory/InterpreterMCFG.v +./coq/Theory/LocalFrame.v +./coq/Theory/OOMRefinementExamples.v +./coq/Theory/Refinement.v +./coq/Theory/StatePredicates.v +./coq/Theory/TopLevelRefinements.v +./coq/Transformations/EquivExpr.v + + diff --git a/src/coq/Analysis/Dom.v b/src/coq/Analysis/Dom.v index a4ba4e02..2e44c2be 100644 --- a/src/coq/Analysis/Dom.v +++ b/src/coq/Analysis/Dom.v @@ -1,12 +1,11 @@ (** Reasoning about dominators in a graph. *) +Set Warnings "-intuition-auto-with-star". Require Import List Equalities Orders RelationClasses Lia. Require Import FSets. Import ListNotations. - - Module Type LATTICE. Include EqLe'. diff --git a/src/coq/Analysis/ssa.v b/src/coq/Analysis/ssa.v index 7bc3d5d2..578f93d1 100644 --- a/src/coq/Analysis/ssa.v +++ b/src/coq/Analysis/ssa.v @@ -6,52 +6,53 @@ From Vellvm Require Import Syntax.Scope Analysis.Dom. (* end hide *) +From stdpp Require Import fin_maps. - Lemma instr_id_eq_dec : forall (x y : instr_id), {x = y} + {x <> y}. - Proof. - intros. destruct (Eqv.eqv_dec_p x y); auto. - Qed. +Lemma instr_id_eq_dec : forall (x y : instr_id), {x = y} + {x <> y}. +Proof. + intros. repeat decide equality. +Qed. - Definition def_sites_phis (phis : list (local_id * phi dtyp)) : list instr_id := - List.map (fun '(x,_) => IId x) phis. +Definition def_sites_phis (phis : list (local_id * phi dtyp)) : list instr_id := + List.map (fun '(x,_) => IId x) phis. - Definition pc : Type := block_id * option (nat * instr_id). +Definition pc : Type := block_id * option (nat * instr_id). - Lemma pc_eq_dec : forall (x y : pc), {x = y} + {x <> y}. - Proof. - repeat decide equality. - Qed. +Lemma pc_eq_dec : forall (x y : pc), {x = y} + {x <> y}. +Proof. + repeat decide equality. +Qed. - Definition opt_succ (mn : option (nat * instr_id)) : nat := - match mn with | Some (n,_) => S n | None => 0 end. +Definition opt_succ (mn : option (nat * instr_id)) : nat := + match mn with | Some (n,_) => S n | None => 0 end. - Definition succ_instr (c : cfg dtyp) (v v' : pc) : Prop := - let '(bid,mx) := v in - match find_block c.(blks) bid with - | Some bk => +Definition succ_instr (c : cfg dtyp) (v v' : pc) : Prop := + let '(bid,mx) := v in + match c.(blks) !! bid with + | Some bk => match List.nth_error (def_sites_phis bk.(blk_phis) ++ List.map fst bk.(blk_code)) (opt_succ mx) with - | None => exists bid', List.In bid' (successors bk) /\ v' = (bid',None) + | None => exists bid', bid' ∈ (successors bk) /\ v' = (bid',None) | Some iid => v' = (bid, Some (opt_succ mx, iid)) end - | None => False - end. + | None => False + end. - Definition mem_instr (c : cfg dtyp) (p : pc) : Prop := - let '(bid,mx) := p in - match find_block c.(blks) bid with - | Some bk => +Definition mem_instr (c : cfg dtyp) (p : pc) : Prop := + let '(bid,mx) := p in + match c.(blks) !! bid with + | Some bk => match mx with | None => True | Some (offset,x) => - match List.nth_error - (def_sites_phis bk.(blk_phis) ++ List.map fst bk.(blk_code)) offset with - | None => False - | Some iid => x = iid - end + match List.nth_error + (def_sites_phis bk.(blk_phis) ++ List.map fst bk.(blk_code)) offset with + | None => False + | Some iid => x = iid + end end - | None => False - end. + | None => False + end. (** ------------------------------------------------------------------------- *) (** * GRAPH instance for dominance calculation *) diff --git a/src/coq/Numeric/Floats.v b/src/coq/Numeric/Floats.v index dad9e3f8..9ba2efc3 100644 --- a/src/coq/Numeric/Floats.v +++ b/src/coq/Numeric/Floats.v @@ -15,6 +15,8 @@ (* *) (* *********************************************************************) +Set Warnings "-intuition-auto-with-star". + (** Formalization of floating-point numbers, using the Flocq library. *) Require Import Psatz. diff --git a/src/coq/Numeric/IEEE754_extra.v b/src/coq/Numeric/IEEE754_extra.v index 8db4d114..f339621f 100644 --- a/src/coq/Numeric/IEEE754_extra.v +++ b/src/coq/Numeric/IEEE754_extra.v @@ -431,7 +431,7 @@ Proof. apply integer_representable_2p. auto. apply (Zpower_gt_0 radix2). lia. -- assert (IZR x <> 0%R) by (apply (IZR_neq _ _ n)). +- assert (IZR x <> 0%R) by (apply (eq_IZR_contrapositive _ _ n)). destruct (BofZ_finite x H) as (A & B & C). destruct (BofZ_representable (2^p)) as (D & E & F). apply integer_representable_2p. auto. @@ -1036,7 +1036,7 @@ Proof with (try discriminate). rewrite <- ! bpow_plus. replace (prec - 1 + e') with (- (prec - 1 + e)) by (unfold e'; lia). rewrite bpow_opp. unfold cond_Ropp; destruct s; auto. - rewrite Ropp_inv_permute. auto. apply Rgt_not_eq. apply bpow_gt_0. + rewrite Rinv_opp. auto. split. simpl. apply F2R_neq_0. destruct s; simpl in H; discriminate. auto. Qed. diff --git a/src/coq/Numeric/Zbits.v b/src/coq/Numeric/Zbits.v index 4761dedc..23eb086b 100644 --- a/src/coq/Numeric/Zbits.v +++ b/src/coq/Numeric/Zbits.v @@ -13,6 +13,8 @@ (* *) (* *********************************************************************) +Set Warnings "-intuition-auto-with-star". + (** Additional operations and proofs about binary integers, on top of the ZArith standard library. *) diff --git a/src/coq/QC/GenAST.v b/src/coq/QC/GenAST.v index 93e04ef3..30efa0e5 100644 --- a/src/coq/QC/GenAST.v +++ b/src/coq/QC/GenAST.v @@ -10,8 +10,6 @@ See vellvm-quickchick-overview.org in the root of the project for more details. *) -Require Import Ceres.Ceres. - From Vellvm Require Import LLVMAst Utilities AstLib Syntax.CFG Syntax.TypeUtil Syntax.TypToDtyp DynamicTypes Semantics.TopLevel QC.Utils QC.Generators Handlers.Handlers DList. Require Import Integers. diff --git a/src/coq/QC/ReprAST.v b/src/coq/QC/ReprAST.v index f341081f..52c2c370 100644 --- a/src/coq/QC/ReprAST.v +++ b/src/coq/QC/ReprAST.v @@ -7,7 +7,7 @@ QuickChick. It may be worthwhile to serialize a counterexample into a format that it can be imported into Coq for debugging. *) - +From stdpp Require Import gmap. From Vellvm Require Import LLVMAst ShowAST Utilities DynamicTypes. @@ -35,6 +35,18 @@ Section ReprInstances. repr l := ("[" ++ contents repr l ++ "]")%string }. + #[global] + Instance reprProd (A B : Type) `{Repr A, Repr B} : Repr (A * B) := + { + repr '(a,b) := ("(" ++ repr a ++ "," ++ repr b ++ ")")%string + }. + + #[global] + Instance reprGmap (K V : Type) `{EqDecision K, Countable K, Repr K, Repr V} : Repr (gmap K V) := + { + repr m := repr (A := list (K * V)) (map_to_list m) + }. + #[global] Instance reprInt : Repr LLVMAst.int := { diff --git a/src/coq/QC/ShowAST.v b/src/coq/QC/ShowAST.v index df23ccc3..04499b99 100644 --- a/src/coq/QC/ShowAST.v +++ b/src/coq/QC/ShowAST.v @@ -18,7 +18,7 @@ Import DList. From Coq Require Import ZArith String Bool.Bool Numbers.HexadecimalString Strings.Ascii. -From QuickChick Require Import Show. +From QuickChick Require Export Show. (* Import QcDefaultNotation. Open Scope qc_scope. *) Set Warnings "-extraction-opaque-accessed,-extraction". @@ -142,6 +142,9 @@ Section ShowInstances. | DTYPE_Vector sz t => "Vector" end. + #[global] Instance showDtyp : Show dtyp := + {| show := show_dtyp |}. + Definition show_linkage (l : linkage) : string := match l with | LINKAGE_Private => "private " @@ -707,7 +710,7 @@ tes on cstring on LLVMAst.v *) := {| dshow p := let '(Phi t phis) := p in DList_join [string_to_DString "phi " ; dshow t ; string_to_DString " "] @@ - concat_DString (string_to_DString ", ") (map show_phi_block phis) + concat_DString (string_to_DString ", ") (map show_phi_block (fin_maps.map_to_list phis)) |}. Definition show_opt_prefix {A} `{Show A} (prefix : string) (ma : option A) : string diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v index cb4fd966..e953d590 100644 --- a/src/coq/Semantics.v +++ b/src/coq/Semantics.v @@ -8,9 +8,9 @@ *) From Vellvm Require Export - Handlers.Handlers + (* Handlers.Handlers *) Semantics.Denotation - Semantics.TopLevel + (* Semantics.TopLevel *) Semantics.DynamicValues - Semantics.InterpretationStack + (* Semantics.InterpretationStack *) Semantics.LLVMEvents. diff --git a/src/coq/Semantics/ConcretizationParams.v b/src/coq/Semantics/ConcretizationParams.v index b9b6e877..b9e65784 100644 --- a/src/coq/Semantics/ConcretizationParams.v +++ b/src/coq/Semantics/ConcretizationParams.v @@ -1,8 +1,7 @@ From Vellvm Require Import Semantics.LLVMParams Semantics.MemoryParams - Semantics.Memory.MemBytes - Handlers.Concretization. + Semantics.Memory.MemBytes. Module Type ConcretizationParams (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule LP.ADDR LP.IP LP.SIZEOF LP.Events MP.BYTE_IMPL). Module CONCBASE := Concretization.MakeBase LP MP Byte. diff --git a/src/coq/Semantics/Denotation.v b/src/coq/Semantics/Denotation.v index de9864d1..babf7734 100644 --- a/src/coq/Semantics/Denotation.v +++ b/src/coq/Semantics/Denotation.v @@ -14,10 +14,12 @@ From Coq Require Import FSets.FMapWeakList Bool.Bool. +From stdpp Require Import base list fin_maps. +Print Instances FinMap. + From ExtLib Require Import Structures.Monads - Structures.Functor - Eqv. + Structures.Functor. From ITree Require Import ITree @@ -32,18 +34,31 @@ From Vellvm Require Import Semantics.VellvmIntegers Semantics.LLVMEvents Semantics.LLVMParams - Semantics.MemoryParams - Semantics.Memory.MemBytes - Semantics.ConcretizationParams - Utils.ListUtil - DynamicValues. - -Require Import Ceres.Ceres. + DynamicValues + QC.ShowAST. Import Sum. Import Subevent. -Import EqvNotation. -Import ListNotations. + +Module MonadNotation. + + Delimit Scope monad_scope with monad. + + Notation "c >>= f" := (@bind _ _ _ _ c f) (at level 58, left associativity) : monad_scope. + + Notation "e1 ;; e2" := (@bind _ _ _ _ e1%monad (fun _ => e2%monad))%monad: monad_scope. + + Notation "x <- c1 ; c2" := (@bind _ _ _ _ c1 (fun x => c2)) + (at level 20, c1 at level 100, c2 at level 200, right associativity) : monad_scope. + (* (at level 60, c1 at next level, right associativity) : monad_scope. *) + + Notation "' pat <- c1 ; c2" := + (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end)) + (at level 20, pat pattern, c1 at level 100, c2 at level 200, right associativity) : monad_scope. + (* (at level 60, pat pattern, c1 at next level, right associativity) : monad_scope. *) + +End MonadNotation. + Import MonadNotation. Set Implicit Arguments. @@ -105,25 +120,24 @@ Open Scope N_scope. itrees in the second phase. *) -Module Denotation (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule LP.ADDR LP.IP LP.SIZEOF LP.Events MP.BYTE_IMPL) (CP : ConcretizationParams LP MP Byte). - Import CP. - Import CONC. - Import MP. +Module Denotation (LP : LLVMParams). Import LP. Import Events. Definition dv_zero_initializer (t:dtyp) : err dvalue := default_dvalue_of_dtyp t. + Notation Ecfg := instr_E. + (** ** Ident lookups Look-ups depend on the nature of the [ident], that may be local or global. In each case, we simply trigger the corresponding read event. Note: global maps contain [dvalue]s, while local maps contain [uvalue]s. We perform the conversion here. *) - Definition lookup_id (i:ident) : itree lookup_E uvalue := + Definition lookup_id (i:ident) : itree Ecfg uvalue := match i with - | ID_Global x => dv <- trigger (GlobalRead x);; ret (dvalue_to_uvalue dv) + | ID_Global x => dv <- trigger (GlobalRead x); ret (dvalue_to_uvalue dv) | ID_Local x => trigger (LocalRead x) end. @@ -141,13 +155,19 @@ Module Denotation (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule LP Definition dvalue_not_zero dv := ~ (dvalue_is_zero dv). + Definition pick_uvalue (uv : uvalue) : PickUvalueE {dv : dvalue | True} + := pick uv. + (* TODO: should the post condition be concretize uv dv ? *) + Definition pick_unique_uvalue (uv : uvalue) : PickUvalueE {dv : dvalue | True} + := pickUnique uv. + (* A trivially concrete [uvalue] does not need to go through a pick event to get concretize. This function therefore either trigger [pick], or perform a direct cast. The value of this "optimization" is debatable. *) Definition concretize_or_pick {E : Type -> Type} `{PickE -< E} `{FailureE -< E} (uv : uvalue) : itree E dvalue := if is_concrete uv then lift_err ret (uvalue_to_dvalue uv) - else dv <- trigger (pick_uvalue uv);; ret (proj1_sig dv). + else dv <- trigger (pick_uvalue uv); ret (proj1_sig dv). (* Pick a possibly poison value, treating poison as nondeterminism. This is used for freeze. *) @@ -160,7 +180,7 @@ Module Denotation (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule LP Definition pickUnique {E : Type -> Type} `{PickE -< E} `{FailureE -< E} (uv : uvalue) : itree E dvalue := if is_concrete uv then lift_err ret (uvalue_to_dvalue uv) - else dv <- trigger (pick_unique_uvalue uv);; ret (proj1_sig dv). + else dv <- trigger (pick_unique_uvalue uv); ret (proj1_sig dv). (** ** Denotation of expressions [denote_exp top o] is the main entry point for evaluating itree expressions. @@ -177,18 +197,14 @@ Module Denotation (LP : LLVMParams) (MP : MemoryParams LP) (Byte : ByteModule LP Expressions are denoted as itrees that return a [uvalue]. *) -(* TODO: show instance for dtyp and push this up *) -From Vellvm Require Import ShowAST. -Print Instances DShow. Fixpoint denote_exp - (top:option dtyp) (o:exp dtyp) {struct o} : itree exp_E uvalue := + (top:option dtyp) (o:exp dtyp) {struct o} : itree Ecfg uvalue := let eval_texp '(dt,ex) := denote_exp (Some dt) ex in match o with (* The translation injects the [lookup_E] interface used by [lookup_id] to the ambient one *) - | EXP_Ident i => - translate LU_to_exp (lookup_id i) + | EXP_Ident i => lookup_id i | EXP_Integer x => match top with @@ -235,7 +251,7 @@ Print Instances DShow. end | EXP_Cstring es => - vs <- map_monad eval_texp es ;; + vs <- map_monad eval_texp es ; ret (UVALUE_Array vs) | EXP_Undef => @@ -247,7 +263,7 @@ Print Instances DShow. (* Question: should we do any typechecking for aggregate types here? *) (* Option 1: do no typechecking: *) | EXP_Struct es => - vs <- map_monad eval_texp es ;; + vs <- map_monad eval_texp es ; ret (UVALUE_Struct vs) (* Option 2: do a little bit of typechecking *) @@ -255,17 +271,17 @@ Print Instances DShow. match top with | None => raise "denote_exp given untyped EXP_Struct" | Some (DTYPE_Packed_struct _) => - vs <- map_monad eval_texp es ;; + vs <- map_monad eval_texp es ; ret (UVALUE_Packed_struct vs) | _ => raise "bad type for VALUE_Packed_struct" end | EXP_Array es => - vs <- map_monad eval_texp es ;; + vs <- map_monad eval_texp es ; ret (UVALUE_Array vs) | EXP_Vector es => - vs <- map_monad eval_texp es ;; + vs <- map_monad eval_texp es ; ret (UVALUE_Vector vs) (* The semantics of operators is complicated by both uvalues and @@ -274,86 +290,86 @@ Print Instances DShow. depends on whether it may raise UB, and how. *) | OP_IBinop iop dt op1 op2 => - v1 <- denote_exp (Some dt) op1 ;; - v2 <- denote_exp (Some dt) op2 ;; + v1 <- denote_exp (Some dt) op1 ; + v2 <- denote_exp (Some dt) op2 ; ret (UVALUE_IBinop iop v1 v2) | OP_ICmp cmp dt op1 op2 => - v1 <- denote_exp (Some dt) op1 ;; - v2 <- denote_exp (Some dt) op2 ;; + v1 <- denote_exp (Some dt) op1 ; + v2 <- denote_exp (Some dt) op2 ; ret (UVALUE_ICmp cmp v1 v2) | OP_FBinop fop fm dt op1 op2 => - v1 <- denote_exp (Some dt) op1 ;; - v2 <- denote_exp (Some dt) op2 ;; + v1 <- denote_exp (Some dt) op1 ; + v2 <- denote_exp (Some dt) op2 ; ret (UVALUE_FBinop fop fm v1 v2) | OP_FCmp fcmp dt op1 op2 => - v1 <- denote_exp (Some dt) op1 ;; - v2 <- denote_exp (Some dt) op2 ;; + v1 <- denote_exp (Some dt) op1 ; + v2 <- denote_exp (Some dt) op2 ; ret (UVALUE_FCmp fcmp v1 v2) | OP_Conversion conv dt_from op dt_to => - v <- denote_exp (Some dt_from) op ;; + v <- denote_exp (Some dt_from) op ; ret (UVALUE_Conversion conv dt_from v dt_to) | OP_GetElementPtr dt1 (dt2, ptrval) idxs => - vptr <- denote_exp (Some dt2) ptrval ;; - vs <- map_monad (fun '(dt, index) => denote_exp (Some dt) index) idxs ;; + vptr <- denote_exp (Some dt2) ptrval ; + vs <- map_monad (fun '(dt, index) => denote_exp (Some dt) index) idxs ; ret (UVALUE_GetElementPtr dt1 vptr vs) | OP_ExtractElement (dt_vec, vecop) (dt_idx, idx) => - vec <- denote_exp (Some dt_vec) vecop ;; - idx <- denote_exp (Some dt_idx) idx ;; + vec <- denote_exp (Some dt_vec) vecop ; + idx <- denote_exp (Some dt_idx) idx ; ret (UVALUE_ExtractElement dt_vec vec idx) | OP_InsertElement (dt_vec, vecop) (dt_elt, eltop) (dt_idx, idx) => - vec <- denote_exp (Some dt_vec) vecop ;; - elt <- denote_exp (Some dt_elt) eltop ;; - idx <- denote_exp (Some dt_idx) idx ;; + vec <- denote_exp (Some dt_vec) vecop ; + elt <- denote_exp (Some dt_elt) eltop ; + idx <- denote_exp (Some dt_idx) idx ; ret (UVALUE_InsertElement dt_vec vec elt idx) | OP_ShuffleVector (dt_vec1, vecop1) (dt_vec2, vecop2) (dt_mask, idxmask) => - vec1 <- denote_exp (Some dt_vec1) vecop1 ;; - vec2 <- denote_exp (Some dt_vec2) vecop2 ;; - idxmask <- denote_exp (Some dt_mask) idxmask;; + vec1 <- denote_exp (Some dt_vec1) vecop1 ; + vec2 <- denote_exp (Some dt_vec2) vecop2 ; + idxmask <- denote_exp (Some dt_mask) idxmask; ret (UVALUE_ShuffleVector dt_vec1 vec1 vec2 idxmask) | OP_ExtractValue (dt, str) idxs => - str <- denote_exp (Some dt) str ;; + str <- denote_exp (Some dt) str ; ret (UVALUE_ExtractValue dt str idxs) | OP_InsertValue (dt_str, strop) (dt_elt, eltop) idxs => - str <- denote_exp (Some dt_str) strop ;; - elt <- denote_exp (Some dt_elt) eltop ;; + str <- denote_exp (Some dt_str) strop ; + elt <- denote_exp (Some dt_elt) eltop ; ret (UVALUE_InsertValue dt_str str dt_elt elt idxs) | OP_Select (dt, cnd) (dt1, op1) (dt2, op2) => - cnd <- denote_exp (Some dt) cnd ;; - v1 <- denote_exp (Some dt1) op1 ;; - v2 <- denote_exp (Some dt2) op2 ;; + cnd <- denote_exp (Some dt) cnd ; + v1 <- denote_exp (Some dt1) op1 ; + v2 <- denote_exp (Some dt2) op2 ; ret (UVALUE_Select cnd v1 v2) | OP_Freeze (dt, e) => - uv <- denote_exp (Some dt) e ;; - dv <- pick_your_poison uv;; + uv <- denote_exp (Some dt) e ; + dv <- pick_your_poison uv; ret (dvalue_to_uvalue dv) end. Arguments denote_exp _ : simpl nomatch. - Definition denote_op (o:exp dtyp) : itree exp_E uvalue := + Definition denote_op (o:exp dtyp) : itree Ecfg uvalue := denote_exp None o. Arguments denote_op _ : simpl nomatch. (* An instruction has only side-effects, it therefore returns [unit] *) Definition denote_instr - (i: (instr_id * instr dtyp)): itree instr_E unit := + (i: (instr_id * instr dtyp)): itree Ecfg unit := match i with (* Pure operations *) | (IId id, INSTR_Op op) => - uv <- translate exp_to_instr (denote_op op) ;; + uv <- denote_op op ; trigger (LocalWrite id uv) (* Allocation *) @@ -376,28 +392,28 @@ Print Instances DShow. in match num_elements with | None => - dv <- trigger (Alloca dt 1 align);; + dv <- trigger (Alloca dt 1 align); trigger (LocalWrite id (dvalue_to_uvalue dv)) | Some (t, num_exp) => - un <- translate exp_to_instr (denote_exp (Some t) num_exp);; - n <- pickUnique un;; - dv <- trigger (Alloca dt (Z.to_N (dvalue_int_unsigned n)) align);; + un <- denote_exp (Some t) num_exp; + n <- pickUnique un; + dv <- trigger (Alloca dt (Z.to_N (dvalue_int_unsigned n)) align); trigger (LocalWrite id (dvalue_to_uvalue dv)) end (* Load *) | (IId id, INSTR_Load dt (du,ptr) _) => - ua <- translate exp_to_instr (denote_exp (Some du) ptr) ;; + ua <- denote_exp (Some du) ptr ; (* Load addresses must be unique *) - da <- pickUnique ua;; - uv <- trigger (Load dt da);; + da <- pickUnique ua; + uv <- trigger (Load dt da); trigger (LocalWrite id uv) (* Store *) | (IVoid _, INSTR_Store (dt, val) (du, ptr) _) => - uv <- translate exp_to_instr (denote_exp (Some dt) val) ;; - ua <- translate exp_to_instr (denote_exp (Some du) ptr) ;; + uv <- denote_exp (Some dt) val ; + ua <- denote_exp (Some du) ptr ; (* Store addresses must be unique *) - da <- pickUnique ua ;; + da <- pickUnique ua ; match da with | DVALUE_Poison dt => raiseUB "Store to poisoned address." | _ => trigger (Store dt da uv) @@ -407,17 +423,17 @@ Print Instances DShow. (* Call *) | (pt, INSTR_Call (dt, f) args _) => - uvs <- map_monad (fun '(t, op) => (translate exp_to_instr (denote_exp (Some t) op))) (List.map fst args) ;; + uvs <- map_monad (fun '(t, op) => (denote_exp (Some t) op)) (List.map fst args) ; returned_value <- match intrinsic_exp f with | Some s => - dvs <- map_monad (fun uv => pickUnique uv) uvs ;; + dvs <- map_monad (fun uv => pickUnique uv) uvs ; fmap dvalue_to_uvalue (trigger (Intrinsic dt s dvs)) | None => - fv <- translate exp_to_instr (denote_exp None f) ;; + fv <- denote_exp None f ; trigger (Call dt fv uvs) end - ;; + ; match pt with | IVoid _ => ret tt | IId id => trigger (LocalWrite id returned_value) @@ -458,19 +474,19 @@ Print Instances DShow. (* A [terminator] either returns from a function call, producing a [dvalue], or jumps to a new [block_id]. *) - Definition denote_terminator (t: terminator dtyp): itree exp_E (block_id + uvalue) := + Definition denote_terminator (t: terminator dtyp): itree Ecfg (block_id + uvalue) := match t with | TERM_Ret (dt, op) => - dv <- denote_exp (Some dt) op ;; + dv <- denote_exp (Some dt) op ; ret (inr dv) | TERM_Ret_void => ret (inr UVALUE_None) | TERM_Br (dt,op) br1 br2 => - uv <- denote_exp (Some dt) op ;; - dv <- concretize_or_pick uv;; + uv <- denote_exp (Some dt) op ; + dv <- concretize_or_pick uv; match dv with | DVALUE_I1 comparison_bit => if equ comparison_bit one then @@ -484,17 +500,17 @@ Print Instances DShow. | TERM_Br_1 br => ret (inl br) | TERM_Switch (dt,e) default_br dests => - uselector <- denote_exp (Some dt) e;; + uselector <- denote_exp (Some dt) e; (* Selection on [undef] is UB *) - selector <- pickUnique uselector;; + selector <- pickUnique uselector; if dvalue_is_poison selector then raiseUB "Switching on poison." else (* We evaluate all the selectors. Note that they are enforced to be constants, we could reflect this in the syntax and avoid this step *) switches <- map_monad (fun '((TInt_Literal sz x),id) => - s <- (coerce_integer_to_int (Some sz) x);; + s <- (coerce_integer_to_int (Some sz) x); ret (s,id)) - dests;; + dests; lift_err (fun b => ret (inl b)) (select_switch selector default_br switches) | TERM_Unreachable => raiseUB "IMPOSSIBLE: unreachable in reachable position" @@ -506,31 +522,31 @@ Print Instances DShow. end. (* Denoting a list of instruction simply binds the trees together *) - Definition denote_code (c: code dtyp): itree instr_E unit := + Definition denote_code (c: code dtyp): itree Ecfg unit := map_monad_ denote_instr c. - Definition denote_phi (bid_from : block_id) (id_p : local_id * phi dtyp) : itree exp_E (local_id * uvalue) := + Definition denote_phi (bid_from : block_id) (id_p : local_id * phi dtyp) : itree Ecfg (local_id * uvalue) := let '(id, Phi dt args) := id_p in - match assoc bid_from args with + match args !! bid_from with | Some op => - uv <- denote_exp (Some dt) op ;; - ret (id,uv) + uv <- denote_exp (Some dt) op ; + ret (id,uv) | None => raise ("jump: phi node doesn't include block ") end. - Definition denote_phis (bid_from: block_id) (phis: list (local_id * phi dtyp)): itree instr_E unit := + Definition denote_phis (bid_from: block_id) (phis: list (local_id * phi dtyp)): itree Ecfg unit := dvs <- map_monad - (fun x => translate exp_to_instr (denote_phi bid_from x)) - phis;; + (fun x => denote_phi bid_from x) + phis; map_monad (fun '(id,dv) => trigger (LocalWrite id dv)) dvs;; ret tt. (* A block ends with a terminator, it either jumps to another block, or returns a dynamic value *) - Definition denote_block (b: block dtyp) (bid_from : block_id) : itree instr_E (block_id + uvalue) := + Definition denote_block (b: block dtyp) (bid_from : block_id) : itree Ecfg (block_id + uvalue) := denote_phis bid_from (blk_phis b);; denote_code (blk_code b);; - translate exp_to_instr (denote_terminator (blk_term b)). + denote_terminator (blk_term b). (* Our denotation currently contains two kinds of indirections: jumps to labels, internal to a cfg, and calls to functions, that jump from a cfg to another. @@ -546,21 +562,21 @@ Print Instances DShow. If it ever returns a dynamic value, we exit the loop by returning the [dvalue]. *) Definition denote_ocfg (bks: ocfg dtyp) - : (block_id * block_id) -> itree instr_E ((block_id * block_id) + uvalue) := + : (block_id * block_id) -> itree Ecfg ((block_id * block_id) + uvalue) := iter (C := ktree _) (bif := sum) (fun '((bid_from,bid_src) : block_id * block_id) => - match find_block bks bid_src with + match bks !! bid_src with | None => ret (inr (inl (bid_from,bid_src))) | Some block_src => - bd <- denote_block block_src bid_from;; + bd <- denote_block block_src bid_from; match bd with | inr dv => ret (inr (inr dv)) | inl bid_target => ret (inl (bid_src,bid_target)) end end). - Definition denote_cfg (f: cfg dtyp) : itree instr_E uvalue := - r <- denote_ocfg (blks f) (init f,init f) ;; + Definition denote_cfg (f: cfg dtyp) : itree Ecfg uvalue := + r <- denote_ocfg (blks f) (init f,init f) ; match r with | inl bid => raise ("Can't find block in denote_cfg " ++ show (snd bid)) | inr uv => ret uv @@ -574,11 +590,11 @@ Print Instances DShow. Definition denote_function (df:definition dtyp (cfg dtyp)) : function_denotation := fun (args : list uvalue) => (* We match the arguments variables to the inputs *) - bs <- lift_err ret (combine_lists_err (df_args df) args) ;; + bs <- lift_err ret (combine_lists_err (df_args df) args) ; (* generate the corresponding writes to the local stack frame *) trigger MemPush ;; - trigger (StackPush bs) ;; - rv <- translate instr_to_L0' (denote_cfg (df_instrs df)) ;; + trigger (StackPush (map (fun '(k,v) => (k, v)) bs)) ;; + rv <- translate instr_to_L0' (denote_cfg (df_instrs df)) ; trigger StackPop ;; trigger MemPop ;; ret rv. @@ -606,14 +622,33 @@ Print Instances DShow. (fun T call => match call with | Call dt fv args => - dfv <- concretize_or_pick fv;; + dfv <- concretize_or_pick fv; match (lookup_defn dfv fundefs) with | Some f_den => (* If the call is internal *) f_den args | None => - dargs <- map_monad (fun uv => pickUnique uv) args ;; + dargs <- map_monad (fun uv => pickUnique uv) args ; fmap dvalue_to_uvalue (trigger (ExternalCall dt fv dargs)) end end) _ (Call dt f_value args). + + + Module SemNotations. + + Notation "⟦ e 'at?' t '⟧e'" := (denote_exp t e). + Notation "⟦ e 'at' t '⟧e'" := (denote_exp (Some t) e). + Notation "⟦ e '⟧e'" := (denote_exp None e). + Notation "⟦ i '⟧i'" := (denote_instr i). + Notation "⟦ c '⟧c'" := (denote_code c). + Notation "⟦ t '⟧t'" := (denote_terminator t). + Notation "⟦ phi '⟧Φ' from" := (denote_phi from phi) (at level 0, from at next level). + Notation "⟦ phis '⟧Φs' from" := (denote_phis from phis) (at level 0, from at next level). + Notation "⟦ bk '⟧b'" := (denote_block bk). + Notation "⟦ bks '⟧bs'" := (denote_ocfg bks). + Notation "⟦ f '⟧cfg'" := (denote_cfg f). + Notation "⟦ f '⟧f'" := (denote_function f). + + End SemNotations. + End Denotation. diff --git a/src/coq/Semantics/DynamicValues.v b/src/coq/Semantics/DynamicValues.v index 70ec974b..77a09a68 100644 --- a/src/coq/Semantics/DynamicValues.v +++ b/src/coq/Semantics/DynamicValues.v @@ -11,8 +11,6 @@ From Coq Require Import Import BinInt. -(* Require Import Ceres.Ceres. *) - Require Import Integers Floats. From Flocq.IEEE754 Require Import @@ -71,16 +69,6 @@ Open Scope N_scope. (* Floating-point rounding mode *) Definition FT_Rounding:mode := mode_NE. -Definition inttyp (x:N) : Type := - match x with - | 1 => int1 - | 8 => int8 - | 16 => int16 - | 32 => int32 - | 64 => int64 - | _ => False - end. - (* TODO: This probably should live somewhere else... *) #[refine]#[local] Instance Decidable_eq_N : forall (x y : N), Decidable (eq x y) := { Decidable_witness := N.eqb x y @@ -3211,34 +3199,37 @@ Module DVALUE(A:Vellvm.Semantics.MemoryAddress.ADDRESS)(IP:Vellvm.Semantics.Memo end. Arguments eval_int_op _ _ _ : simpl nomatch. - (* Evaluate the given iop on the given arguments according to the bitsize *) - Definition integer_op {M} `{Monad M} `{RAISE_ERROR M} `{RAISE_UB M} `{RAISE_OOM M} (bits:N) (iop:ibinop) (x y:inttyp bits) : M dvalue := - match bits, x, y with - | 1, x, y => eval_int_op iop x y - | 8, x, y => eval_int_op iop x y - | 16, x, y => eval_int_op iop x y - | 32, x, y => eval_int_op iop x y - | 64, x, y => eval_int_op iop x y - | _, _, _ => raise_error "unsupported bitsize" - end. - Arguments integer_op _ _ _ _ : simpl nomatch. + Variant int_size : Set := | sz1 | sz8 | sz16 | sz32 | sz64. - (* Convert written integer constant to corresponding integer with bitsize bits. + Definition get_size : N -> option int_size := + fun bits => match bits with + | 1 => Some sz1 + | 8 => Some sz8 + | 16 => Some sz16 + | 32 => Some sz32 + | 64 => Some sz64 + | _ => None + end + . + + (* Convert written integer constant to corresponding integer with bitsize bits. Takes the integer modulo 2^bits. *) - Definition coerce_integer_to_int {M} `{Monad M} `{RAISE_ERROR M} `{RAISE_UB M} `{RAISE_OOM M} (bits:option N) (i:Z) : M dvalue := - match bits with - | Some 1 => ret (DVALUE_I1 (repr i)) - | Some 8 => ret (DVALUE_I8 (repr i)) - | Some 16 => ret (DVALUE_I16 (repr i)) - | Some 32 => ret (DVALUE_I32 (repr i)) - | Some 64 => ret (DVALUE_I64 (repr i)) - | None => - i' <- lift_OOM (mrepr i);; - ret (DVALUE_IPTR i') - | _ => - raise_error "unsupported integer size" - end. - Arguments coerce_integer_to_int _ _ : simpl nomatch. + Definition coerce_integer_to_int {M} `{Monad M, RAISE_ERROR M, RAISE_UB M, RAISE_OOM M} + (bits:option N) (i:Z) : M dvalue := + match bits with + | None => + i' <- lift_OOM (mrepr i);; + ret (DVALUE_IPTR i') + | Some sz => match get_size sz with + | Some sz1 => ret (DVALUE_I1 (repr i)) + | Some sz8 => ret (DVALUE_I8 (repr i)) + | Some sz16 => ret (DVALUE_I16 (repr i)) + | Some sz32 => ret (DVALUE_I32 (repr i)) + | Some sz64 => ret (DVALUE_I64 (repr i)) + | None => raise_error "unsupported integer size" + end + end. + Arguments coerce_integer_to_int _ _ : simpl nomatch. (* Helper for looping 2 argument evaluation over vectors, producing a vector *) diff --git a/src/coq/Semantics/GepM.v b/src/coq/Semantics/GepM.v index 5d3d3ec0..27367cac 100644 --- a/src/coq/Semantics/GepM.v +++ b/src/coq/Semantics/GepM.v @@ -178,106 +178,6 @@ Module Type GEPM (Addr:ADDRESS) (PTOI : PTOI Addr) (PROV : PROVENANCE Addr) (ITO auto. Qed. - (* Lemma handle_gep_addr_cons_inv : *) - (* forall t base_addr idx idxs final_addr, *) - (* handle_gep_addr t base_addr (idx :: idxs) = inr (ret final_addr) -> *) - (* exists res_addr, *) - (* handle_gep_addr t base_addr [idx] = inr (ret res_addr) /\ *) - (* handle_gep_addr t res_addr idxs = inr (ret res_addr). *) - (* Proof. *) - (* intros t base_addr idx idxs final_addr H. *) - (* cbn in H. *) - (* break_match_hyp_inv. *) - (* - break_match_hyp_inv. *) - (* exists final_addr. *) - - - (* remember (int_to_ptr (ptr_to_int base_addr + Z.of_N (sizeof_dtyp t) * DynamicValues.Int8.unsigned x) (address_provenance base_addr)). *) - (* pose proof int_to_ptr_ptr_to_int_exists. *) - (* exists (int_to_ptr (ptr_to_int base_addr + Z.of_N (sizeof_dtyp t) * DynamicValues.Int8.unsigned x) (address_provenance base_addr)). *) - - (* Qed. *) - - (* Lemma handle_gep_h_cons : *) - (* forall idxs idx t base_addr res_addr final_addr, *) - (* handle_gep_h t base_addr [idx] = inr res_addr -> *) - (* handle_gep_h t res_addr idxs = inr final_addr -> *) - (* handle_gep_h t base_addr (idx :: idxs) = inr final_addr. *) - (* Proof. *) - (* intros idxs. *) - (* induction idxs; intros idx t base_addr res_addr final_addr GEP_START GEP_REST. *) - (* - cbn in GEP_REST. inv GEP_REST; auto. *) - (* - specialize *) - (* cbn in GEP_REST. *) - (* break_match_hyp_inv. *) - (* + break_match_hyp_inv. *) - (* specialize x (res_addr + DynamicValues.Int8.unsigned x * Z.of_N (sizeof_dtyp d)) *) - (* * cbn in H1. *) - - (* specialize (IHidxs a t res_addr). *) - - - (* cbn; cbn in GEP_START. *) - (* break_match_hyp_inv. *) - (* - break_match_hyp_inv. *) - (* + generalize dependent final_addr. *) - (* generalize dependent base_addr. *) - (* induction idxs; intros base_addr final_addr GEP_REST. *) - (* * cbn in *; auto. *) - (* * cbn in *. *) - (* break_match_hyp_inv. *) - (* -- *) - (* Qed. *) - - (* Lemma handle_gep_addr_cons : *) - (* forall idx idxs t base_addr res_addr final_addr, *) - (* handle_gep_addr t base_addr [idx] = inr (ret res_addr) -> *) - (* handle_gep_addr t res_addr idxs = inr (ret final_addr) -> *) - (* handle_gep_addr t base_addr (idx :: idxs) = inr (ret final_addr). *) - (* Proof. *) - (* intros idx. *) - (* induction idxs; intros t base_addr res_addr final_addr GEP_START GEP_REST. *) - (* - cbn in GEP_REST. inv GEP_REST. *) - (* - cbn in GEP_START. *) - (* cbn. *) - (* break_match_hyp_inv. *) - (* + cbn in GEP_REST. *) - (* break_match_hyp_inv. *) - (* * break_match_hyp_inv. *) - (* break_match_goal. *) - (* admit. *) - - (* break_match_hyp_inv. *) - - - - (* intros t base_addr idx idxs res_addr final_addr GEP_START GEP_REST. *) - (* cbn. *) - (* cbn in GEP_START. *) - (* break_match_hyp_inv. *) - (* - unfold handle_gep_addr in GEP_REST. *) - (* induction idxs; inv GEP_REST. *) - (* forward IHidxs. *) - - - (* generalize dependent res_addr. *) - (* induction idxs; intros res_addr GEP_REST H0. *) - (* + inv GEP_REST. *) - (* + cbn. *) - (* setoid_rewrite GEP_REST. *) - (* break_match_goal. *) - (* + unfold handle_gep_addr in GEP_REST. *) - (* break_match_hyp_inv. *) - (* break_match_hyp_inv. *) - (* cbn in *. *) - (* break_match_hyp_inv. *) - (* break_match_hyp_inv. *) - - - - (* reflexivity. *) - (* Qed. *) - Lemma handle_gep_addr_preserves_provenance : forall (dt : dtyp) ixs (p p' : addr), handle_gep_addr dt p ixs = inr (ret p') -> diff --git a/src/coq/Semantics/LLVMEvents.v b/src/coq/Semantics/LLVMEvents.v index c03ddb34..3aea2816 100644 --- a/src/coq/Semantics/LLVMEvents.v +++ b/src/coq/Semantics/LLVMEvents.v @@ -169,7 +169,7 @@ Module Type LLVM_INTERACTIONS (ADDR : MemoryAddress.ADDRESS) (IP:MemoryAddress.I Variant CallE : Type -> Type := | Call : forall (t:dtyp) (f:uvalue) (args:list uvalue), CallE uvalue. - (* ExternalCallE values are the "observable" events by which one should compare the + (* ExternalCallE values are the "observable" events by which one should compare the equivalence of two LLVM IR programs. These should never be interpreted away by the Coq semantics. However, for practicality, we _do_ interpet some calls that generate outputs to [stdout] (SAZ: and eventuall[stderr]). The stream of bytes @@ -184,9 +184,9 @@ Module Type LLVM_INTERACTIONS (ADDR : MemoryAddress.ADDRESS) (IP:MemoryAddress.I Variant ExternalCallE : Type -> Type := | ExternalCall : forall (t:dtyp) (f:uvalue) (args:list dvalue), ExternalCallE dvalue - (* This event corresponds to writing to the [stdout] channel. ] *) + (* This event corresponds to writing to the [stdout] channel. ] *) | IO_stdout : forall (str : list int8), ExternalCallE unit - (* This event corresponds to writing to the [stderr] channel. ] *) + (* This event corresponds to writing to the [stderr] channel. ] *) | IO_stderr : forall (str : list int8), ExternalCallE unit. (* Call to an intrinsic whose implementation do not rely on the implementation of the memory model *) diff --git a/src/coq/Semantics/Memory/DvalueBytes.v b/src/coq/Semantics/Memory/DvalueBytes.v index 1b35db48..08392624 100644 --- a/src/coq/Semantics/Memory/DvalueBytes.v +++ b/src/coq/Semantics/Memory/DvalueBytes.v @@ -317,7 +317,7 @@ Module Type DvalueByte (LP : LLVMParams). (fun idx => (DVALUE_ExtractByte dv dt idx)) (Nseq 0 (N.to_nat (sizeof_dtyp dt))). - Obligation Tactic := try Tactics.program_simpl; try solve [cbn; try lia]. + #[local] Obligation Tactic := try Tactics.program_simpl; try solve [cbn; try lia]. Fixpoint dvalue_bytes_to_dvalue {M} `{Monad M} `{RAISE_ERROR M} `{RAISE_POISON M} `{RAISE_OOMABLE M} (dbs : list dvalue_byte) (dt : dtyp) : M dvalue := let list_dvalue_bytes_to_dvalue := diff --git a/src/coq/Syntax/AstLib.v b/src/coq/Syntax/AstLib.v index 91c37178..3a24f5bb 100644 --- a/src/coq/Syntax/AstLib.v +++ b/src/coq/Syntax/AstLib.v @@ -14,56 +14,6 @@ Import ListNotations. (* end hide *) -(* Equalities --------------------------------------------------------------- *) - -#[global] Instance EqDecision_raw_id : EqDecision raw_id. -solve_decision. -Defined. - -Definition Countable_raw_id_obligation : - ∀ x : raw_id, - match - match x with - | Name s => (encode s)~0~0 - | Anon i => (encode i)~0~1 - | Raw i => (encode i)~1~0 - end - with - | p~0~1 => Anon <$> decode p - | p~1~0 => Raw <$> decode p - | p~0~0 => Name <$> decode p - | _ => None - end = Some x. -Proof. now intros []; cbn; rewrite decode_encode. Qed. - -#[global] Instance Countable_raw_id : Countable raw_id := - {| - encode id := match id with - | Name s => (encode s)~0~0%positive - | Anon i => (encode i)~0~1%positive - | Raw i => (encode i)~1~0%positive - end; - decode p := match p with - | p~0~0 => Name <$> decode p - | p~0~1 => Anon <$> decode p - | p~1~0 => Raw <$> decode p - | _ => None - end; - decode_encode := Countable_raw_id_obligation - |}. - -#[global] Instance EqDecision_block_id : EqDecision block_id. -solve_decision. -Defined. - -#[global] Instance EqDecision_instr_id : EqDecision instr_id. -solve_decision. -Defined. - -#[global] Instance EqDecision_ident : EqDecision ident. -solve_decision. -Defined. - (* Scheme Induction seems to still be too stupid to derive this automatically, fails to handle the nested lists *) Section TypInd. diff --git a/src/coq/Syntax/LLVMAst.v b/src/coq/Syntax/LLVMAst.v index 651ed7f6..456275be 100644 --- a/src/coq/Syntax/LLVMAst.v +++ b/src/coq/Syntax/LLVMAst.v @@ -7,6 +7,8 @@ From Coq Require Import From Vellvm Require Import Utilities. +From stdpp Require Import gmap strings. + Import ListNotations. Open Scope string_scope. Open Scope list_scope. @@ -46,7 +48,6 @@ Variant ident : Set := | ID_Local (id:raw_id) (* %id *) . - Unset Elimination Schemes. Inductive typ : Set := | TYPE_I (sz:N) @@ -150,7 +151,7 @@ Variant param_attr : Set := | PARAMATTR_Alignstack (a : int) | PARAMATTR_Allocalign | PARAMATTR_Allocptr -| PARAMATTR_Writeonly +| PARAMATTR_Writeonly . Variant frame_pointer_val : Set := @@ -251,7 +252,63 @@ Definition local_id := raw_id. Definition global_id := raw_id. Definition block_id := raw_id. Definition function_id := global_id. +Variant instr_id : Set := + | IId (id:raw_id) (* "Anonymous" or explicitly named instructions *) + | IVoid (n:int) (* "Void" return type, for "store", "void call", and terminators. + Each with unique number (NOTE: these are distinct from Anon raw_id) *) +. + +(* Equalities --------------------------------------------------------------- *) +#[global] Instance EqDecision_raw_id : EqDecision raw_id. +solve_decision. +Defined. + +Definition Countable_raw_id_obligation : + ∀ x : raw_id, + match + match x with + | Name s => (encode s)~0~0%positive + | Anon i => (encode i)~0~1%positive + | Raw i => (encode i)~1~0%positive + end + with + | p~0~1%positive => Anon <$> decode p + | p~1~0%positive => Raw <$> decode p + | p~0~0%positive => Name <$> decode p + | _ => None + end = Some x. +Proof. now intros []; cbn; rewrite decode_encode. Qed. + +#[global] Instance Countable_raw_id : Countable raw_id := + {| + encode id := match id with + | Name s => (encode s)~0~0%positive + | Anon i => (encode i)~0~1%positive + | Raw i => (encode i)~1~0%positive + end; + decode p := match p with + | p~0~0%positive => Name <$> decode p + | p~0~1%positive => Anon <$> decode p + | p~1~0%positive => Raw <$> decode p + | _ => None + end; + decode_encode := Countable_raw_id_obligation + |}. + +#[global] Instance EqDecision_local_id : EqDecision local_id := EqDecision_raw_id. +#[global] Instance Countable_local_id : Countable local_id := Countable_raw_id. + +#[global] Instance EqDecision_block_id : EqDecision block_id := EqDecision_raw_id. +#[global] Instance Countable_block_id : Countable block_id := Countable_raw_id. + +#[global] Instance EqDecision_instr_id : EqDecision instr_id. +solve_decision. +Defined. + +#[global] Instance EqDecision_ident : EqDecision ident. +solve_decision. +Defined. (* NOTE: We could separate return types from types, but that needs mutually recursive types. @@ -389,14 +446,8 @@ Inductive metadata : Set := Variant tint_literal : Set := | TInt_Literal (sz:N) (x:int). -Variant instr_id : Set := - | IId (id:raw_id) (* "Anonymous" or explicitly named instructions *) - | IVoid (n:int) (* "Void" return type, for "store", "void call", and terminators. - Each with unique number (NOTE: these are distinct from Anon raw_id) *) -. - Variant phi : Set := - | Phi (t:T) (args:list (block_id * exp)) + | Phi (t:T) (args: gmap block_id exp) . Variant ordering : Set := diff --git a/src/coq/Syntax/Scope.v b/src/coq/Syntax/Scope.v index b2c5f5ce..8fc87dcf 100644 --- a/src/coq/Syntax/Scope.v +++ b/src/coq/Syntax/Scope.v @@ -133,7 +133,7 @@ Section LABELS_OPERATIONS. disjoint_bid bks1 bks2. Definition phi_sources (φ : phi T) : gset block_id := - let '(Phi _ l) := φ in list_to_set (map fst l). + let '(Phi _ l) := φ in dom l. (* Over a closed graph, phi nodes should expect exactly jumps from their predecessors: - For any block [bk] in the graph @@ -322,13 +322,14 @@ Section REGISTER_OPERATIONS. |}. #[global] Instance phi_use_sites {T} : Use_sites (phi T) := - {| use_sites := fun '(Phi _ l) => set_flat_map_list (fun x => use_sites (snd x)) l |}. + {| use_sites := fun '(Phi _ l) => + map_fold (fun _ x acc => use_sites x ∪ acc) ∅ l + |}. #[global] Instance block_use_sites {T} : Use_sites (block T) := {| use_sites bk := - set_flat_map_list (fun x => use_sites (snd x)) bk.(blk_phis) - ∪ use_sites bk.(blk_code) - ∪ use_sites bk.(blk_term) |}. + set_flat_map_list (fun x => use_sites (snd x)) + bk.(blk_phis) ∪ use_sites bk.(blk_code) ∪ use_sites bk.(blk_term) |}. #[global] Instance ocfg_use_sites {T} : Use_sites (ocfg T) := {| use_sites := map_fold (fun k bk acc => use_sites bk ∪ acc) ∅ |}. diff --git a/src/coq/Syntax/Traversal.v b/src/coq/Syntax/Traversal.v index 922c3225..9811753f 100644 --- a/src/coq/Syntax/Traversal.v +++ b/src/coq/Syntax/Traversal.v @@ -237,7 +237,7 @@ Section Endo. `{Endo (exp T)} : Endo (phi T) | 50 := fun p => match p with - | Phi t args => Phi (endo t) (endo args) + | Phi t args => Phi (endo t) (fmap endo args) end. #[global] Instance Endo_block @@ -593,8 +593,8 @@ Section TFunctor. `{Endo raw_id} `{TFunctor exp} : TFunctor phi | 50 := - fun U V f '(Phi t args) => - Phi (f t) (tfmap (fun '(id,e) => (endo id, tfmap f e)) args). + fun U V f '(Phi t args) => + Phi (f t) (fmap (tfmap (T := exp) f) args). #[global] Instance TFunctor_code `{Endo raw_id} diff --git a/src/coq/Theory.v b/src/coq/Theory.v index 882e7bfb..b8e59305 100644 --- a/src/coq/Theory.v +++ b/src/coq/Theory.v @@ -3,10 +3,10 @@ *) From Vellvm Require Export - Theory.ExpLemmas - Theory.InstrLemmas + (* Theory.ExpLemmas *) + (* Theory.InstrLemmas *) Theory.DenotationTheory - Theory.InterpreterCFG - Theory.InterpreterMCFG + (* Theory.InterpreterCFG *) + (* Theory.InterpreterMCFG *) Theory.SymbolicInterpreter Syntax.ScopeTheory. diff --git a/src/coq/Theory/DenotationTheory.v b/src/coq/Theory/DenotationTheory.v index 15f998fe..635b7b13 100644 --- a/src/coq/Theory/DenotationTheory.v +++ b/src/coq/Theory/DenotationTheory.v @@ -1,4 +1,6 @@ (* begin hide *) +From stdpp Require Import base gmap fin_maps tactics. +(* ssreflect. *) From Coq Require Import String @@ -12,10 +14,12 @@ From ITree Require Import From Vellvm Require Import Utilities Syntax - Semantics + Semantics.LLVMParams + Semantics.Denotation Syntax.ScopeTheory Utils.PostConditions Utils.ITreeRaise. +Import LLVMEvents. #[export] Remove Hints Eqv.EqvWF_Build : typeclass_instances. @@ -26,13 +30,48 @@ Import MonadNotation. Open Scope list_scope. Open Scope monad_scope. Open Scope itree. -Import ITreeNotations. -Import EitherMonad. -Import IdentityMonad. +(* Import ITreeNotations. *) +(* Import EitherMonad. *) +(* Import IdentityMonad. *) Import ListNotations. (* end hide *) +(* TO MOVE *) +Lemma eq_itree_eq_bind : forall E R1 R2 RR U (t: itree E U) (k1: U -> itree E R1) (k2: U -> itree E R2), + (forall u, eq_itree RR (k1 u) (k2 u)) -> eq_itree RR (ITree.bind t k1) (ITree.bind t k2). +Proof. + intros. + apply eq_itree_clo_bind with (UU := Logic.eq); [reflexivity |]. + intros ? ? ->; apply H. +Qed. + +Lemma euttge_clo_bind {E : Type -> Type} {R1 R2 : Type} (RR : R1 -> R2 -> Prop) {U1 U2 UU} t1 t2 k1 k2 + (EQT: @euttge E U1 U2 UU t1 t2) + (EQK: forall u1 u2, UU u1 u2 -> euttge RR (k1 u1) (k2 u2)): + euttge RR (ITree.bind t1 k1) (ITree.bind t2 k2). +Proof. + eapply eqit_bind'; eauto. +Qed. + +Lemma euttge_eq_bind : forall E R1 R2 RR U (t: itree E U) (k1: U -> itree E R1) (k2: U -> itree E R2), + (forall u, euttge RR (k1 u) (k2 u)) -> euttge RR (ITree.bind t k1) (ITree.bind t k2). +Proof. + intros. + apply euttge_clo_bind with (UU := Logic.eq); [reflexivity |]. + intros ? ? ->; apply H. +Qed. + +Tactic Notation "ibind" := (eapply eutt_clo_bind || eapply eq_itree_clo_bind || eapply euttge_clo_bind). +Tactic Notation "ibind=" := + (apply eutt_eq_bind || eapply eq_itree_eq_bind || eapply euttge_eq_bind). +Tactic Notation "ibind" "with" uconstr(R) := + (eapply eutt_clo_bind with (UU := R) + || eapply eq_itree_clo_bind with (UU := R) + || eapply euttge_clo_bind with (UU := R)). + +(* END TO MOVE *) + (** * Structural equations at the representation level We prove here the equational theory that holds independently of the @@ -45,10 +84,10 @@ In particular, notice that since [interp] is a iterative-monad morphism that res [eutt eq], these equations get transported at all levels of interpretations. *) -Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). - Export TOP. - Export IS. - Export IS.LLVM. +Module Type DenotationTheory (LP : LLVMParams). + Module D := Denotation LP. + Import D. + Import LP. Import SemNotations. @@ -62,246 +101,316 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). Hint Rewrite @translate_bind : rwexp. Hint Rewrite @translate_trigger : rwexp. - Ltac go := autorewrite with rwexp. + Ltac go := + (match goal with + |- eutt _ ?t ?u => + let fresh := fresh in + remember t as fresh; + autorewrite with rwexp; + subst fresh; + remember u as fresh; + autorewrite with rwexp; + subst fresh + end) || + (match goal with + |- eq_itree _ ?t ?u => + let fresh := fresh in + remember t as fresh; + autorewrite with rwexp; + subst fresh; + remember u as fresh; + autorewrite with rwexp; + subst fresh + end) || + (match goal with + |- eqit _ _ _ ?t ?u => + let fresh := fresh in + remember t as fresh; + autorewrite with rwexp; + subst fresh; + remember u as fresh; + autorewrite with rwexp; + subst fresh + end) || + autorewrite with rwexp. + Tactic Notation "go*" := cbn; go. + Tactic Notation "go**" := repeat (cbn; go). End DenoteTactics. Import DenoteTactics. - (** [denote_code] *) + (** [denote_code] + - ⟦ [] ⟧c ≈ Ret tt [denote_code_nil] + - ⟦ [i] ⟧c ≈ ⟦ i ⟧i [denote_code_singleton] + - ⟦ i :: c ⟧c ≈ (⟦ i ⟧i ;; ⟦ c ⟧c) [denote_code_cons] + - ⟦ a ++ b ⟧c ≈ (⟦ a ⟧c ;; ⟦ b ⟧c) [denote_code_app] + *) Lemma denote_code_nil : ⟦ [] ⟧c ≈ Ret tt. - Proof using. - intros. - cbn. - go. - reflexivity. + Proof. + by go*. Qed. - Lemma denote_code_app : + Lemma denote_code_app_eq_itree : forall a b, - ⟦ a ++ b ⟧c ≈ ⟦ a ⟧c;; ⟦ b ⟧c. - Proof using. + ⟦ a ++ b ⟧c ≅ (⟦ a ⟧c ;; ⟦ b ⟧c). + Proof. induction a; intros b. - - cbn; go; reflexivity. + - by cbn; go. - cbn in *. go. - apply eutt_eq_bind; intros (). + ibind=; intros []. go. setoid_rewrite bind_ret_l. rewrite IHa. - go. - reflexivity. + by go. Qed. - Lemma denote_code_app_eq_itree : + Lemma denote_code_app : forall a b, - ⟦ a ++ b ⟧c ≅ ITree.bind ⟦ a ⟧c (fun _ => ⟦ b ⟧c). - Proof using. - induction a; intros b. - - cbn. - go. - eapply eq_itree_clo_bind with (UU := eq); [reflexivity | intros ? ? ->; reflexivity]. - - cbn in *. - go. - eapply eq_itree_clo_bind with (UU := eq); [reflexivity | intros ? ? ->]. - setoid_rewrite bind_ret_l. - setoid_rewrite bind_bind. - setoid_rewrite bind_ret_l. - rewrite IHa. - setoid_rewrite bind_bind. - eapply eq_itree_clo_bind with (UU := eq); [reflexivity | intros ? ? ->]. - setoid_rewrite bind_ret_l. - eapply eq_itree_clo_bind with (UU := eq); [reflexivity | intros ? ? ->]. - reflexivity. + ⟦ a ++ b ⟧c ≈ (⟦ a ⟧c ;; ⟦ b ⟧c). + Proof. + intros; by rewrite denote_code_app_eq_itree. Qed. Lemma denote_code_cons : forall i c, - ⟦ i::c ⟧c ≈ ⟦ i ⟧i;; ⟦ c ⟧c. - Proof using. + ⟦ i :: c ⟧c ≈ (⟦ i ⟧i ;; ⟦ c ⟧c). + Proof. intros. - cbn. - go. - apply eutt_eq_bind; intros (). - go. - setoid_rewrite bind_ret_l. - reflexivity. + go*. + ibind=; intros []. + go*. + by setoid_rewrite bind_ret_l. Qed. Lemma denote_code_singleton : forall i, ⟦ [i] ⟧c ≈ ⟦ i ⟧i. - Proof using. + Proof. intros a. - cbn. - go. + rewrite denote_code_cons. bind_ret_r2. - apply eutt_eq_bind; intros []. - go. - reflexivity. + ibind=; intros []. + apply denote_code_nil. Qed. - (** [denote_phi] *) - (* TODO: make a choice about it and move *) - Opaque assoc. - Lemma denote_phi_hd : forall bid e id τ tl, - ⟦ (id, Phi τ ((bid,e)::tl)) ⟧Φ bid ≈ uv <- ⟦ e at τ ⟧e;; Ret (id,uv). - Proof using. + (** [denote_phi] + - ⟦ (x, Phi τ ({[bid := e]} ∪ tl)) ⟧Φ bid ≈ (uv <- ⟦ e at τ ⟧e; Ret (x,uv)). + *) + + Lemma denote_phi_in : forall bid e x τ args, + args !! bid = Some e -> + ⟦ (x, Phi τ args) ⟧Φ bid ≈ (uv <- ⟦ e at τ ⟧e; Ret (x,uv)). + Proof. intros; cbn. - rewrite assoc_hd; reflexivity. + by simplify_map_eq. Qed. - Lemma denote_phi_tl : forall bid bid' e id τ tl, + Lemma denote_phi_cup_l : forall bid x τ args args', + args !! bid = None -> + ⟦ (x, Phi τ (args ∪ args')) ⟧Φ bid ≈ ⟦ (x, Phi τ args') ⟧Φ bid. + Proof. + intros; cbn. + by rewrite lookup_union_r. + Qed. + + Lemma denote_phi_cup_r : forall bid x τ args args', + args' !! bid = None -> + ⟦ (x, Phi τ (args ∪ args')) ⟧Φ bid ≈ ⟦ (x, Phi τ args) ⟧Φ bid. + Proof. + intros; cbn. + by rewrite lookup_union_l. + Qed. + + Lemma denote_phi_add : forall bid e x τ tl, + ⟦ (x, Phi τ ({[bid := e]} ∪ tl)) ⟧Φ bid ≈ (uv <- ⟦ e at τ ⟧e; Ret (x,uv)). + Proof. + intros; cbn. + by simplify_map_eq. + Qed. + + Lemma denote_phi_add_ne : forall bid bid' e x τ tl, bid <> bid' -> - ⟦ (id, Phi τ ((bid',e)::tl)) ⟧Φ bid ≈ ⟦ (id, Phi τ tl) ⟧Φ bid. - Proof using. + ⟦ (x, Phi τ ({[bid' := e ]} ∪ tl)) ⟧Φ bid ≈ ⟦ (x, Phi τ tl) ⟧Φ bid. + Proof. intros; cbn. - rewrite assoc_tl; auto; reflexivity. + rewrite lookup_union_r; [done | by simplify_map_eq]. Qed. - Lemma denote_no_phis : forall x, + (** [denote_phis] + *) + + Lemma denote_phis_nil : forall x, ⟦ [] ⟧Φs x ≈ Ret tt. - Proof using. + Proof. intros. - cbn. go. - cbn; go. - unfold denote_phis; cbn. - reflexivity. + go*. + by go*. Qed. + (* This only holds after interpretation: we can't justify the commutation of writes at this level + Lemma denote_phis_cons : forall b φ φs, + ⟦φ :: φs⟧Φs b ≈ + (v <- ⟦φ⟧Φ b; + ⟦φs⟧Φs b;; + trigger (LocalWrite (fst v) (snd v))) + . + Proof. + intros ???; revert φ; induction φs as [| φhd φs IH]. + - intros [? []]. + go*. + ibind=; intros []; go*. + go**. + bind_ret_r2. + by ibind=; intros []; go*. + - intros [? []]. + cbn. + rewrite bind_bind. + ibind=; intros []. + specialize (IH φhd); cbn in IH. + rewrite IH. + go**. + ibind=; intros []; go*. + ibind=; intros vs; go**. + repeat setoid_rewrite bind_bind. + repeat setoid_rewrite bind_ret_l. + cbn. + cbn in IH. + + match goal with + |- context[raise ?s] => generalize s + end. + intros s. + cbn. + match goal with + |- context[raise ?s] => generalize s + end. + intros s'. + rewrite ?bind_bind. + apply eutt_eq_bind. + intros []. + rewrite ?bind_bind, ?bind_ret_l. + cbn. + cbn in IH. + Admitted. + *) + + (** [denote_block] *) Lemma denote_block_unfold_cont : - forall {R} id phis c t s origin (k : _ -> itree _ R), - ⟦ mk_block id phis c t s ⟧b origin >>= k - ≈ - ⟦ phis ⟧Φs origin;; + forall {R} phis c t s origin (k : _ -> itree _ R), + ⟦ mk_block phis c t s ⟧b origin >>= k + ≈ + (⟦ phis ⟧Φs origin;; ⟦ c ⟧c;; - translate exp_to_instr ⟦ t ⟧t >>= k. - Proof using. - intros; cbn; repeat setoid_rewrite bind_bind. - reflexivity. + ⟦ t ⟧t >>= k). + Proof. + by intros; cbn; repeat setoid_rewrite bind_bind. Qed. Lemma denote_block_unfold : - forall id phis c t s origin, - ⟦ mk_block id phis c t s ⟧b origin ≈ - ⟦ phis ⟧Φs origin;; + forall phis c t s origin, + ⟦ mk_block phis c t s ⟧b origin ≈ + (⟦ phis ⟧Φs origin;; ⟦ c ⟧c;; - translate exp_to_instr ⟦ t ⟧t. - Proof using. - intros; cbn; reflexivity. + ⟦ t ⟧t). + Proof. + done. Qed. (** [denote_ocfg] *) - Lemma denote_ocfg_nil: forall s, ⟦ [] ⟧bs s ≈ Ret (inl s). - Proof using. + Lemma denote_ocfg_empty: forall s, ⟦ ∅ ⟧bs s ≈ Ret (inl s). + Proof. intros []; unfold denote_ocfg. - match goal with - | |- CategoryOps.iter (C := ktree _) ?body ?s ≈ _ => - rewrite (unfold_iter body s) - end. - cbn; go. - reflexivity. + setoid_rewrite unfold_iter. + simplify_map_eq. + by go*. Qed. - Lemma denote_ocfg_unfold_in: forall bks bid_from bid_src bk, - find_block bks bid_src = Some bk -> - ⟦ bks ⟧bs (bid_from, bid_src) ≈ - vob <- ⟦ bk ⟧b bid_from ;; + Lemma denote_ocfg_in_eq_itree: forall bks bid_from bid_src bk, + bks !! bid_src = Some bk -> + ⟦ bks ⟧bs (bid_from, bid_src) ≅ + (vob <- ⟦ bk ⟧b bid_from ; match vob with | inr v => Ret (inr v) - | inl bid_target => ⟦ bks ⟧bs (bid_src, bid_target) - end. - Proof using. - intros * GET_BK. + | inl bid_target => Tau (⟦ bks ⟧bs (bid_src, bid_target)) + end). + Proof. + intros * lu. cbn. unfold denote_ocfg at 1. - rewrite KTreeFacts.unfold_iter_ktree. cbn. - rewrite GET_BK. - repeat setoid_rewrite bind_bind. - repeat (apply eutt_eq_bind; intros ?). - break_sum; rewrite bind_ret_l; [|reflexivity]. - rewrite tau_eutt; reflexivity. - Qed. - - Lemma denote_ocfg_unfold_not_in: forall bks bid_from bid_src, - find_block bks bid_src = None -> - ⟦ bks ⟧bs (bid_from, bid_src) ≈ Ret (inl (bid_from,bid_src)). - Proof using. - intros * GET_BK. - unfold denote_ocfg. - rewrite KTreeFacts.unfold_iter_ktree. - rewrite GET_BK; cbn. - rewrite bind_ret_l. - reflexivity. + setoid_rewrite unfold_iter_ktree. + rewrite lu. + go*. + repeat (ibind=; intros ?). + break_sum; go*; [| done]. + by apply eqit_Tau. Qed. - Lemma denote_ocfg_unfold_in_euttge: forall bks bid_from bid_src bk, - find_block bks bid_src = Some bk -> + Lemma denote_ocfg_in_euttge: forall bks bid_from bid_src bk, + bks !! bid_src = Some bk -> ⟦ bks ⟧bs (bid_from, bid_src) ≳ - vob <- ⟦ bk ⟧b bid_from ;; + (vob <- ⟦ bk ⟧b bid_from ; match vob with | inr v => Ret (inr v) | inl bid_target => ⟦ bks ⟧bs (bid_src, bid_target) - end. - Proof using. - intros * GET_BK. - cbn. unfold denote_ocfg at 1. - rewrite KTreeFacts.unfold_iter_ktree. cbn. - rewrite GET_BK. - repeat setoid_rewrite bind_bind. - repeat (eapply eqit_bind; [reflexivity | intros ?]). - break_sum; rewrite bind_ret_l; [|reflexivity]. - rewrite tau_euttge; reflexivity. + end). + Proof. + intros * lu. + rewrite denote_ocfg_in_eq_itree; eauto. + ibind=; intros ?. + break_sum; go*; [| done]. + by rewrite tau_euttge. Qed. - Lemma denote_ocfg_unfold_in_eq_itree: forall bks bid_from bid_src bk, - find_block bks bid_src = Some bk -> - ⟦ bks ⟧bs (bid_from, bid_src) ≅ - vob <- ⟦ bk ⟧b bid_from ;; + Lemma denote_ocfg_in: forall bks bid_from bid_src bk, + bks !! bid_src = Some bk -> + ⟦ bks ⟧bs (bid_from, bid_src) + ≈ + (vob <- ⟦ bk ⟧b bid_from ; match vob with | inr v => Ret (inr v) - | inl bid_target => Tau (⟦ bks ⟧bs (bid_src, bid_target)) - end. - Proof using. - intros * GET_BK. - cbn. unfold denote_ocfg at 1. - rewrite KTreeFacts.unfold_iter_ktree. cbn. - rewrite GET_BK. - repeat setoid_rewrite bind_bind. - repeat (eapply eqit_bind; [reflexivity | intros ?]). - break_sum; rewrite bind_ret_l; [|reflexivity]. - apply eqit_Tau. - reflexivity. + | inl bid_target => ⟦ bks ⟧bs (bid_src, bid_target) + end). + Proof. + intros * lu. + by rewrite denote_ocfg_in_euttge. Qed. - Lemma denote_ocfg_unfold_not_in_eq_itree: forall bks bid_from bid_src, - find_block bks bid_src = None -> + Lemma denote_ocfg_nin_eq_itree: forall bks bid_from bid_src, + bks !! bid_src = None -> ⟦ bks ⟧bs (bid_from, bid_src) ≅ Ret (inl (bid_from,bid_src)). - Proof using. - intros * GET_BK. + Proof. + intros * lu. unfold denote_ocfg. - rewrite KTreeFacts.unfold_iter_ktree. - rewrite GET_BK; cbn. - rewrite bind_ret_l. - reflexivity. + rewrite unfold_iter_ktree, lu. + by go*. Qed. - Lemma denote_ocfg_unfold_eq_itree: forall bks bid_from bid_src, + Lemma denote_ocfg_nin: forall bks bid_from bid_src, + bks !! bid_src = None -> + ⟦ bks ⟧bs (bid_from, bid_src) ≈ Ret (inl (bid_from,bid_src)). + Proof. + intros * lu. + by rewrite denote_ocfg_nin_eq_itree. + Qed. + + Lemma denote_ocfg_unfold: forall bks bid_from bid_src, ⟦ bks ⟧bs (bid_from, bid_src) ≅ - match find_block bks bid_src with - | Some bk => vob <- ⟦ bk ⟧b bid_from ;; - match vob with - | inr v => Ret (inr v) - | inl bid_target => Tau (⟦ bks ⟧bs (bid_src, bid_target)) - end - | None => Ret (inl (bid_from,bid_src)) - end. - Proof using. + (match bks !! bid_src with + | Some bk => vob <- ⟦ bk ⟧b bid_from ; + match vob with + | inr v => Ret (inr v) + | inl bid_target => Tau (⟦ bks ⟧bs (bid_src, bid_target)) + end + | None => Ret (inl (bid_from,bid_src)) + end). + Proof. intros *. break_match_goal. - - rewrite denote_ocfg_unfold_in_eq_itree; eauto; reflexivity. - - rewrite denote_ocfg_unfold_not_in_eq_itree; eauto; reflexivity. + - by rewrite denote_ocfg_in_eq_itree. + - by rewrite denote_ocfg_nin_eq_itree. Qed. Section Outputs. @@ -310,37 +419,38 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). Lemma raise_has_all_posts : forall {E X} `{FailureE -< E} s Q, @raise E X _ s ⤳ Q. - Proof using. + Proof. unfold raise; intros. apply has_post_bind; intros []. Qed. Lemma raiseUB_has_all_posts : forall {E X} `{UBE -< E} s Q, @raiseUB E _ X s ⤳ Q. - Proof using. + Proof. unfold raise; intros. apply has_post_bind; intros []. Qed. - Lemma unEither_eta : forall {T m A} (x : eitherT T m A), {|unEitherT := unEitherT x|} = x. - Proof using. + Lemma raise_has_all_posts_cont : forall {E X Y} `{FailureE -< E} s (k : X -> itree E Y) Q, + (x <- @raise E X _ s; k x) ⤳ Q. + Proof. intros. - destruct x. - f_equal. + rewrite raise_bind_itree. + apply raise_has_all_posts. Qed. - - Lemma unIdent_eta : forall {A} (x : ident A), {|unIdent := unIdent x|} = x. - Proof using. + Lemma raiseUB_has_all_posts_cont : forall {E X Y} `{UBE -< E} s (k : X -> itree E Y) Q, + (x <- @raiseUB E _ X s; k x) ⤳ Q. + Proof. intros. - destruct x. - f_equal. + rewrite raiseUB_bind_itree. + apply raiseUB_has_all_posts. Qed. Lemma select_switch_in : forall x default_dest brs id, select_switch x default_dest brs = inr id -> id = default_dest \/ In id (List.map snd brs). - Proof using. + Proof. intros x default_dest brs id SELECT. induction brs. - inversion SELECT; auto. @@ -352,110 +462,100 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). break_match_hyp; inversion SELECT; subst; cbn; tauto. Qed. + Ltac hpbind := apply has_post_bind; intros ?. + Ltac ehpbind := eapply has_post_bind_strong. + Ltac uehpbind := unshelve eapply has_post_bind_strong. + Tactic Notation "hpbind" "with" uconstr(t) := apply has_post_bind_strong with t. + Ltac hpret := apply eutt_Ret. + Ltac hpabs := + try (apply raise_has_all_posts || apply raiseUB_has_all_posts || + apply raise_has_all_posts_cont || apply raiseUB_has_all_posts_cont + ). + + Lemma has_post_map_monad : + forall {E} {A B} (f : A -> itree E B) (P : B -> Prop) (l : list A), + (forall x, List.In x l -> f x ⤳ P) -> + map_monad f l ⤳ Forall P. + Proof. + intros * IH'. + induction l as [| t l IH]. + - by hpret. + - go*. + hpbind with P; [apply IH'; by left | ]. + intros ? HP. + hpbind with (Forall P); [apply IH; intros; apply IH'; right; auto | ]. + intros ? HP'; hpret. + by apply Forall_cons. + Qed. + + Ltac hpmap := apply has_post_map_monad. + + Tactic Notation "break_err" "as" ident(H) := + match goal with + |- context[lift_err _ ?x] => destruct x eqn:H; cbn [lift_err] + end . + Ltac break_err := let H := fresh in break_err as H. + + Tactic Notation "hperr" "as" ident(H) := break_err as H; [hpabs |]. + Tactic Notation "hperr" := let H := fresh in hperr as H. + + Import ITree. + Import Events.DV. + Lemma denote_terminator_exits_in_outputs : forall term, - ⟦ term ⟧t ⤳ sum_pred (fun id => In id (terminator_outputs term)) TT. - Proof using. - intros term; destruct term eqn:Hterm; cbn; try (apply raise_has_all_posts || apply eutt_Ret; cbn; eauto). + ⟦ term ⟧t ⤳ sum_pred (fun id => id ∈ terminator_outputs term) TT. + Proof with set_solver. + intros term; destruct term eqn:Hterm; cbn; try (hpabs || hpret; set_solver). - destruct v. - apply has_post_bind; intros ?. - apply eutt_Ret; cbn; eauto. + hpbind. + hpret... - destruct v; cbn. - apply has_post_bind; intros ?. - apply has_post_bind; intros ?. - break_match_goal; try (apply raise_has_all_posts || apply raiseUB_has_all_posts). - break_match_goal; apply eutt_Ret; cbn; eauto. + hpbind. + hpbind. + break_match_goal; hpabs. + break_match_goal; hpret... - destruct v; cbn. - apply has_post_bind; intros ?. - apply has_post_bind; intros ?. - break_match_goal; - try (apply raise_has_all_posts || apply raiseUB_has_all_posts). - - clear Hterm. - clear term. - - eapply has_post_bind_strong with - (S := fun switches => - Forall - (fun id => In id (List.map snd brs)) - (List.map snd switches)). - - + induction brs; cbn. - * apply eutt_Ret. cbn. - apply Forall_nil. - * break_match_goal; subst. - break_match_goal; subst. - - repeat break_match_goal; - try (cbn; go; setoid_rewrite raise_bind_itree; apply raise_has_all_posts). - - -- (* 64 *) - go. - eapply eutt_clo_bind; eauto. - intros u1 u2 H. - apply eutt_Ret. - cbn. - cbn in H. - apply Forall_cons; eauto. - apply Forall_impl with (P := fun id => In id (List.map snd brs)); eauto. - -- - go. - eapply eutt_clo_bind; eauto. - intros u1 u2 H. - apply eutt_Ret. - cbn. - cbn in H. - apply Forall_cons; eauto. - apply Forall_impl with (P := fun id => In id (List.map snd brs)); eauto. - -- - go. - eapply eutt_clo_bind; eauto. - intros u1 u2 H. - apply eutt_Ret. - cbn. - cbn in H. - apply Forall_cons; eauto. - apply Forall_impl with (P := fun id => In id (List.map snd brs)); eauto. - -- - go. - eapply eutt_clo_bind; eauto. - intros u1 u2 H. - apply eutt_Ret. - cbn. - cbn in H. - apply Forall_cons; eauto. - apply Forall_impl with (P := fun id => In id (List.map snd brs)); eauto. - -- - go. - eapply eutt_clo_bind; eauto. - intros u1 u2 H. - apply eutt_Ret. - cbn. - cbn in H. - apply Forall_cons; eauto. - apply Forall_impl with (P := fun id => In id (List.map snd brs)); eauto. - + intros x1 H. - destruct (select_switch x0 default_dest x1) eqn:HSwitch; cbn. - apply raise_has_all_posts. - apply select_switch_in in HSwitch. - apply eutt_Ret; cbn. - destruct HSwitch; auto; right. - eapply Forall_forall in H; eauto. - - apply raiseUB_has_all_posts. + hpbind. + hpbind. + break_match_goal; hpabs. + clear Hterm term. + + hpbind with (Forall (fun id => In (snd id) (List.map snd brs))). + + hpmap. + intros [[] ?] ?. + case_match; hpabs. + case_match; go; hpret. + subst. + all: by apply in_map with (f := snd) in H. + + intros ? FORALL. + hperr as Hswitch. + hpret; cbn. + apply select_switch_in in Hswitch. + destruct_or?. + set_solver. + (* The remaining of this proof should not be so messy. Why [gset_semi_set] is not visible earlier? *) + apply Coqlib.list_in_map_inv in Hswitch as ([? ?] & -> & IN). + rewrite Forall_forall in FORALL. + apply FORALL in IN. + cbn in *. + apply elem_of_list_In in IN. + eapply elem_of_list_to_set in IN. + apply elem_of_union_r. + apply IN. + Unshelve. + apply gset_semi_set. Qed. Definition exits_in_outputs {t} ocfg : block_id * block_id + uvalue -> Prop := - sum_pred (fun fto => In (snd fto) (@outputs t ocfg)) TT. + sum_pred (fun fto => snd fto ∈ @outputs t ocfg) TT. Lemma denote_bk_exits_in_outputs : forall b from, - ⟦ b ⟧b from ⤳ sum_pred (fun id => In id (successors b)) TT. - Proof using. - intros. - cbn. - apply has_post_bind; intros []. - apply has_post_bind; intros []. - apply has_post_translate. + ⟦ b ⟧b from ⤳ sum_pred (fun id => id ∈ successors b) TT. + Proof. + intros; cbn. + repeat hpbind. apply denote_terminator_exits_in_outputs. Qed. @@ -469,10 +569,10 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). (INIT : Qb fto) (IND : forall fto (b : block dtyp), Qb fto -> - find_block bks (snd fto) = Some b -> + bks !! snd fto = Some b -> ⟦ b ⟧b (fst fto) ⤳ sum_pred (fun to => Qb (snd fto, to)) Qv), ⟦ bks ⟧bs fto ⤳ sum_pred Qb Qv. - Proof using. + Proof. intros * INIT IND. eapply has_post_iter_strong; eauto. intros [f to] PRE. @@ -490,14 +590,14 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). *) Lemma denote_ocfg_has_post : forall (bks : ocfg _) fto (Qb : block_id -> Prop) (Qv : uvalue -> Prop) - (ENTER : In (snd fto) (inputs bks)) + (ENTER : snd fto ∈ inputs bks) (IND : forall fto (b : block dtyp), - find_block bks (snd fto) = Some b -> + bks !! snd fto = Some b -> ⟦ b ⟧b (fst fto) ⤳ sum_pred Qb Qv), ⟦ bks ⟧bs fto ⤳ sum_pred (prod_pred TT Qb) Qv. - Proof using. + Proof. intros * IN IND. - apply has_post_iter_strong with (Inv := fun x => In (snd x) (inputs bks) \/ Qb (snd x)) + apply has_post_iter_strong with (Inv := fun x => snd x ∈ inputs bks \/ Qb (snd x)) ; eauto. intros [f to] HYP. flatten_goal. @@ -512,109 +612,90 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). Lemma denote_ocfg_exits_in_outputs : forall bks fto, - In (snd fto) (inputs bks) -> + snd fto ∈ inputs bks -> ⟦ bks ⟧bs fto ⤳ exits_in_outputs bks. - Proof using. + Proof. intros * IN. - apply has_post_weaken with (P := sum_pred (prod_pred TT (fun b => In b (outputs bks))) TT). + apply has_post_weaken with (P := sum_pred (prod_pred TT (fun b => b ∈ outputs bks)) TT). 2: intros [[]|] ?; cbn in *; intuition. apply denote_ocfg_has_post; eauto. intros. eapply has_post_weaken. eapply denote_bk_exits_in_outputs. intros []; cbn; intuition. - eapply In_bk_outputs; eauto. + by eapply outputs_elem_of. Qed. End Outputs. (** * denote_ocfg *) - Lemma denote_ocfg_app_no_edges : + Lemma denote_ocfg_union_no_edges : forall (bks1 bks2 : ocfg _) fto, - find_block bks1 (snd fto) = None -> + bks1 !! snd fto = None -> no_reentrance bks1 bks2 -> - ⟦ bks1 ++ bks2 ⟧bs fto ≈ ⟦ bks2 ⟧bs fto. - Proof using. + ⟦ bks1 ∪ bks2 ⟧bs fto ≈ ⟦ bks2 ⟧bs fto. + Proof. intros bks1 bks2 [f to] FIND NOBACK. - apply (@KTreeFacts.eutt_iter_gen _ _ _ (fun fto fto' => fto' = fto /\ find_block bks1 (snd fto) = None)); auto. + apply (@KTreeFacts.eutt_iter_gen _ _ _ (fun fto fto' => fto' = fto /\ bks1 !! snd fto = None)); auto. clear f to FIND; intros fto fto' [-> FIND]; destruct fto as [f to] . cbn in *. - epose proof (find_block_none_app _ bks2 _ FIND) as FIND_L1L2. - rewrite FIND_L1L2. - destruct (find_block bks2 to) eqn:FIND_L2. + rewrite lookup_union_r; auto. + case_match eqn:FIND_L2. - eapply eutt_post_bind. apply denote_bk_exits_in_outputs. intros [id | v] ?; cbn; apply eutt_Ret; eauto. eapply inl_morphism; split; auto. - eapply find_block_not_in_inputs,no_reentrance_not_in; eauto. - eapply In_bk_outputs; eauto. - + cbn. cbn in *. + eapply free_out_of_inputs,no_reentrance_not_in; eauto. + eapply outputs_elem_of; eauto. - apply eutt_Ret; right; auto. Qed. - Lemma denote_ocfg_app : + Lemma denote_ocfg_union : forall bks1 bks2 fto, no_reentrance bks1 bks2 -> - ⟦ bks1 ++ bks2 ⟧bs fto ≈ - 'x <- ⟦ bks1 ⟧bs fto;; + ⟦ bks1 ∪ bks2 ⟧bs fto ≈ + ('x <- ⟦ bks1 ⟧bs fto; match x with | inl fto2 => ⟦ bks2 ⟧bs fto2 | inr v => Ret (inr v) - end. - Proof using. + end). + Proof. intros * NOBACK. revert fto. einit. ecofix CIH. intros [f to]. - destruct (find_block bks1 to) eqn:FIND. - - unfold denote_ocfg. - unfold iter, Iter_Kleisli, Basics.iter, MonadIter_itree. - match goal with - |- euttG _ _ _ _ _ ?t _ => remember t; rewrite unfold_iter; subst - end. - rewrite unfold_iter; cbn. - match_rewrite. - rewrite !bind_bind. - pose proof find_block_some_app bks1 bks2 to FIND as FIND_APP. - rewrite FIND_APP. - cbn. - rewrite !bind_bind. - match goal with - |- euttG _ _ _ _ _ ?t _ => remember t - end. - subst; ebind; econstructor; [reflexivity | intros ? ? <-]. - ebind; econstructor; [reflexivity | intros ? ? <-]. - ebind; econstructor; [reflexivity | intros ? ? <-]. - destruct u2 as [bid | v]. - + rewrite !bind_ret_l. - rewrite bind_tau. - etau. - + rewrite !bind_ret_l. - eret. + case (bks1 !! to) eqn:FIND. + - rewrite 2 denote_ocfg_unfold. + simplify_map_eq. + go. + ebind; econstructor; [reflexivity | intros ??<-]. + case_match. + rewrite bind_tau; etau. + by go. - efinal. - rewrite denote_ocfg_app_no_edges; auto. - rewrite denote_ocfg_unfold_not_in with (bks := bks1); auto. - rewrite bind_ret_l; reflexivity. + rewrite denote_ocfg_union_no_edges; auto. + by rewrite (denote_ocfg_nin bks1); auto; go*. Qed. Lemma denote_ocfg_flow_left : forall ocfg1 ocfg2 fto, independent_flows ocfg1 ocfg2 -> - In (snd fto) (inputs ocfg1) -> - ⟦ ocfg1 ++ ocfg2 ⟧bs fto ≈ - ⟦ ocfg1 ⟧bs fto. - Proof using. + snd fto ∈ inputs ocfg1 -> + ⟦ ocfg1 ∪ ocfg2 ⟧bs fto ≈ + ⟦ ocfg1 ⟧bs fto. + Proof. intros * INDEP IN. - rewrite denote_ocfg_app; [| auto using independent_flows_no_reentrance_l]. + rewrite denote_ocfg_union; [| auto using independent_flows_no_reentrance_l]. bind_ret_r2. eapply eutt_post_bind; [apply denote_ocfg_exits_in_outputs; eauto |]. intros [[f to] | ?] EXIT; [| reflexivity]. - rewrite denote_ocfg_unfold_not_in; [reflexivity |]. + rewrite denote_ocfg_nin; [reflexivity |]. cbn in *. - apply find_block_not_in_inputs. + apply free_out_of_inputs. eapply no_reentrance_not_in; eauto. apply INDEP. Qed. @@ -625,7 +706,7 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). In (snd fto) (inputs ocfg2) -> ⟦ ocfg1 ++ ocfg2 ⟧bs fto ≈ ⟦ ocfg2 ⟧bs fto. - Proof using. + Proof. intros * INDEP IN. rewrite denote_ocfg_app; [| auto using independent_flows_no_reentrance_l]. destruct fto as [f to]; cbn in *. @@ -646,7 +727,7 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). | inr x => Ret (inr x) end . - Proof using. + Proof. intros * ->; revert from to. einit. ecofix CIH. @@ -677,6 +758,7 @@ Module Type DenotationTheory (IS : InterpreterStack) (TOP : LLVMTopLevel IS). Transparent denote_block. End DenotationTheory. + Module Make (IS : InterpreterStack) (TOP : LLVMTopLevel IS) : DenotationTheory IS TOP. Include DenotationTheory IS TOP. End Make. diff --git a/src/coq/Utils/ListUtil.v b/src/coq/Utils/ListUtil.v index b23b982d..ea5f31f3 100644 --- a/src/coq/Utils/ListUtil.v +++ b/src/coq/Utils/ListUtil.v @@ -1,3 +1,5 @@ +Set Warnings "-intuition-auto-with-star". + From Coq Require Import String List diff --git a/src/coq/Utils/MonadEq1Laws.v b/src/coq/Utils/MonadEq1Laws.v index d23a8789..489d21fe 100644 --- a/src/coq/Utils/MonadEq1Laws.v +++ b/src/coq/Utils/MonadEq1Laws.v @@ -83,9 +83,10 @@ Section EitherT. End EitherT. +Require Import ITree.Core.ITreeMonad. + Section ITree. Variable E : Type -> Type. - Require Import ITree.Core.ITreeMonad. Lemma eq1_ret_ret_itree : forall {A} (x y : A), (ret x : itree E A) ≈ ret y -> x = y. diff --git a/src/coq/Utils/MonadReturnsLaws.v b/src/coq/Utils/MonadReturnsLaws.v index ff111c4c..e14eee67 100644 --- a/src/coq/Utils/MonadReturnsLaws.v +++ b/src/coq/Utils/MonadReturnsLaws.v @@ -69,12 +69,12 @@ Section ExtraLaws. (* Won't work when a refinement can fail and not return something *) Class MonadReturnsProper := - { MReturns_Proper :> forall {A} (a : A), + { MReturns_Proper :: forall {A} (a : A), Proper ((fun x y => eq1 y x) ==> Basics.impl) (MReturns a) }. Class MFailsProper := - { MFails_Proper :> forall A, Proper (eq1 (A:=A) ==> Basics.impl) MFails }. + { MFails_Proper :: forall A, Proper (eq1 (A:=A) ==> Basics.impl) MFails }. (* These won't work with UB / Error refinement relations *) Class MonadReturnsFails := @@ -105,7 +105,7 @@ Section MReturns_ProperFlip. Context {MRET : @MonadReturns M Monad Eq1}. Class MonadReturns_ProperFlip := - { MReturns_ProperFlip :> forall {A} (a : A), + { MReturns_ProperFlip :: forall {A} (a : A), Proper (eq1 ==> Basics.impl) (MReturns a) }. @@ -119,7 +119,7 @@ Section MonadReturnsInv. Context {Eq1 : @Eq1 M}. Context {MRET : @MonadReturns M Monad Eq1}. Class MonadReturns_Proper_inv := - { MReturns_Proper_inv :> forall {A} (a: A), + { MReturns_Proper_inv :: forall {A} (a: A), Proper ((fun (x y : M A) => MReturns a x <-> MReturns a y) ==> Monad.eq1) (fun x => x) }. End MonadReturnsInv. @@ -333,8 +333,8 @@ Section Sum. Qed. End Sum. +Import IdentityMonad. Section Ident. - Import IdentityMonad. Definition IdentReturns {A} (a : A) (ma : ident A) : Prop := match ma with @@ -499,8 +499,8 @@ Section Ident. Qed. End Ident. +Import EitherMonad. Section EitherT. - Import EitherMonad. Context {E : Type}. Context {M : Type -> Type}. @@ -690,14 +690,14 @@ Section EitherT. End EitherT. -Section StateT. - From ITree Require Import - ITree. +From ITree Require Import + ITree. - Import Monads. +Import Monads. - From Vellvm Require Import Utils.StateMonads. +From Vellvm Require Import Utils.StateMonads. +Section StateT. Context {S : Type}. Context {SINHAB : Inhabited S}. Context {M : Type -> Type}. diff --git a/src/coq/Utils/Monads.v b/src/coq/Utils/Monads.v index 515e0030..8c80e61e 100644 --- a/src/coq/Utils/Monads.v +++ b/src/coq/Utils/Monads.v @@ -1,3 +1,5 @@ +Set Warnings "-intuition-auto-with-star". + From Coq Require Import List Morphisms. diff --git a/src/coq/Utils/NoEvent.v b/src/coq/Utils/NoEvent.v index a89be3ba..5ca201ec 100644 --- a/src/coq/Utils/NoEvent.v +++ b/src/coq/Utils/NoEvent.v @@ -1032,119 +1032,3 @@ Lemma no_event_inject_r : eauto. Qed. -(** * Other discussions *) - -(* YZ TODO: This file should not depend on VIR, this section should be eventually moved - somewhere in [Theory/] -*) -(* We want to express that a tree contains no [pickE] events, - and that if so that entails that the interpretation by the pick handlers - leads to the singleton predicate containing the elimination of the pick event. - Something like: - no_pick t -> - forall t', model_pick t t' -> t' ≈ elim_pick t - *) - -From Vellvm Require Import - Utils.Tactics - Utils.Util - Utils.PropT - Utils.PostConditions - Utils.NoFailure - Syntax.Traversal - Syntax.LLVMAst - Syntax.AstLib - Syntax.CFG - Syntax.DynamicTypes - Syntax.TypToDtyp - Semantics.LLVMEvents - Semantics.Denotation - Semantics.InterpretationStack - Semantics.TopLevel - Handlers.Handlers - Theory.InterpreterCFG - Theory.InterpreterMCFG - Theory.TopLevelRefinements - Theory.DenotationTheory - Theory.InstrLemmas. - - - -Import MonadNotation. -Open Scope monad_scope. - -Definition trigger_prop {E F} : F ~> PropT (E +' F) := - fun R e => fun t => t = r <- trigger e ;; ret r. - -Definition trigger_prop' {F} : F ~> PropT F := - fun R e => fun t => t = r <- trigger e ;; ret r. - -Definition is_singleton {E X} (ts : PropT E X) (t : itree E X) : Prop := - forall u, ts u -> u ≈ t. - -(* - Initially : E is UB (non det stuff) - F is other effects. -we have E +' F -E gets interepreted into a non-deterministic computation : PropT ?? -F gets "preserved" - *) - -(* Lemma deterministic_is_singleton : *) -(* forall {E F X} (RX : relation X) *) -(* (t : itree (E +' F) X) *) -(* (h : E ~> PropT F), *) -(* no_event_l t -> *) -(* is_singleton *) -(* (interp_prop (case_ h trigger_prop') X RX t) *) -(* (elim_l t). *) -(* Proof using. *) - -(* Admitted. *) - -(* t --pick> {t} --UB> {t} *) - -(* Definition interp_from_prop {E F} T (RR: T -> T -> Prop) (h : E ~> PropT F) : PropT (E +' F) T -> PropT F T := *) -(* fun Pt (t : itree F T) => *) -(* exists (t' : itree (E +' F) T) , *) -(* Pt t' /\ *) -(* (interp_prop (case_ h trigger_prop') _ RR t' t). *) - -Section DeterministicSingleton. - - (* Lemma deterministic_is_singleton' : *) - (* forall {E F X} (RX : relation X) *) - (* (ts : PropT (E +' F) X) *) - (* (t : itree (E +' F) X) *) - (* (h : E ~> PropT F), *) - (* is_singleton ts t -> *) - (* no_event_l t -> *) - (* is_singleton (interp_from_prop RX h ts) (elim_l t). *) - (* Proof using. *) - (* Admitted. *) - - (* - (* Definition deterministic_vellvm *) - Lemma deterministc_llvm_is_singleton : forall R RR t g sl mem, - deterministic_vellvm t -> - is_singleton (interp_mcfg5 (R := R) RR t g sl mem) (remove_pick_ub (interp_mcfg3 (R := R) t g sl mem)). - - (* - Then the same statement on llvm syntax by applying it with (t := denote_llvm p) - Then on the helix side: - - we know that there is (t: itree void1 X), - "inject (ExternalCallE +' PickE +' UBE +' DebugE +' FailureE) t ≈ interp_mcfg3 (denote_llvm p)" - *) - Proof using. Admitted. -*) -End DeterministicSingleton. - -Require Import MemoryAddress. -Require Import Sizeof. - -Module PICK_REMOVE (ADDR : ADDRESS) (IP : INTPTR) (SIZE : Sizeof) (Events : LLVM_INTERACTIONS ADDR IP SIZE). - Import Events. - - Variable remove_pick_ub : itree (ExternalCallE +' PickUvalueE +' UBE +' DebugE +' FailureE) ~> itree (ExternalCallE +' DebugE +' FailureE). - Variable deterministic_vellvm : forall R, itree L0 R -> Prop. -End PICK_REMOVE. diff --git a/src/coq/Utils/ParserHelper.v b/src/coq/Utils/ParserHelper.v index b979f6c5..4cdb0e01 100644 --- a/src/coq/Utils/ParserHelper.v +++ b/src/coq/Utils/ParserHelper.v @@ -16,7 +16,7 @@ Definition BFloat := Flocq.Core.Defs.Float radix2. Definition inc_e (f : bfloat) (de : positive) : option bfloat := let '(m, e) := (Fnum f, Fexp f) in let rm := two_power_pos de in - if (Zmod m rm =? 0) + if (Z.modulo m rm =? 0) then Some (BFloat (m / two_power_pos de) (e + Z.pos de)) else None. @@ -442,7 +442,7 @@ Section Correctness. all: subst. all: try lia. assert (m mod 2 ^ Z.pos d < 2 ^ Z.pos d); try lia. - apply Zmod_pos_bound. + apply Z.mod_pos_bound. apply Z.pow_pos_nonneg; lia. rewrite two_power_pos_equiv; generalize (Z.pow_pos_nonneg 2 (Z.pos d)); lia. Qed. diff --git a/src/coq/Utils/Util.v b/src/coq/Utils/Util.v index 9d69da96..59062285 100644 --- a/src/coq/Utils/Util.v +++ b/src/coq/Utils/Util.v @@ -26,7 +26,7 @@ Section nat_Show. let acc' := get_last_digit n ++ acc in match n / 10 with | 0 => acc' - | n' => string_of_nat_aux acc' n' + | _n' => string_of_nat_aux acc' _n' end. intros _ n m ineq. unfold id; simpl. @@ -61,9 +61,9 @@ Section nat_Show. subst. exfalso. destruct n8. - 2: generalize (Nat.mod_upper_bound n 10 (ltac:(auto))); intros EQ; rewrite Heq in EQ; lia. + 2: generalize (Nat.mod_upper_bound n 10 (ltac:(auto))); intros EQ; rewrite Heq in EQ; lia. destruct n9. - 2: generalize (Nat.mod_upper_bound m 10 (ltac:(auto))); intros EQ; rewrite Heq0 in EQ; lia. + 2: generalize (Nat.mod_upper_bound m 10 (ltac:(auto))); intros EQ; rewrite Heq0 in EQ; lia. exfalso; apply ineq,(mod_div_eq n m 10); lia. Qed. @@ -101,7 +101,7 @@ Section nat_Show. s1 = s1'. Proof using. induction s2 as [| c s2 IH]. - - intros s1 s1' H; rewrite 2 append_EmptyString in H; auto. + - intros s1 s1' H; rewrite 2 append_EmptyString in H; auto. - intros s1 s1' H. rewrite append_String in H. rewrite (append_String s1' c s2) in H. @@ -174,7 +174,7 @@ Section nat_Show. s1 = s1'. Proof using. induction s1 as [| c1 s1 IH]; simpl; intros. - - destruct s1'; [reflexivity | inv H0]. + - destruct s1'; [reflexivity | inv H0]. - destruct s1' as [| c1' s1']; [inv H0 |]. simpl in *. inv H0. @@ -193,12 +193,12 @@ Section nat_Show. assert (String.length s1 = String.length s1'). { generalize (length_append s1 s2). intros ?. - rewrite H0,H, length_append in H1. + rewrite H0,H, length_append in H1. lia. } eapply append_same_length_eq_l in H1; eauto. subst. - eapply append_simplify_l; eauto. + eapply append_simplify_l; eauto. Qed. Ltac eq_fun H f := @@ -233,8 +233,8 @@ Section nat_Show. + intros abs. apply (get_last_digit_inj n m); try lia. apply append_simplify_r in abs; auto. - + destruct (string_of_nat_aux_prepends (S n0) (get_last_digit m ++ acc)) as (hd & nonnil & ->). - intros abs. + + destruct (string_of_nat_aux_prepends (S n0) (get_last_digit m ++ acc)) as (hd & nonnil & ->). + intros abs. match type of abs with | ?s1 = ?s2 => assert (abs':String.length s1 = String.length s2) by (rewrite abs; reflexivity) end. @@ -243,8 +243,8 @@ Section nat_Show. apply length_nonEmpty in nonnil; simpl in *. lia. - flatten_goal. - + destruct (string_of_nat_aux_prepends (S n0) (get_last_digit n ++ acc)) as (hd & nonnil & ->). - intros abs. + + destruct (string_of_nat_aux_prepends (S n0) (get_last_digit n ++ acc)) as (hd & nonnil & ->). + intros abs. match type of abs with | ?s1 = ?s2 => assert (abs':String.length s1 = String.length s2) by (rewrite abs; reflexivity) end. @@ -265,7 +265,7 @@ Section nat_Show. auto with arith. auto. * destruct (string_of_nat_aux_prepends (S n0) (get_last_digit n ++ acc)) as (hd & nonnil & ->). - destruct (string_of_nat_aux_prepends (S n1) (get_last_digit m ++ acc)) as (hd' & nonnil' & ->). + destruct (string_of_nat_aux_prepends (S n1) (get_last_digit m ++ acc)) as (hd' & nonnil' & ->). intros abs. rewrite 2 append_assoc in abs. apply append_simplify_r in abs. @@ -274,12 +274,12 @@ Section nat_Show. unfold get_last_digit in abs. apply H0; clear H0. do 9 (flatten_all; [do 9 (flatten_all; try easy) |]). - do 9 (flatten_all; try easy). + do 9 (flatten_all; try easy). subst. assert (tmp:10 <> 0) by lia. destruct n8; [| generalize (Nat.mod_upper_bound n 10 tmp); intros ineq; rewrite Heq in ineq; lia]. destruct n17; [easy| generalize (Nat.mod_upper_bound m 10 tmp); intros ineq; rewrite Heq8 in ineq; lia]. - Qed. + Qed. Lemma string_of_nat_inj: forall n m, n <> m -> @@ -315,14 +315,14 @@ Section nat_Show. flatten_hyp H. + rewrite append_EmptyString in H. rewrite get_last_digit_0_iff in H. - generalize (Nat.mod_eq (S n) 10 (ltac:(lia))). + generalize (Nat.Div0.mod_eq (S n) 10). rewrite H, Heq; simpl; intros abs; inv abs. - + rewrite append_EmptyString in H; destruct (string_of_nat_aux_prepends (S n0) (get_last_digit (S n))) as (hd & eq & eq'). + + rewrite append_EmptyString in H; destruct (string_of_nat_aux_prepends (S n0) (get_last_digit (S n))) as (hd & eq & eq'). rewrite H in eq'. replace "0" with ("" ++ "0") in eq' by reflexivity. apply append_same_length_eq_r' in eq' ; [| rewrite get_last_digit_len1; reflexivity]. subst; tauto. - - subst; reflexivity. + - subst; reflexivity. Qed. Lemma pos_to_nat_inj: @@ -330,7 +330,7 @@ Section nat_Show. p <> p' -> Pos.to_nat p <> Pos.to_nat p'. Proof using. - intros; intro abs; apply Pos2Nat.inj in abs; easy. + intros; intro abs; apply Pos2Nat.inj in abs; easy. Qed. Lemma string_of_nat_aux_hd_get_last_digit: @@ -461,9 +461,9 @@ Lemma Forall2_impl : forall {A B} (P Q : A -> B -> Prop) l1 l2 Proof using. intros; induction H; auto. Qed. Lemma Forall2_impl' : forall {A B} (P Q : A -> B -> Prop) l1 l2 - (Himpl : forall a b, In a l1 -> P a b -> Q a b), + (Himpl : forall a b, In a l1 -> P a b -> Q a b), Forall2 P l1 l2 -> Forall2 Q l1 l2. -Proof using. +Proof using. intros; induction H; auto. constructor. - apply Himpl; simpl; auto. @@ -475,7 +475,7 @@ Lemma Forall2_length : forall {A B} (P : A -> B -> Prop) l1 l2, Proof using. intros; induction H; simpl; auto. Qed. -Inductive Forall3 (A B C : Type) (R : A -> B -> C -> Prop) +Inductive Forall3 (A B C : Type) (R : A -> B -> C -> Prop) : list A -> list B -> list C -> Prop := | Forall3_nil : Forall3 R [] [] [] | Forall3_cons : forall x y z l m n, @@ -491,12 +491,12 @@ Definition forall2b {A B} (f : A -> B ->bool) (l:list A) (m:list B) : bool := Definition Nth {A:Type} (l:list A) (n:nat) (a:A) : Prop := nth_error l n = Some a. -Arguments Nth _ _ _ _ /. +Arguments Nth _ _ _ _ /. Lemma not_Nth_nil : forall X n (x:X), ~ Nth [] n x. Proof using. - destruct n; discriminate. + destruct n; discriminate. Qed. #[export] Hint Resolve not_Nth_nil : core. @@ -517,7 +517,7 @@ Lemma Nth_map : forall (A B:Type) (f:A -> B) l n a b Proof using. induction l; intros; subst. destruct n; inversion Hnth. - destruct n. inversion Hnth. simpl; auto. + destruct n. inversion Hnth. simpl; auto. inversion Hnth; eapply IHl; eauto. Qed. @@ -547,7 +547,7 @@ Proof using. destruct l. inversion H0. inversion H; eauto. Qed. - + Lemma Nth_Forall2_Nth : forall n (A B:Type) l1 l2 P (b:B), Nth l2 n b -> Forall2 P l1 l2 -> @@ -676,7 +676,7 @@ Qed. (* Intervals ---------------------------------------------------------------- *) -Fixpoint interval n m := +Fixpoint interval n m := match m with | O => [] | S j => if le_lt_dec n j then interval n j ++ [j] else [] @@ -714,7 +714,7 @@ Proof using. destruct (le_lt_dec (S n) n); auto; lia. Qed. -Lemma interval_alt : forall m n, interval n m = +Lemma interval_alt : forall m n, interval n m = if lt_dec n m then n :: interval (S n) m else []. Proof using. induction m; auto; intro. @@ -735,7 +735,7 @@ Proof using. - rewrite app_length, IHm; simpl. destruct n; lia. - destruct n; simpl; lia. -Qed. +Qed. Lemma nth_error_nil : forall A n, nth_error ([] : list A) n = None. Proof using. @@ -744,7 +744,7 @@ Qed. Lemma nth_error_In : forall {A} l n (a : A), nth_error l n = Some a -> In a l. Proof using. - induction l; intros; destruct n; simpl in *; inversion H; eauto. + induction l; intros; destruct n; simpl in *; inversion H; eauto. Qed. Lemma in_nth_error : forall A (x : A) l, In x l -> @@ -799,7 +799,7 @@ Proof using. destruct Hdistinct; split; eauto; intro Hin'. rewrite in_app_iff in *; simpl in *; destruct Hin' as [? | [? | ?]]; auto. -Qed. +Qed. Lemma interval_distinct : forall m n, distinct (interval n m). Proof using. @@ -811,7 +811,7 @@ Proof using. Qed. -Lemma Nth_app1 : forall {A} l n (a : A) (Hnth : Nth l n a) l', +Lemma Nth_app1 : forall {A} l n (a : A) (Hnth : Nth l n a) l', Nth (l ++ l') n a. Proof using. induction l; simpl; intros; destruct n; unfold Nth in *; simpl in *; @@ -883,14 +883,14 @@ Proof using. * destruct n; lia. Qed. - + Lemma Forall2_forall : forall {A B} (P : A -> B -> Prop) al bl, - Forall2 P al bl <-> (length al = length bl /\ + Forall2 P al bl <-> (length al = length bl /\ forall i a b, Nth al i a -> Nth bl i b -> P a b). Proof using. induction al; simpl; intros. - split; [intro H; inversion H; subst | intros [H ?]]. - + split; auto; intros ? ? ? Hnth ?; destruct i; simpl in Hnth; + + split; auto; intros ? ? ? Hnth ?; destruct i; simpl in Hnth; inversion Hnth. + destruct bl; inversion H; auto. - destruct bl; simpl; [split; [intro H | intros [H ?]]; inversion H|]. @@ -902,7 +902,7 @@ Proof using. * specialize (H0 0); simpl in *; eauto. * rewrite IHal; split; auto; intros. specialize (H0 (S i)); simpl in H0; auto. -Qed. +Qed. Opaque minus. Lemma interval_shift : forall j i k, k <= i -> interval i j = @@ -999,7 +999,7 @@ Proof using. + simpl. destruct (dec y a); subst; auto. right. apply IHl; auto. Qed. - + Lemma remove_length_le : forall l x, length (remove dec x l) <= length l. Proof using. @@ -1014,11 +1014,11 @@ Lemma remove_length : forall l x, Proof using. induction l; intros. - inversion H. - - inversion H. + - inversion H. + subst. simpl. destruct (dec x x) as [_ | contra]. unfold Peano.lt. eapply le_n_S. apply remove_length_le. contradict contra; auto. - + simpl. specialize (IHl x H0). + + simpl. specialize (IHl x H0). destruct (dec x a); subst; simpl; lia. Qed. @@ -1043,7 +1043,7 @@ Proof using. - destruct n; inversion H. - destruct n; inversion H; subst. eexists; intuition eauto. - ecase IHl as [? [? ?]]; eauto. + ecase IHl as [? [? ?]]; eauto. Qed. @@ -1070,7 +1070,7 @@ Lemma nth_f_nth_error : forall A B (d:B) (f:A->B) l n, end. Proof using. induction l; intros; destruct n; simpl; auto. -Qed. +Qed. (* to appease termination checker *) @@ -1135,7 +1135,7 @@ Section With_Eqv_Rel_Dec. rewrite eq_dec_eq; reflexivity. Qed. - Lemma assoc_tl : forall (a c:A) (b:B) l + Lemma assoc_tl : forall (a c:A) (b:B) l (Hneq : a <> c), assoc a ((c,b)::l) = assoc a l. @@ -1155,7 +1155,7 @@ Section With_Eqv_Rel_Dec. (* left. inversion Hl. tauto. *) (* right. tauto. *) (* Qed. *) - + (* Lemma assoc_In_snd : forall A B (l:list (A * B)) eq_dec a b, *) (* assoc eq_dec a l = Some b -> *) (* In b (map (@snd _ _) l). *) @@ -1191,7 +1191,7 @@ Section With_Eqv_Rel_Dec. End With_Eqv_Rel_Dec. -#[global] Instance string_eqv_dec : Eqv string := eq. +#[global] Instance string_eqv_dec : Eqv string := eq. (* @@ -1215,7 +1215,7 @@ Proof using. - destruct n; auto. - destruct n. inversion H. simpl. apply IHl; auto. -Qed. +Qed. Lemma nth_error_out: forall A (l : list A) (n : nat), @@ -1227,11 +1227,11 @@ Proof using. Qed. Lemma map_ext_in : forall A B (f g : A -> B) l, - (forall a, In a l -> f a = g a) -> + (forall a, In a l -> f a = g a) -> map f l = map g l. Proof using. induction l; auto. intros Heq. - simpl. f_equal. apply Heq. simpl; auto. + simpl. f_equal. apply Heq. simpl; auto. apply IHl. intros ? Hin. apply Heq. simpl; auto. Qed. @@ -1271,7 +1271,7 @@ Proof using. - destruct (f (g a)). + rewrite IHl. reflexivity. + reflexivity. -Qed. +Qed. Lemma map_option_nth : forall A B (f : A -> option B) l l', map_option f l = Some l' -> @@ -1376,7 +1376,7 @@ Definition option_bind2 {A B C} (m: option (A * B)) (f: A -> B -> option C) : op Module OptionNotations. - Notation "'do' x <- m ; f" := (option_bind m (fun x => f)) + Notation "'do' x <- m ; f" := (option_bind m (fun x => f)) (at level 200, x name, m at level 100, f at level 200). Notation "'do' x , y <- m ; f" := (option_bind2 m (fun x y => f)) @@ -1397,7 +1397,7 @@ Definition map_prod {A B C D} (p:A * B) (f:A -> C) (g:B -> D) : (C * D) := Definition flip := @Basics.flip. Definition comp := @Basics.compose. -Notation "g `o` f" := (Basics.compose g f) +Notation "g `o` f" := (Basics.compose g f) (at level 40, left associativity). Lemma map_prod_distr_comp : forall A B C D E F @@ -1441,28 +1441,28 @@ Qed. Tactic Notation "inv_bind" hyp(H) := repeat rewrite option_bind_assoc in H; match type of H with - | option_bind ?o ?p = Some ?b => + | option_bind ?o ?p = Some ?b => let hy := fresh H in destruct o eqn:hy; [|discriminate]; simpl in H end. From Vellvm Require Import Numeric.Coqlib. - + Infix "⊍" := list_disjoint (at level 60). Lemma not_in_app_l : forall {A} (l1 l2 : list A) x, not (In x (l1 ++ l2)) -> not (In x l1). Proof using. - intros * NIN abs; eapply NIN, in_or_app; auto. + intros * NIN abs; eapply NIN, in_or_app; auto. Qed. Lemma not_in_app_r : forall {A} (l1 l2 : list A) x, not (In x (l1 ++ l2)) -> not (In x l2). Proof using. - intros * NIN abs; eapply NIN, in_or_app; auto. + intros * NIN abs; eapply NIN, in_or_app; auto. Qed. Section DisjointLists. @@ -1487,7 +1487,7 @@ Section DisjointLists. split; intros H. - split; [eapply list_disjoint_cons_left; eauto |]. intros abs; eapply H; eauto; constructor; reflexivity. - - apply list_disjoint_cons_l; apply H. + - apply list_disjoint_cons_l; apply H. Qed. Lemma list_disjoint_singleton_left : forall {A} (l : list A) (x : A), @@ -1512,15 +1512,15 @@ Section DisjointLists. Proof using. intros; induction l1 as [| hd l1 IH]; cbn. - split; intros H. - + split; auto using list_disjoint_nil_l. + + split; auto using list_disjoint_nil_l. + apply H. - split; intros H. + apply list_disjoint_cons_l_iff in H as [H1 H2]. apply IH in H1 as [? ?]. - split; auto. - apply list_disjoint_cons_l; auto. + split; auto. + apply list_disjoint_cons_l; auto. + destruct H as [H1 H2]. - apply list_disjoint_cons_l_iff in H1 as [? ?]. + apply list_disjoint_cons_l_iff in H1 as [? ?]. eapply list_disjoint_cons_l. apply IH; auto. auto. @@ -1532,8 +1532,8 @@ Section DisjointLists. Proof using. intros; induction l1 as [| hd l1 IH]; cbn. - split; intros H. - + split; auto using list_disjoint_nil_l. - + auto using list_disjoint_nil_l. + + split; auto using list_disjoint_nil_l. + + auto using list_disjoint_nil_l. - split; intros H. + apply list_disjoint_cons_l_iff in H as [H1 H2]. apply IH in H1 as [? ?]. @@ -1544,7 +1544,7 @@ Section DisjointLists. eapply not_in_app_r; eauto. + destruct H as [H1 H2]. apply list_disjoint_cons_l_iff in H1 as [? ?]. - apply list_disjoint_cons_l_iff in H2 as [? ?]. + apply list_disjoint_cons_l_iff in H2 as [? ?]. eapply list_disjoint_cons_l. apply IH; auto. intros abs; apply in_app_or in abs as [|]; eauto.