Academia

Barcelona


Warning: A non-numeric value encountered in /var/www/mortendahl.dk/public_html/blog/wp-includes/SimplePie/Parse/Date.php on line 694

Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

First time in Barcelona a few weeks ago. Went there as part of work (the NIPS’16 workshop on private machine learning) but stayed for the weekend to enjoy the city. Lovely place, saw the mayor attractions, including several of Gaudi’s work.

Kalami: Evaluation


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

It’s been a while now since the last post in my little series on Kalami, but I’ve finally polished the code for evaluating programmes as I wanted to. Overall, it’s not that different from the wellformed code of the previous post; in fact, the most challenging aspect is how to enumerate all guesses.

As earlier, we’re dealing with statements, conditions, and expressions. The first one is the tricky one, so to start off simple I’ll first look at the other two. The full source code is available in the evalwoa branch on GitHub.

 

Assuming bindings in environment env for all identifiers in an expression expr, it may be evaluated straight-forwardly by the following recursive function eval_expr:

let rec eval_expr env expr =
    match expr with

        ExprNumber(n) ->
            n

        | ExprVariable(id) ->
            List.assoc id env

        | ExprProduct(expr1, expr2) ->
            let val1 = eval_expr env expr1 in
            let val2 = eval_expr env expr2 in
            val1 * val2

        | ExprDivision(expr1, expr2) ->
            let val1 = eval_expr env expr1 in
            let val2 = eval_expr env expr2 in
            val1 / val2

        | ExprSum(expr1, expr2) ->
            let val1 = eval_expr env expr1 in
            let val2 = eval_expr env expr2 in
            val1 + val2

        | ExprSubtraction(expr1, expr2) ->
            let val1 = eval_expr env expr1 in
            let val2 = eval_expr env expr2 in
            val1 - val2

        | ExprPower(expr1, expr2) ->
            let val1 = eval_expr env expr1 in
            let val2 = eval_expr env expr2 in
            power val1 val2

Note first that since env is just a list of pairs binding identifiers to integers

let env = [ (id1, n1); (id2, n2); ... (idk, nk) ];;

we may extract the latter using built-in function List.assoc as in case ExprVariable. Next, note that there’s no built-in function for integer exponentiation, hence the power function used in case ExprPower is implemented in evaluation.ml as a tail recursive repeated squaring (initially it was using the naive approach, but since I did do my PhD in crypto, this was one of the small changes needed; see separate file power.ml for the various implementations).

 

Evaluating condition cnd is similar, with the small difference that for one reason or another (purist perhaps) I used the prefix notation for function invocation here:

let rec eval_cnd env cnd =
    match cnd with

        CndTrue ->
            true

        | CndFalse ->
            false

        | CndEqual(expr1, expr2) ->
            let val1 = eval_expr env expr1 in
            let val2 = eval_expr env expr2 in
            (=) val1 val2

        | CndLessthan(expr1, expr2) ->
            let val1 = eval_expr env expr1 in
            let val2 = eval_expr env expr2 in
            (<) val1 val2

        | CndNegation(cnd) ->
            let val1 = eval_cnd env cnd in
            (not) val1

        | CndOr(cnd1, cnd2) ->
            let val1 = eval_cnd env cnd1 in
            let val2 = eval_cnd env cnd2 in
            (||) val1 val2

        | CndAnd(cnd1, cnd2) ->
            let val1 = eval_cnd env cnd1 in
            let val2 = eval_cnd env cnd2 in
            (&&) val1 val2

 

For statement stmt it finally gets a bit more interesting. Cases StmtLet and StmtIf are straight-forward, as are StmtAccept and StmtReject which respectively return the current environment and None. However, for a guessing statement it’s a bit more involved. If the guess has an upper bound then we may just try all possibilities as in case StmtGuessLowerUpperBound below. But this will of course not work when no upper bound is specified since an inner guess will prevent outer guesses from ever increasing. As an example, consider programme:

guess x in
guess y in
if x == y+1 then accept
otherwise reject

which has solution [ ("x", 1); ("y", 0) ], yet if we first let x=0 and then use the strategy of enumerating all values for y then we’ll never make it back to incrementing x.

Instead, for a programme with n (unbounded) guesses, i.e. guesses without an upper bound, the simple strategy used here is to enumerate all n-arity integer tuples in an outer loop, and for each evaluate the main statement with a second environment guesses linking the tuples with the identifiers of the (unbounded) guesses. Statements may then be evaluated as follows, using an initial empty environment env for the main statement:

let rec eval_stmt env guesses stmt =
    match stmt with

        StmtLet(id, expr, stmt) ->
            let expr_value = eval_expr env expr in
            let env' = (id, expr_value) :: env in
            eval_stmt env' guesses stmt

        | StmtIf(cnd, stmt_true, stmt_false) ->
            let cnd_value = eval_cnd env cnd in
            if cnd_value then
                eval_stmt env guesses stmt_true
            else
                eval_stmt env guesses stmt_false

        | StmtGuess(id, stmt) ->
            let guess = List.assoc id guesses in
            let env' = (id, guess) :: env in
            eval_stmt env' guesses stmt

        | StmtGuessLowerBound(id, lower_bound_expr, stmt) ->
            let lower_bound = eval_expr env lower_bound_expr in
            let guess = List.assoc id guesses in
            if guess < lower_bound then
                  None
             else
                 let env' = (id, guess) :: env in
                 eval_stmt env' guesses stmt

        | StmtGuessLowerUpperBound(id, lb_expr, ub_expr, stmt) ->
            let lower_bound = eval_expr env lb_expr in
            let upper_bound = eval_expr env ub_expr in
            let rec helper guess =
                let env' = (id, guess) :: env in
                let result = eval_stmt env' guesses stmt in
                match result with
                    None ->
                        if guess < upper_bound then
                            helper (guess + 1)
                        else
                            None
                    | Some(_) ->
                        result
            in
            helper lower_bound

        | StmtAccept ->
            Some(env)

        | StmtReject ->
            None

where we see that in cases StmtGuess and StmtGuessLowerBound the guess performed in the outer enumeration is simply added to the environment.

The only thing missing is hence the outer enumeration. First we have a simple function collecting identifiers:

let rec get_unbounded_guesses stmt =
    match stmt with

        StmtLet(_, _, stmt) ->
            get_unbounded_guesses stmt

        | StmtIf(_, stmt_true, stmt_false) ->
            (get_unbounded_guesses stmt_true) 
            @ (get_unbounded_guesses stmt_false)

        | StmtGuess(id, stmt) ->
            id :: (get_unbounded_guesses stmt)

        | StmtGuessLowerBound(id, _, stmt) ->
            id :: (get_unbounded_guesses stmt)

        | StmtGuessLowerUpperBound(_, _, _, stmt) ->
            get_unbounded_guesses stmt

        | StmtAccept ->
            []

        | StmtReject ->
            []

Next is a projection function project arity number performing a one-to-one mapping of an integer into a integer tuple with the given arity (see also projection.ml). The code for this gets a bit messy so I won’t give it here, yet the main principle is to partition the digits in number such that for instance:

# project 3 123456;;
- : (int * int) list = [(3, 14); (2, 25); (1, 36)]

It could definitely be done in other ways (as well as optimised), but I vaguely remember going with this simply because of it keeping the projected numbers slightly “balanced”.

Finally, we put this together to obtain:

let eval stmt =
    let unb_guess_ids = get_unbounded_guesses stmt in
    if (List.length unb_guess_ids) > 0 then
        let projector = project (List.length unb_guess_ids) in
        let rec helper number = 
            let projection = projector number in
            let guesses = List.combine unb_guess_ids projection in
            let result = eval_stmt [] guesses stmt in
            match result with
                None ->
                    helper (number + 1)
                | Some(_) ->
                    result
        in
        helper 0
    else
        eval_stmt [] [] stmt

that will indeed find a solution to the example programme from above!

 

While this is now a working interpreter, it does have its shortcomings when used without any kind of static analysis thrown in. For example, on programme:

guess x in
reject

the interpreter will enter an infinite loop, despite the fact that the programme obviously doesn’t have any solutions. Fixing this will be the topic of the next post.

Kalami: Working with the Syntax Tree


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

While the grammar from the previous post on parsing puts some restrictions on the form of a valid Kalami programme, it doesn’t reject all invalid programmes. In particular, it doesn’t ensure that all variables are bound (declared) before use. Defining a simple type system to check for this is straight forward, but will also serve to illustrate how easy it is to work with an abstract syntax tree in Caml.

To quickly illustrate the problem, consider programmes such as:

if x == 5 then accept
otherwise reject

which are meaningless since x is unbound. Now, since I don’t know any good way to present the rules of the type system here on the blog in the usual visual style of inference rules (see the appendix in my master’s thesis for instance), I’m just going to give the code implementing them. Fortunately though, Caml allows us to express such rules so concisely that not much is lost this way anyway — a legacy of ML (its distant father) being a language for formulating logical rules for theorem provers!

Starting with expressions, we assume that a list definedvars of variables have already been bound (by outer statements) and by recursion on the structure of expression expr check that all variables it mentions are in the list. The code looks as follows:

let rec wellformed_expr definedvars expr =
    match expr with

        ExprNumber(n) ->
            true

        | ExprVariable(id) ->
            List.mem id definedvars

        | ExprProduct(expr1, expr2) ->
            (wellformed_expr definedvars expr1) &&
            (wellformed_expr definedvars expr2)

        | ExprDivision(expr1, expr2) ->
            (wellformed_expr definedvars expr1) &&
            (wellformed_expr definedvars expr2)

        | ExprSum(expr1, expr2) ->
            (wellformed_expr definedvars expr1) &&
            (wellformed_expr definedvars expr2)

        | ExprSubtraction(expr1, expr2) ->
            (wellformed_expr definedvars expr1) &&
            (wellformed_expr definedvars expr2)

        | ExprPower(expr1, expr2) ->
            (wellformed_expr definedvars expr1) &&
            (wellformed_expr definedvars expr2)

with the most interesting case being for ExprVariable where a call to standard library function List.mem checks the id is a member of the list. Checking a condition is similar, again assuming a list of variables that have already been bound; notice that it calls the above function for cases CndEqual and CndLessthan:

let rec wellformed_cnd definedvars cnd =
    match cnd with

        CndTrue ->
            true

        | CndFalse ->
            true

        | CndEqual(expr1, expr2) ->
            (wellformed_expr definedvars expr1) &&
            (wellformed_expr definedvars expr2)

        | CndLessthan(expr1, expr2) ->
            (wellformed_expr definedvars expr1) &&
            (wellformed_expr definedvars expr2)

        | CndNegation(cnd) ->
            wellformed_cnd definedvars cnd

        | CndOr(cnd1, cnd2) ->
            (wellformed_cnd definedvars cnd1) &&
            (wellformed_cnd definedvars cnd2)

        | CndAnd(cnd1, cnd2) ->
            (wellformed_cnd definedvars cnd1) &&
            (wellformed_cnd definedvars cnd2)

Now, for statements it finally gets slightly more interesting. The function still takes a list definedvars as input since it calls itself recursively, and hence some variables may be bound by outer statements. But it now also extends this list when a let– or guess-statement is encountered; in these cases it also ensures that no variable is re-bound:

let rec wellformed_stmt definedvars stmt =
    match stmt with

        StmtLet(id, expr, stmt) ->
            (not (List.mem id definedvars)) &&
            (wellformed_expr definedvars expr) && 
            (wellformed_stmt (id::definedvars) stmt)

        | StmtIf(cnd, stmt_true, stmt_false) ->
            (wellformed_cnd definedvars cnd) &&
            (wellformed_stmt definedvars stmt_true) &&
            (wellformed_stmt definedvars stmt_false)

        | StmtGuess(id, stmt) ->
            (not (List.mem id definedvars)) &&
            (wellformed_stmt (id::definedvars) stmt)

        | StmtGuessLowerBound(id, _, stmt) ->
            (not (List.mem id definedvars)) &&
            (wellformed_stmt (id::definedvars) stmt)

        | StmtGuessLowerUpperBound(id, _, _, stmt) ->
            (not (List.mem id definedvars)) &&
            (wellformed_stmt (id::definedvars) stmt)

        | StmtAccept ->
            true

        | StmtReject ->
            true

The above functions are all that is needed to perform our validation check: simply invoke wellformed_stmt on the main programme statement with an empty list, and check that it returns true. We may wrap this in function:

let wellformed stmt =
    wellformed_stmt [] stmt

in order to hide some of the implementation details.

Kalami: Parsing


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Next up in the presentation of the little toy language Kalami is parsing. I remember how we used SableCC during my undergraduate years, and I also remember how we simply couldn’t make it pretty no matter what measure we used! Perhaps it can be made better in the Java environment than we ever managed to, but after I saw how it is done in the Caml environment I never looked back: all of a sudden it became fun to write parsers and interpreters!

So, parsing is basically about how to turn a input text string into an in-memory representation in the form of an abstract syntax tree. I don’t want to go into a lot of background but a good source for slightly more details is Chapter 12 in the Ocaml Manual.

The files needed can be found in the ZIP file kalami-parsing.zip; out of these the most important are structure.ml, lexer.mll, and parser.mly.

Starting with structure.ml we first have a piece of Caml code defining what we would like the abstract syntax tree of a Kalami programme to look like:

type identifier = string
type number = int
type bound = int

type expression =
	ExprNumber of number
	| ExprVariable of identifier
	| ExprProduct of expression * expression
	| ExprDivision of expression * expression
	| ExprSum of expression * expression
	| ExprSubtraction of expression * expression
	| ExprPower of expression * expression

type condition =
	CndTrue
	| CndFalse
	| CndEqual of expression * expression
	| CndLessthan of expression * expression
	| CndNegation of condition
	| CndOr of condition * condition
	| CndAnd of condition * condition

type statement =
	StmtLet of identifier * expression * statement
	| StmtIf of condition * statement * statement
	| StmtGuess of identifier * statement
	| StmtGuessLowerBound of identifier * ...
	| StmtGuessLowerUpperBound of identifier * ...
	| StmtAccept
	| StmtReject

Essentially, the above code defines expressions, conditions, and statements as labelled tuples, such that when we for instance write “4*5” in Kalami then this can be represented in memory as expression ExprProduct(ExprNumber(4), ExprNumber(5)). We shall later see that in the end a Kalami programme is simply a statement.

By the way, note the elegance with which we can express an abstract syntax tree in Caml: were we to express the same in Java it would look a lot less intuitive, at least in my experience. This is one of the great strengths of Caml, of which there are plenty more when we start evaluating and analysing the abstract syntax tree in later posts.

Next up is the lexer responsible for the first layer of abstraction of the input, namely turning the raw string into a stream of tokens. Looking in lexer.mll we see that several regular expressions are used to abstract strings, from the very basic labelling of characters and keywords:

	| '('				{ LPAREN }
	| ')'				{ RPAREN }
	| '+'				{ PLUS }
	| '-'				{ MINUS }

	| "let"				{ LET }
	| "in"				{ IN }
	| "if"				{ IF }
	| "then"			{ THEN }

to the slightly more advanced regular expressions:

	| (['0'-'9']+ as i)		{ INT(int_of_string i) }

that also includes a native Caml instruction for turning a string into a number.

Besides this abstraction of strings as tokens not much happens in the lexer, perhaps apart from the little extra code needed for allowing nested comments, and the insistence that STRs, and in turn identifiers, start with a digit (an easy way to distinguish them from INTs).

However, in parser.mly we may use these tokens to put together a grammar. In particular we see from rule main that an input (now a string of tokens) is a Kalami programme if it can be parsed according to rule “stmt” and its sub-rules as given by:

id:
	STR				{ $1 }
;

expr:
	INT				{ ExprNumber($1) }
	| id				{ ExprVariable($1) }
	| expr MULT expr		{ ExprProduct($1, $3) }
	| expr DIV expr			{ ExprDivision($1, $3) }
	| expr PLUS expr		{ ExprSum($1, $3) }
	| expr MINUS expr		{ ExprSubtraction($1...) }
	| expr EXP expr			{ ExprPower($1, $3) }
	| LPAREN expr RPAREN		{ $2 }
;

cnd:
	expr EQ expr			{ CndEqual($1, $3) }
	| expr LT expr			{ CndLessthan($1, $3) }
	| NOT cnd			{ CndNegation($2) }
	| cnd OR cnd			{ CndOr($1, $3) }
	| cnd AND cnd			{ CndAnd($1, $3) }
;

stmt:
	LET id ASSIGN expr IN stmt	{ StmtLet($2, $4, $6) }
	| IF cnd THEN stmt OTHERWI...	{ StmtIf($2, $4, $6) }
	| GUESS id IN stmt		{ StmtGuess($2, $4) }
	| GUESS id FROM expr IN ...	{ StmtGuessLowerBo... }
	| GUESS id FROM expr TO ...	{ StmtGuessLowerUp... }
	| ACCEPT			{ StmtAccept }
	| REJECT			{ StmtReject }
;

Besides these rules the file also contains instructions defining the precedence of for example the mathematical operations as well as their associativity, as needed to help the parser solve ambiguity.

Having looked at the primary files for the parser we turn to the plumbing needed to put them together. File printing.ml simply takes a statement and recursively prints it on the screen, and file kalamiparsing.ml contains Caml code that reads the input, invokes the lexer and the parser, and prints the statement in case no error occurred:

open Printing

let _ =
	try
		let lexbuf = Lexing.from_channel stdin in
		let stmt = Parser.main Lexer.token lexbuf in

		print_string "\n*** Statement ***\n\n";
		print_stmt stmt;
		print_string "\n\n"

	with 
		Lexer.Eof ->
			print_string "End of file\n";
			exit 0
		| Parsing.Parse_error ->
			print_string "Parsing error\n";
			exit 1

The only thing missing now is how to compile everything. This is not completely straight-forward since the lexer and the parser are referencing each other, and as a result we must execute the compilation commands in the specific order as seen in file compile.sh. Doing so will produce the kalamiparsing binary which we can tell to either load a programme from a file through

./kalamiparsing < "inputfile"

or run “interactively” by simply executing

./kalamiparsing

and typing a programme directly into it (ending with an EOF signal by pressing control + d).

In the next post we’ll look at how we may evaluate an in-memory Kalami programme in order to find a satisfying guess; as mentioned previously this requires something slightly more involved than a trivial brute-force.

Kalami: Introduction


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

A few years ago I was the teaching assistant in a course on computability and as such was involved in explaining the concept of non-deterministic “guessing”. I always found this topic fascinating myself, so since I also had to come up with a few project suggestions I thought some of them might be interested in making a programming language with a guessing construct. And to give them a place to start I quickly put together a prototype interpreter in Caml that I’ll explain over the course of a few posts. But let’s first get an idea of what the little toy language can do.

Say you want to find two factors in a given number. There are many ways to do this, but using non-determinism we may simple ask the computer to “guess” them. Expressed in the toy language we can write:

let n = 681 in

guess p from 2 in
guess q from 2 in

if n == p*q then accept
otherwise reject

where p and q are the factors to be guessed, and assumed to be larger than 2 to avoid the trivial solutions with p=1 or q=1. This could of course be expressed similarly in e.g. Prolog, but the aim was also for the project to have a touch of finding suitable evaluation strategies and using static analysis, as well as to illustrate the power of working with languages in Caml.

To illustrate some of the issues consider programme

guess x in
guess y in
if x == y+1 then accept
otherwise reject

which have solution x=1 and y=0. Yet if the evaluation strategy simply starts with x=0 and tries all values for y then it will never find it; in other words, the evaluation strategy must eventually enumerate all tuples of values.

For some programmes we may also benefit from first employing static analysis. Consider for instance programme

guess x in
if x == x+1 then accept
otherwise reject

that is easily seen to not have any solutions — yet the interpreter might not realise this without some kind of static analyse. Likewise, for programmes such as

guess n in
if n == 1*2*3 then accept
otherwise reject

static analysis may speed up execution time by letting the interpreter discover that it only needs to consider a subset of values — in this case only n=6 — instead of it simply brute forcing for all possibly values.

So there you have it. In the next post I’ll provide the source code for the interpreter and begin dinning into it by looking at its parser. Oh, and by the way, the name Kalami came from The Meaning of Liff by Douglas Adams and John Lloyd, which I was reading at the time.

Doctor Dahl


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

The official diploma has arrived, and the Faculty of Science and Technology at Aarhus University has thereby allowed me to address myself as Doctor Dahl in future conversations!

That’s definitely it then, no more university for me, no more formal education, no more student identity. Let the existential crisis commence!

Ph.D. Defense


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Successfully defended my Ph.D. thesis today!

The committee (Bogdan WarinschiKristian Gjøsteen, and Anders Møller) was there, the crypto group was there, and close family and friends were there — a big thank you to all of you for showing up and looking entertained!

Per tradition we went out for dinner with the group and the committee afterwards, this time at Den Rustikke with finishing beer at Cockney Pub (since we no longer have a flat in Aarhus we had to catch the last train to my parent’s in Esbjerg).

Super day, couldn’t have dreamt it any better..

Presentation used for my defense — never have a practised a presentation in front of an audience as much as I did this one; but it surely paid off.

Ph.D. Thesis


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

It’s taken too long, it’s taken too much energy, but my thesis is finally done!

Part exhaustion, part laziness, and part lack of time, it ended up being a collection of my previous papers with a brand new unifying introduction stuck in front: under the title Symbolic Analysis of Cryptographic Protocols – Models, Methods, and Soundness I’ve gathered the full version of the Japanese paper, one of the French papers, and the full version of the Aarhus Eel. It turns out (I really haven’t been very streamlined in my research) that besides symbolic models and cryptographic protocols the three papers are also related through the expressive power vs usability scale: the Japanese paper aims for an efficient method suitable for non-experts, while the Aarhus Eel exchanges the hope for non-experts with an expressive power fitting for advanced modern cryptographic protocols such as secure computation. It took a while to screw this link together but it was a good day when it happened.

Obviously there was the small devil in my head longing for writing everything into a long proper monologue, avoiding the duplications and making it seem as if I have been a lot more streamlined during the last few years, but here, at the end, he has been far easier to keep quiet than I imagined — being done has been pretty hard to beat. Not that I’m unhappy with the outcome by the way, not at all; this is only about its ‘visual appearance’, and underneath it would have been exactly the same.

The next step now is for it to go through revision by my committee and then hopefully getting accepted. But for now it’s no-writing-and-no-computer for a while!

Universally Composable Symbolic Analysis for Two-Party Protocols based on Homomorphic Encryption


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Retrospectively dubbed The Aarhus Eel for it’s ability to repeatedly avoid capture yet good juicy taste when it finally gave in, we yesterday submitted the result of more than a year’s worth of research!

It started with my supervisor saying “Wouldn’t it be nice to have a paper uniting your previous work (symbolic analysis) with your new work (secure computation)?” and me replying “Oh, it would, and it shouldn’t take that long!“.

This was summer 2012, followed by an autumn working out backwards what would be nice to have. For the following Christmas I managed to give my self the present of finally knowing where we wanted to go; concretely, we now had a model of an interesting protocol and its security requirements that we could analyse with current tools (ProVerif). The rest, I thought, would be somewhat straight-forward.

Spring came and went. Summer came and went. Terribly frustrating period to be honest, with some progress but mostly a lot of unforeseen problems, dead ends, and steps back. My view of the project go switch from motivated to hopeless, from relevant to useless, all within a few days. Not only did was a tired after work during this period, insecurities also started to creep in from the fear of spending this much time on something that might be trivial.

Then during autumn the proofs we needed finally started to form. There were far too many details in them to comfortably keep in my head at once so progress was still slow and often felt highly redundant: at this point, changing a small thing to get past an obstacle meant at least an hour or two reworking the proofs and checking that it didn’t break down somewhere else.

Around winter we settled for the technical material and I started working on applications, presentation, and polishing. This meant escaping the mind-filling proofs, and from seeing a product taking its final form motivation started to come back. The pressure of also having a thesis to finish replaced any last resistance to ever go over the report again with a pure mechanical approach of just finishing.

And after making a short 12-page version we then finally submitted the work to Crypto ’13 yesterday! Oh yay, oh yiy, the joy!

Here’s the abstract:

We consider a class of two-party function evaluation protocols in which the parties are allowed to use ideal functionalities as well as a set of powerful primitives, namely commitments, homomorphic encryption, and certain zero-knowledge proofs. With these it is possible to capture protocols for oblivious transfer, coin-flipping, and generation of multiplication-triple.

We show how any protocol in our class can be compiled to a symbolic representation expressed as a process in an abstract process calculus, and prove a general computational soundness theorem implying that if the protocol realises a given ideal functionality in the symbolic setting, then the original version also realises the ideal functionality in the standard computational UC setting. In other words, the theorem allows us to transfer a proof in the abstract symbolic setting to a proof in the standard UC model.

Finally, we have verified that the symbolic interpretation is simple enough in a number of cases for the symbolic proof to be partly automated using the ProVerif tool.

Joint work with Ivan Damgård, and with thanks to Ran Canetti at Boston University and Hubert Comon-Lundh at ENS de Cachan.

Update, 25 May 2013: the full version is online as IACR ePrint report 2013/296.

Update, 15 October 2013: after rejection from Crypto due to lack of full proofs, we have now added these from the full version and re-submitted to Eurocrypt 2014.

Update, 14 January 2014: the paper was been accepted for Eurocrypt, hurray!

Update, 21 March 2014: finally got around to clean up some of the ProVerif source files enough to not be ashamed of releasing them (DNO08 OT protocol)

Update, 15 May 2014: as the final talk of the conference I presented the paper today, thereby putting a nice end to the last PhD paper! (presentation slides, intentionally kept somewhat high-level as this literally was the end of a packed four conference)

Introduction to Cryptography (in Danish)


Warning: preg_match() [function.preg-match]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 1384

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

Warning: preg_match_all() [function.preg-match-all]: Compilation failed: invalid range in character class at offset 4 in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 700

Warning: Invalid argument supplied for foreach() in /var/www/mortendahl.dk/public_html/blog/wp-content/plugins/lightbox-plus/classes/shd.class.php on line 707

I’m not really posting a lot on university-related matters, for two reasons I suppose. Firstly, this blog is mostly a recreational thing right now satisfying a need to do something else than work. Secondly, my PhD is rather technical; I like this, but by it’s very nature also very specialised.

One thing kind of slips through these two filter though, and that is teaching “outsiders” about the basics of crypto. Doing this gets me even more excited today than when I first came across crypto in secondary school about 10-11 years ago in 2002 (through Applied Cryptography and Security Engineering).

During the years I’ve somehow ended up getting involving in three graduation projects of secondary school students writing about crypto. Funnily enough one book has really put itself on this marked — Kryptologi – fra viden til videnskab — with the result that I have yet to hear about someone not writing about either of the topics covered in this book: classic crypto and the RSA crypto system (I wrote about the latter myself).

Last spring I furthermore had the pleasure of actually giving an introduction to cryptography to a class of the brightest students from secondary schools across the country, Sciencetalenter to be precise. And for one and a half day! Work rarely felt less like working.

First they visited our department at Aarhus University where we worked on the RSA system, and a month later I visited the Sorø Science Centre where we covered modern crypto such as secure multi-party computation and classic crypto such as the Vigenère cipher and the Enigma. This latter is a great place by the way, with a very cool cloud chamber!

The notes we used have been iterated over with each PhD student who have had this class during the years and is available below in my rendition. For good or bad these are in Danish.

Masterclass note om RSA Kryptosystemet.

Masterclass note om Sikre Beregninger.

Masterclass note om Historisk Kryptografi.