Update HMAC proofs for PR aws/aws-lc#1574 (#157)

* Update HMAC proofs for PR aws/aws-lc#1574

HMAC precomputed keys PR aws/aws-lc#1574 adds fields to
`hmac_methods_st`, which made the original proof failed.

This commit updates the proof.

This is a breaking change: the updated proof only works
after PR aws/aws-lc#1574 is merged.

* Fix .gitmodules src to point to github.com/fabrice102/aws-lc

---------

Co-authored-by: Fabrice Benhamouda <[email protected]>

.gitmodules

@@ -1,7 +1,7 @@
 [submodule "src"]
 	path = src
-	branch = main
-	url = https://github.com/aws/aws-lc.git
+	branch = hmac-precompute
+	url = https://github.com/fabrice102/aws-lc.git
 [submodule "cryptol-specs"]
 	path = cryptol-specs
 	branch = sha-imperative

SAW/proof/HMAC/HMAC-common.saw

@@ -72,10 +72,17 @@ let points_to_md_methods md ptr md_ptr = do {
 
   crucible_points_to (crucible_elem ptr 0) md_ptr;
 
+  // Field element 1 is chaining_length. 
+  // Ignoring it, since it is only used when computing HMAC with precomputed keys
+  // (which is not formally verified).
+
   if md then do {
-    crucible_points_to (crucible_elem ptr 1) (crucible_global HMAC_MD_INIT);
-    crucible_points_to (crucible_elem ptr 2) (crucible_global HMAC_MD_UPDATE);
-    crucible_points_to (crucible_elem ptr 3) (crucible_global HMAC_MD_FINAL);
+    crucible_points_to (crucible_elem ptr 2) (crucible_global HMAC_MD_INIT);
+    crucible_points_to (crucible_elem ptr 3) (crucible_global HMAC_MD_UPDATE);
+    crucible_points_to (crucible_elem ptr 4) (crucible_global HMAC_MD_FINAL);
+    // Field elements 5 & 6 are ..._Init_from_state and ..._get_state.
+    // Ignoring them, since they are only used when computing HMAC with precomputed keys
+    // (which is not formally verified).
   } else do {
     return ();
   };