vericert.hls.AssocMap

Definition reg := positive.

Module AssocMap := Maps.PTree.

Module AssocMapExt.

  #[export] Hint Resolve elements_correct elements_complete elements_keys_norepet : assocmap.
  #[export] Hint Resolve gso gss : assocmap.

  Section Operations.

    Variable A : Type.

    Definition get_default (a : A) (k : reg) (m : t A) : A :=
      match get k m with
      | None => a
      | Some v => v
      end.

    Fixpoint merge (m1 m2 : t A) : t A :=
      match m1, m2 with
      | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2)
      | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2)
      | Leaf, _ => m2
      | _, _ => m1
      end.

    Lemma merge_base_1 :
      forall am,
      merge (empty A) am = am.

    Lemma merge_base_2 :
      forall am,
      merge am (empty A) = am.

    Lemma merge_add_assoc :
      forall r am am' v,
      merge (set r v am) am' = set r v (merge am am').

    Lemma merge_correct_1 :
      forall am bm k v,
      get k am = Some v ->
      get k (merge am bm) = Some v.

    Lemma merge_correct_2 :
      forall am bm k v,
      get k am = None ->
      get k bm = Some v ->
      get k (merge am bm) = Some v.

    Lemma merge_correct_3 :
      forall am bm k,
      get k am = None ->
      get k bm = None ->
      get k (merge am bm) = None.

    Definition merge_fold (am bm : t A) : t A :=
      fold_right (fun p a => set (fst p) (snd p) a) bm (elements am).

    Lemma add_assoc :
      forall (k : elt) (v : A) l bm,
      List.In (k, v) l ->
      list_norepet (List.map fst l) ->
      @get A k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v.

    Lemma not_in_assoc :
      forall k v l bm,
      ~ List.In k (List.map (@fst elt A) l) ->
      @get A k bm = Some v ->
      get k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v.

    Lemma elements_iff :
      forall am k,
      (exists v, get k am = Some v) <->
      List.In k (List.map (@fst _ A) (elements am)).

    #[local] Hint Resolve merge_base_1 : core.
    #[local] Hint Resolve merge_base_2 : core.
    #[local] Hint Resolve merge_add_assoc : core.
    #[local] Hint Resolve merge_correct_1 : core.
    #[local] Hint Resolve merge_correct_2 : core.
    #[local] Hint Resolve merge_correct_3 : core.
    #[local] Hint Resolve add_assoc : core.
    #[local] Hint Resolve not_in_assoc : core.
    #[local] Hint Resolve elements_iff : core.

    Lemma elements_correct' :
      forall am k,
      ~ (exists v, get k am = Some v) <->
      ~ List.In k (List.map (@fst _ A) (elements am)).

    Lemma elements_correct_none :
      forall am k,
      get k am = None ->
      ~ List.In k (List.map (@fst _ A) (elements am)).

    Lemma merge_fold_add :
      forall k v am bm,
      am ! k = Some v ->
      (merge_fold am bm) ! k = Some v.

    #[local] Hint Resolve elements_correct' : core.
    #[local] Hint Resolve elements_correct_none : core.
    #[local] Hint Resolve merge_fold_add : core.

    Lemma merge_fold_not_in :
      forall k v am bm,
      get k am = None ->
      get k bm = Some v ->
      get k (merge_fold am bm) = Some v.

    Lemma merge_fold_base :
      forall am,
      merge_fold (empty A) am = am.

  End Operations.

  #[export] Hint Resolve merge_base_1 : assocmap.
  #[export] Hint Resolve merge_base_2 : assocmap.
  #[export] Hint Resolve merge_add_assoc : assocmap.
  #[export] Hint Resolve merge_correct_1 : assocmap.
  #[export] Hint Resolve merge_correct_2 : assocmap.
  #[export] Hint Resolve merge_correct_3 : assocmap.
  #[export] Hint Resolve add_assoc : assocmap.
  #[export] Hint Resolve not_in_assoc : assocmap.
  #[export] Hint Resolve elements_iff : assocmap.
  #[export] Hint Resolve elements_correct' : assocmap.
  #[export] Hint Resolve merge_fold_not_in : assocmap.
  #[export] Hint Resolve merge_fold_base : assocmap.
  #[export] Hint Resolve elements_correct_none : assocmap.
  #[export] Hint Resolve merge_fold_add : assocmap.

End AssocMapExt.

Definition assocmap := AssocMap.t value.

Definition find_assocmap (n : nat) : reg -> assocmap -> value :=
  get_default value (ZToValue 0).

Definition empty_assocmap : assocmap := AssocMap.empty value.

Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value.


Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap.
Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap.
Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap.
Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap.
Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap.

Lemma find_get_assocmap :
  forall assoc r v,
  assoc ! r = Some v ->
  assoc # r = v.