Skip to content

Formalise map standard functions (maps:put, maps:get) #67

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
berpeti merged 2 commits into from
May 18, 2026
Merged

Formalise map standard functions (maps:put, maps:get) #67

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ed74b08
Add map primitives
berpeti May 15, 2026
a54581e
Interpreter re-extraction (Haskell & OCaml)
MTLEVR May 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
127 changes: 124 additions & 3 deletions src/Auxiliaries.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -53,6 +56,8 @@ Inductive BIFCode :=
| BSend | BSpawn | BSpawnLink | BProcessFlag | BSelf | BLink | BUnLink
| BNothing
| BFunInfo
(* map primitives *)
| BGet | BPut
.

(**
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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,
Expand All @@ -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.
Expand Down Expand Up @@ -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',
Expand Down Expand Up @@ -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.
37 changes: 32 additions & 5 deletions src/Concurrent/NodeSemanticsLemmas.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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') ->
Expand All @@ -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 :
Expand Down
45 changes: 45 additions & 0 deletions src/Concurrent/PIDRenaming.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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') ->
Expand Down Expand Up @@ -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 :
Expand Down
Loading
Loading