[WIP] Refactor extraction to build an easycrypt AST, then pretty-print it.

[cassiersg]

This allows to simplify the code and make it easier to extend.

The main commit is the last one (31b149b7) and does not change the extracted .ec for all test cases (besides the amount of whitespace).

The first 4 commits prepare for testing the changes, then 9a26005f fixes a bug in the extraction, d0b25cdb removes the unused safety extraction, and 4957f20f changes the parentheses and whitespace (the code from that commit is completely over-written in 31b149b7, but that allows to check that 31b149b7 is a no-op).

I left the option for setting the pretty-printing width (205e83c2) and the comparison test scripts (0db786d3), but they can be removed if deemed not useful.

cc @bgregoir

[vbgl]

The fixes to the testing infrastructure should be moved to a different PR (and merged quickly).

The removal of extraction for safety deserves a changelog entry and misses some cleaning in the eclib/ directory. It cannot be merged before the next release (2024.06.0).

[lyonel2017]

@bgregoir, to answer your question. Yes, this PR is interesting for the changes I'm doing in the EC extraction for checking soundness of the Cryptoline approach. I think it will make the code much cleaner.

Maybe a little remark that came to me while looking at the code: I don't really understand why the ec_item type has a newline constructor.

[cassiersg]

@lyonel2017 Thanks for spotting this, it should be removed.

The back-story is that the current change tries very hard to replicate the output of the previous extraction in order to make sure to not break the logic somewhere, since I have not seen a way to test the extraction. The newline is an artifact of this, but should indeed be removed (along with a few idiosyncrasies in the pretty-printing).

[lyonel2017]

Some additional remarks.

• For the constructor for lambda (Efun1) in ec_expr, to avoid currying, I would propose to replacing the string (for the bound variable) with a list of strings.

• The constructor for lambda (Efun1) in ec_expr takes a string for the bound variable which is for me unnatural; I would expect a variable. The reason for that, I think, is the ec_ident type which is a list of strings. Maybe it would be interesting to have a more sophisticated types for identifier of variables and record, tuples, and modules access.

• I have the impression that using a functor to manage the Normal and ConstantTime models would result in cleaner code (example) and simplify the addition of new models in the future.

[cassiersg]

@lyonel2017 Thanks for the feedback. I have basically no experience with OCaml, any suggestion is welcome.

If I understand correctly, for Efun1, you'd suggest to generalize it to lambda with multiple bound variables (currently it's only one because that's what was used in the code, and I didn't clean it up afterwards). So, something like Efun of ec_varname list * ec_expr ?

Regarding the types for identifier of variables and record, tuples, and modules access, how would that look like?

For the use of functors to manage Normal vs ConstantTime, that's a bit how it was done before, which resulted in a lot of code duplication. It's definitely possible to do better using that technique, but I fear that it makes the code overall a bit more complex. Something I'd like to do before merging this PR is to minimize differences between between Normal and ConstantTime modes. Many of these differences are actually artifacts of how code evolved in two modules, producing different (but semantically equivalent) outputs, and until now I tried to avoid changing the output. In the end, I propose to revisit the functor question once this cleanup is done.

[lyonel2017]

• For Efun1, yes exactly.
• For the type of identifiers and the ec_expr type, perhaps something like this (to be discussed):

type ec_type = ...
type ec_op = ...

type ec_var = {
   var_name = string
   var_type = ec_type
}

type ec_expr =
   ...
   | Efun   of (ec_var list) * ec_expr
   | Eproj  of ec_expr * int              (* projection of tuple *)
   | Evar   of ec_var
   | Eop    of ec_op
   | Eapp   of ec_expr * ec_expr list
   ...

Record access uses a projection operator in EC, if I've understood correctly (maybe wrong). The case is therefore taken into account by Eapp. The printer for ec_expr needs to be adapted, and some information needs to be added to the ec_op type so that we print the right thing.

• For the functor part, I had something a little different in mind. For example, for toec_intr:

module type Model = sig
....
val assign : env -> lval -> expr -> instr
...
end.

module Normal : Model = struct
....
let assign env l e =
            let e = toec_cast env (ty_lval lv) e in
            [toec_lval1 env lv e]
....
end.

module ConstantTime : Model = struct
....
let assign env l e =
            let tys = [ty_expr e] in
            (ec_leaks_e env e) @
            ec_call env [lv] tys tys (toec_expr env e)
....
end.

module EC (M: Model) = struct
.....
and toec_instr asmOp env i =
 match i.i_desc with
    | Cassgn (lv, _, _, (Parr_init _ as e)) ->
        (ec_leaks_e env e) @
        [toec_lval1 env lv (ec_ident "witness")]
    | Cassgn (lv, _, _, e) -> M.assign env lv e
    | .......
....
end

[cassiersg]

@vbgl This has now been rebased following last week's discussion (first step of the plan).

I think that it's best to merge this PR in its current state, and defer further cleanups/improvements to future PRs.

For future reference, possible improvements are:

• more unification of the Normal and ConstantTime code paths (that would slightly change the extracted easycrypt code)
• making the easycrypt AST a bit more general (see [WIP] Refactor extraction to build an easycrypt AST, then pretty-print it. #846 (comment))
• investigate the move to functors for handling the various extraction modes (see [WIP] Refactor extraction to build an easycrypt AST, then pretty-print it. #846 (comment)). Doing this without too much code duplication would likely require de above clean-ups to be performed first.