Metatheoretic Approaches to Programming Language Specification & Verification Rob Simmons Princeton University Introduction • “A precise description of a programming language is a prerequisite for its implementation and its use” (The Definition of Standard ML, 1990) Introduction • “A precise description of a programming language is a prerequisite for its implementation and its use” (The Definition of Standard ML, 1990) • “We hold that ‘formal’ means ‘admits logical reasoning’” (C formalised in HOL, 1998) Introduction • “A precise description of a programming language is a prerequisite for its implementation and its use” (The Definition of Standard ML, 1990) • “We hold that ‘formal’ means ‘admits logical reasoning’” (C formalised in HOL, 1998) • “Use computers to check your proof. Note that [this] task is not trivial. A whole new scientific discipline may be needed. Let me call it Pedantics.” (Yuri Gurevich) Introduction • Lots of theorem proving systems! – – – – – – – – ACL2 Coq HOL Isabelle Nuprl LEGO PVS Twelf • Twelf can do things others can’t Outline of Talk • Introduction to Twelf • Semantics in Twelf – Denotational semantics – Axiomatic semantics • Proofs as programs • Metalogic proofs • Safety for the simply typed lambda calculus Introduction to Twelf syntax • Define new categories nat : type. exp : type. tp : type. animal : type. _ Introduction to Twelf syntax • Define new categories nat : type. exp : type. tp : type. animal : type. _ Introduction to Twelf syntax • Define new categories nat : type. • Define elements in the categories z : nat. s : nat -> nat. four : nat = s (s (s (s z))). % datatype nat = Z % | S of nat % val four = S (S (S (S Z))) n : nat -> exp. int : tp. plus : exp -> exp -> exp. test : exp = plus (n four) (n (s z)). Introduction to Twelf syntax • Define new categories nat : type. • Define elements in the categories z : nat. s : nat -> nat. four : nat = s (s (s (s z))). % datatype nat = Z % | S of nat % val four = S (S (S (S Z))) n : nat -> exp. int : tp. plus : exp -> exp -> exp. test : exp = plus (n four) (n (s z)). Introduction to Twelf syntax • Define new categories nat : type. • Define elements in the categories z : nat. s : nat -> nat. four : nat = s (s (s (s z))). % datatype nat = Z % | S of nat % val four = S (S (S (S Z))) • Define relationships between categories sum : nat -> nat -> nat -> type. sum : {a: nat}{b: nat}{c: nat} type. % Equivalent Introduction to Twelf syntax • Define new categories nat : type. • Define elements in the categories z : nat. s : nat -> nat. four : nat = s (s (s (s z))). % datatype nat = Z % | S of nat % val four = S (S (S (S Z))) • Define relationships between categories sum : nat -> nat -> nat -> type. sum : {a: nat}{b: nat}{c: nat} type. % Equivalent typed : exp -> tp -> type. steps : exp -> exp -> type. What does a judgment ‘mean’? • Right now, we know nothing about sum, other than that it is a three-part relation. • I called it “sum,” so I apparently have some expected meaning for it. What does a judgment ‘mean’? • Right now, we know nothing about sum, other than that it is a three-part relation. • I called it “sum,” so I apparently have some expected meaning for it. • How do we specify that 2 + 1 = 3 ? i.e. sum (s (s z)) (s z) (s (s (s z))) • How do we specify that addition is commutative? What does a judgment ‘mean’? • Right now, we know nothing about sum, other than that it is a three-part relation. • I called it “sum,” so I apparently have some expected meaning for it. • How do we specify that 2 + 1 = 3 ? i.e. sum (s (s z)) (s z) (s (s (s z))) • How do we specify that addition is commutative? • (At least) two ways of looking at this – Assign an underlying semantic meaning, write a proof (denotational semantics, object logic) – Write an inductive definition, write an inductive proof (operational semantics, metalogic) Assigning semantic meaning nat : type = tm num. z : nat = const 0. s : nat -> nat = [x] const 1 + x. Assigning semantic meaning nat : type = tm num. z : nat = const 0. s : nat -> nat = [x] const 1 + x. sum : nat -> nat -> nat -> type = [a][b][c] pf (a + b == c). Assigning semantic meaning nat : type = tm num. z : nat = const 0. s : nat -> nat = [x] const 1 + x. sum : nat -> nat -> nat -> type = [a][b][c] pf (a + b == c). sum1+1 : sum (s z) (s z) (s (s z)) = cut (plus_cong plus_zero plus_zero) [p1] trans3 p1 (symm plus_zero) plus_assoc. sum_comm : sum N1 N2 N3 -> sum N2 N1 N3 = [p1 : pf (N1 + N2 == N3)] trans comm_add p1. Assigning semantic meaning nat : type = tm num. z : nat = const 0. s : nat -> nat = [x] const 1 + x. sum : nat -> nat -> nat -> type = [a][b][c] pf (a + b == c). sum1+1 : sum (s z) (s z) (s (s z)) = cut (plus_cong plus_zero plus_zero) [p1] Has Been Checked By A Computer trans3 p1This (symm plus_zero) plus_assoc. sum_comm : sum N1 N2 N3 -> sum N2 N1 N3 = [p1 : pf (N1 + N2 == N3)] This Has Been Checked By A Computer trans comm_add p1. Assigning axiomatic meaning nat : type. z : nat. s : nat -> nat. sum : nat -> nat -> nat -> type. Assigning axiomatic meaning nat : type. z : nat. s : nat -> nat. sum : nat -> nat -> nat -> type. sum_z : sum z N N. sum_s : sum (s N1) N2 (s N3) <- sum N1 N2 N3. sum N1 N2 N3 sum (s N1) N2 (s N3) sum_s sum_z sum z N N Assigning axiomatic meaning 1 = s z. 2 = s 1. 3 = s 2. sum2+1 : sum 2 1 3 = ???. sum (s (s z)) (s z) (s (s (s z))) 2 1 3 Assigning axiomatic meaning 1 = s z. 2 = s 1. 3 = s 2. sum2+1 : sum 2 1 3 = sum_s (sum_s sum_z). sum_z sum z (s z) (s z) sum_s sum (s z) (s z) (s (s z)) sum_s sum (s (s z)) (s z) (s (s (s z))) 2 1 3 Assigning axiomatic meaning 1 = s z. 2 = s 1. 3 = s 2. sum2+1 : sum 2 1 3 = sum_s (sum_s sum_z). Both of these represent an OBJECT sum_z sum z (s z) (s z) sum_s sum (s z) (s z) (s (s z)) sum_s sum (s (s z)) (s z) (s (s (s z))) 2 1 3 Axiomatic Relations Relations (which represent judgments or proofs) sum, mul, typed, steps, etc… Axiomatic Relations Relations (which represent judgments or proofs) sum, mul, typed, steps, etc… Relations ABOUT relations representing proofs Axiomatic Relations Relations (which represent judgments or proofs) sum, mul, typed, steps, etc… Relations ABOUT relations representing proofs Relations AS PROGRAMS Proofs as programs • The input to Twelf %solve sum2+1 : sum 2 1 _. Proofs as programs • The input to Twelf %solve sum2+1 : sum 2 1 _. • Twelf’s response sum2+1 : sum 2 1 (s (s 1)) = sum_s (sum_s sum_z). %% OK %% Proofs as programs • The input to Twelf %solve sum2+1 : sum 2 1 _. • Twelf’s response sum2+1 : sum 2 1 (s (s 1)) = sum_s (sum_s sum_z). %% OK %% • The input to Twelf %solve sum2+1 : sum _ 1 _. • Twelf’s response sum2+1 : sum z 1 1 = sum_z. %% OK %% Proofs as programs • It is sometimes useful to think at these definitions as a function that recursively calls itself - so the second line (the subgoal) acts like a recursive call to sum. sum_s : sum (s N1) N2 (s N3) <- sum N1 N2 N3. Reasoning about programs • Mode declarations %mode sum +N1 +N2 –N3. • “If the first two positions contain well-defined (i.e. ground, without metavariables) inputs, then IF the search succeeds in a finite amount of time, the search will generate well-defined outputs” Reasoning about programs • Mode declarations %mode sum +N1 +N2 –N3. • “If the first two positions contain well-defined (i.e. ground, without metavariables) inputs, then IF the search succeeds in a finite amount of time, the search will generate well-defined outputs” sum_z_bad : sum z N N'. Occurrence of variable N' in output (-) argument not necessarily ground %% ABORT %% Reasoning about programs • World declarations %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). • The program is using the “closed worlds assumption” - no new things (a new natural number, or a new rule for sum) will appear during execution. Reasoning about programs • World declarations %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). • The program is using the “closed worlds assumption” - no new things (a new natural number, or a new rule for sum) will appear during execution. sum_s_bad : sum (s N1) N2 (s N3) <- {n: nat} sum N1 n N3. Constant sum_s_bad World violation %% ABORT %% Reasoning about programs • Totality declarations %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). %total N1 (sum N1 N2 N3). • The program acts like a total function – – – – This involves three things: Termination Input coverage Output coverage Reasoning about programs • Totality declarations & termination %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). %total N1 (sum N1 N2 N3). • The program always terminates (has a term which always strictly decreases in size) sum_bad : sum N1 N2 N3 <- sum N2 N1 N3. Reasoning about programs • Totality declarations & termination %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). %total N1 (sum N1 N2 N3). • The program always terminates (has a term which always strictly decreases in size) sum_bad : sum N1 N2 N3 <- sum N2 N1 N3. Termination violation: ---> (N2) < (N1) %% ABORT %% Reasoning about programs • Totality declarations & input coverage %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). %total N1 (sum N1 N2 N3). • All possible inputs are covered (case analysis) Reasoning about programs • Totality declarations & input coverage %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). %total N1 (sum N1 N2 N3). • All possible inputs are covered (case analysis) • If we remove the sum_z rule, Twelf will complain Coverage error --- missing cases: {X1:nat} {X2:nat} |- sum z X1 X2. %% ABORT %% Reasoning about programs • Totality declarations & output coverage %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). %total N1 (sum N1 N2 N3). • All possible OUTPUTS are covered Reasoning about programs • Totality declarations & output coverage %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). %total N1 (sum N1 N2 N3). • All possible OUTPUTS are covered sum_s_bad : sum (s N1) N2 (s N3) <- sum N1 N2 (s N3). Totality: Output of subgoal not covered Output coverage error --- missing cases: {X1:nat} {X2:nat} |- sum X1 X2 z. %% ABORT %% Reasoning about programs • Totality declarations %mode sum +N1 +N2 –N3. %worlds () (sum _ _ _). %total N1 (sum N1 N2 N3). • The sum function is TOTAL – – – – – It has clearly defined inputs and outputs No new terms will be defined during execution It always terminates It will always be able to handle any inputs Recursive calls place no constraints on outputs Metatheorems in Twelf Relations (which represent judgments or proofs) sum, mul, typed, steps, etc… Relations ABOUT relations representing proofs Relations AS PROGRAMS Metatheorems in Twelf • Addition is commutative Metatheorems in Twelf • Addition is commutative • If N1 + N2 = N3, then N2 + N1 = N3 Metatheorems in Twelf • Addition is commutative • If N1 + N2 = N3, then N2 + N1 = N3 • If I can derive “sum N1 N2 N3,” then “sum N2 N1 N3” should also be derivable Metatheorems in Twelf • Addition is commutative • If N1 + N2 = N3, then N2 + N1 = N3 • If I can derive “sum N1 N2 N3,” then “sum N2 N1 N3” should also be derivable sum_comm: sum N1 N2 N3 -> sum N2 N1 N3 -> type. %mode sum_comm +SUM -SUM'. • Can we show this is total? Metatheorems in Twelf sum_comm: sum N1 N2 N3 -> sum N2 N1 N3 -> type. %mode sum_comm +SUM -SUM'. sum_ident : {N: nat} sum N z N -> type. %mode sum_ident +N -SUM. sum_ident_z : sum_ident z (sum_z : sum z z z). sum_ident_s : sum_ident (s N) ((sum_s SUM): sum (s N) z (s N)) <- sum_ident N (SUM: sum N z N). %worlds () (sum_ident _ _). %total N (sum_ident N _). sum_inc : sum A B C -> sum A (s B) (s C) -> type. %mode sum_inc +SUM -SUM'. sum_inc_z : sum_inc (sum_z : sum z N N) (sum_z : sum z (s N) (s N)). sum_inc_s : sum_inc (sum_s D) (sum_s D') <- sum_inc D D'. %worlds () (sum_inc _ _). %total SUM (sum_inc SUM _). & : sum_comm (sum_z : sum z N N) SUM <- sum_ident N SUM. & : sum_comm (sum_s SUM) SUM'‘ <- sum_comm SUM SUM‘ <- sum_inc SUM' SUM''. %worlds () (sum_comm _ _). %total SUM (sum_comm SUM SUM'). Metatheorems in Twelf sum_comm: sum N1 N2 N3 -> sum N2 N1 N3 -> type. %mode sum_comm +SUM -SUM'. sum_ident : {N: nat} sum N z N -> type. %mode sum_ident +N -SUM. sum_ident_z : sum_ident z (sum_z : sum z z z). sum_ident_s : sum_ident (s N) ((sum_s SUM): sum (s N) z (s N)) <- sum_ident N (SUM: sum N z N). %worlds () (sum_ident _ _). %total N (sum_ident N _). sum_inc : sum A B C -> sum A (s B) (s C) -> type. %mode sum_inc +SUM -SUM'. This Has Been Checked By A Computer sum_inc_z : sum_inc (sum_z : sum z N N) (sum_z : sum z (s N) (s N)). sum_inc_s : sum_inc (sum_s D) (sum_s D') <- sum_inc D D'. %worlds () (sum_inc _ _). %total SUM (sum_inc SUM _). & : sum_comm (sum_z : sum z N N) SUM <- sum_ident N SUM. & : sum_comm (sum_s SUM) SUM'‘ <- sum_comm SUM SUM‘ <- sum_inc SUM' SUM''. %worlds () (sum_comm _ _). %total SUM (sum_comm SUM SUM'). Now what? •Introduction of the simply typed lambda calculus in Twelf •Proof of progress (it turns out to be the most interesting one in several respects) •The full safety proof is on the web at http://www.princeton.edu/~rsimmons/talk.elf The simply typed λ-calculus •Expressions e := () | λ x:t.e |ee •Types t := unit |t→t The simply typed λ-calculus •Expressions exp : type. unit : exp. lam : tp -> (exp -> exp) -> exp. @ : exp -> exp -> exp. %infix left 10 @. e := () | λ x:t.e |ee •Types t := unit |t→t The simply typed λ-calculus •Expressions exp : type. unit : exp. lam : tp -> (exp -> exp) -> exp. @ : exp -> exp -> exp. %infix left 10 @. e := () | λ x:t.e |ee •Types tp : type. unittp : tp. => : tp -> tp -> tp. %infix right 10 =>. t := unit |t→t The simply typed λ-calculus Γ├ () : unit •The typing relation Γ[x:t]├ e : t’ Γ├ e : t → t’ Γ├ λ x:t.e : t → t’ Γ├ e : t Γ├ e e’ : t’ Γ(x) = t Γ├ x : t The simply typed λ-calculus •The typing relation Γ[x:t]├ e : t’ Γ├ λ x:t.e : t → t’ Γ├ () : unit Γ├ e : t → t’ Γ├ e : t Γ├ e e’ : t’ typed : exp -> tp -> type. t_unit : typed unit unittp. t_lam : typed (lam T ([x] E x)) (T => T') <- ({x} typed x T -> typed (E x) T'). t_app : typed (E1 @ E2) T <- typed E1 (T' => T) <- typed E2 T'. The simply typed λ-calculus •The value relation isval : exp -> type. v_unit : isval unit. v_lam : isval (lam T ([x] E x)). The simply typed λ-calculus •The step relation (λ x:t.e) v [x←v]e e 1 e 1’ e 2 e 2’ e 1 e 2 e 1’ e 2 v e2 v e 2 ’ The simply typed λ-calculus •The step relation (λ x:t.e) v [x←v]e e 1 e 1’ e 2 e 2’ e 1 e 2 e 1’ e 2 v e2 v e 2 ’ eval : exp -> exp -> type. s_app1 : eval (E1 @ E2) (E1' @ E2) <- eval E1 E1'. s_app2 : eval (E1 @ E2) (E1 @ E2') <- isval E1 <- eval E2 E2'. e_app : eval (lam T ([x] E x) @ V) (E V) <- isval V. The simply typed λ-calculus • The Progress Theorem – If an expression e has type t, then the expression is not stuck (the expression steps or is a value) – Proof by induction and case analysis on the last step of the typing derivation – If the last step in the typing derivation is t_unit or t_lam, then the expression is a value – If the last step in the typing derivation is t_app, then the inductive case establishes that the two subexpressions aren’t stuck – If either subexpression steps, then either s_app1 or s_app2 will allow the expression to step – If both subexpressions are values, then because the first subexpression has type t → t’, the canonical forms lemma says that it must be a function, so the expression can step by e_app The simply typed λ-calculus • The Progress Theorem – If an expression e has type t, then the expression is not stuck (the expression steps or is a value) – Proof by induction and case analysis on the last step of the typing derivation notstuck : exp -> type. ns_isval : notstuck E <- isval E. ns_steps : notstuck E <- eval E E'. progress : typed E T -> notstuck E -> type. %mode progress +T -E. The simply typed λ-calculus • The Progress Theorem – If the last step in the typing derivation is t_unit or t_lam, then the expression is a value & : progress t_unit (ns_isval v_unit). & : progress (t_lam _) (ns_isval v_lam). The simply typed λ-calculus • The Progress Theorem – If the last step in the typing derivation is t_app, then the inductive case establishes that the two subexpressions aren’t stuck – If either subexpression steps, then either s_app1 or s_app2 will allow the expression to step – If both subexpressions are values, then because the first subexpression has type t → t’, the canonical forms lemma says that it must be a function, so the expression can step by e_app & : progress (t_app T2 T1) (ns_steps (s_app1 E)) <- progress T1 (ns_steps E). The simply typed λ-calculus • The Progress Theorem – If the last step in the typing derivation is t_app, then the inductive case establishes that the two subexpressions aren’t stuck – If either subexpression steps, then either s_app1 or s_app2 will allow the expression to step – If both subexpressions are values, then because the first subexpression has type t → t’, the canonical forms lemma says that it must be a function, so the expression can step by e_app & : progress (t_app T2 T1) (ns_steps (s_app1 E)) <- progress T1 (ns_steps E). The simply typed λ-calculus • The Progress Theorem – If either subexpression steps, then either s_app1 or s_app2 will allow the expression to step – If both subexpressions are values, then because the first subexpression has type t → t’, the canonical forms lemma says that it must be a function, so the expression can step by e_app lemma : typed E (T' => T) -> notstuck E -> notstuck E' -> notstuck (E @ E') -> type. %mode lemma +T +NS1 +NS2 -NS. & : lemma _ (ns_steps E) _ (ns_steps (s_app1 E)). & : lemma _ (ns_isval v_lam) (ns_steps E) (ns_steps (s_app2 E v_lam)). & : lemma _ (ns_isval v_lam) (ns_isval V) (ns_steps (e_app V)). %worlds () (lemma _ _ _ _). %total {} (lemma _ _ _ _). The simply typed λ-calculus • The Progress Theorem – If the last step in the typing derivation is t_app, then the inductive case establishes that the two subexpressions aren’t stuck – If either subexpression steps, then either s_app1 or s_app2 will allow the expression to step – If both subexpressions are values, then because the first subexpression has type t → t’, the canonical forms lemma says that it must be a function, so the expression can step by e_app & : progress (t_app T2 T1) NS <- progress T1 NS1 <- progress T2 NS2 <- lemma T1 NS1 NS2 NS. %worlds () (progress _ _). %total T (progress T E). For More Information, Call: • MiniML – Distributed with Twelf in the examples directory – The simply typed polymorphic lambda calculus w/ type reconstruction – Many tutorials discuss this, such as The Twelf User’s Guide • Chapter 2 of my thesis report – Develops what is more or less the simply typed lambda calculus with a mutable store – Describes the full proof in more detail and in a different way – http://www.princeton.edu/~rsimmons/thesis.pdf • A metalogical approach to foundational proof carrying code (Crary and Sarkar, 2003) – Presents an introductory approach starting with the sum – I adapted the sum examples from that code – Concerned with assembly code more than formalizing programming languages Conclusions • Twelf metatheory is a good system for formalizing programming languages, and seems well suited for a variety of other tasks as well • Twelf is a pretty good system to ‘tinker’ with formal programming language descriptions – Chapter 3 of my thesis describes some strategies for keeping descriptions ‘tinkerable’ as they get larger. • The tools are hopefully going to keep getting better – Delphin is a very interesting upcoming tool to keep an eye on

Descargar
# Slide 1