Modularize leakage extraction

[cassiersg]

(Summary of discussion consensus in Bristol. - I hope this is faithful. @bgregoir @mbbarbosa @bacelar @strub @lyonel2017)

In order to allow for easier local reasoning about the leakage, it should be returned by functions instead of being accumulated in a global variable. Furthermore, functions could be tree structure of leakage (with a node for each function call, each while/for/if block, each instruction...).
While this would break easycrypt CT proofs, they should be easy to fix (the CT security statement would be modified a bit to take the leakage from the return of the function, but the proc; inline *; sim. proofs should still work).

This paves the way for introduction of a value leakage extraction mode, where each manipulated word gets leaked.