***NO_CI*** syncing with latest hs changes

hacl-star · Dec 26, 2017 · f83c498 · f83c498
1 parent f02bf26
commit f83c498
Show file tree

Hide file tree

Showing 3 changed files with 95 additions and 88 deletions.
diff --git a/secure_api/aead/Crypto.AEAD.Encrypt.fst b/secure_api/aead/Crypto.AEAD.Encrypt.fst
@@ -244,7 +244,6 @@ let reestablish_inv i st n #aadlen aad #plainlen plain cipher_tag ak acc h0 h1 h
   lemma_propagate_inv_enxor st n aad plain cipher_tag h0 h1;
   FStar.Buffer.lemma_intro_modifies_0 h1 h2;
   lemma_propagate_inv_accumulate false st n aad plain cipher_tag h1 h2;
-  assume (h2.HS.tip == h3.HS.tip);
   lemma_propagate_inv_mac_wrapper st n aad plain cipher_tag ak acc h2 h3;
   reestablish_inv st n aad plain cipher_tag h3 h4 //needs some optimization
 #reset-options