diff options
| -rw-r--r-- | code/krivine.ml | 32 | ||||
| -rw-r--r-- | code/zam.ml | 134 | ||||
| -rw-r--r-- | tfm.pdf | bin | 598715 -> 573256 bytes | |||
| -rw-r--r-- | tfm.tex | 33 |
4 files changed, 68 insertions, 131 deletions
diff --git a/code/krivine.ml b/code/krivine.ml index 0c34d3f..6e0eeb3 100644 --- a/code/krivine.ml +++ b/code/krivine.ml @@ -77,43 +77,27 @@ module Lambda = struct (* Examples *) (* (λx.((λy.y) x)) *) - let m1 = + let ex_m1 = let x = symbol "x" in let y = symbol "y" in Abs (x, App (Abs (y, Var y), Var x)) (* (((λx.(λy.(y x))) (λz.z)) (λy.y)) *) - let m2 = + let ex_m2 = let x = symbol "x" in let y = symbol "y" in let z = symbol "z" in App (App (Abs (x, Abs (y, App (Var y, Var x))), Abs (z, Var z)), Abs (y, Var y)) - let plus = - let m = symbol "m" in - let n = symbol "n" in - let f = symbol "f" in - let x = symbol "x" in - Abs (m, Abs (n, Abs (f, Abs (x, App (App (Var m, Var f), - App (App (Var n, Var f), Var x)))))) - - let nested_if = - If (True, If (False, False, True), False) - - (* s((λx.x) z) *) - let constr_test = - let x = symbol "x" in - peano_of_int ~base:(App (Abs (x, Var x), Constr (z, []))) 1 - (* (λc. case c of (Some(x) → x) (None → c)) Some(s(z))) *) - let case_some = + let ex_case_some = let c = symbol "c" in let x = symbol "x" in App (Abs (c, Case (Var c, [((some, [x]), Var x); ((none, []), Var c)])), Constr (some, [peano_of_int 1])) (* (λc. case c of (Triple(x,y,z) → y)) Triple(1,2,3)) *) - let case_triple = + let ex_case_tuple = let c = symbol "c" in let x = symbol "x" in let y = symbol "y" in @@ -123,7 +107,7 @@ module Lambda = struct Constr (triple, List.map peano_of_int [1;2;3])) (* fix(λf.λc. case c of (s(x) → s(s(f x))) (z → z)) s(s(s(z))) *) - let fix_dup = + let ex_fixpt_mul2 = let f = symbol "f" in let c = symbol "c" in let x = symbol "x" in @@ -133,7 +117,7 @@ module Lambda = struct peano_of_int 3) (* fix(λf.λg.λc. case c of (s(x) → g (f g x)) (z → z)) (λy.s(s(s(y)))) s(s(s(z))) *) - let fix_scale = + let ex_fix_scale = let f = symbol "f" in let g = symbol "g" in let c = symbol "c" in @@ -259,5 +243,5 @@ let dbi_and_red m = let () = let open Lambda in - List.iter dbi_and_red [m1; m2; plus; nested_if; constr_test; - case_some; case_triple; fix_dup; fix_scale] + List.iter dbi_and_red [ex_m1; ex_m2; ex_case_some; + ex_case_tuple; ex_fixpt_mul2; ex_fix_scale] diff --git a/code/zam.ml b/code/zam.ml index 07fb85e..bd39ad4 100644 --- a/code/zam.ml +++ b/code/zam.ml @@ -1,3 +1,13 @@ +(*********************************************) +(* (Extended) Krivine Machine implementation *) +(* *) +(* Guillermo Ramos Gutiérrez (2015) *) +(*********************************************) + + +(*********) +(* Utils *) +(*********) let print_with f x = print_endline (f x) let concat_with sep f xs = String.concat sep (List.map f xs) let split n xs = @@ -15,16 +25,20 @@ let fold_left1 f = function | [] -> raise (Invalid_argument "empty string") | (x::xs) -> List.fold_left f x xs -let dbg_lev = 5 +let dbg_lev = 1 let debug lev spaces s = if dbg_lev >= lev then print_endline (" -- " ^ String.concat "" (repeat spaces " ") ^ s) + (* Compile, decompile and reduce errors *) exception CpErr of string exception DcErr of string exception RdErr of string +(************************************) +(* Calculus of Constructions terms *) +(************************************) module CCLambda = struct type symbol = string * int let symbol : string -> symbol = @@ -67,66 +81,42 @@ module CCLambda = struct let x = symbol s in Abs (x, Var x) - let rec appN n f m = if n = 0 then m else appN (n-1) f (App (f, m)) let apps = fold_left1 (fun m n -> App (m, n)) - let church_of_int n = - let f = symbol "f" in - let x = symbol "x" in - Abs (f, Abs (x, appN n (Var f) (Var x))) - let none = symbol "None" let some = symbol "Some" let cons = symbol "Cons" let nil = symbol "Nil" - (* Peano arithmetic *) + (* Peano arithmetic helpers *) let z = symbol "z" let s = symbol "s" let rec peano_add n x = if n == 0 then x else peano_add (n-1) (Constr (s, [x])) - let peano_of_int n = peano_add n (Constr (z, [])) + let peano_of_int ?(base=Constr (z, [])) n = peano_add n base (* Examples *) - (* (λx.λy. (x y)) (λxx.xx) *) - let partial = - let x = symbol "x" in + (* (λx.x) (λy. ((λz.z) y) (λt.t) *) + let ex_m1 = let y = symbol "y" in - App (Abs (x, Abs (y, App (Var x, Var y))), - identity "xx") - - (* (λm.λn.λf.λx. (m f)((n f) x) *) - let plus = - let m = symbol "m" in - let n = symbol "n" in - let f = symbol "f" in - let x = symbol "x" in - Abs (m, Abs (n, Abs (f, Abs (x, App (App (Var m, Var f), - App (App (Var n, Var f), Var x)))))) - - let _3plus1 = - App (App (plus, church_of_int 3), church_of_int 1) + App (identity "x", + Abs (y, App (App (identity "z", + Var y), + identity "t"))) (* (λf.λx. f (f x)) (λy.y) (λz.z) *) - let twiceId = + let ex_id_id = let f = symbol "f" in let x = symbol "x" in App (App (Abs (f, Abs (x, App (Var f, App (Var f, Var x)))), identity "y"), identity "z") - (* (λc. case c of (Some(x) → x) (None → c)) Some(s(z))) *) - let case_some = - let c = symbol "c" in - let x = symbol "x" in - App (Abs (c, Case (Var c, [((some, [x]), Var x); ((none, []), Var c)])), - Constr (some, [peano_of_int 1])) - (* (λc. case c of (Cons(x, xs) → x) (Nil → Nil)) Cons(λx.x, Nil) *) - let case_head = + let ex_case_head = let c = symbol "c" in let x = symbol "x" in let xs = symbol "xs" in @@ -135,7 +125,7 @@ module CCLambda = struct Constr (cons, [identity "m"; Constr (nil, [])])) (* fix_0(λf.λc. case c of (s(x) → s(s(f x))) (z → z)) s(s(s(z))) *) - let fix_dup = + let ex_fixpt_dup = let f = symbol "f" in let c = symbol "c" in let x = symbol "x" in @@ -143,45 +133,6 @@ module CCLambda = struct [((s, [x]), peano_add 2 (App (Var f, Var x))); ((z, []), peano_of_int 0)])), peano_of_int 3) - - (* fix_1(λf.λg.λc. case c of (s(x) → g(f x)) (z → z)) (λy.s(s(y))) s(s(s(z))) *) - let fix_scale = - let f = symbol "f" in - let g = symbol "g" in - let c = symbol "c" in - let x = symbol "x" in - let y = symbol "y" in - App (App (Fix (f, [g], c, Case (Var c, - [((s, [x]), App (Var g, (App (Var f, Var x)))); - ((z, []), peano_of_int 0)])), - Abs (y, peano_add 2 (Var y))), - peano_of_int 1) - - (* (λx.x) (λy. ((λz.z) y) (λt.t) *) - let acc_app = - let y = symbol "y" in - App (identity "x", - Abs (y, App (App (identity "z", - Var y), - identity "t"))) - - (* (λc. case c of (Cons(x, xs) → x) (Nil → Nil)) *) - let acc_case = - let c = symbol "c" in - let x = symbol "x" in - let xs = symbol "xs" in - Abs (c, Case (Var c, [((cons, [x;xs]), Var c); - ((nil, []), Constr (nil, []))])) - - (* fix_0(λf.λn. case c of (s(x) → s(s(f x))) (z → z)) *) - let acc_fix = - let f = symbol "f" in - let c = symbol "c" in - let x = symbol "x" in - Fix (f, [], c, Case (Var c, - [((s, [x]), peano_add 2 (App (Var f, Var x))); - ((z, []), peano_of_int 0)])) - end module WeakRed : sig @@ -234,10 +185,9 @@ end = struct st_n : int; } - let show_dbi = function - | (x, i) -> - string_of_int i ^ - if dbg_lev > 2 then " (" ^ show_symbol x ^ ")" else "" + let show_dbi (x, i) = + string_of_int i ^ + if dbg_lev > 2 then " (" ^ show_symbol x ^ ")" else "" let rec show_instr = function | ACCESS dbi -> "ACCESS(" ^ show_dbi dbi ^ ")" | CLOSURE is -> "CLOSURE(" ^ show_instrs is ^ ")" @@ -494,7 +444,6 @@ module StrongRed = struct let f' = unique f in let c' = unique c in let accs = List.map (fun x -> Acc (Var x)) (f' :: xs' @ [c']) in - (* debug 2 10 (concat_with " # " show accs); *) let m' = reduce (apps (m :: accs)) in Fix (f', xs', c', m') | _ -> readback (WeakRed.reduce m) @@ -507,7 +456,6 @@ module StrongRed = struct | Acc k -> readback_acc k | App (Fix (f, xs, c, m), p) -> App (reduce (Fix (f, xs, c, m)), readback p) - (* | Fix (f, xs, c, m) -> *) | _ -> raise (RdErr "Readback of invalid value") and readback_acc m = debug 2 2 ("R'( " ^ show m ^ " )"); @@ -525,22 +473,22 @@ module StrongRed = struct | _ -> raise (RdErr "Readback of invalid accumulator") end -let test_weakred m = +let weakred m = print_endline "WEAK REDUCTION TEST"; - print_endline ("Target expression: '" ^ CCLambda.show m ^ "'..."); - - print_string "Compiling... "; + print_endline ("Lambda term:\n " ^ CCLambda.show m); let compiled = WeakRed.compile m in - - print_endline "Reducing..."; let reduced = WeakRed.am_reduce compiled in - print_endline ("Final value: " ^ CCLambda.show (WeakRed.extract reduced)) + print_endline ("Reduced term:\n " ^ CCLambda.show (WeakRed.extract reduced)); + print_endline "----------------------------------------------------------\n" -let test_strongred m = +let strongred m = print_endline "STRONG REDUCTION TEST"; - print_endline ("Target expression: '" ^ CCLambda.show m ^ "'..."); - print_endline ("Final value: " ^ CCLambda.show (StrongRed.reduce m)) + print_endline ("Lambda term:\n " ^ CCLambda.show m); + print_endline ("Reduced term:\n " ^ CCLambda.show (StrongRed.reduce m)); + print_endline "----------------------------------------------------------\n" let () = - let m = CCLambda.fix_scale in - test_strongred m + let open CCLambda in + let examples = [ex_m1; ex_id_id; ex_case_head; ex_fixpt_dup] in + List.iter weakred examples; + List.iter strongred examples Binary files differ@@ -65,6 +65,10 @@ recientemente en el Instituto IMDEA Software en respuesta a la creciente necesidad de disponer de herramientas fiables de verificación formal de criptografía. +En este trabajo se abordará la implementación de una mejora en el procesador de +lenguaje de EasyCrypt, sustituyéndolo por una máquina abstracta derivada de la +ZAM (lenguaje OCaml). + (TODO: crypto, reescritura de términos, máquinas abstractas, mejoras a EasyCrypt) \chapter*{Abstract} @@ -246,12 +250,6 @@ what can be improved) -\section{Symmetric Cryptography} %% - -(TODO: not sure if this section is really needed) - - - \section{Asymmetric Cryptography} %% Here we will introduce some of the most fundamental concepts in asymmetric @@ -570,7 +568,7 @@ that can be applied over terms in order to perform the computation: \subsection{Reduction rules} -Arguably the most important rule in Lambda Calculus is the \textbf{beta +The most prominent reduction rule in Lambda Calculus is the \textbf{beta reduction}, or $\beta$-reduction. This rule represents function evaluation, and can be outlined in the following way: @@ -856,7 +854,7 @@ is evaluating ($C$), an auxiliar \textbf{stack} ($S$) and the current \textbf{environment} ($E$). The code is just a Lambda expression, the stack is where the machine will store \textbf{closures} consisting of non-evaluated code together with its environment at the time the closure was created, and an -environment associates variables (de Bruijn indices) to closures. +environment associates variables (de Bruijn indices) to closures. The typical description of the Krivine Machine \cite{Douence07} is given by the following set of rules: @@ -934,12 +932,12 @@ example $\lambda$-terms: \begin{code} \begin{minted}[fontsize=\scriptsize]{ocaml} -let m1 = (* (λx.((λy.y) x)) *) +let ex_m1 = (* (λx.((λy.y) x)) *) let x = symbol "x" in let y = symbol "y" in Abs (x, App (Abs (y, Var y), Var x)) -let m2 = (* (((λx.(λy.(y x))) (λz.z)) (λy.y)) *) +let ex_m2 = (* (((λx.(λy.(y x))) (λz.z)) (λy.y)) *) let x = symbol "x" in let y = symbol "y" in let z = symbol "z" in @@ -966,7 +964,7 @@ The results: \begin{code} \begin{verbatim} -ocaml> List.iter dbi_and_red [m1; m2];; +ocaml> List.iter dbi_and_red [ex_m1; ex_m2];; # Lambda term: (λx.((λy.y) x)) @@ -989,7 +987,7 @@ variables: \begin{code} \begin{verbatim} -ocaml> List.iter dbi_and_red [m1; m2];; +ocaml> List.iter dbi_and_red [ex_m1; ex_m2];; # Lambda term: (λ.((λ.0) 0)) @@ -1150,7 +1148,7 @@ let peano_of_int ?(base=Constr (z, [])) n = peano_add n base The second extension we are going to implement in our Krivine Machine is the ability to support fixpoints, that is, limited recursion. To prevent infinite reductions, every fixpoint must be defined over a constructor, in a way that -TODO. +(TODO: this is ZAM!). Again, we extend the data structures of the Lambda Calculus. As the extension to DBILambda follows trivially, we will omit it here: @@ -1278,6 +1276,11 @@ its argument, so the whole term is a ``by 3'' multiplier. \chapter{CONCLUSIONS} %%%%%%%%%% +In this work we began by exposing the need to verify cryptographic protocols and +what is the role that the EasyCrypt framework plays in the field. After +some background in cryptography and analysing the inner working of +EasyCrypt. + \begin{itemize} \item Brief wrapping of importance of verified crypto today \item Survey of available reduction machineries, differences between them @@ -1307,11 +1310,13 @@ its argument, so the whole term is a ``by 3'' multiplier. \section{Krivine Machine source code} %% \label{sec:kriv-mach-source} -\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml} +% TODO: UNCOMMENT +%\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/krivine.ml} %\newpage \section{ZAM source code} %% +% TODO: UNCOMMENT %\inputminted[linenos=true,fontsize=\scriptsize]{ocaml}{code/zam.ml} \pagebreak \bibliography{bib}{} \bibliographystyle{ieeetr} |