https://github.com/EasyCrypt/easycrypt
Revision 12af606772a9093ee2feb443da13277a7868e6ed authored by Cameron Low on 15 December 2023, 10:45:02 UTC, committed by GitHub on 15 December 2023, 10:45:02 UTC
The main idea is to provide an inverse to inline when proving an equiv.
Currently, it supports basic procedure unification that requires
manual selection of the program slice to unify with, as well as,
requiring near exact matches on program structure.
An optional return value can be supplied for situations where the
return expression is just a program variable and needs to be
renamed/deconstructed.
There is also support for statement outlining although, this is more
of a transitivity * with program slicing so may require change.
Syntax and variants:
- Procedure outlining:
outline {m} [s - e] lv? <@ M.foo
- Statement outlining:
outline {m} [s - e] { s1; s2; ... }
with
- m: 1 or 2
- s,e: code position
- M.foo: path to procedure
- lv: a left-value
when `s = e`, one can use `[s]` instead of `[s-s]`
For example usage see: tests/outline.ec 1 parent 1733c19
Tip revision: 12af606772a9093ee2feb443da13277a7868e6ed authored by Cameron Low on 15 December 2023, 10:45:02 UTC
New tactic: `outline` (#473)
New tactic: `outline` (#473)
Tip revision: 12af606
| File | Mode | Size |
|---|---|---|
| .github | ||
| config | ||
| examples | ||
| scripts | ||
| src | ||
| tests | ||
| theories | ||
| .dir-locals.el | -rw-r--r-- | 285 bytes |
| .gitignore | -rw-r--r-- | 118 bytes |
| AUTHORS | -rw-r--r-- | 543 bytes |
| LICENSE | -rw-r--r-- | 1.2 KB |
| Makefile | -rw-r--r-- | 1.3 KB |
| README.md | -rw-r--r-- | 7.7 KB |
| default.nix | -rw-r--r-- | 626 bytes |
| dune | -rw-r--r-- | 221 bytes |
| dune-project | -rw-r--r-- | 450 bytes |
| easycrypt.opam | -rw-r--r-- | 1.2 KB |
| easycrypt.opam.template | -rw-r--r-- | 915 bytes |
| easycrypt.png | -rw-r--r-- | 182.6 KB |
| shell.nix | -rw-r--r-- | 308 bytes |
Computing file changes ...
