Skip to content

Commit ef02e81

Browse files
committed
Merge branch 'main' into bdep_ecCircuitsRefactor
Merging main updates into bdep refactoring in preparation for PR
2 parents 3addec7 + 4f84b7c commit ef02e81

34 files changed

+431
-574
lines changed

README.md

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -182,26 +182,26 @@ following [these instructions](https://nixos.org/manual/nix/stable/#chap-install
182182
183183
Then, at the root of the EasyCrypt source tree, type:
184184
185-
```
186-
$> make nix-build
187-
```
185+
```
186+
$> make nix-build
187+
```
188188
189189
Once completed, you will find the EasyCrypt binary in `result/bin`.
190190
191191
You can also run
192192
193-
```
194-
$> make nix-build-with-provers
195-
```
193+
```
194+
$> make nix-build-with-provers
195+
```
196196
197197
to install EasyCrypt along with a set of provers.
198198
199199
200200
For getting a development environment, you can run:
201201
202-
```
203-
$> make nix-develop
204-
```
202+
```
203+
$> make nix-develop
204+
```
205205
206206
These will install all the required dependencies, a set of provers and
207207
will then drop you into a shell. From there, simply run `make` to

examples/MEE-CBC/FunctionalSpec.ec

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,7 @@ clone import BitWord as Octet with
1212
op n <- 8
1313
rename "word" as "octet"
1414
rename "Word" as "Octet"
15-
proof *.
16-
realize gt0_n by trivial.
17-
realize getE by rewrite /"_.[_]".
18-
realize setE by rewrite /"_.[_<-_]".
15+
proof * by trivial.
1916

2017
op o2int (o : octet) : int = bs2int (ofoctet o).
2118
op int2o (i : int) : octet = mkoctet (int2bs 8 i).
@@ -41,8 +38,6 @@ rename "Word" as "Block"
4138
proof *.
4239
realize Alphabet.enum_spec by exact/Octet.enum_spec.
4340
realize ge0_n by trivial.
44-
realize getE by rewrite /"_.[_]".
45-
realize setE by rewrite /"_.[_<-_]".
4641

4742
abbrev dblock = DBlock.dunifin.
4843

@@ -136,8 +131,6 @@ rename "Word" as "Tag"
136131
proof *.
137132
realize Alphabet.enum_spec by exact/Octet.enum_spec.
138133
realize ge0_n by trivial.
139-
realize getE by rewrite /"_.[_]".
140-
realize setE by rewrite /"_.[_<-_]".
141134

142135
(** Messages are just octet lists **)
143136
type msg = octet list.

scripts/docker/Dockerfile.build

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,15 @@ COPY --chmod=0755 --chown=1001:0 docker-parts/alt-ergo bin/run-alt-ergo
1515

1616
ENV PATH="/home/charlie/bin:$PATH"
1717

18+
RUN \
19+
version=2.6.0 && \
20+
opam switch create --no-switch alt-ergo-${version} ocaml-system && \
21+
opam pin --switch=alt-ergo-${version} add -n alt-ergo ${version} && \
22+
opam install --switch=alt-ergo-${version} --deps-only --confirm-level=unsafe-yes alt-ergo && \
23+
opam install --switch=alt-ergo-${version} alt-ergo && \
24+
opam clean --switch=alt-ergo-${version} && \
25+
ln -s run-alt-ergo ~/bin/alt-ergo-${version}
26+
1827
RUN \
1928
version=2.5.4 && \
2029
opam switch create --no-switch alt-ergo-${version} ocaml-system && \

src/ecCoreLib.ml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -268,6 +268,7 @@ module CI_Logic = struct
268268
let p_and_proj_r = _Logic "andWr"
269269
let p_anda_proj_l = _Logic "andaWl"
270270
let p_anda_proj_r = _Logic "andaWr"
271+
let p_anda_proj_rs = _Logic "andaWrs"
271272
let p_or_elim = _Logic "orW"
272273
let p_ora_elim = _Logic "oraW"
273274
let p_iff_elim = _Logic "iffW"
@@ -276,6 +277,7 @@ module CI_Logic = struct
276277
let p_true_intro = _Logic "trueI"
277278
let p_and_intro = _Logic "andI"
278279
let p_anda_intro = _Logic "andaI"
280+
let p_anda_intro_s = _Logic "andaIs"
279281
let p_or_intro_l = _Logic "orIl"
280282
let p_ora_intro_l = _Logic "oraIl"
281283
let p_or_intro_r = _Logic "orIr"

src/ecCoreLib.mli

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -240,6 +240,7 @@ module CI_Logic : sig
240240
val p_and_proj_r : path
241241
val p_anda_proj_l : path
242242
val p_anda_proj_r : path
243+
val p_anda_proj_rs : path
243244
val p_or_elim : path
244245
val p_ora_elim : path
245246
val p_iff_elim : path
@@ -248,6 +249,7 @@ module CI_Logic : sig
248249
val p_true_intro : path
249250
val p_and_intro : path
250251
val p_anda_intro : path
252+
val p_anda_intro_s : path
251253
val p_or_intro_l : path
252254
val p_ora_intro_l : path
253255
val p_or_intro_r : path

src/ecFol.ml

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1039,9 +1039,7 @@ let destr_ands ~deep =
10391039

10401040
in fun f -> doit f
10411041

1042-
1043-
(*---------------------------------------------*)
1044-
1042+
(* -------------------------------------------------------------------- *)
10451043
let rec one_sided mem fp =
10461044
match fp.f_node with
10471045
| Fint _ -> true

src/ecHiGoal.ml

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2025,10 +2025,17 @@ let process_right (tc : tcenv1) =
20252025
tc_error !!tc "cannot apply `right` on that goal"
20262026

20272027
(* -------------------------------------------------------------------- *)
2028-
let process_split (tc : tcenv1) =
2029-
try t_ors [EcLowGoal.t_split; EcLowGoal.t_split_prind] tc
2028+
let process_split ?(i : int option) (tc : tcenv1) =
2029+
let tactics : FApi.backward list =
2030+
match i with
2031+
| None -> [EcLowGoal.t_split; EcLowGoal.t_split_prind]
2032+
| Some i -> [EcLowGoal.t_split ~i] in
2033+
2034+
try t_ors tactics tc
20302035
with InvalidGoalShape ->
2031-
tc_error !!tc "cannot apply `split` on that goal"
2036+
tc_error !!tc
2037+
"cannot apply `split/%a` on that goal"
2038+
(EcPrinting.pp_opt Format.pp_print_int) i
20322039

20332040
(* -------------------------------------------------------------------- *)
20342041
let process_elim (pe, qs) tc =

src/ecHiGoal.mli

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ val process_cut : ?mode:cutmode -> engine -> ttenv -> cut_t -> backward
8282
val process_cutdef : ttenv -> cutdef_t -> backward
8383
val process_left : backward
8484
val process_right : backward
85-
val process_split : backward
85+
val process_split : ?i:int -> backward
8686
val process_elim : prevert * pqsymbol option -> backward
8787
val process_case : ?doeq:bool -> prevertv -> backward
8888
val process_exists : ppt_arg located list -> backward

src/ecHiTacticals.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) =
129129
| Preflexivity -> process_reflexivity
130130
| Passumption -> process_assumption
131131
| Psmt pi -> process_smt ~loc:(loc t) ttenv (Some pi)
132-
| Psplit -> process_split
132+
| Psplit i -> process_split ?i
133133
| Pfield st -> process_algebra `Solve `Field st
134134
| Pring st -> process_algebra `Solve `Ring st
135135
| Palg_norm -> EcStrongRing.t_alg_eq

src/ecLoader.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -65,15 +65,16 @@ let rec addidir ?namespace ?(recursive = false) (idir : string) (ecl : ecloader)
6565
| None -> ()
6666
| Some st -> begin
6767
let idx = (st.Unix.st_dev, st.Unix.st_ino) in
68+
let idirs = List.filter (fun ((nm, _), _) -> nm = namespace) ecl.ecl_idirs in
6869

6970
match Sys.os_type with
7071
| "Win32" ->
7172
let test ((_, name), _) = name = idir in
72-
if not (List.exists test ecl.ecl_idirs) then
73+
if not (List.exists test idirs) then
7374
ecl.ecl_idirs <- ((namespace, idir), idx) :: ecl.ecl_idirs
7475

7576
| _ ->
76-
if not (List.exists ((=) idx |- snd) ecl.ecl_idirs) then
77+
if not (List.exists ((=) idx |- snd) idirs) then
7778
ecl.ecl_idirs <- ((namespace, idir), idx) :: ecl.ecl_idirs
7879
end
7980

0 commit comments

Comments
 (0)