From ed74b086181a8740ff1951f8904002da6833c14a Mon Sep 17 00:00:00 2001
From: berpeti <peti.ber007@gmail.com>
Date: Fri, 15 May 2026 15:29:34 +0200
Subject: [PATCH 1/2] Add map primitives

---
 src/Auxiliaries.v                      | 127 ++++++++++++++++++++++-
 src/Concurrent/NodeSemanticsLemmas.v   |  37 ++++++-
 src/Concurrent/PIDRenaming.v           |  45 +++++++++
 src/FrameStack/Compatibility.v         | 134 +++++++++++++++++++++++++
 src/Interpreter/InterpreterAux.v       |  43 ++++++++
 src/Interpreter/InterpreterAuxLemmas.v |  21 +++-
 src/Maps.v                             |  33 +++++-
 src/Syntax.v                           |   4 +
 8 files changed, 430 insertions(+), 14 deletions(-)

diff --git a/src/Auxiliaries.v b/src/Auxiliaries.v
index 4edf70ea..1529d796 100644
--- a/src/Auxiliaries.v
+++ b/src/Auxiliaries.v
@@ -15,7 +15,10 @@
   - Concurrent/NodeSemanticsLemmas.v
 *)
 
-From CoreErlang Require Export SideEffects ScopingLemmas Equalities.
+From CoreErlang Require Export SideEffects
+                               ScopingLemmas
+                               Equalities
+                               Maps.
 Require Export Stdlib.Sorting.Permutation.
 From Stdlib Require Export Ascii.
 From Stdlib Require Export Numbers.DecimalString Decimal.
@@ -53,6 +56,8 @@ Inductive BIFCode :=
 | BSend | BSpawn | BSpawnLink | BProcessFlag | BSelf | BLink | BUnLink
 | BNothing
 | BFunInfo
+(* map primitives *)
+| BGet | BPut
 .
 
 (**
@@ -126,6 +131,9 @@ match s with
 | ("erlang"%string, "unlink"%string) => BUnLink
 (** lists *)
 | ("lists"%string, "split"%string) => BSplit
+(** maps *)
+| ("maps"%string, "get"%string) => BGet
+| ("maps"%string, "put"%string) => BPut
 (** anything else *)
 | _ => BNothing
 end.
@@ -575,6 +583,42 @@ match convert_string_to_code (mname, fname) with
 | _                              => Some (undef (VLit (Atom fname)))
 end.
 
+Definition eval_map_bifs (mname fname : string)
+                         (params : list Val) : Redex :=
+match convert_string_to_code (mname, fname) with
+| BPut => match params with
+          | key :: value :: map :: [] =>
+            match map with
+            | VMap contents => RValSeq [VMap (map_put key value contents)]
+            | _ => RExc (badmap (VTuple [VLit "put"%string;key;value;map]))
+            end
+          | _ => RExc (undef (VLit (Atom fname)))
+          end
+| BGet => match params with
+          | key :: map :: [] =>
+            match map with
+            | VMap contents =>
+              match map_get key contents with
+              | Some v => RValSeq [v]
+              | None   => RExc (badkey key)
+              end
+            | _ => RExc (badmap map)
+            end
+          | key :: map :: default :: [] =>
+            match map with
+            | VMap contents =>
+              match map_get key contents with
+              | Some v => RValSeq [v]
+              | None   => RValSeq [default]
+              end
+            | _ => RExc (badmap map)
+            end
+          | _ => RExc (undef (VLit (Atom fname)))
+          end
+| _ => RExc (undef (VLit (Atom fname)))
+end.
+
+
 (* Note: Always can be extended, this function simulates inter-module calls *)
 (**
   This function defines the simulated semantics of BIFs and standard functions.
@@ -601,8 +645,11 @@ match convert_string_to_code (mname, fname) with
                                                       | None => None
                                                      end
 | BFunInfo                                        => Some (eval_funinfo params, None)
+| BGet | BPut => Some (eval_map_bifs mname fname params, None)
+
 (** undefined functions *)
 | BNothing                                        => Some (RExc (undef (VLit (Atom fname))), None)
+
 (* concurrent BIFs *)
 | BSend | BSpawn | BSpawnLink | BSelf | BProcessFlag
 | BLink | BUnLink                                 => match eval_concurrent mname fname params with
@@ -746,7 +793,7 @@ Proof.
   intros. unfold eval in *.
   break_match_hyp; unfold eval_arith, eval_logical, eval_equality,
   eval_transform_list, eval_list_tuple, eval_convert, eval_cmp, eval_io,
-  eval_hd_tl, eval_elem_tuple, eval_check, eval_error, eval_concurrent in *; try rewrite Heqb in *; try invSome.
+  eval_hd_tl, eval_elem_tuple, eval_check, eval_error, eval_concurrent, eval_map_bifs in *; try rewrite Heqb in *; try invSome.
   all: repeat break_match_goal; try invSome; subst.
   all: try (constructor; eexists; reflexivity).
   1-2: repeat break_match_hyp; auto; try invSome.
@@ -795,6 +842,42 @@ Proof.
     all: now constructor.
 Qed.
 
+Lemma map_insert_is_closed (v v0 : Val)
+(l2 : list (Val * Val)) :
+  VALCLOSED v -> VALCLOSED v0 ->
+  (forall i : nat,
+  i < Datatypes.length l2 -> VALCLOSED (nth i (map fst l2) VNil)) ->
+  (forall i : nat,
+  i < Datatypes.length l2 -> VALCLOSED (nth i (map snd l2) VNil))
+  ->
+VALCLOSED (VMap (map_put v v0 l2)).
+Proof.
+  intros. induction l2; simpl.
+  * constructor; simpl; destruct i; try lia; now intros.
+  * destruct a as [k' v']. simpl in *.
+    break_match_goal. 2: break_match_goal.
+    - constructor; intros.
+      all: destruct i; [|destruct i]; simpl; try assumption.
+      1: apply (H1 0); lia.
+      1: apply (H1 (S i)); simpl in H3; lia.
+      1: apply (H2 0); lia.
+      1: apply (H2 (S i)); simpl in H3; lia.
+    - constructor; intros.
+      all: destruct i; simpl; try assumption.
+      1: apply (H1 (S i)); simpl in H3; lia.
+      1: apply (H2 (S i)); simpl in H3; lia.
+    - unshelve (epose proof (IHl2 _ _)).
+      1: intros. apply (H1 (S i)); simpl in H3; lia.
+      1: intros. apply (H2 (S i)); simpl in H3; lia.
+      inv H3.
+      constructor; intros.
+      all: destruct i; simpl; try assumption.
+      1: apply (H1 0); lia.
+      2: apply (H2 0); lia.
+      1: apply H5; simpl in H3; lia.
+      1: apply H7; simpl in H3; lia.
+Qed.
+
 
 Lemma eval_is_closed_result :
   forall f m vl r eff,
@@ -805,7 +888,7 @@ Proof.
   intros. unfold eval in *.
   break_match_hyp; unfold eval_arith, eval_logical, eval_equality,
   eval_transform_list, eval_list_tuple, eval_convert, eval_cmp, eval_io,
-  eval_hd_tl, eval_elem_tuple, eval_check, eval_error, eval_concurrent in *; try rewrite Heqb in *; try invSome.
+  eval_hd_tl, eval_elem_tuple, eval_check, eval_error, eval_concurrent, eval_map_bifs in *; try rewrite Heqb in *; try invSome.
   all: repeat break_match_goal; try invSome; subst.
   all: try now constructor; auto.
   all: destruct_foralls; destruct_redex_scopes.
@@ -912,6 +995,23 @@ Proof.
   * repeat break_match_hyp; repeat invSome; unfold undef; auto.
   * unfold eval_funinfo. repeat break_match_goal; unfold undef; auto.
     all: do 2 constructor; apply indexed_to_forall; subst; destruct_foralls; auto.
+  * clear - Heqo H4. induction l1; simpl in Heqo.
+    invSome.
+    destruct a as [k' v'].
+    break_match_hyp.
+    - apply IHl1 in Heqo. assumption.
+      intros. apply (H4 (S i)). slia.
+    - break_match_hyp; invSome.
+      apply (H4 0). slia.
+  * clear - Heqo H5. induction l2; simpl in Heqo.
+    invSome.
+    destruct a as [k' v'].
+    break_match_hyp.
+    - apply IHl2 in Heqo. assumption.
+      intros. apply (H5 (S i)). slia.
+    - break_match_hyp; invSome.
+      apply (H5 0). slia.
+  * now apply map_insert_is_closed.
 Qed.
 
 Corollary closed_primop_eval : forall f vl r eff',
@@ -1348,4 +1448,25 @@ Proof. reflexivity. Qed.
 Goal eval "erlang" "fun_info" [VClos [] 0 2 (˝VNil); VLit "arity"%string] = Some (RValSeq [VLit 2%Z], None).
 Proof. reflexivity. Qed.
 
+Goal eval "maps" "get" [VNil; VMap [(VNil, VNil)]] = Some (RValSeq [VNil], None).
+Proof. reflexivity. Qed.
+Goal eval "maps" "get" [VLit 2%Z; VMap [(VLit 1%Z, VLit 1%Z);(VLit 2%Z, VLit 2%Z);(VLit 3%Z, VLit 3%Z)]] = Some (RValSeq [VLit 2%Z], None).
+Proof. reflexivity. Qed.
+Goal eval "maps" "get" [VNil; VMap [(VLit 1%Z, VNil)]] = Some (RExc (badkey VNil), None).
+Proof. reflexivity. Qed.
+Goal eval "maps" "get" [VNil; VMap [(VNil, VNil)];VTuple []] = Some (RValSeq [VNil], None).
+Proof. reflexivity. Qed.
+Goal eval "maps" "get" [VLit 2%Z; VMap [(VLit 1%Z, VLit 1%Z);(VLit 2%Z, VLit 2%Z);(VLit 3%Z, VLit 3%Z)];VTuple []] = Some (RValSeq [VLit 2%Z], None).
+Proof. reflexivity. Qed.
+Goal eval "maps" "get" [VNil; VMap [(VLit 1%Z, VNil)];VTuple []] = Some (RValSeq [VTuple []], None).
+Proof. reflexivity. Qed.
+
+
+Goal eval "maps" "put" [VNil; VNil; VMap [(VNil, VLit 1%Z)]] = Some (RValSeq [VMap [(VNil, VNil)]], None).
+Proof. cbn. reflexivity. Qed.
+Goal eval "maps" "get" [VLit 2%Z; VMap [(VLit 1%Z, VLit 1%Z);(VLit 2%Z, VLit 2%Z);(VLit 3%Z, VLit 3%Z)]] = Some (RValSeq [VLit 2%Z], None).
+Proof. reflexivity. Qed.
+Goal eval "maps" "get" [VNil; VMap [(VLit 1%Z, VNil)]] = Some (RExc (badkey VNil), None).
+Proof. reflexivity. Qed.
+
 End Tests.
diff --git a/src/Concurrent/NodeSemanticsLemmas.v b/src/Concurrent/NodeSemanticsLemmas.v
index a589260d..4aadc8e8 100644
--- a/src/Concurrent/NodeSemanticsLemmas.v
+++ b/src/Concurrent/NodeSemanticsLemmas.v
@@ -2609,7 +2609,7 @@ Proof with try set_solver.
   unfold eval_convert. intros.
   case_match; inv H; simpl.
   1-23: set_solver.
-  3-28: set_solver.
+  3-30: set_solver.
   * case_match.
     1:inv H2; simpl...
     subst. case_match.
@@ -2726,6 +2726,32 @@ Proof with try set_solver.
   intros. unfold eval_funinfo. repeat case_match...
 Qed.
 
+Lemma eval_map_bifs_usedPIDs :
+  forall vl m f,
+    usedPIDsRed (eval_map_bifs m f vl) ⊆ flat_union usedPIDsVal vl.
+Proof with try set_solver.
+  intros. unfold eval_map_bifs.
+  case_match; simpl.
+  1-51: rewrite union_empty_r_L; apply empty_subseteq.
+  all: destruct vl; [|destruct vl; [|destruct vl;[|destruct vl]]]; simpl.
+  all: try by rewrite union_empty_r_L; apply empty_subseteq.
+  1-2: destruct v0. 19: destruct v1.
+  all: cbn; try by rewrite union_empty_r_L; apply empty_subseteq.
+  1-3, 5-8, 10-15, 17-19: set_solver.
+  * clear. induction l; simpl. set_solver.
+    destruct a. destruct Val_ltb.
+    - set_solver.
+    - destruct Val_eqb; simpl; set_solver.
+  * clear. induction l; simpl. set_solver.
+    destruct a. destruct Val_ltb.
+    - set_solver.
+    - destruct Val_eqb; simpl; set_solver.
+  * clear. induction l; simpl. set_solver.
+    destruct a. destruct Val_ltb.
+    - set_solver.
+    - destruct Val_eqb; simpl; set_solver.
+Qed.
+
 Lemma eval_usedPIDs :
   forall vl m f r eff',
     eval m f vl = Some (r, eff') ->
@@ -2748,12 +2774,13 @@ Proof with try assumption; try by auto.
   pose proof eval_error_usedPIDs vl m f.
   pose proof eval_arith_usedPIDs vl m f.
   pose proof eval_funinfo_usedPIDs vl.
+  pose proof eval_map_bifs_usedPIDs vl m f.
   case_match; try invSome...
   all: try case_match; try invSome...
-  * by apply H0 in H18.
-  * by apply H0 in H18.
-  * by apply H5 in H18.
-  * by apply H5 in H18.
+  * by apply H0 in H19.
+  * by apply H0 in H19.
+  * by apply H5 in H19.
+  * by apply H5 in H19.
 Qed.
 
 Lemma primop_eval_usedPIDs :
diff --git a/src/Concurrent/PIDRenaming.v b/src/Concurrent/PIDRenaming.v
index 805a63a2..54b7ea02 100644
--- a/src/Concurrent/PIDRenaming.v
+++ b/src/Concurrent/PIDRenaming.v
@@ -1036,6 +1036,50 @@ Proof.
   all: destruct vs; inv H0; simpl; try reflexivity.
 Qed.
 
+Lemma renamePID_eval_map_bifs :
+  forall m f vs r,
+    eval_map_bifs m f vs = r ->
+    forall from to,
+      eval_map_bifs m f (map (renamePIDVal from to) vs) = renamePIDRed from to r.
+Proof.
+  intros. unfold eval_map_bifs in *.
+  rewrite <- H. clear H.
+  case_match; try reflexivity.
+  all: destruct vs; simpl; try reflexivity.
+  all: destruct vs; simpl; try reflexivity.
+  all: destruct vs; simpl; try reflexivity.
+  2-3: destruct vs; simpl; try reflexivity.
+  * destruct v0; try reflexivity.
+    cbn. by destruct Nat.eqb eqn:P.
+    simpl. induction l; simpl; try reflexivity.
+    destruct a; simpl.
+    repeat rewrite <- renamePID_Val_ltb. simpl.
+    repeat rewrite <- renamePID_Val_eqb_alt.
+    destruct (Val_ltb v0) eqn:P.
+    - assumption.
+    - destruct (Val_eqb v) eqn:P2; reflexivity.
+  * destruct v0; try reflexivity.
+    cbn. by destruct Nat.eqb eqn:P.
+    simpl. induction l; simpl; try reflexivity.
+    destruct a; simpl.
+    repeat rewrite <- renamePID_Val_ltb. simpl.
+    repeat rewrite <- renamePID_Val_eqb_alt.
+    destruct (Val_ltb v0) eqn:P.
+    - assumption.
+    - destruct (Val_eqb v) eqn:P2; reflexivity.
+  * destruct v1; try reflexivity.
+    cbn. by destruct Nat.eqb eqn:P.
+    simpl. repeat f_equal.
+    induction l; simpl; try reflexivity.
+    destruct a; simpl.
+    repeat rewrite <- renamePID_Val_ltb. simpl.
+    repeat rewrite <- renamePID_Val_eqb_alt.
+    destruct (Val_ltb v) eqn:P.
+    - repeat f_equal.
+    - destruct (Val_eqb v) eqn:P2; repeat f_equal.
+      cbn. f_equal. apply IHl.
+Qed.
+
 Proposition renamePID_eval :
   forall m f vs r eff',
     eval m f vs = Some (r, eff') ->
@@ -1066,6 +1110,7 @@ Proof.
   1-7: break_match_hyp; try congruence; destruct e, p;
        eapply renamePID_eval_concurrent in Heqo; rewrite Heqo; inv H1; reflexivity.
   reflexivity.
+  1-2: erewrite renamePID_eval_map_bifs; try eassumption; reflexivity.
 Qed.
 
 Proposition renamePID_primop_eval :
diff --git a/src/FrameStack/Compatibility.v b/src/FrameStack/Compatibility.v
index 96fbeae3..a0c07294 100644
--- a/src/FrameStack/Compatibility.v
+++ b/src/FrameStack/Compatibility.v
@@ -2589,6 +2589,132 @@ Unshelve.
   all: lia.
 Qed.
 
+Lemma Rel_eval_map_bifs m mname f l l':
+  list_biforall (Vrel m) l l' ->
+  (exists vl vl' : list Val,
+   list_biforall (Vrel m) vl vl' /\
+   (eval_map_bifs mname f l) = RValSeq vl /\ (eval_map_bifs mname f l') = RValSeq vl') \/
+  (exists ex ex' : Exception,
+   Excrel m ex ex' /\
+   (eval_map_bifs mname f l) = ex /\ (eval_map_bifs mname f l') = ex').
+Proof.
+  intros. unfold eval_map_bifs.
+  break_match_goal; try solve_complex_Excrel; clear Heqb; inv H; try solve_complex_Excrel.
+  all: inv H1; try solve_complex_Excrel.
+  2: inv H2; try solve_complex_Excrel.
+  {
+    inv H2. 2: inv H3; try solve_complex_Excrel.
+    all: apply Vrel_possibilities in H as H'; intuition; destruct_hyps; subst; try by solve_complex_Excrel.
+    1,2,4,5,6,8: right; do 2 eexists; repeat split; try reflexivity; split; try reflexivity; intros; split; try downclose_Vrel;
+      by choose_compat_lemma.
+    * apply Vrel_Map_compat_rev in H.
+      clear mname f.
+      induction H; simpl. solve_complex_Excrel. downclose_Vrel.
+      destruct hd0 as [k1 v1].
+      destruct hd'0 as [k2 v2], H.
+      pose proof Vrel_Val_eqb _ _ _ H as EQk.
+      pose proof Vrel_Val_eqb _ _ _ H0 as EQhd.
+      rewrite Val_eqb_sym in EQk.
+      destruct Val_ltb eqn:LT.
+      - pose proof Val_eqb_ltb_trans _ _ _ EQk LT as LT2.
+        pose proof Val_ltb_eqb_trans _ _ _ LT2 EQhd as X.
+        rewrite X. assumption.
+      - pose proof Val_geb_eqb_trans _ _ _ EQk LT as LT3.
+        pose proof Val_eqb_geb_trans _ _ _ LT3 EQhd as X.
+        rewrite X.
+        destruct (Val_eqb hd k1) eqn:EQ.
+        + rewrite Val_eqb_sym in EQk, EQhd.
+          pose proof Val_eqb_trans _ _ _ EQ EQk as EQ2.
+          pose proof Val_eqb_trans _ _ _ EQhd EQ2 as EQ3.
+          rewrite EQ3.
+          solve_complex_Vrel.
+        + rewrite Val_eqb_sym in EQk.
+          pose proof Val_eqb_neqb _ _ _ EQ EQk as EQ2.
+          rewrite Val_eqb_sym in EQ2.
+          pose proof Val_eqb_neqb _ _ _ EQ2 EQhd as EQ3.
+          rewrite Val_eqb_sym in EQ3. rewrite EQ3.
+          solve_complex_Excrel. downclose_Vrel.
+    (** almost the same as before, but with the
+        default value; therefore, solve_complex_Vrel is
+        used instead of solve_complex_Excrel *)
+    * apply Vrel_Map_compat_rev in H.
+      clear mname f.
+      induction H; simpl. by solve_complex_Vrel.
+      destruct hd0 as [k1 v1].
+      destruct hd'0 as [k2 v2], H.
+      pose proof Vrel_Val_eqb _ _ _ H as EQk.
+      pose proof Vrel_Val_eqb _ _ _ H0 as EQhd.
+      rewrite Val_eqb_sym in EQk.
+      destruct Val_ltb eqn:LT.
+      - pose proof Val_eqb_ltb_trans _ _ _ EQk LT as LT2.
+        pose proof Val_ltb_eqb_trans _ _ _ LT2 EQhd as X.
+        rewrite X. assumption.
+      - pose proof Val_geb_eqb_trans _ _ _ EQk LT as LT3.
+        pose proof Val_eqb_geb_trans _ _ _ LT3 EQhd as X.
+        rewrite X.
+        destruct (Val_eqb hd k1) eqn:EQ.
+        + rewrite Val_eqb_sym in EQk, EQhd.
+          pose proof Val_eqb_trans _ _ _ EQ EQk as EQ2.
+          pose proof Val_eqb_trans _ _ _ EQhd EQ2 as EQ3.
+          rewrite EQ3.
+          solve_complex_Vrel.
+        + rewrite Val_eqb_sym in EQk.
+          pose proof Val_eqb_neqb _ _ _ EQ EQk as EQ2.
+          rewrite Val_eqb_sym in EQ2.
+          pose proof Val_eqb_neqb _ _ _ EQ2 EQhd as EQ3.
+          rewrite Val_eqb_sym in EQ3. rewrite EQ3.
+          solve_complex_Vrel.
+  }
+  {
+    inv H3; try solve_complex_Excrel.
+    apply Vrel_possibilities in H1 as H'; intuition; destruct_hyps; subst; try by solve_complex_Excrel. left.
+    apply Vrel_Map_compat_rev in H1 as IND.
+    clear mname f.
+    induction IND; simpl.
+    {
+      do 2 eexists; repeat split; try reflexivity.
+      by auto.
+    }
+    destruct hd1 as [k1 v1].
+    destruct hd'1 as [k2 v2], H2.
+    assert (Vrel m (VMap tl) (VMap tl')) as X. {
+      by apply Vrel_Map_compat_closed.
+    }
+    specialize (IHIND X). clear X.
+    pose proof Vrel_Val_eqb _ _ _ H2 as EQk.
+    pose proof Vrel_Val_eqb _ _ _ H0 as EQhd.
+    rewrite Val_eqb_sym in EQhd.
+    destruct Val_ltb eqn:LT.
+    - pose proof Val_ltb_eqb_trans _ _ _ LT EQk as LT2.
+      pose proof Val_eqb_ltb_trans _ _ _ EQhd LT2 as X.
+      rewrite X.
+      do 2 eexists; repeat split; try reflexivity.
+      constructor. 2: by auto.
+      choose_compat_lemma. by repeat constructor.
+    - pose proof Val_geb_eqb_trans _ _ _ EQhd LT as LT3.
+      pose proof Val_eqb_geb_trans _ _ _ LT3 EQk as X.
+      rewrite X.
+      destruct (Val_eqb hd k1) eqn:EQ.
+      + pose proof Val_eqb_trans _ _ _ EQhd EQ as EQ2.
+        pose proof Val_eqb_trans _ _ _ EQ2 EQk as EQ3.
+        rewrite EQ3.
+        do 2 eexists; repeat split; try reflexivity.
+        by constructor; auto.
+      + pose proof Val_eqb_neqb _ _ _ EQ EQk as EQ2.
+        rewrite Val_eqb_sym in EQ2, EQhd.
+        pose proof Val_eqb_neqb _ _ _ EQ2 EQhd as EQ3.
+        rewrite Val_eqb_sym in EQ3. rewrite EQ3.
+        destruct IHIND as [vl [vl' [Hall [Eq1 Eq2]]]].
+        do 2 eexists; repeat split; try reflexivity.
+        constructor; auto.
+        choose_compat_lemma. constructor. by auto.
+        inv Eq1.
+        inv Hall. by apply Vrel_Map_compat_rev in H7.
+  }
+  Unshelve.
+    all: lia.
+Qed.
+
 (* Ltac Rel_solver :=
   try apply Rel_eval_io;
   try apply Rel_eval_arith;
@@ -2682,6 +2808,14 @@ Proof.
     intuition; destruct_hyps; try rewrite H; try rewrite H0; try rewrite H2.
     - left. do 2 eexists. solve_complex_Excrel.
     - now right.
+  * pose proof Rel_eval_map_bifs m mname0 f0 _ _ H1.
+    intuition; destruct_hyps; try rewrite H; try rewrite H0; try rewrite H2.
+    - left. do 2 eexists. by solve_complex_Vrel.
+    - left. do 2 eexists. by solve_complex_Excrel.
+  * pose proof Rel_eval_map_bifs m mname0 f0 _ _ H1.
+    intuition; destruct_hyps; try rewrite H; try rewrite H0; try rewrite H2.
+    - left. do 2 eexists. by solve_complex_Vrel.
+    - left. do 2 eexists. by solve_complex_Excrel.
   * left. pose proof (Rel_eval_io m mname0 f0 _ _ H1).
     destruct eval_io, eval_io. simpl in *; subst.
     intuition; destruct_hyps; try rewrite H0; try rewrite H2; subst.
diff --git a/src/Interpreter/InterpreterAux.v b/src/Interpreter/InterpreterAux.v
index cb0ed7b0..d877a730 100644
--- a/src/Interpreter/InterpreterAux.v
+++ b/src/Interpreter/InterpreterAux.v
@@ -382,6 +382,12 @@ Definition convert_string_to_code_Interp : (string * string) -> BIFCode :=
         if String.eqb sn "split"%string then BSplit
         else BNothing
       )
+    else if String.eqb sf "maps"%string
+      then (
+        if String.eqb sn "get"%string then BGet
+        else if String.eqb sn "put"%string then BPut
+        else BNothing
+      )
     else BNothing.
 
 Definition eval_arith_Interp (mname : string) (fname : string) (params : list Val) :  Redex :=
@@ -639,6 +645,41 @@ match convert_string_to_code_Interp (mname, fname) with
 | _                              => Some (undef (VLit (Atom fname)))
 end.
 
+Definition eval_map_bifs_Interp (mname fname : string)
+                         (params : list Val) : Redex :=
+match convert_string_to_code_Interp (mname, fname) with
+| BPut => match params with
+          | key :: value :: map :: [] =>
+            match map with
+            | VMap contents => RValSeq [VMap (map_put key value contents)]
+            | _ => RExc (badmap (VTuple [VLit "put"%string;key;value;map]))
+            end
+          | _ => RExc (undef (VLit (Atom fname)))
+          end
+| BGet => match params with
+          | key :: map :: [] =>
+            match map with
+            | VMap contents =>
+              match map_get key contents with
+              | Some v => RValSeq [v]
+              | None   => RExc (badkey key)
+              end
+            | _ => RExc (badmap map)
+            end
+          | key :: map :: default :: [] =>
+            match map with
+            | VMap contents =>
+              match map_get key contents with
+              | Some v => RValSeq [v]
+              | None   => RValSeq [default]
+              end
+            | _ => RExc (badmap map)
+            end
+          | _ => RExc (undef (VLit (Atom fname)))
+          end
+| _ => RExc (undef (VLit (Atom fname)))
+end.
+
 Definition eval_Interp (mname : string) (fname : string) (params : list Val) 
    : option (Redex * option SideEffect) :=
 match convert_string_to_code_Interp (mname, fname) with
@@ -661,6 +702,8 @@ match convert_string_to_code_Interp (mname, fname) with
                                                       | None => None
                                                      end
 | BFunInfo                                        => Some (eval_funinfo_Interp params, None)
+| BGet | BPut => Some (eval_map_bifs_Interp mname fname params, None)
+
 (** undefined functions *)
 | BNothing                                        => Some (RExc (undef (VLit (Atom fname))), None)
 (* concurrent BIFs *)
diff --git a/src/Interpreter/InterpreterAuxLemmas.v b/src/Interpreter/InterpreterAuxLemmas.v
index 1dce6f9d..23abcb52 100644
--- a/src/Interpreter/InterpreterAuxLemmas.v
+++ b/src/Interpreter/InterpreterAuxLemmas.v
@@ -352,14 +352,17 @@ Proof.
           destruct b1; try reflexivity; destruct b2; try reflexivity; destruct b3; try reflexivity;
           destruct b4; try reflexivity; destruct b5; try reflexivity; destruct b6; try reflexivity.
         all:destruct s1; try reflexivity; try congruence.
+        all:try destruct s1; try reflexivity; try congruence.
+        all:destruct s2; try reflexivity; try congruence.
         all:destruct a; try reflexivity; destruct b; try reflexivity; destruct b0; try reflexivity;
           destruct b1; try reflexivity; destruct b2; try reflexivity; destruct b3; try reflexivity;
           destruct b4; try reflexivity; destruct b5; try reflexivity; destruct b6; try reflexivity.
-        all:destruct s1; try reflexivity; try congruence.
-        all:destruct a; try reflexivity; destruct b; try reflexivity; destruct b0; try reflexivity;
-          destruct b1; try reflexivity; destruct b2; try reflexivity; destruct b3; try reflexivity;
-          destruct b4; try reflexivity; destruct b5; try reflexivity; destruct b6; try reflexivity.
-        all:destruct s1; try reflexivity; try congruence.
+        all:try destruct s2; try reflexivity; try congruence.
+        all:try destruct s2; try reflexivity; try congruence.
+        all: cbn.
+        all: do 9 (case_match; try reflexivity; try congruence).
+        all: do 9 (case_match; try reflexivity; try congruence).
+        all: do 9 (case_match; try reflexivity; try congruence).
 Qed.
 
 Lemma eval_arith_equiv: forall (mname : string) (fname : string) (params : list Val),
@@ -470,6 +473,13 @@ Proof.
   rewrite <- convert_string_to_code_equiv. reflexivity.
 Qed.
 
+Lemma eval_map_bifs_equiv: forall (mname : string) (fname : string) (params : list Val),
+  eval_map_bifs mname fname params = eval_map_bifs_Interp mname fname params.
+Proof.
+  intros. unfold eval_map_bifs_Interp.
+  rewrite <- convert_string_to_code_equiv. reflexivity.
+Qed.
+
 Lemma eval_equiv: forall (mname : string) (fname : string) (params : list Val),
   eval mname fname params = eval_Interp mname fname params.
 Proof.
@@ -489,6 +499,7 @@ Proof.
   rewrite <- eval_funinfo_equiv.
   rewrite <- eval_concurrent_equiv.
   rewrite <- eval_arith_equiv.
+  rewrite <- eval_map_bifs_equiv.
   reflexivity.
 Qed.
 
diff --git a/src/Maps.v b/src/Maps.v
index 7fc91e47..7883fbb8 100644
--- a/src/Maps.v
+++ b/src/Maps.v
@@ -11,7 +11,10 @@
   assumption.
 *)
 
+(**
+  TODO: use stdpp's maps instead for representation!
 
+*)
 
 From CoreErlang Require Export Equalities.
 Import ListNotations.
@@ -20,7 +23,7 @@ Import ListNotations.
 
 (** Building Val maps based on the Val ordering Val_ltb
     This function inserts a key-value pair into the map. This operation
-    overwrites existing keys.
+    does not overwrite existing keys.
 *)
 Fixpoint map_insert (k v : Val) (m : list (Val * Val))
   : (list (Val * Val)) :=
@@ -34,6 +37,34 @@ match m with
                     else (k', v')::(map_insert k v ms)
 end.
 
+Fixpoint map_put (k v : Val) (m : list (Val * Val))
+  : (list (Val * Val)) :=
+match m with
+| [] => [(k,v)]
+| (k',v')::ms => if Val_ltb k k' 
+                 then ((k, v)::(k',v')::ms) 
+                 else
+                    if Val_eqb k k' 
+                    then (k, v)::ms
+                    else (k', v')::(map_put k v ms)
+end.
+
+Fixpoint map_get (k : Val) (m : list (Val * Val)) : option Val :=
+match m with
+| [] => None
+| (k', v') :: ms =>
+  if Val_ltb k' k
+  then map_get k ms
+  else
+     if Val_eqb k k'
+     then Some v'
+     else None
+end.
+
+Goal map_get (VLit 1%Z) (map_insert (VLit 1%Z) VNil []) = Some VNil. Proof. reflexivity. Qed.
+Goal map_get (VLit 2%Z) (map_insert (VLit 1%Z) VNil []) = None. Proof. reflexivity. Qed.
+Goal map_get (VLit 2%Z) (map_insert (VLit 1%Z) VNil (map_insert (VLit 2%Z) (VLit 3%Z) [])) = Some (VLit 3%Z). Proof. reflexivity. Qed.
+
 (** This function collapses a list of value pairs into a map *)
 Fixpoint make_val_map (l: list (Val * Val)) : list (Val * Val) :=
 match l with
diff --git a/src/Syntax.v b/src/Syntax.v
index cf0355ac..c4bcc377 100644
--- a/src/Syntax.v
+++ b/src/Syntax.v
@@ -164,6 +164,10 @@ Definition badarith (v : Val) : Exception :=
   (Error, VLit (Atom "badarith"%string), v).
 Definition badarg (v : Val) : Exception :=
   (Error, VLit (Atom "badarg"%string), v).
+Definition badmap (v : Val) : Exception :=
+  (Error, VLit (Atom "badmap"%string), v).
+Definition badkey (v : Val) : Exception :=
+  (Error, VLit (Atom "badkey"%string), v).
 Definition undef (v : Val) : Exception :=
   (Error, VLit (Atom "undef"%string), v).
 Definition badfun (v : Val) : Exception := 

From a54581e221296edcd2ce3327384d7ff07edebe5b Mon Sep 17 00:00:00 2001
From: mtlevr <mtlevr@inf.elte.hu>
Date: Sat, 16 May 2026 14:45:48 +0200
Subject: [PATCH 2/2] Interpreter re-extraction (Haskell & OCaml)

---
 .../HaskellSrc/exe/RocqExtraction.hs          | 106 +++++++++++++++++-
 src/Interpreter/OCamlSrc/RocqExtraction.ml    |  94 +++++++++++++++-
 2 files changed, 198 insertions(+), 2 deletions(-)

diff --git a/src/Interpreter/HaskellSrc/exe/RocqExtraction.hs b/src/Interpreter/HaskellSrc/exe/RocqExtraction.hs
index 96b920cb..2c169651 100644
--- a/src/Interpreter/HaskellSrc/exe/RocqExtraction.hs
+++ b/src/Interpreter/HaskellSrc/exe/RocqExtraction.hs
@@ -511,6 +511,14 @@ badarg :: Val -> Exception
 badarg v =
   (,) ((,) Error (VLit (Atom "badarg"))) v
 
+badmap :: Val -> Exception
+badmap v =
+  (,) ((,) Error (VLit (Atom "badmap"))) v
+
+badkey :: Val -> Exception
+badkey v =
+  (,) ((,) Error (VLit (Atom "badkey"))) v
+
 undef :: Val -> Exception
 undef v =
   (,) ((,) Error (VLit (Atom "undef"))) v
@@ -877,6 +885,34 @@ map_insert k v m =
          Prelude.True -> m;
          Prelude.False -> (:) ((,) k' v') (map_insert k v ms)}}}}
 
+map_put :: Val -> Val -> (([]) ((,) Val Val)) -> ([]) ((,) Val Val)
+map_put k v m =
+  case m of {
+   ([]) -> (:) ((,) k v) ([]);
+   (:) p ms ->
+    case p of {
+     (,) k' v' ->
+      case val_ltb k k' of {
+       Prelude.True -> (:) ((,) k v) ((:) ((,) k' v') ms);
+       Prelude.False ->
+        case val_eqb k k' of {
+         Prelude.True -> (:) ((,) k v) ms;
+         Prelude.False -> (:) ((,) k' v') (map_put k v ms)}}}}
+
+map_get :: Val -> (([]) ((,) Val Val)) -> Prelude.Maybe Val
+map_get k m =
+  case m of {
+   ([]) -> Prelude.Nothing;
+   (:) p ms ->
+    case p of {
+     (,) k' v' ->
+      case val_ltb k' k of {
+       Prelude.True -> map_get k ms;
+       Prelude.False ->
+        case val_eqb k k' of {
+         Prelude.True -> Prelude.Just v';
+         Prelude.False -> Prelude.Nothing}}}}
+
 make_val_map :: (([]) ((,) Val Val)) -> ([]) ((,) Val Val)
 make_val_map l =
   case l of {
@@ -1090,6 +1126,8 @@ data BIFCode =
  | BUnLink
  | BNothing
  | BFunInfo
+ | BGet
+ | BPut
 
 is_shallow_proper_list :: Val -> Prelude.Bool
 is_shallow_proper_list v =
@@ -1940,7 +1978,19 @@ convert_string_to_code_Interp pat =
                  sn "split" of {
            Prelude.True -> BSplit;
            Prelude.False -> BNothing};
-         Prelude.False -> BNothing}}}}
+         Prelude.False ->
+          case ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool)
+                 sf "maps" of {
+           Prelude.True ->
+            case ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool)
+                   sn "get" of {
+             Prelude.True -> BGet;
+             Prelude.False ->
+              case ((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool)
+                     sn "put" of {
+               Prelude.True -> BPut;
+               Prelude.False -> BNothing}};
+           Prelude.False -> BNothing}}}}}
 
 eval_arith_Interp :: Prelude.String -> Prelude.String -> (([]) Val) -> Redex
 eval_arith_Interp mname fname params =
@@ -3490,6 +3540,56 @@ eval_concurrent_Interp mname fname params =
      (:) _ _ -> Prelude.Nothing};
    _ -> Prelude.Just (undef (VLit (Atom fname)))}
 
+eval_map_bifs_Interp :: Prelude.String -> Prelude.String -> (([]) Val) ->
+                        Redex
+eval_map_bifs_Interp mname fname params =
+  case convert_string_to_code_Interp ((,) mname fname) of {
+   BGet ->
+    case params of {
+     ([]) -> RExc (undef (VLit (Atom fname)));
+     (:) key l ->
+      case l of {
+       ([]) -> RExc (undef (VLit (Atom fname)));
+       (:) map l0 ->
+        case l0 of {
+         ([]) ->
+          case map of {
+           VMap contents ->
+            case map_get key contents of {
+             Prelude.Just v -> RValSeq ((:) v ([]));
+             Prelude.Nothing -> RExc (badkey key)};
+           _ -> RExc (badmap map)};
+         (:) default0 l1 ->
+          case l1 of {
+           ([]) ->
+            case map of {
+             VMap contents ->
+              case map_get key contents of {
+               Prelude.Just v -> RValSeq ((:) v ([]));
+               Prelude.Nothing -> RValSeq ((:) default0 ([]))};
+             _ -> RExc (badmap map)};
+           (:) _ _ -> RExc (undef (VLit (Atom fname)))}}}};
+   BPut ->
+    case params of {
+     ([]) -> RExc (undef (VLit (Atom fname)));
+     (:) key l ->
+      case l of {
+       ([]) -> RExc (undef (VLit (Atom fname)));
+       (:) value l0 ->
+        case l0 of {
+         ([]) -> RExc (undef (VLit (Atom fname)));
+         (:) map l1 ->
+          case l1 of {
+           ([]) ->
+            case map of {
+             VMap contents -> RValSeq ((:) (VMap
+              (map_put key value contents)) ([]));
+             _ -> RExc
+              (badmap (VTuple ((:) (VLit (Atom "put")) ((:) key ((:) value
+                ((:) map ([])))))))};
+           (:) _ _ -> RExc (undef (VLit (Atom fname)))}}}};
+   _ -> RExc (undef (VLit (Atom fname)))}
+
 eval_Interp :: Prelude.String -> Prelude.String -> (([]) Val) ->
                Prelude.Maybe ((,) Redex (Prelude.Maybe SideEffect))
 eval_Interp mname fname params =
@@ -3592,6 +3692,10 @@ eval_Interp mname fname params =
     Prelude.Nothing);
    BFunInfo -> Prelude.Just ((,) (eval_funinfo_Interp params)
     Prelude.Nothing);
+   BGet -> Prelude.Just ((,) (eval_map_bifs_Interp mname fname params)
+    Prelude.Nothing);
+   BPut -> Prelude.Just ((,) (eval_map_bifs_Interp mname fname params)
+    Prelude.Nothing);
    _ -> Prelude.Just ((,) (eval_arith_Interp mname fname params)
     Prelude.Nothing)}
 
diff --git a/src/Interpreter/OCamlSrc/RocqExtraction.ml b/src/Interpreter/OCamlSrc/RocqExtraction.ml
index 02d722c3..e6d1dcd4 100644
--- a/src/Interpreter/OCamlSrc/RocqExtraction.ml
+++ b/src/Interpreter/OCamlSrc/RocqExtraction.ml
@@ -1210,6 +1210,16 @@ let badarith v =
 let badarg v =
   ((Error, (VLit (Atom ('b'::('a'::('d'::('a'::('r'::('g'::[]))))))))), v)
 
+(** val badmap : val0 -> exception0 **)
+
+let badmap v =
+  ((Error, (VLit (Atom ('b'::('a'::('d'::('m'::('a'::('p'::[]))))))))), v)
+
+(** val badkey : val0 -> exception0 **)
+
+let badkey v =
+  ((Error, (VLit (Atom ('b'::('a'::('d'::('k'::('e'::('y'::[]))))))))), v)
+
 (** val undef : val0 -> exception0 **)
 
 let undef v =
@@ -1674,6 +1684,26 @@ let rec map_insert k v m = match m with
   then (k, v) :: ((k', v') :: ms)
   else if val_eqb k k' then m else (k', v') :: (map_insert k v ms)
 
+(** val map_put : val0 -> val0 -> (val0 * val0) list -> (val0 * val0) list **)
+
+let rec map_put k v = function
+| [] -> (k, v) :: []
+| p :: ms ->
+  let (k', v') = p in
+  if val_ltb k k'
+  then (k, v) :: ((k', v') :: ms)
+  else if val_eqb k k' then (k, v) :: ms else (k', v') :: (map_put k v ms)
+
+(** val map_get : val0 -> (val0 * val0) list -> val0 option **)
+
+let rec map_get k = function
+| [] -> None
+| p :: ms ->
+  let (k', v') = p in
+  if val_ltb k' k
+  then map_get k ms
+  else if val_eqb k k' then Some v' else None
+
 (** val make_val_map : (val0 * val0) list -> (val0 * val0) list **)
 
 let rec make_val_map = function
@@ -1882,6 +1912,8 @@ type bIFCode =
 | BUnLink
 | BNothing
 | BFunInfo
+| BGet
+| BPut
 
 (** val is_shallow_proper_list : val0 -> bool **)
 
@@ -3770,7 +3802,13 @@ let convert_string_to_code_Interp = function
             then if eqb0 sn ('s'::('p'::('l'::('i'::('t'::[])))))
                  then BSplit
                  else BNothing
-            else BNothing
+            else if eqb0 sf ('m'::('a'::('p'::('s'::[]))))
+                 then if eqb0 sn ('g'::('e'::('t'::[])))
+                      then BGet
+                      else if eqb0 sn ('p'::('u'::('t'::[])))
+                           then BPut
+                           else BNothing
+                 else BNothing
 
 (** val eval_arith_Interp : char list -> char list -> val0 list -> redex **)
 
@@ -5478,6 +5516,58 @@ let eval_concurrent_Interp mname fname params =
      | _ :: _ -> None)
   | _ -> Some (undef (VLit (Atom fname)))
 
+(** val eval_map_bifs_Interp :
+    char list -> char list -> val0 list -> redex **)
+
+let eval_map_bifs_Interp mname fname params =
+  match convert_string_to_code_Interp (mname, fname) with
+  | BGet ->
+    (match params with
+     | [] -> RExc (undef (VLit (Atom fname)))
+     | key :: l ->
+       (match l with
+        | [] -> RExc (undef (VLit (Atom fname)))
+        | map0 :: l0 ->
+          (match l0 with
+           | [] ->
+             (match map0 with
+              | VMap contents ->
+                (match map_get key contents with
+                 | Some v -> RValSeq (v :: [])
+                 | None -> RExc (badkey key))
+              | _ -> RExc (badmap map0))
+           | default :: l1 ->
+             (match l1 with
+              | [] ->
+                (match map0 with
+                 | VMap contents ->
+                   (match map_get key contents with
+                    | Some v -> RValSeq (v :: [])
+                    | None -> RValSeq (default :: []))
+                 | _ -> RExc (badmap map0))
+              | _ :: _ -> RExc (undef (VLit (Atom fname)))))))
+  | BPut ->
+    (match params with
+     | [] -> RExc (undef (VLit (Atom fname)))
+     | key :: l ->
+       (match l with
+        | [] -> RExc (undef (VLit (Atom fname)))
+        | value :: l0 ->
+          (match l0 with
+           | [] -> RExc (undef (VLit (Atom fname)))
+           | map0 :: l1 ->
+             (match l1 with
+              | [] ->
+                (match map0 with
+                 | VMap contents ->
+                   RValSeq ((VMap (map_put key value contents)) :: [])
+                 | _ ->
+                   RExc
+                     (badmap (VTuple ((VLit (Atom
+                       ('p'::('u'::('t'::[]))))) :: (key :: (value :: (map0 :: [])))))))
+              | _ :: _ -> RExc (undef (VLit (Atom fname)))))))
+  | _ -> RExc (undef (VLit (Atom fname)))
+
 (** val eval_Interp :
     char list -> char list -> val0 list -> (redex * sideEffect option) option **)
 
@@ -5556,6 +5646,8 @@ let eval_Interp mname fname params =
      | None -> None)
   | BNothing -> Some ((RExc (undef (VLit (Atom fname)))), None)
   | BFunInfo -> Some ((eval_funinfo_Interp params), None)
+  | BGet -> Some ((eval_map_bifs_Interp mname fname params), None)
+  | BPut -> Some ((eval_map_bifs_Interp mname fname params), None)
   | _ -> Some ((eval_arith_Interp mname fname params), None)
 
 (** val create_result_Interp :