Mapreduce paper simple examples

Author: Gustavo2622

examples/mapreduce_paper.ec

@@ -0,0 +1,108 @@
+require import AllCore Bool IntDiv CoreMap List Distr QFABV.
+from Jasmin require import JModel JArray.
+
+
+bind bitstring W8.w2bits W8.bits2w W8.to_uint W8.to_sint W8.of_int W8.t 8.
+realize size_tolist by auto.
+realize tolistP by auto.
+realize oflistP by admit.
+realize ofintP by admit.
+realize touintP by admit.
+realize tosintP by admit.
+
+bind op W8.t W8.(+^) "xor".
+realize bvxorP by admit.
+
+op bool2bits (b : bool) : bool list = [b].
+op bits2bool (b: bool list) : bool = List.nth false b 0.
+
+op i2b (i : int) = (i %% 2 <> 0).
+op b2si (b: bool) = 0.
+
+bind bitstring bool2bits bits2bool b2i b2si i2b bool 1.
+realize size_tolist by auto.
+realize tolistP by auto.
+realize oflistP by admit.
+realize ofintP by admit.
+realize touintP by admit.
+realize tosintP by auto.
+
+bind op bool (^^) "add".
+realize bvaddP by admit.
+
+op predT_bool : bool -> bool = fun _ => true.
+op xor1_bool (b: bool) = b ^^ true.
+
+op xor_left (w1 : W8.t) =
+  (w1 +^ (W8.of_int 42)) +^ (W8.of_int 213).
+
+op xor_right (w1 : W8.t) =
+  w1 +^ ((W8.of_int 42)) +^ (W8.of_int 213).
+
+op xor_left_spec : W8.t -> W8.t.
+
+bind circuit xor_left_spec "XOR_LEFT8".
+
+op predT_W8 : W8.t -> bool = fun _ => true.
+
+module M = {
+  proc xor_left_proc (w1: W8.t) = {
+    w1 <- w1 +^ (W8.of_int 42);
+    w1 <- w1 +^ (W8.of_int 213);
+    return w1;
+  }
+
+  proc xor_right_proc (w1: W8.t) = {
+    var w2 : W8.t;
+    w2 <- (W8.of_int 42);
+    w2 <- w2 +^ (W8.of_int 213);
+    w1 <-w1 +^ w2;
+    return w1;
+  } 
+}.
+
+lemma xor_left_corr (w: W8.t) :
+    hoare [ M.xor_left_proc : w = w1 ==> res = xor_left w].
+proof.
+proc.
+bdep 8 8 [w] [w1] [w1] xor_left predT_W8.
+admit.
+admit.
+qed.
+
+lemma xor_left_equiv_xor_right_proc (w: W8.t) : 
+    equiv [ M.xor_left_proc ~ M.xor_right_proc : w = arg{1} /\ arg{1} = arg{2} ==> res{1} = res{2} ]. 
+proof.
+proc.
+bdepeq 8 [w1] [w1] {8 : [w1 ~ w1]} predT_W8.
+admit.
+auto.
+qed.
+
+lemma xor_left_equiv_xor_right_proc_lanes (w: W8.t) : 
+    equiv [ M.xor_left_proc ~ M.xor_right_proc : w = arg{1} /\ arg{1} = arg{2} ==> res{1} = res{2} ]. 
+proof.
+proc.
+bdepeq 1 [w1] [w1] {1 : [w1 ~ w1]} predT_bool.
+admit.
+auto.
+qed.
+
+
+lemma xor_left_corr_lanes (w: W8.t) :
+    hoare [ M.xor_left_proc : w = w1 ==> res = xor_left w].
+proof.
+proc.
+bdep 1 1 [w] [w1] [w1] xor1_bool predT_bool.
+admit.
+admit.
+qed.
+
+lemma xor_left_corr_spec (w: W8.t) :
+    hoare [ M.xor_left_proc : w = w1 ==> res = xor_left w].
+proof.
+proc.
+bdep 8 8 [w] [w1] [w1] xor_left_spec predT_W8.
+admit.
+admit.
+qed.

flake.nix

@@ -7,7 +7,6 @@
     nixpkgs.url = "github:nixos/nixpkgs/24.05";
     stable.url = "github:nixos/nixpkgs/24.05";
     nixpkgs.follows = "opam-nix/nixpkgs";
-    emacs-overlay.url = "github:nix-community/emacs-overlay";
 
     prover_cvc4_1_8 = {
       url = "github:CVC4/CVC4-archived/1.8";
@@ -20,7 +19,7 @@
     };
 
     prover_z3_4_12_6 = {
-      url = "github:z3prover/z3/z3-4.13.3";
+      url = "github:z3prover/z3/z3-4.12.6";
       flake = false;
     };
   };
@@ -110,19 +109,5 @@
            ++ [ pkgs.git scope'.why3 packages.provers ]
            ++ (with pkgs.python3Packages; [ pyyaml ]);
         };
-
-	devShells.withDevTools = pkgs.mkShell rec {
-	  inputsFrom = [ scope'.easycrypt ];
-	  buildInputs = 
-	      devPackages
- 	   ++ devTools
-	   ++ [ scope'.why3 packages.provers ]
-	   ++ (with pkgs.python3Packages; [ pyyaml ]);
-	  SHELL = ''${pkgs.bashInteractive + "/bin/bash"}'';
-	  shellHook = builtins.replaceStrings ["\n"] [" "] ''
-	    export SHELL=${SHELL} &&
-	    export PATH=$PATH:`realpath .`
-	  '';
-	};
       });
 }

libs/lospecs/specs/avx2.spec

@@ -431,3 +431,10 @@ VPSHUFB_128(w@128, widx@128) -> @128 =
     fun idx@8 . idx[7] ? 0 : w[@8|idx[@4|0]],
     widx
   )
+
+# MAPREDUCE EXAMPLE
+XOR_LEFT8(w@8) -> @8 =
+  xor<8>(xor<8>(w, 42@8), 213@8)
+
+XOR_RIGHT8(w@8) -> @8 =
+  xor<8>(w, xor<8>(42@8, 213@8))