EC: add unit tests for extraction

.gitlab-ci.yml

@@ -198,6 +198,7 @@ check-proofs:
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt why3config -why3 $WHY3_CONF'
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'easycrypt     config -why3 $WHY3_CONF'
   - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler/examples/gimli/proofs CT_MODE=$CT_MODE'
+  - nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run 'make -C compiler/examples/extraction-unit-tests'
 
 libjade-compile-to-asm:
   stage: test

compiler/examples/extraction-unit-tests/.gitignore

@@ -0,0 +1 @@
+loops.ec

compiler/examples/extraction-unit-tests/Makefile

@@ -0,0 +1,16 @@
+ECARGS ?= -I Jasmin:../../../eclib
+
+JASMIN2EC := ../../jasmin2ec
+
+.SUFFIXES: .jazz .ec
+
+all: loops.ec proofs.ec
+	easycrypt runtest $(ECARGS) ec.config $@
+
+clean:
+	$(RM) loops.ec
+
+%.ec: %.jazz
+	$(JASMIN2EC) -o $@ $^
+
+.PHONY: all

compiler/examples/extraction-unit-tests/ec.config

@@ -0,0 +1,6 @@
+[default]
+bin = easycrypt
+
+[test-all]
+okdirs = .
+

compiler/examples/extraction-unit-tests/loops.jazz

@@ -0,0 +1,24 @@
+/* Tests bounds of decreasing for loops */
+export
+fn forty() -> reg u32 {
+  inline int i j = 0;
+  for i = 10 downto 5 {
+    j += i;
+  }
+  reg u32 r = j;
+  return r;
+}
+
+/* Tests nested for loops with non-immediate bounds */
+param int a = 10;
+export
+fn for_nest() -> reg u32 {
+  inline int i j k = 0;
+  for i = 0 to a + a {
+     for j = 0 to a * a {
+       k += 1;
+     }
+  }
+  reg u32 r = k;
+  return r;
+}

compiler/examples/extraction-unit-tests/proofs.ec

@@ -0,0 +1,16 @@
+require import AllCore.
+from Jasmin require import JWord.
+
+require Loops.
+
+lemma loops_forty_correct : hoare [ Loops.M.forty: true ==> res = W32.of_int 40 ].
+proof. by proc; unroll for ^while; auto. qed.
+
+lemma loops_for_nest_correct : hoare [ Loops.M.for_nest: true ==> res = W32.of_int 2000 ].
+proof.
+  proc; wp.
+  while (0 <= i <= inc /\ k = 100 * i).
+  - wp.
+    while (0 <= j <= inc_0 /\ k = 100 * i + j); by auto => /#.
+  auto => /#.
+qed.