Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
05 April 2024, 19:20:55 UTC
Revision 2efb9e74ca457ea89e6e28e00d7fdbc97d3fa581 authored by François Dupressoir on 10 February 2020, 09:50:13 UTC, committed by François Dupressoir on 10 February 2020, 09:50:13 UTC 
Consolidate PRP and PRF libraries
 
Including weak PRP-PRF switching lemma, but not its strong version

Squashed commit of the following:

commit 005342f19a55b0ae01c88c0c729fdbad3f2519ff
Merge: 5407570b 7325ae6d
Author: François Dupressoir <fdupress@gmail.com>
Date:   Mon Feb 10 09:48:54 2020 +0000

    Merge branch '1.0' into deploy-simpler-rp

commit 5407570bbdeaee7b725f57fcdbbf764ff301ac9e
Author: François Dupressoir <fdupress@gmail.com>
Date:   Fri Jan 24 12:00:21 2020 +0000

    move towards merging PRF and RO

    also clean assignment notation

commit 65e0c4eb8c702729500148e34900dc5971e583a7
Author: François Dupressoir <fdupress@gmail.com>
Date:   Tue Jan 21 14:14:29 2020 +0000

    Integrate PRP-PRF switching lemma into PRP lib

    Not done for the strong version yet

commit 456a7c96e40fa6827d92fbc36d8cd75fdd8abab1
Author: François Dupressoir <fdupress@gmail.com>
Date:   Tue Jan 21 09:40:25 2020 +0000

    Simplifying the PRF interface

    No keys are needed for the ideal RP,
    The raw interface can be defined separately as needed.

commit e7dea73e6eae21f192efc45f42e9cdc9e5ec4eb8
Author: François Dupressoir <fdupress@gmail.com>
Date:   Tue Jan 21 09:19:04 2020 +0000

    Some nits

commit 8bb90549b6084ea8189e3a4067a155f977ccd34a
Author: François Dupressoir <fdupress@gmail.com>
Date:   Mon Jan 20 16:38:30 2020 +0000

    Cleanup PRP/PRF and PRP-PRF
1 parent 7325ae6
Raw File
Tip revision: 2efb9e74ca457ea89e6e28e00d7fdbc97d3fa581 authored by François Dupressoir on 10 February 2020, 09:50:13 UTC
Consolidate PRP and PRF libraries
Tip revision: 2efb9e7
myocamlbuild.ml 
open Ocamlbuild_plugin

let _ = dispatch begin function
   | After_options ->
       Options.ocamlc   := S[!Options.ocamlc  ; A"-rectypes"];
       Options.ocamlopt := S[!Options.ocamlopt; A"-rectypes"];

   | After_rules ->
       (* Numerical warnings *)
       begin
         let wflag error mode wid =
           let mode = match mode with
             | `Enable  -> "+"
             | `Disable -> "-"
             | `Mark    -> "@"
           in
             match error with
             | false -> S[A"-w"; A(Printf.sprintf "%s%d" mode wid)]
             | true  -> S[A"-warn-error"; A(Printf.sprintf "%s%d" mode wid)]
         in
           for i = 1 to 59 do
             flag ["ocaml"; "compile"; Printf.sprintf "warn_+%d" i] & (wflag false `Enable  i);
             flag ["ocaml"; "compile"; Printf.sprintf "warn_-%d" i] & (wflag false `Disable i);
             flag ["ocaml"; "compile"; Printf.sprintf "warn_@%d" i] & (wflag false `Mark    i);
             flag ["ocaml"; "compile"; Printf.sprintf "werr_+%d" i] & (wflag true  `Enable  i);
             flag ["ocaml"; "compile"; Printf.sprintf "werr_-%d" i] & (wflag true  `Disable i);
             flag ["ocaml"; "compile"; Printf.sprintf "werr_@%d" i] & (wflag true  `Mark    i)
           done
       end;

       (* menhir & --explain/--trace/--table *)
       flag ["ocaml"; "parser"; "menhir"; "menhir_explain"] & A"--explain";
       flag ["ocaml"; "parser"; "menhir"; "menhir_trace"  ] & A"--trace";
       flag ["ocaml"; "parser"; "menhir"; "menhir_table"  ] & A"--table";

       (* Threads switches *)
       flag ["ocaml"; "pkg_threads"; "compile"] (S[A "-thread"]);
       flag ["ocaml"; "pkg_threads"; "link"] (S[A "-thread"]);

       (* Bisect *)
       flag ["ocaml"; "compile" ;  "bisect"] & S[A"-package"; A"bisect"];
       flag ["ocaml"; "compile" ;  "bisect"] & S[A"-syntax" ; A"camlp4o"];
       flag ["ocaml"; "compile" ;  "bisect"] & S[A"-syntax" ; A"bisect_pp"];
       flag ["ocaml"; "ocamldep";  "bisect"] & S[A"-package"; A"bisect"];
       flag ["ocaml"; "ocamldep";  "bisect"] & S[A"-syntax" ; A"camlp4o"];
       flag ["ocaml"; "ocamldep";  "bisect"] & S[A"-syntax" ; A"bisect_pp"];
       flag ["ocaml"; "link"    ;  "bisect"] & S[A"-package"; A"bisect"];

       (* Lint switches *)
       flag ["ocaml"; "lint"; "compile"] (S[A "-ppx"; A "../lint/ppx_lint.native"])

   | _ -> ()
end
back to top