diff --git a/SAW/proof/AES/AES-GCM.saw b/SAW/proof/AES/AES-GCM.saw
index 2f20533c..ceb1d4d4 100644
--- a/SAW/proof/AES/AES-GCM.saw
+++ b/SAW/proof/AES/AES-GCM.saw
@@ -307,27 +307,28 @@ llvm_verify m "EVP_EncryptUpdate"
   , aesni_gcm_decrypt_array_ov
   ]
   true
-  (EVP_CipherUpdate_array_spec {{ 1 : [32] }} 15 1)
+  (EVP_CipherUpdate_array_spec {{ 1 : [32] }} 1 15)
   (do {
     simplify (cryptol_ss ());
-    //goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "aes_gcm_encrypt_update_bytes"];
     goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod"];
     simplify (addsimps [aesni_gcm_encrypt_Yi_thm] empty_ss);
     goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod"];
     simplify (addsimps [bvand_bvudiv_thm, bvudiv_bvmul_bvudiv_thm, bvurem_16_append_thm] basic_ss);
-    simplify (addsimps [arrayLookupUnint_thm, arrayUpdateUnint_thm, arrayCopyUnint_thm] empty_ss);
+    simplify (addsimps [arrayLookupUnint_thm, arrayUpdateUnint_thm, arrayCopyUnint_thm, arrayConstantUnint_thm] empty_ss);
     simplify (addsimps add_xor_slice_thms basic_ss);
-    goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
-    goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
-    goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
-    //hoist_ifs_in_goal;
-    //goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
-    //goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
-    //w4_unint_z3 ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "aes_gcm_encrypt_update_bytes", "arrayCopyUnint"];
+    goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    simplify (addsimps [ite_bveq_0_thm, ite_bveq_1_thm, bveq_ite_bv8_0_thm, bveq_ite_bv8_1_thm, arrayeq_ite_0_thm, arrayeq_ite_1_thm, foo_thm, bar_thm] basic_ss);
+    goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
     print_goal;
-    w4_unint_z3 ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
-    //offline_w4_unint_z3 ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"] "lala";
-    //w4_unint_yices ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
+    is_out_post <- goal_has_some_tag ["output buffer postcondition"];
+    is_Xi_post <- goal_has_some_tag ["Xi postcondition"];
+    if is_out_post then do {
+      w4_unint_yices ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    } else if is_Xi_post then do {
+      w4_unint_z3_using "qfufbv" ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    } else do {
+      w4_unint_z3 ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    };
   });
 
 llvm_verify m "EVP_DecryptUpdate"
@@ -340,26 +341,28 @@ llvm_verify m "EVP_DecryptUpdate"
   , aesni_gcm_decrypt_array_ov
   ]
   true
-  (EVP_CipherUpdate_array_spec {{ 0 : [32] }} 15 1)
+  (EVP_CipherUpdate_array_spec {{ 0 : [32] }} 1 15)
   (do {
     simplify (cryptol_ss ());
-    //goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "aes_gcm_decrypt_update_bytes"];
     goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod"];
     simplify (addsimps [aesni_gcm_decrypt_Yi_thm] empty_ss);
     goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod"];
     simplify (addsimps [bvand_bvudiv_thm, bvudiv_bvmul_bvudiv_thm, bvurem_16_append_thm] basic_ss);
-    simplify (addsimps [arrayLookupUnint_thm, arrayUpdateUnint_thm, arrayCopyUnint_thm] empty_ss);
+    simplify (addsimps [arrayLookupUnint_thm, arrayUpdateUnint_thm, arrayCopyUnint_thm, arrayConstantUnint_thm] empty_ss);
     simplify (addsimps add_xor_slice_thms basic_ss);
-    goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
-    goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
-    goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
-    //hoist_ifs_in_goal;
-    //goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
-    //goal_eval_unint ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
-    //w4_unint_z3 ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "aes_gcm_encrypt_update_bytes", "arrayCopyUnint"];
-    w4_unint_z3 ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint"];
-    //offline_w4_unint_z3 ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"] "lala";
-    //w4_unint_yices ["aesni_gcm_encrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayCopyUnint"];
+    goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    simplify (addsimps [ite_bveq_0_thm, ite_bveq_1_thm, bveq_ite_bv8_0_thm, bveq_ite_bv8_1_thm, arrayeq_ite_0_thm, arrayeq_ite_1_thm, foo_thm, bar_thm] basic_ss);
+    goal_eval_unint ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    print_goal;
+    is_out_post <- goal_has_some_tag ["output buffer postcondition"];
+    is_Xi_post <- goal_has_some_tag ["Xi postcondition"];
+    if is_out_post then do {
+      w4_unint_yices ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    } else if is_Xi_post then do {
+      w4_unint_z3_using "qfufbv" ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    } else do {
+      w4_unint_z3 ["aesni_gcm_decrypt", "aes_ctr32_encrypt_blocks_array", "aes_hw_encrypt", "gcm_ghash_blocks_array", "gcm_polyval", "pmult", "pmod", "arrayLookupUnint", "arrayUpdateUnint", "arrayCopyUnint", "arrayConstantUnint"];
+    };
   });
 
 disable_what4_eval;
diff --git a/SAW/proof/AES/evp-function-specs.saw b/SAW/proof/AES/evp-function-specs.saw
index 2b70ef04..65639b75 100644
--- a/SAW/proof/AES/evp-function-specs.saw
+++ b/SAW/proof/AES/evp-function-specs.saw
@@ -74,36 +74,6 @@ let EVP_CipherUpdate_spec enc gcm_len len = do {
   crucible_return (crucible_term {{ 1 : [32] }});
 };
 
-let EVP_EncryptFinal_ex_spec gcm_len = do {
-  cipher_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_cipher_st");
-  points_to_evp_cipher_st cipher_ptr;
-
-  cipher_data_ptr <- crucible_alloc_aligned 16 (llvm_struct "struct.EVP_AES_GCM_CTX");
-  ctx <- fresh_aes_gcm_ctx gcm_len;
-  let mres = eval_size {| gcm_len % AES_BLOCK_SIZE |};
-  points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx mres {{ 1 : [32] }} 0xffffffff;
-
-  ctx_ptr <- crucible_alloc (llvm_struct "struct.evp_cipher_ctx_st");
-  points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr {{ 1 : [32]}};
-
-  out_ptr <- crucible_fresh_pointer (llvm_array AES_BLOCK_SIZE (llvm_int 8));
-  out_len_ptr <- crucible_alloc (llvm_int 32);
-
-  crucible_execute_func [ctx_ptr, out_ptr, out_len_ptr];
-
-  Xi' <- crucible_fresh_var "Xi" (llvm_array AES_BLOCK_SIZE (llvm_int 8));
-  let ctx' = {{ { key = ctx.key, iv = ctx.iv, Xi = Xi', len = ctx.len } : AES_GCM_Ctx }};
-  points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx' mres {{ 0 : [32] }} AES_BLOCK_SIZE;
-
-  points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr {{ 1 : [32]}};
-
-  crucible_points_to_untyped (crucible_field ctx_ptr "buf") (crucible_term {{ cipher_final ctx }});
-
-  crucible_points_to out_len_ptr (crucible_term {{ 0 : [32] }});
-
-  crucible_return (crucible_term {{ 1 : [32] }});
-};
-
 let EVP_CipherUpdate_array_spec enc mres res_mres = do {
   global_alloc_init "OPENSSL_ia32cap_P" {{ ia32cap }};
 
@@ -138,16 +108,49 @@ let EVP_CipherUpdate_array_spec enc mres res_mres = do {
     aes_gcm_decrypt_update ctx in_ (sext len) out
   }};
 
-  //points_to_EVP_AES_GCM_CTX'' cipher_data_ptr {{ res.0 }}  {{ 1 : [32] }} 0xffffffff;
-  points_to_EVP_AES_GCM_CTX cipher_data_ptr {{ res.0 }} res_mres {{ 1 : [32] }} 0xffffffff;
+  llvm_setup_with_tag "Xi postcondition" do {
+    points_to_EVP_AES_GCM_CTX cipher_data_ptr {{ res.0 }} res_mres {{ 1 : [32] }} 0xffffffff;
+  };
 
-  llvm_points_to_array_prefix out_ptr {{ res.1 }} {{ sext len : [64] }};
+  llvm_setup_with_tag "output buffer postcondition" do {
+    llvm_points_to_array_prefix out_ptr {{ res.1 }} {{ sext len : [64] }};
+  };
 
   crucible_points_to out_len_ptr (crucible_term len);
 
   crucible_return (crucible_term {{ 1 : [32] }});
 };
 
+let EVP_EncryptFinal_ex_spec gcm_len = do {
+  cipher_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_cipher_st");
+  points_to_evp_cipher_st cipher_ptr;
+
+  cipher_data_ptr <- crucible_alloc_aligned 16 (llvm_struct "struct.EVP_AES_GCM_CTX");
+  ctx <- fresh_aes_gcm_ctx gcm_len;
+  let mres = eval_size {| gcm_len % AES_BLOCK_SIZE |};
+  points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx mres {{ 1 : [32] }} 0xffffffff;
+
+  ctx_ptr <- crucible_alloc (llvm_struct "struct.evp_cipher_ctx_st");
+  points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr {{ 1 : [32]}};
+
+  out_ptr <- crucible_fresh_pointer (llvm_array AES_BLOCK_SIZE (llvm_int 8));
+  out_len_ptr <- crucible_alloc (llvm_int 32);
+
+  crucible_execute_func [ctx_ptr, out_ptr, out_len_ptr];
+
+  Xi' <- crucible_fresh_var "Xi" (llvm_array AES_BLOCK_SIZE (llvm_int 8));
+  let ctx' = {{ { key = ctx.key, iv = ctx.iv, Xi = Xi', len = ctx.len } : AES_GCM_Ctx }};
+  points_to_EVP_AES_GCM_CTX cipher_data_ptr ctx' mres {{ 0 : [32] }} AES_BLOCK_SIZE;
+
+  points_to_evp_cipher_ctx_st ctx_ptr cipher_ptr cipher_data_ptr {{ 1 : [32]}};
+
+  crucible_points_to_untyped (crucible_field ctx_ptr "buf") (crucible_term {{ cipher_final ctx }});
+
+  crucible_points_to out_len_ptr (crucible_term {{ 0 : [32] }});
+
+  crucible_return (crucible_term {{ 1 : [32] }});
+};
+
 let EVP_DecryptFinal_ex_spec gcm_len = do {
   cipher_ptr <- crucible_alloc_readonly (llvm_struct "struct.evp_cipher_st");
   points_to_evp_cipher_st cipher_ptr;
diff --git a/SAW/proof/AES/goal-rewrites.saw b/SAW/proof/AES/goal-rewrites.saw
index 180c89a1..908a6e2b 100644
--- a/SAW/proof/AES/goal-rewrites.saw
+++ b/SAW/proof/AES/goal-rewrites.saw
@@ -755,6 +755,8 @@ let {{
   arrayUpdateUnint = arrayUpdate
   arrayCopyUnint : Array[64][8] -> [64] -> Array[64][8] -> [64] -> [64] -> Array[64][8]
   arrayCopyUnint = arrayCopy
+  arrayConstantUnint : [8] -> Array[64][8]
+  arrayConstantUnint = arrayConstant
 }};
 arrayLookupUnint_thm <- prove_theorem
   (w4_unint_z3 [])
@@ -765,6 +767,9 @@ arrayUpdateUnint_thm <- prove_theorem
 arrayCopyUnint_thm <- prove_theorem
   (w4_unint_z3 [])
   (rewrite (cryptol_ss ()) {{ \a i b j n -> arrayEq (arrayCopy a i b j n) (arrayCopyUnint a i b j n) }});
+arrayConstantUnint_thm <- prove_theorem
+  (w4_unint_z3 [])
+  (rewrite (cryptol_ss ()) {{ \x -> arrayEq (arrayConstant x) (arrayConstantUnint x) }});
 
 let aesni_gcm_encrypt_Yi_stmt = rewrite (cryptol_ss ()) {{ \len in out key iv ctr Xi i out' Xi' ->
   (aesni_gcm_encrypt len in out key iv ctr Xi i out' Xi').2
@@ -797,6 +802,24 @@ aesni_gcm_decrypt_Yi_thm <- prove_theorem
 bvand_bvudiv_thm <- prove_folding_theorem {{ \x -> 0xfffffffffffffff0 && x == 16 * (x / 16) }};
 bvudiv_bvmul_bvudiv_thm <- prove_folding_theorem {{ \(x : [64]) -> (16 * (x / 16)) / 16 == x / 16 }};
 bvurem_16_append_thm <- prove_folding_theorem {{ \(x : [60]) (y : [4]) -> (x # y) % 16 == 0 # y }};
+ite_bveq_0_thm <- prove_folding_theorem (normalize_term {{ \(x : [64]) y -> (if x == y then x else y) == y }});
+ite_bveq_1_thm <- prove_folding_theorem (normalize_term {{ \(x : [64]) y -> (if x == y then y else x) == x }});
+bveq_ite_bv8_0_thm <- prove_folding_theorem (normalize_term {{ \b (x : [8]) y z -> ((if b then x else y) == (if b then x else z)) == if b then True else y == z }});
+bveq_ite_bv8_1_thm <- prove_folding_theorem (normalize_term {{ \b (x : [8]) y z -> ((if b then y else x) == (if b then z else x)) == if b then y == z else True }});
+arrayeq_ite_0_thm <- prove_folding_theorem {{ \b (x : Array[64][8]) y z -> arrayEq (if b then x else y) (if b then x else z) == if b then True else arrayEq y z }};
+arrayeq_ite_1_thm <- prove_folding_theorem {{ \b (x : Array[64][8]) y z -> arrayEq (if b then y else x) (if b then z else x) == if b then arrayEq y z else True }};
+foo_thm <- prove_folding_theorem {{ \(x : [64]) b c -> (
+  (x_55 + x_70) + c == 16 * (x / 16) + c
+  where
+    x_55 = (if b then 0 else 96 * (x / 96))
+    x_70 = 16 * ((x + (-1) * x_55) / 16)
+)}};
+bar_thm <- prove_folding_theorem {{ \(x : [64]) b c -> (
+  (c + x_149) + x_147 == 16 * (x / 16) + c
+  where
+    x_147 = (if b then 0 else 96 * (x / 96))
+    x_149 = 16 * ((x + (-1) * x_147) / 16)
+)}};
 
 
 /*
diff --git a/SAW/spec/AES/AES-GCM-unbounded.cry b/SAW/spec/AES/AES-GCM-unbounded.cry
index 34870be4..8f588cc4 100644
--- a/SAW/spec/AES/AES-GCM-unbounded.cry
+++ b/SAW/spec/AES/AES-GCM-unbounded.cry
@@ -429,7 +429,7 @@ gcm_ghash_blocks_array H blocks len i Xi =
 
 aes_gcm_encrypt_update : AES_GCM_Ctx -> Array[64][8] -> [64] -> Array[64][8] -> (AES_GCM_Ctx, Array[64][8])
 aes_gcm_encrypt_update ctx in len out =
-  if ctx.len % 16 != 0 /\ (ctx.len % 16) + len < 16
+  if ctx.len % 16 != 0 /\ (ctx.len % 16) + (0 # drop`{60} len) < 16 /\ len - (0 # drop`{60} len) == 0
     then (res_ctx', res_out')
     else (res_ctx, res_out)
   where
@@ -507,7 +507,7 @@ aes_gcm_encrypt_update_bytes eki in offset n j (out, Xi) =
 
 aes_gcm_decrypt_update : AES_GCM_Ctx -> Array[64][8] -> [64] -> Array[64][8] -> (AES_GCM_Ctx, Array[64][8])
 aes_gcm_decrypt_update ctx in len out =
-  if ctx.len % 16 != 0 /\ (ctx.len % 16) + len < 16
+  if ctx.len % 16 != 0 /\ (ctx.len % 16) + (0 # drop`{60} len) < 16 /\ len - (0 # drop`{60} len) == 0
     then (res_ctx', res_out')
     else (res_ctx, res_out)
   where