Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[pull] master from formalize:master #35

Merged
merged 1 commit into from
Dec 17, 2020
Merged

[pull] master from formalize:master #35

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
347 changes: 319 additions & 28 deletions Calldag.v
View file
Open in desktop

Large diffs are not rendered by default.

14 changes: 7 additions & 7 deletions ConstFold.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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').
Expand All @@ -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').
Expand All @@ -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').
Expand Down Expand Up @@ -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. }
Expand Down Expand Up @@ -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. }
Expand Down Expand Up @@ -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.
Expand Down
18 changes: 9 additions & 9 deletions From10To20/Call.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down
6 changes: 5 additions & 1 deletion From10To20/FunCtx.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
14 changes: 7 additions & 7 deletions From10To20/Stmt.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -884,15 +884,15 @@ 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
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'
Expand All @@ -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
Expand All @@ -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
Expand Down
6 changes: 3 additions & 3 deletions From20To30/Call.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
10 changes: 5 additions & 5 deletions From20To30/Expr.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
=
Expand Down Expand Up @@ -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)
=
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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. }
Expand Down
6 changes: 3 additions & 3 deletions From20To30/Stmt.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
=
Expand Down Expand Up @@ -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. }
Expand Down
2 changes: 1 addition & 1 deletion L10/Descend.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
2 changes: 1 addition & 1 deletion L20/Descend.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
2 changes: 1 addition & 1 deletion L30/Descend.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down