From 74e0818bcef0ac0c2b095a661b5c2f69c24626e9 Mon Sep 17 00:00:00 2001 From: "formalize.eth" Date: Thu, 17 Dec 2020 19:49:51 +0200 Subject: [PATCH] permit calls to builtins in L10 calldag --- Calldag.v | 347 ++++++++++++++++++++++++++++++++++++++++---- ConstFold.v | 14 +- From10To20/Call.v | 18 +-- From10To20/FunCtx.v | 6 +- From10To20/Stmt.v | 14 +- From20To30/Call.v | 6 +- From20To30/Expr.v | 10 +- From20To30/Stmt.v | 6 +- L10/Descend.v | 2 +- L20/Descend.v | 2 +- L30/Descend.v | 2 +- 11 files changed, 361 insertions(+), 66 deletions(-) diff --git a/Calldag.v b/Calldag.v index 183a210..9b7601d 100644 --- a/Calldag.v +++ b/Calldag.v @@ -1,8 +1,13 @@ -From Coq Require Import String Arith. -From Vyper Require Import Config. +From Coq Require Import String List ListSet Arith NArith. +From Vyper Require Map FSet MapSig. +From Vyper Require Import Config Graph.Depthmap. -Record generic_calldag {C: VyperConfig} (decl_type: Type) (callset: decl_type -> string_set) := { - cd_decls: string_map decl_type; +Record generic_calldag {C: VyperConfig} + {Decl: Type} + (callset: Decl -> string_set) + (may_call_undeclared: bool) +:= { + cd_decls: string_map Decl; cd_depthmap: string -> option nat; cd_depthmap_ok: let _ := string_map_impl in @@ -16,20 +21,23 @@ Record generic_calldag {C: VyperConfig} (decl_type: Type) (callset: decl_type -> let _ := string_set_impl in FSet.for_all (callset decl) (fun callee => match cd_depthmap callee with - | None => false + | None => may_call_undeclared | Some y => y string_set} - (d: generic_calldag decl_type callset) +Definition cd_declmap {C: VyperConfig} + {Decl: Type} + {callset: Decl -> string_set} + {may_call_undeclared: bool} + (d: generic_calldag callset may_call_undeclared) := let _ := string_map_impl in Map.lookup (cd_decls d). @@ -37,30 +45,32 @@ Definition cd_declmap {C: VyperConfig} {decl_type: Type} {callset: decl_type -> A functional context is the result of looking up a function by name in a calldag. *) Record fun_ctx {C: VyperConfig} - {decl_type: Type} - {decl_callset: decl_type -> string_set} - (cd: generic_calldag decl_type decl_callset) + {Decl: Type} + {decl_callset: Decl -> string_set} + {may_call_undeclared: bool} + (cd: generic_calldag decl_callset may_call_undeclared) (bound: nat) := { fun_name: string; fun_depth: nat; fun_depth_ok: cd_depthmap cd fun_name = Some fun_depth; - fun_decl: decl_type; + fun_decl: Decl; fun_decl_ok: cd_declmap cd fun_name = Some fun_decl; fun_bound_ok: fun_depth string_set} - {cd: generic_calldag decl_type decl_callset} + {Decl: Type} + {decl_callset: Decl -> string_set} + {may_call_undeclared: bool} + {cd: generic_calldag decl_callset may_call_undeclared} {name: string} - {d: decl_type} + {d: Decl} (Ed: cd_declmap cd name = Some d) (Edepth: cd_depthmap cd name = None): False. @@ -72,9 +82,10 @@ Qed. (** Create a function context from scratch (meaning that there's no pre-existing bound). *) Definition make_fun_ctx_and_bound {C: VyperConfig} - {decl_type: Type} - {decl_callset: decl_type -> string_set} - (cd: generic_calldag decl_type decl_callset) + {Decl: Type} + {decl_callset: Decl -> string_set} + {may_call_undeclared: bool} + (cd: generic_calldag decl_callset may_call_undeclared) (name: string) : option { bound: nat & fun_ctx cd bound } := match cd_declmap cd name as maybe_d return _ = maybe_d -> _ with @@ -195,4 +206,284 @@ destruct (Map.alist_lookup KeyEqDec (Map.items m) key); inversion E; subst. now rewrite Map.of_alist_ok. } now rewrite Map.of_alist_ok. -Qed. \ No newline at end of file +Qed. + +(**************************************************************************************************) + +(** Convert a list of declarations into a dictionary. + A duplicate declaraton name will result in an error. + *) +Fixpoint make_declmap {C: VyperConfig} {Decl: Type} (get_decl_name: Decl -> string) (decls: list Decl) +: string + string_map Decl +:= let _ := string_map_impl in + match decls with + | nil => inr Map.empty + | (h :: t)%list => + match make_declmap get_decl_name t with + | inl err => inl err + | inr m => let name := get_decl_name h in + match Map.lookup m name with + | Some _ => inl ("duplicate name: " ++ name)%string + | None => inr (Map.insert m name h) + end + end + end. + +(** Same as [make_declmap] but doesn't check for duplicates. *) +Fixpoint make_declmap_unchecked {C: VyperConfig} {Decl: Type} + (get_decl_name: Decl -> string) + (decls: list Decl) +: string_map Decl +:= let _ := string_map_impl in + match decls with + | nil => Map.empty + | (h :: t)%list => Map.insert (make_declmap_unchecked get_decl_name t) (get_decl_name h) h + end. + +(** An alternative implementation of [make_declmap_unchecked]. *) +Lemma make_declmap_unchecked_alt {C: VyperConfig} {Decl: Type} + (get_decl_name: Decl -> string) + (decls: list Decl): + make_declmap_unchecked get_decl_name decls + = + let _ := string_map_impl in + Map.of_alist (map (fun d => (get_decl_name d, d)) decls). +Proof. +induction decls. { easy. } +cbn in *. now rewrite IHdecls. +Qed. + +Lemma make_declmap_nodup {C: VyperConfig} {Decl: Type} + (get_decl_name: Decl -> string) + (decls: list Decl) + (Ok: NoDup (List.map get_decl_name decls)): + make_declmap get_decl_name decls = inr (make_declmap_unchecked get_decl_name decls). +Proof. +induction decls. { easy. } +cbn in Ok. rewrite NoDup_cons_iff in Ok. destruct Ok as (NotIn, NoDupTail). +cbn. rewrite (IHdecls NoDupTail). +rewrite make_declmap_unchecked_alt. cbn. +rewrite Map.of_alist_ok. +rewrite Map.alist_lookup_not_in. { trivial. } +now rewrite map_map. +Qed. + +(***************************************************************************) + +Definition has {C: VyperConfig} {Value: Type} + (m: string_map Value) + (key: string) +: bool +:= let _ := string_map_impl in + match Map.lookup m key with + | Some _ => true + | None => false + end. + +Definition declared_name {C: VyperConfig} {Decl: Type} (declmap: string_map Decl) +: Type +:= {name: string | has declmap name = true}. + +Lemma declared_name_irrel {C: VyperConfig} {Decl: Type} (declmap: string_map Decl) + (a b: declared_name declmap) + (E: proj1_sig a = proj1_sig b): + a = b. +Proof. +destruct a as (a_name, a_ok). +destruct b as (b_name, b_ok). +cbn in E. subst. +enough (a_ok = b_ok) by now subst. +apply Eqdep_dec.eq_proofs_unicity. +decide equality. +Qed. + +Local Lemma decl_of_declared_name_helper {C: VyperConfig} {Decl: Type} {declmap: string_map Decl} + (query: declared_name declmap) + (E: let _ := string_map_impl in + Map.lookup declmap (proj1_sig query) = None) + (ok: has declmap (proj1_sig query) = true): + False. +Proof. +unfold has in ok. cbn in E. +now destruct Map.lookup. +Qed. + +Definition decl_of_declared_name {C: VyperConfig} {Decl: Type} {declmap: string_map Decl} + (query: declared_name declmap) +: Decl +:= let _ := string_map_impl in + match Map.lookup declmap (proj1_sig query) as result return _ = result -> _ with + | Some x => fun _ => x + | None => fun E => False_rect _ (decl_of_declared_name_helper query E (proj2_sig query)) + end eq_refl. + +Definition Calls {C: VyperConfig} {Decl: Type} {declmap: string_map Decl} + (callset: Decl -> string_set) + (caller callee: declared_name declmap) +: Prop +:= let _ := string_set_impl in + FSet.has (callset (decl_of_declared_name caller)) (proj1_sig callee) = true. + +(** Build a list of dependent pairs from a list and a Forall condition. *) +Fixpoint list_exist {T: Type} {P: T -> Prop} {l: list T} (F: Forall P l) +: list {x: T | P x} +:= match l as l' return l = l' -> _ with + | nil => fun _ => nil + | h :: t => fun E => let F': Forall P (h :: t) := eq_ind l (Forall P) F (h :: t) E in + exist _ h (Forall_inv F') :: list_exist (Forall_inv_tail F') + end eq_refl. + +Lemma list_exist_in {T: Type} {P: T -> Prop} {l: list T} (F: Forall P l) + (Irrel: forall (a b: {x: T | P x}), + proj1_sig a = proj1_sig b -> a = b) + (x: T) (Px: P x): + In x l <-> In (exist _ x Px) (list_exist F). +Proof. +induction l as [|h]. { easy. } +cbn. split; intro H; case H; clear H; intro H. +{ left. subst. now apply Irrel. } +{ right. now apply IHl. } +{ left. now inversion H. } +right. now apply IHl in H. +Qed. + +Definition all_names {C: VyperConfig} {Decl: Type} (declmap: string_map Decl) +:= let _ := string_map_impl in + map fst (Map.items declmap). + +Lemma all_names_ok {C: VyperConfig} {Decl: Type} (declmap: string_map Decl) (name: string): + In name (all_names declmap) <-> has declmap name = true. +Proof. +unfold has. unfold all_names. +assert (ItemsOk := let _ := string_map_impl in Map.items_ok declmap name). +rewrite ItemsOk. clear ItemsOk. +remember (Map.items declmap) as l. clear Heql. induction l as [|head]. { easy. } +destruct head as (key, value). cbn. +destruct (string_dec name key) as [E|NE]. { symmetry in E. tauto. } +assert (NE': key <> name). { intro H. symmetry in H. contradiction. } +tauto. +Qed. + +Lemma all_declared_names_helper {C: VyperConfig} {Decl: Type} (declmap: string_map Decl): + let _ := string_map_impl in + Forall (fun name => has declmap name = true) (all_names declmap). +Proof. +rewrite Forall_forall. intros name. apply all_names_ok. +Qed. + +Definition all_declared_names {C: VyperConfig} {Decl: Type} (declmap: string_map Decl) +: list (declared_name declmap) +:= list_exist (all_declared_names_helper declmap). + +Lemma all_declared_names_ok {C: VyperConfig} {Decl: Type} (declmap: string_map Decl) + (d: declared_name declmap): + In d (all_declared_names declmap). +Proof. +destruct d as (name, is_declared). +apply (list_exist_in (all_declared_names_helper declmap) + (declared_name_irrel declmap)). +unfold all_names. +unfold has in is_declared. +assert (ItemsOk := let _ := string_map_impl in Map.items_ok declmap name). +destruct (Map.lookup declmap name). 2:{ discriminate. } +remember (Map.items declmap) as l. clear Heql. induction l as [|head]. { easy. } +destruct head as (head_name, head_decl). +cbn in *. +destruct string_dec. { left. now symmetry. } +right. exact (IHl ItemsOk). +Qed. + +Definition declset {C: VyperConfig} {Decl: Type} (declmap: string_map Decl) +: string_set +:= let _ := string_set_impl in + let _ := string_map_impl in + FSet.from_list (map fst (Map.items declmap)). + +(** The list of called functions but restricted to the actually declared symbols + (not actually declared functions because with parameterized [Decl] + we have no way to distinguish function declarations from other declarations) + *) +Definition restricted_call_list {C: VyperConfig} {Decl: Type} + {declmap: string_map Decl} + (callset: Decl -> string_set) + (d: declared_name declmap) +: list string +:= let _ := string_set_impl in + set_inter string_dec (FSet.to_list (callset (decl_of_declared_name d))) (all_names declmap). + +Lemma restricted_call_list_nodup {C: VyperConfig} {Decl: Type} + (declmap: string_map Decl) + (callset: Decl -> string_set) + (d: declared_name declmap): + NoDup (restricted_call_list callset d). +Proof. +apply set_inter_nodup. +{ apply FSet.to_list_nodup. } +apply Map.items_nodup. +Qed. + +Lemma restricted_call_list_all_declared {C: VyperConfig} {Decl: Type} + {declmap: string_map Decl} + (callset: Decl -> string_set) + (d: declared_name declmap): + Forall (fun name => has declmap name = true) + (restricted_call_list callset d). +Proof. +rewrite Forall_forall. intros name H. +unfold restricted_call_list in H. +apply set_inter_elim2 in H. +revert name H. rewrite<- Forall_forall. +apply all_declared_names_helper. +Qed. + +Definition declared_call_list {C: VyperConfig} {Decl: Type} + {declmap: string_map Decl} + (callset: Decl -> string_set) + (d: declared_name declmap) +: list (declared_name declmap) +:= list_exist (restricted_call_list_all_declared callset d). + + +Lemma declared_call_list_ok {C: VyperConfig} {Decl: Type} + {declmap: string_map Decl} + (callset: Decl -> string_set) + (a b: declared_name declmap): + In b (declared_call_list callset a) <-> Calls callset a b. +Proof. +unfold Calls. unfold declared_call_list. +destruct b as (b_name, b_ok). +rewrite<- (list_exist_in (restricted_call_list_all_declared callset a) + (declared_name_irrel declmap)). +unfold restricted_call_list. cbn. +rewrite FSet.has_to_list. +remember (FSet.to_list (callset (decl_of_declared_name a))) as l. destruct Heql. +rewrite ListSet2.set_mem_true. +rewrite set_inter_iff. +enough (In b_name (all_names declmap)) by tauto. +now apply all_names_ok. +Qed. + +Definition make_depthmap {C: VyperConfig} {Decl: Type} + (declmap: string_map Decl) + (callset: Decl -> string_set) +: Cycle.t (Calls callset) + + { f: declared_name declmap -> N | + forall a b : declared_name declmap, + Calls callset a b -> (f b < f a)%N } +:= cycle_or_depthmap (Calls callset) (all_declared_names declmap) (all_declared_names_ok declmap) + (MapSig.instance + (string_map_impl ({start : declared_name declmap & Path.t (Calls callset) start} * N))) + (declared_call_list callset) + (declared_call_list_ok callset). + +Definition cycle_error_message {C: VyperConfig} {Decl: Type} + (declmap: string_map Decl) + {callset: Decl -> string_set} + (cycle: Cycle.t (@Calls C Decl declmap callset)) +: string +:= let fix path_to_string {v: declared_name declmap} (p: Path.t (Calls callset) v) + := match p with + | Path.Nil _ => proj1_sig v + | Path.Cons _ _ rest => (proj1_sig v ++ " -> " ++ path_to_string rest)%string + end + in ("recursion is not allowed but a call cycle is detected: " ++ path_to_string (Cycle.path cycle)). \ No newline at end of file diff --git a/ConstFold.v b/ConstFold.v index c4ff7e1..f87a6e7 100644 --- a/ConstFold.v +++ b/ConstFold.v @@ -1383,7 +1383,7 @@ destruct ss; cbn in StmtOk; unfold sum_map in *; cbn. (@eq_refl (@small_stmt C) (@Return C e)) CallOk' = @callset_descend_return C (@Return C e) e - (@decl_callset C (@fun_decl C (@decl C) (@decl_callset C) cd' + (@decl_callset C (@fun_decl C (@decl C) (@decl_callset C) false cd' bigger_call_depth_bound (@const_fold_fun_ctx C bigger_call_depth_bound cd cd' ok fc))) (@eq_refl (@small_stmt C) (@Return C e)) CallOk'). @@ -1404,7 +1404,7 @@ destruct ss; cbn in StmtOk; unfold sum_map in *; cbn. (@eq_refl (@small_stmt C) (@Raise C e)) CallOk' = @callset_descend_raise C (@Raise C e) e - (@decl_callset C (@fun_decl C (@decl C) (@decl_callset C) cd' + (@decl_callset C (@fun_decl C (@decl C) (@decl_callset C) false cd' bigger_call_depth_bound (@const_fold_fun_ctx C bigger_call_depth_bound cd cd' ok fc))) (@eq_refl (@small_stmt C) (@Raise C e)) CallOk'). @@ -1425,7 +1425,7 @@ destruct ss; cbn in StmtOk; unfold sum_map in *; cbn. (@eq_refl (@small_stmt C) (@Assign C lhs e)) CallOk' = @callset_descend_assign_rhs C (@Assign C lhs e) lhs e - (@decl_callset C (@fun_decl C (@decl C) (@decl_callset C) cd' + (@decl_callset C (@fun_decl C (@decl C) (@decl_callset C) false cd' bigger_call_depth_bound (@const_fold_fun_ctx C bigger_call_depth_bound cd cd' ok fc))) (@eq_refl (@small_stmt C) (@Assign C lhs e)) CallOk'). @@ -1461,7 +1461,7 @@ assert (R: @callset_descend_expr_stmt C (@ExprStmt C e') e' = @callset_descend_expr_stmt C (@ExprStmt C e') e' (@decl_callset C - (@fun_decl C (@decl C) (@decl_callset C) cd' bigger_call_depth_bound + (@fun_decl C (@decl C) (@decl_callset C) false cd' bigger_call_depth_bound (@const_fold_fun_ctx C bigger_call_depth_bound cd cd' ok fc))) (@eq_refl (@small_stmt C) (@ExprStmt C e')) CallOk'). { easy. } @@ -1539,7 +1539,7 @@ induction s; intros; cbn in StmtOk; unfold sum_map in *; unfold sum_ap in *. = (@callset_descend_var_scope C (@LocalVarDecl C name init' body) name init' body (@decl_callset C - (@fun_decl C (@decl C) (@decl_callset C) cd' bigger_call_depth_bound + (@fun_decl C (@decl C) (@decl_callset C) false cd' bigger_call_depth_bound (@const_fold_fun_ctx C bigger_call_depth_bound cd cd' ok fc))) (@eq_refl (@stmt C) (@LocalVarDecl C name init' body)) CallOk')). { easy. } @@ -1689,12 +1689,12 @@ assert (FixCallL: assert (FixCallR: (@callset_descend_loop_body C (@Loop C var start count' body) body var start count' (@decl_callset C - (@fun_decl C (@decl C) (@decl_callset C) cd bigger_call_depth_bound fc)) + (@fun_decl C (@decl C) (@decl_callset C) false cd bigger_call_depth_bound fc)) (@eq_refl (@stmt C) (@Loop C var start count' body)) CallOk) = (@callset_descend_loop_body C (@Loop C var start count body) body var start count (@decl_callset C - (@fun_decl C (@decl C) (@decl_callset C) cd bigger_call_depth_bound fc)) + (@fun_decl C (@decl C) (@decl_callset C) false cd bigger_call_depth_bound fc)) (@eq_refl (@stmt C) (@Loop C var start count body)) CallOk)) by apply PropExtensionality.proof_irrelevance. rewrite FixCallL in IH. rewrite FixCallR in IH. clear FixCallL FixCallR. diff --git a/From10To20/Call.v b/From10To20/Call.v index ed4cd93..00fd914 100644 --- a/From10To20/Call.v +++ b/From10To20/Call.v @@ -180,22 +180,22 @@ assert (SomeBranchOk: forall d Ed' Ed, (* This is even more messed up than usual because just the implicit arguments weren't enough. *) remember (fun depth (Edepth : @eq (option nat) - (@cd_depthmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd fun_name) + (@cd_depthmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd fun_name) (@Some nat depth)) => @Some (@sigT nat (fun bound : nat => - @fun_ctx C (@AST.decl C) (@Callset.decl_callset C) (@translate_calldag C cd) bound)) + @fun_ctx C (@AST.decl C) (@Callset.decl_callset C) false (@translate_calldag C cd) bound)) (@existT nat (fun bound : nat => - @fun_ctx C (@AST.decl C) (@Callset.decl_callset C) (@translate_calldag C cd) bound) + @fun_ctx C (@AST.decl C) (@Callset.decl_callset C) false (@translate_calldag C cd) bound) (S depth) - (Build_fun_ctx C (@AST.decl C) (@Callset.decl_callset C) (@translate_calldag C cd) + (Build_fun_ctx C (@AST.decl C) (@Callset.decl_callset C) false (@translate_calldag C cd) (S depth) fun_name depth Edepth (@translate_decl C (fun name : string => match - @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd name return bool + @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd name return bool with | Some _ => true | None => false @@ -206,15 +206,15 @@ assert (SomeBranchOk: forall d Ed' Ed, as depth_lhs_some_branch. remember (fun (depth: nat) (Edepth : @eq (option nat) - (@cd_depthmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd fun_name) + (@cd_depthmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd fun_name) (@Some nat depth)) => @Some (@sigT nat - (fun bound : nat => @fun_ctx C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd bound)) + (fun bound : nat => @fun_ctx C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd bound)) (@existT nat - (fun bound : nat => @fun_ctx C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd bound) + (fun bound : nat => @fun_ctx C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd bound) (S depth) - (Build_fun_ctx C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd + (Build_fun_ctx C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd (S depth) fun_name depth Edepth d Ed (@proj2 (forall _ : @eq bool (Nat.leb depth depth) true, lt depth (S depth)) (forall _ : lt depth (S depth), @eq bool (Nat.leb depth depth) true) diff --git a/From10To20/FunCtx.v b/From10To20/FunCtx.v index 9d548bf..fff7016 100644 --- a/From10To20/FunCtx.v +++ b/From10To20/FunCtx.v @@ -42,13 +42,17 @@ rewrite FSet.for_all_ok in *. intros x H. rewrite callset_translate_decl in H. apply Bool.andb_true_iff in H. assert (Q := D x (proj1 H)). clear D. +destruct H as (Has, IsPrivate). +unfold is_private_call in IsPrivate. +unfold cd_declmap in IsPrivate. +assert (X := cd_depthmap_ok cd x). +destruct (Map.lookup (cd_decls cd) x) as [xdecl|]. 2:easy. destruct (cd_depthmap cd x). 2:easy. destruct n; rewrite Nat.ltb_lt in Q. { now apply Nat.nlt_0_r in Q. } rewrite Nat.leb_le. apply Nat.lt_succ_r. exact Q. Qed. - Definition translate_calldag {C: VyperConfig} (cd: L10.Descend.calldag) : L20.Descend.calldag := let is_private_call (name: string) diff --git a/From10To20/Stmt.v b/From10To20/Stmt.v index 7aa3ff0..40b4d32 100644 --- a/From10To20/Stmt.v +++ b/From10To20/Stmt.v @@ -768,13 +768,13 @@ induction s10 using L10.AST.stmt_ind'; intros. (@AST.Loop C var (@translate_expr C (fun name : string => - match @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd name with + match @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd name with | Some _ => true | None => false end) start) count (translate_stmt_list' body)) (translate_stmt_list' body) var (@translate_expr C (fun name : string => - match @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd name with + match @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd name with | Some _ => true | None => false end) start) count @@ -785,7 +785,7 @@ induction s10 using L10.AST.stmt_ind'; intros. (@AST.Loop C var (@translate_expr C (fun name : string => - match @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd name with + match @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd name with | Some _ => true | None => false end) start) count (translate_stmt_list' body))) CallOk20) @@ -884,7 +884,7 @@ induction s10 using L10.AST.stmt_ind'; intros. (@translate_expr C (fun name : string => match - @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd name + @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd name with | Some _ => true | None => false @@ -892,7 +892,7 @@ induction s10 using L10.AST.stmt_ind'; intros. var (@translate_expr C (fun name : string => - match @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd name with + match @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd name with | Some _ => true | None => false end) start) count' @@ -905,7 +905,7 @@ induction s10 using L10.AST.stmt_ind'; intros. (@translate_expr C (fun name : string => match - @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd name + @cd_declmap C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd name with | Some _ => true | None => false @@ -916,7 +916,7 @@ induction s10 using L10.AST.stmt_ind'; intros. assert (FixCount10: @L10.Callset.callset_descend_fixed_count_loop_body C (@AST.FixedCountLoop C var start count' body) body var start count' (@L10.Callset.decl_callset C - (@fun_decl C (@L10.AST.decl C) (@L10.Callset.decl_callset C) cd + (@fun_decl C (@L10.AST.decl C) (@L10.Callset.decl_callset C) true cd (S smaller_call_depth_bound) fc)) (@eq_refl (@L10.AST.stmt C) (@AST.FixedCountLoop C var start count' body)) CallOk10 diff --git a/From20To30/Call.v b/From20To30/Call.v index ba1c1a5..fdf604f 100644 --- a/From20To30/Call.v +++ b/From20To30/Call.v @@ -784,12 +784,12 @@ subst. cbn. intros. (* This is even more messed up than usual because just the implicit arguments weren't enough. *) remember (fun depth (Edepth : @eq (option nat) - (@cd_depthmap C (@AST.decl C) (@Callset.decl_callset C) cd30 fun_name) + (@cd_depthmap C (@AST.decl C) (@Callset.decl_callset C) false cd30 fun_name) (@Some nat depth)) => @Some - (@sigT nat (fun bound : nat => @fun_ctx C (@AST.decl C) (@Callset.decl_callset C) cd30 bound)) + (@sigT nat (fun bound : nat => @fun_ctx C (@AST.decl C) (@Callset.decl_callset C) false cd30 bound)) (@existT nat - (fun bound : nat => @fun_ctx C (@AST.decl C) (@Callset.decl_callset C) cd30 bound) + (fun bound : nat => @fun_ctx C (@AST.decl C) (@Callset.decl_callset C) false cd30 bound) (S depth) _)) as depth_lhs_some_branch. diff --git a/From20To30/Expr.v b/From20To30/Expr.v index 8d59eb6..9f5bc06 100644 --- a/From20To30/Expr.v +++ b/From20To30/Expr.v @@ -282,7 +282,7 @@ assert (H := HeadOk (L20.Callset.callset_descend_head eq_refl CallOk20) clear HeadOk. assert (R: (@Callset.callset_descend_semicolon_left C s tail30 (@AST.Semicolon C s tail30) (@Callset.decl_callset C - (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) cd30 bigger_call_depth_bound + (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) false cd30 bigger_call_depth_bound (@translate_fun_ctx C bigger_call_depth_bound cd20 fc cd30 ok))) (@eq_refl (@AST.stmt C) (@AST.Semicolon C s tail30)) CallOk30) = @@ -311,7 +311,7 @@ subst world20 value. assert (R: (@Callset.callset_descend_semicolon_right C s tail30 (@AST.Semicolon C s tail30) (@Callset.decl_callset C - (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) cd30 bigger_call_depth_bound + (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) false cd30 bigger_call_depth_bound (@translate_fun_ctx C bigger_call_depth_bound cd20 fc cd30 ok))) (@eq_refl (@AST.stmt C) (@AST.Semicolon C s tail30)) CallOk30) = @@ -1052,7 +1052,7 @@ induction e20 using L20.AST.expr_ind'; intros; cbn in ExprOk. (@AST.PrivateCall C dst name offset (N.of_nat (@Datatypes.length (@AST.expr C) args)))) (@AST.PrivateCall C dst name offset (N.of_nat (@Datatypes.length (@AST.expr C) args))) (@Callset.decl_callset C - (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) cd30 bigger_call_depth_bound + (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) false cd30 bigger_call_depth_bound (@translate_fun_ctx C bigger_call_depth_bound cd20 fc cd30 ok))) (@eq_refl (@AST.stmt C) (@AST.SmallStmt C @@ -1065,7 +1065,7 @@ induction e20 using L20.AST.expr_ind'; intros; cbn in ExprOk. (@AST.PrivateCall C dst name offset (N.of_nat (@Datatypes.length (@AST.expr C) args))))) (@Callset.decl_callset C - (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) cd30 bigger_call_depth_bound + (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) false cd30 bigger_call_depth_bound (@translate_fun_ctx C bigger_call_depth_bound cd20 fc cd30 ok))) (@eq_refl (@AST.stmt C) (@AST.Semicolon C s0 @@ -1298,7 +1298,7 @@ assert (GoodBranch30Ok: let _ := memory_impl in assert (Earity = Earity'). { apply PropExtensionality.proof_irrelevance. } subst Earity'. destruct (call_builtin value Earity (builtin world20_args)). - destruct e. + destruct e. 2:{ split. { trivial. } split. 2: { trivial. } diff --git a/From20To30/Stmt.v b/From20To30/Stmt.v index 2c54550..2ee8f31 100644 --- a/From20To30/Stmt.v +++ b/From20To30/Stmt.v @@ -418,7 +418,7 @@ induction s20; intros. assert (R: (@Callset.callset_descend_semicolon_right C s s0 (@AST.Semicolon C s s0) (@Callset.decl_callset C - (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) cd30 bigger_call_depth_bound + (@fun_decl C (@AST.decl C) (@Callset.decl_callset C) false cd30 bigger_call_depth_bound (@translate_fun_ctx C bigger_call_depth_bound cd20 fc cd30 ok))) (@eq_refl (@AST.stmt C) (@AST.Semicolon C s s0)) CallOk30) = @@ -796,14 +796,14 @@ assert (FixCall20: (@L20.Callset.callset_descend_loop_body C (@L20.AST.Loop C var start count' s20) s20 var start count' (@L20.Callset.decl_callset C - (@fun_decl C (@L20.AST.decl C) (@L20.Callset.decl_callset C) cd20 + (@fun_decl C (@L20.AST.decl C) (@L20.Callset.decl_callset C) false cd20 bigger_call_depth_bound fc)) (@eq_refl (@L20.AST.stmt C) (@L20.AST.Loop C var start count' s20)) CallOk20) = (@L20.Callset.callset_descend_loop_body C (@L20.AST.Loop C var start count s20) s20 var start count (@L20.Callset.decl_callset C - (@fun_decl C (@L20.AST.decl C) (@L20.Callset.decl_callset C) cd20 + (@fun_decl C (@L20.AST.decl C) (@L20.Callset.decl_callset C) false cd20 bigger_call_depth_bound fc)) (@eq_refl (@L20.AST.stmt C) (@L20.AST.Loop C var start count s20)) CallOk20)). { apply PropExtensionality.proof_irrelevance. } diff --git a/L10/Descend.v b/L10/Descend.v index 40fc4de..fc35f7e 100644 --- a/L10/Descend.v +++ b/L10/Descend.v @@ -9,7 +9,7 @@ Local Open Scope string_scope. Section Descend. Context {C: VyperConfig}. -Definition calldag := generic_calldag decl decl_callset. +Definition calldag := generic_calldag decl_callset true. Lemma call_descend {call_depth_bound new_call_depth_bound current_fun_depth: nat} diff --git a/L20/Descend.v b/L20/Descend.v index 3c9706c..f4fbf35 100644 --- a/L20/Descend.v +++ b/L20/Descend.v @@ -6,7 +6,7 @@ From Vyper.L20 Require Import AST Callset. Section Descend. Context {C: VyperConfig}. -Definition calldag := generic_calldag decl decl_callset. +Definition calldag := generic_calldag decl_callset false. (* Unfortunately this is a huge duplication of L10/Descend.v due to the fact that L10 has this: [E: e = PrivateOrBuiltinCall name args] diff --git a/L30/Descend.v b/L30/Descend.v index 5cea052..abbeabe 100644 --- a/L30/Descend.v +++ b/L30/Descend.v @@ -6,7 +6,7 @@ From Vyper.L30 Require Import AST Callset. Section Descend. Context {C: VyperConfig}. -Definition calldag := generic_calldag decl decl_callset. +Definition calldag := generic_calldag decl_callset false. (* Unfortunately this is a huge duplication of L10/Descend.v due to the fact that L10 has this: [E: e = PrivateOrBuiltinCall name args]