From 2f4a6c2df55c07c67c73b34bf0d33266725b16d8 Mon Sep 17 00:00:00 2001
From: k32 <10274441+k32@users.noreply.github.com>
Date: Sun, 15 Feb 2026 16:32:39 +0100
Subject: [PATCH 1/2] Add an instance for FMapAVL

---
 README.org                       |  3 +-
 _CoqProject                      |  1 +
 theories/Storage/Classes.v       |  6 +-
 theories/Storage/Instances/AVL.v | 99 ++++++++++++++++++++++++++++++++
 4 files changed, 105 insertions(+), 4 deletions(-)
 create mode 100644 theories/Storage/Instances/AVL.v

diff --git a/README.org b/README.org
index 114e484..3aa9b0e 100644
--- a/README.org
+++ b/README.org
@@ -14,4 +14,5 @@ This repository contains:
 - Some theorems related to Wlog equivalence
 
 Instances:
-- =LibTx.Storage.Instances.List=
+- =LibTx.Storage.Instances.List=: pure storage instance based on flat lists
+- =LibTx.Storage.Instances.AVL=: pure storage instance based on AVL-tree (wrapper over =FMapAVL= from the standard library)
diff --git a/_CoqProject b/_CoqProject
index b317f4b..d82e56f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,3 +4,4 @@ theories/Storage/Tactics.v
 theories/Storage/Properties.v
 theories/Storage.v
 theories/Storage/Instances/List.v
+theories/Storage/Instances/AVL.v
diff --git a/theories/Storage/Classes.v b/theories/Storage/Classes.v
index 05485f4..ca0595d 100644
--- a/theories/Storage/Classes.v
+++ b/theories/Storage/Classes.v
@@ -1,7 +1,7 @@
 From Coq Require Import
-     List
-     Classes.EquivDec
-     Classes.SetoidClass.
+  List
+  Classes.EquivDec
+  Classes.SetoidClass.
 
 Section defns.
   Context {K V : Type}.
diff --git a/theories/Storage/Instances/AVL.v b/theories/Storage/Instances/AVL.v
new file mode 100644
index 0000000..22bb6a1
--- /dev/null
+++ b/theories/Storage/Instances/AVL.v
@@ -0,0 +1,99 @@
+From Coq Require Import
+  FMapInterface
+  FMapAVL
+  OrderedType
+  OrderedTypeEx
+  ZArith.
+
+Require Import Classes.
+
+Module Type Make (E : OrderedType).
+  Include FMapAVL.Make E.
+
+  Parameter dec_eq_is_eq : forall a b, E.eq a b <-> a = b.
+
+  Lemma fmap_new_empty {ValT : Type} k : find k (@empty ValT) = None.
+  Proof.
+    remember (find k (empty ValT)) as maybe_v.
+    destruct maybe_v as [v|].
+    - exfalso.
+      specialize (@empty_1 ValT k v) as H.
+      symmetry in Heqmaybe_v. now apply find_2 in Heqmaybe_v.
+    - reflexivity.
+  Qed.
+
+  Lemma fmap_keep {ValT : Type} s k (v : ValT) : find k (add k v s) = Some v.
+  Proof.
+    specialize (@add_1 ValT s k k v (E.eq_refl k)) as H.
+    now apply find_1.
+  Qed.
+
+  Lemma fmap_distinct {ValT : Type} s k1 k2 (v2 : ValT) :
+    k1 <> k2 ->
+    find k1 s = find k1 (add k2 v2 s).
+  Proof.
+    intros Hk.
+    assert (Hk' : ~E.eq k2 k1). {
+      intros Habsurd.
+      apply not_eq_sym in Hk.
+      now apply dec_eq_is_eq in Habsurd.
+    }
+    apply Raw.Proofs.find_find.
+    intros v. split.
+    - intros H.
+      apply find_1.
+      apply find_2 in H.
+      now apply add_2.
+    - intros H.
+      apply find_1.
+      apply find_2 in H.
+      eapply add_3; eauto.
+  Qed.
+
+  Lemma fmap_delete_keep {ValT : Type} s k:
+      @find ValT k (remove k s) = None.
+  Proof.
+    specialize (@remove_1 ValT s k k (E.eq_refl k)) as H.
+    remember (remove (elt:=ValT) k s) as s'.
+    unfold find, remove, In in H.
+    destruct s' as [s' bst'].
+    apply Raw.Proofs.not_find_iff.
+    - assumption.
+    - now rewrite Raw.Proofs.In_alt in H.
+  Qed.
+
+  Lemma fmap_delete_distinct {ValT : Type} (s : t ValT) k1 k2 :
+    k1 <> k2 ->
+    find k1 s = find k1 (remove k2 s).
+  Proof.
+    intros Hk.
+    assert (Hk' : ~E.eq k2 k1). {
+      intros Habsurd.
+      apply not_eq_sym in Hk.
+      now apply dec_eq_is_eq in Habsurd.
+    }
+    apply Raw.Proofs.find_find.
+    intros v1. split.
+    - intros H.
+      apply find_1.
+      apply find_2 in H.
+      now apply remove_2.
+    - intros H.
+      apply find_1.
+      apply find_2 in H.
+      eapply remove_3; eauto.
+  Qed.
+
+  Global Instance fmapStorage {Val : Type} : @Storage E.t Val (t Val) :=
+    {|
+      new := @empty Val;
+      get := @find Val;
+      put := @add Val;
+      delete := @remove Val;
+      new_empty := @fmap_new_empty Val;
+      keep := @fmap_keep Val;
+      distinct := @fmap_distinct Val;
+      delete_keep := @fmap_delete_keep Val;
+      delete_distinct := @fmap_delete_distinct Val;
+    |}.
+End Make.

From 38f535b78eefa94001e42192a3d66b15b5dba16b Mon Sep 17 00:00:00 2001
From: k32 <10274441+k32@users.noreply.github.com>
Date: Sun, 15 Feb 2026 16:43:50 +0100
Subject: [PATCH 2/2] Remove unused coq-record-update dependency

---
 Makefile               | 2 +-
 coq-libtx-storage.opam | 8 +++-----
 2 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/Makefile b/Makefile
index 66fde74..8be83d7 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@ CoqMakefile: Makefile _CoqProject
 invoke-coqmakefile: CoqMakefile
 	$(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS))
 
-.PHONY: invoke-coqmakefile record-update $(KNOWNFILES)
+.PHONY: invoke-coqmakefile $(KNOWNFILES)
 
 ####################################################################
 ##                      Your targets here                         ##
diff --git a/coq-libtx-storage.opam b/coq-libtx-storage.opam
index 988888b..28f02f1 100644
--- a/coq-libtx-storage.opam
+++ b/coq-libtx-storage.opam
@@ -5,7 +5,7 @@ homepage: "https://github.com/libtx/Storage"
 dev-repo: "git+https://github.com/libtx/Storage.git"
 license: "GPL3"
 maintainer: "noreply@example.com"
-synopsis: "Formal model of storage backend"
+synopsis: "Axiomatic abstraction of storage container"
 description: """
 """
 
@@ -14,14 +14,12 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.19") | (= "dev")}
-  "coq-record-update" {(>= "0.3" & < "0.4~")}
+  "coq" {(>= "8.19")}
   "coq-hammer"
 ]
 
 tags: [
-  "keyword:program verification"
-  "keyword:distributed algorithms"
+  "keyword:containers"
 ]
 authors: [
   "k32"