From 7dc2f99d6f5a70eb0c7b52021cf460b8dc0c7b21 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 5 Feb 2025 00:28:19 -0800
Subject: [PATCH] Handle fallible allocation (abort if OOM)

---
 src/MerkleTree.EverCrypt.fst | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/MerkleTree.EverCrypt.fst b/src/MerkleTree.EverCrypt.fst
index 493e925..a4f0129 100644
--- a/src/MerkleTree.EverCrypt.fst
+++ b/src/MerkleTree.EverCrypt.fst
@@ -39,7 +39,11 @@ let mt_sha256_compress src1 src2 dst =
   B.blit src2 0ul cb 32ul hash_size;
 
   // ONLY WORKS BECAUSE hash_alg is inline_for_extraction and is known to be SHA2_256
-  let st = EHS.create_in hash_alg HyperStack.root in
+  let st =
+    match EHS.create_in hash_alg HyperStack.root with
+    | Some st -> st
+    | None -> LowStar.Failure.failwith "out of memory"
+  in
   EHS.init #(Ghost.hide hash_alg) st;
   let hh1 = HST.get () in
   assert (S.equal (S.append