restore w.r.t F* and steel main branches

Zeta.fst.config.json

@@ -0,0 +1,32 @@
+{
+    "fstar_exe": "fstar.exe",
+    "options": [
+      "--max_fuel", "0",
+      "--max_ifuel", "2",
+      "--initial_ifuel", "2",
+      "--warn_error", "-271",
+      "--z3cliopt", "timeout=600000",
+      "--z3cliopt", "smt.arith.nl=false",
+      "--smtencoding.elim_box", "true",
+      "--smtencoding.l_arith_repr", "native",
+      "--smtencoding.nl_arith_repr", "wrapped",
+      "--smt", "/home/nswamy/workspace/z3/z3/build/z3",
+      "--z3version", "4.12.3",
+      "--compat_pre_typed_indexed_effects",
+      "--cache_dir", "_output/cache",
+      "--load_cmxs", "steel"
+    ],
+    "include_dirs": [
+      "_output",
+      "utils",
+      "generic",
+      "high",
+      "intermediate",
+      "steel",
+      "steel/crypto",
+      "${KRML_HOME}/krmllib",
+      "${KRML_HOME}/krmllib/obj",
+      "../steel/lib/steel"
+    ]
+  }
+

steel/Zeta.Steel.HashAccumulator.fst

@@ -283,7 +283,7 @@ let aggregate_raw_hashes
             (inv 0);
     Loops.for_loop 0sz hash_len_sz inv body;
     assert (xor_bytes_pfx s1 s2 hash_len `Seq.equal` xor_bytes s1 s2);
-    rewrite (inv hash_len)
+    rewrite (inv (FStar.SizeT.v hash_len_sz))
             (A.pts_to b1 _ _ `star` A.pts_to b2 _ _);
     return ()
 

steel/Zeta.Steel.ThreadStateModel.fst

@@ -759,7 +759,7 @@ let rec read_slots (tsm:thread_state_model)
                      | DValue None -> A.Null
                      | DValue (Some d) -> A.DValue d
                  in
-                 Some (Seq.Properties.cons (k, d) tl)
+                 Some (Seq.cons (k, d) tl)
                | _ ->
                  None
     )