https://github.com/EasyCrypt/easycrypt

sort by:
Revision Author Date Message Commit Date
3f4a0bd In loop fusion/fission, add more constraints on the epilog Loops' epilogs must now be deterministic and loop/calls-free. This forbids the following unsoundness: ``` require import AllCore DBool. module E = { var i,j : int proc foo () = { var c; i <- 0; j <- 0; c <- false; while (!c) { i <- i + 1; j <- j + 1; c <$ {0,1}; } return i = j; } proc bar () = { var c; i <- 0; j <- 0; c <- false; while (!c) { i <- i + 1; c <$ {0,1}; } c <- false; while (!c) { j <- j + 1; c <$ {0,1}; } return i = j; } }. equiv bad : E.foo ~ E.bar : true ==> ={res}. proof. proc. fission{1} 4!1 @1,2. by sim. qed. ``` Fix #210 13 June 2022, 09:22:31 UTC
b9af81d Add an option that allows EasyCrypt to connect to an external Why3 server The option is -why3server and takes the unix domain socket path as argument. 13 June 2022, 09:22:31 UTC
83417f0 Clear the blocked signals mask on startup. In some circumstances, the inherited mask disturbs Why3 server. 13 June 2022, 08:33:47 UTC
d44bc68 new command: exit (stops EasyCrypt) 13 June 2022, 08:33:47 UTC
ddf82fe [runtest]: use all cores by default 13 June 2022, 08:33:47 UTC
963c9e3 rename depext to opam-depext The `depext` package fails to install with recent versions of opam. The fix suggested in the package information is to use the renamed package `opam-depext` instead. 13 June 2022, 08:33:47 UTC
f7adef3 [dune]: (re)-codesign promoted binaries Dune substitution breaks the initial code-signing. The problem has been acknowledge by the dune team and should be fixed on their side at some point. 13 June 2022, 08:33:47 UTC
e717abd smt option to dump a smt query to a file 13 June 2022, 08:33:47 UTC
b4dc5af default.nix: use why3 1.5.0 13 June 2022, 08:33:47 UTC
30da1ec [runtest]: exit with a non-zero exit status in case of failure. 13 June 2022, 08:33:47 UTC
50b36d0 [runtest]: do not display warnings/infos as errors Fix #198 13 June 2022, 08:33:47 UTC
38e640d Fix pretty-printing of projections. Former printer was using an invalid priority for projections. Fixes #200 13 June 2022, 08:33:47 UTC
f5ea865 Updating README for current why3 requirements. 13 June 2022, 08:33:47 UTC
12c9168 mark `transpose` as parse-only We have suffered long enough 13 June 2022, 08:33:47 UTC
86a6ffb [stdlib]: more lemmas around dfun. Main result is the equivalence between sampling a function and sampling a function in the same function space, but for one point that is sample a posteriori. 13 June 2022, 08:33:47 UTC
90b7c63 [stdlib] new lemmas around dscalar & dlet. 13 June 2022, 08:33:47 UTC
c79e18e [stdlib]: new operator for updating a function at one point. Notation is "f.[x <- v]" for the function that is equal to "f" but at value "x" where it returns "v". 13 June 2022, 08:33:47 UTC
a5633b1 New `runtest` script - more readable output (for tty / no-tty) - more readable report 13 June 2022, 08:33:47 UTC
611f991 Fix pretty-printing of mixfix notations. The notation was not printed when the operators was over-applied. E.g., f.[x <- v] y was printed "_.[_<-_]" f x v y. 13 June 2022, 08:33:47 UTC
75c489d README: remove "make PREFIX=" 13 June 2022, 08:33:47 UTC
3e364fa README: configuration Why3 using EasyCrypt 13 June 2022, 08:33:47 UTC
d1dfe94 When configuring Why3, create the configuration file destination directory first 13 June 2022, 08:33:47 UTC
d0b1178 [stdlib]: link Finite & FinType. 13 June 2022, 08:33:47 UTC
909cfa1 error on potential procedure call in RHS of <- If the RHS of a <- fails to typecheck as an expression but could be a procedure call, mention <@ as an alternative 13 June 2022, 08:33:45 UTC
96cdc83 Enforce separation between <- and <@ more strictly This removes the error message when the RHS is a procedure call. This allows us to accept things that were rejected before, when a procedure and operator share their name. A follow-up may re-enable it. Fix #189 13 June 2022, 08:30:51 UTC
194eca8 [stdlib]: add various small lemmas (Logic, FSet, Distr, DInterval, Bigop) - #non-backward-compatible: this commits generalizes `Bigop.reindex` to restrict the cancellation property to the index list. 13 June 2022, 08:29:57 UTC
058aeeb progress in composition cost 12 May 2022, 17:14:27 UTC
1f7d4a7 cleaned-up various cost (in particular epoch-related) todos 12 May 2022, 16:19:56 UTC
e8473ba simplification rules of cost comparison based on epochs 12 May 2022, 10:19:49 UTC
f4b4c0f [WIP] cost simplification using epochs 11 May 2022, 17:11:58 UTC
af6a0ed fix subtyping bug 11 May 2022, 16:03:59 UTC
2fdc6e1 fixed: refresh module instead of module substitution 11 May 2022, 15:45:31 UTC
0853556 check that CHoare is loaded before generating proof obligation. 11 May 2022, 15:08:17 UTC
163c0a0 added epoch in local declarations 11 May 2022, 10:05:32 UTC
b6602ec Change configuration file resolution Do not consider locations that point to non-existing files. The configuration file location is now printing by the `config` command. 10 May 2022, 13:34:29 UTC
eedf9d2 Finite.to_seq: now have a body based on choiceb Co-authored-by: Christian Doczkal <christian.doczkal@mpi-sp.org> 10 May 2022, 13:34:29 UTC
c7851aa Bump Why3 version from 1.4.x to 1.5.0 fix #184 10 May 2022, 13:34:29 UTC
b753c9f [github-action]: do not start as root This requires a modification of the docker image s.t. the user UID is compatible with the one used by Github Action 10 May 2022, 13:34:29 UTC
f1093b8 Use local configuration file in priority 10 May 2022, 13:34:29 UTC
260f326 Fic computation of source root for local builds 10 May 2022, 13:34:29 UTC
1368273 Fix the license announced in the banner 10 May 2022, 13:34:29 UTC
f3071a1 refactoring: local declarations are now records 09 May 2022, 16:45:49 UTC
65e3be8 tentative new technique to make complexity proof obligation still work in progress 05 May 2022, 16:44:46 UTC
8352f49 add test file for cost 05 May 2022, 14:49:26 UTC
28c4bf8 destruct_cost using hypothesis 05 May 2022, 14:46:47 UTC
d411922 started to adapt the composition cost proof 05 May 2022, 13:39:01 UTC
4335cc5 fixed bad implicit arguments for cost call rule 05 May 2022, 13:06:40 UTC
94dcd47 fixed issue with infinite intrinsic cost infinite intrinsic cost was absorbing oracle call constraints 05 May 2022, 11:36:12 UTC
c13099e rules to prove subcond side-conditions 04 May 2022, 11:30:55 UTC
2312419 removed projection over concrete cost, which is unsound. 04 May 2022, 09:22:07 UTC
29b926f added additional opacity check in LowGoal 04 May 2022, 07:49:37 UTC
4015176 abstract module now have an opacity, giving their cost when called The opacity of a module is either Opaque (default) or Open. Essentially, the opacity tells what is the intrinsic cost of an abstract module when it is called. If `A` has type `M[f : [c, ...]]` then: - if A module type is opaque, then calling A.f costs `[A.f : '1]` - if A module type is open, then calling A.f costs `c` Opacity is denoted by adding the `open` or `opaque` keyword in a module complexity restriction, e.g. `M[open f : ...]`. No explicit opacity means Opaque. 03 May 2022, 15:22:13 UTC
17ae2d3 better printing + work on costs 29 April 2022, 15:32:59 UTC
f37b697 bigcost morphism rule added to reduce_logic 29 April 2022, 12:41:50 UTC
163abd8 printing: better alignement in cost vectors 29 April 2022, 09:31:14 UTC
6ab4890 simplifications of choare statements 29 April 2022, 08:43:58 UTC
f37eff5 removed projection over abstract procedures, which is unsound 28 April 2022, 16:54:57 UTC
e399dc5 new cost axiom 27 April 2022, 23:09:11 UTC
2055e8f minor 27 April 2022, 17:08:08 UTC
c3146c2 cleanup 27 April 2022, 17:08:03 UTC
3a46371 fixed cost librairies 27 April 2022, 17:07:53 UTC
db88428 fix projection printing 27 April 2022, 14:27:46 UTC
89f954e can parse projections 27 April 2022, 14:05:40 UTC
753f746 fixed `hint simplify` usage for cost theory also moved axiom out of pervasive 27 April 2022, 09:59:18 UTC
91761d1 better form dumping 27 April 2022, 09:49:14 UTC
324ba73 Makefile 26 April 2022, 16:46:37 UTC
2dabde1 move cost axioms in abstract theories (fix #175) 26 April 2022, 16:46:15 UTC
5d283f2 Reject `x <- RHS` when `RHS` is a procedure call 26 April 2022, 16:42:47 UTC
7e0f6ba Improve parser for anonymous proc parameters Anonymous and named parameters can be mixed for abstract procedures. Corner cases are not exercised by test suites and may crop up. Resolves #108. 26 April 2022, 16:42:12 UTC
20564b5 Fixing list of authors 26 April 2022, 16:35:39 UTC
716f354 [env]: fully head-norm the type before fetching its top-level decl. This commit involves a lot of code motion. partially address #121 26 April 2022, 16:35:39 UTC
8abdc7d [reduction]: in cbv, fix handling of stack arguments The API was s.t. it was possibly to detect a non-empty stack as an empty one. Partially address #121 26 April 2022, 16:35:39 UTC
3aee866 error message if cost information are missing in the call tactic 26 April 2022, 16:35:18 UTC
44a632c Fix typing of modules expressions fix #171 26 April 2022, 16:33:30 UTC
a5de7bc [reduction]: use symmetric "and" when reducing tuples equality fix #171 26 April 2022, 16:33:30 UTC
1c52e78 pretty printer improvements for module restrs + local memtypes 26 April 2022, 16:33:17 UTC
75f6941 Remove superflous renamings fixes #146 26 April 2022, 16:30:56 UTC
312ac25 [tactic]: [proc*]: fix procedure's arguments substitution Instead of introduce a single variable for the arguments tuple, introduce all the procedure's arguments as single program variables. Fix #166 26 April 2022, 16:30:56 UTC
86b62e5 [chore] update theories/dune 26 April 2022, 16:30:56 UTC
7dbdbe0 [tactic]: [rewrite]: support for multi-rules `rewrite h` with `h : eq1 /\ eq2 /\ ... /\ eqn` is equivalent to `rewrite ?(h1, h2, ..., hn)` with `hi : eqi` address #155 26 April 2022, 16:30:56 UTC
32578da License change: CeCILL B/C -> MIT 26 April 2022, 16:30:22 UTC
a307890 dopt: extend subdistribution to lossless distributions on options 26 April 2022, 16:29:04 UTC
47a2f63 [tactic]: in `apply... in...`, check that all variables are instantiated fix #149 26 April 2022, 16:29:04 UTC
53651e1 [build]: [dune]: auto-generation of theories/dune 26 April 2022, 16:29:04 UTC
5dd9a9c improved substitution API for module idents 11 April 2022, 09:12:40 UTC
50961c7 fix: use the functor to retrieve the cost information and not the applied module 08 April 2022, 09:41:52 UTC
6cabd84 comments + assert 16 March 2022, 09:45:03 UTC
3466266 minor 15 March 2022, 17:44:34 UTC
905023b Merge branch 'deploy-cost-1.0-preview' into deploy-new-cost 15 March 2022, 17:09:54 UTC
45559bb [WIP] 15 March 2022, 15:43:37 UTC
9108d72 [WIP] 15 March 2022, 15:12:18 UTC
c3be289 [WIP] 15 March 2022, 12:49:19 UTC
a0fed93 [WIP] 14 March 2022, 18:57:39 UTC
928152b subst: distinguish between refreshing module and instantiating 14 March 2022, 17:18:57 UTC
b93754a fixed hashed elgamal 14 March 2022, 15:02:48 UTC
aa86882 changed name of lemma 14 March 2022, 13:40:02 UTC
c502b6b added stronger version of dmap1E_can 14 March 2022, 13:40:02 UTC
6f177e1 pragma to retrieve the old behaviour on memory restrictions 14 March 2022, 13:40:02 UTC
2a9c1a7 smart constructors for module type and module sigs 13 March 2022, 07:40:36 UTC
15d9859 [WIP] substitution in module types 10 March 2022, 14:38:50 UTC
back to top