prove type check; adapt new signature

theories/mask_core/calculus.v

@@ -62,9 +62,6 @@ Record signature := {
   sig_length : nat;
   sig_ranges : vec range sig_length;
   sig_mono : ranges_monotone sig_ranges;
-  (* properties on ranges *)
-  (* sig_disjoint : ∀ f1 f2, f1 ≠ f2 →
-    (sig_ranges !!! f1 ≺ sig_ranges !!! f2) ∨ (sig_ranges !!! f2 ≺ sig_ranges !!! f1); *)
   (* total bits *)
   sig_bits : nat;
   sig_max_range_bounded : ∃ r, last sig_ranges = Some r ∧
@@ -92,22 +89,41 @@ Definition field_width (σ : signature) f : nat :=
 Arguments field_width _ !_ /.
 
 Definition recognize (σ : signature) (r : range) : option (fin σ.(sig_length)) :=
-    match filter (λ f, σ.(sig_ranges) !!! f = r) (enum (fin σ.(sig_length))) with
-    | [] => None
-    | f :: _ => Some f
-    end.
+  match filter (λ f, σ.(sig_ranges) !!! f = r) (enum (fin σ.(sig_length))) with
+  | [] => None
+  | f :: _ => Some f
+  end.
 
 Lemma sig_disjoint σ f1 f2 :
   f1 ≠ f2 →
   (sig_ranges σ !!! f1 ≺ sig_ranges σ !!! f2) ∨
   (sig_ranges σ !!! f2 ≺ sig_ranges σ !!! f1).
 Proof.
-Admitted.
+  remember (sig_ranges σ !!! f1) as r1 eqn:Heq1.
+  remember (sig_ranges σ !!! f2) as r2 eqn:Heq2.
+  symmetry in Heq1. apply vlookup_lookup in Heq1.
+  symmetry in Heq2. apply vlookup_lookup in Heq2.
+  intros. have Hne : fin_to_nat f1 ≠ fin_to_nat f2.
+  { intros ?. have ? : f1 = f2 by eapply fin_to_nat_inj. contradiction. }
+  have Hmono := (sig_mono σ).
+  rewrite /ranges_monotone bool_decide_spec in Hmono.
+  apply nat_total_order in Hne as [|]; [left|right]; eapply Sorted_lookup_mono; eauto; apply range_lt_trans.
+Qed.
 
 Lemma sig_ranges_bounded σ f :
   Z.of_nat (offset (sig_ranges σ !!! f)) + Z.of_nat (width (sig_ranges σ !!! f)) ≤ sig_bits σ.
 Proof.
-Admitted.
+  remember (sig_ranges σ !!! f) as r eqn:Heqr.
+  symmetry in Heqr. apply vlookup_lookup in Heqr.
+  have [r' [Hr' /bool_decide_spec Hm]] := (sig_max_range_bounded σ).
+  have Hmono := (sig_mono σ).
+  rewrite /ranges_monotone bool_decide_spec in Hmono.
+  have [? | ->] : r ≺ r' ∨ r = r'.
+  { eapply Sorted_last_max; eauto. apply range_lt_trans.
+    eapply elem_of_list_lookup_2; eauto. }
+  - unfold range_lt in *. lia.
+  - done.
+Qed.
 
 Ltac solve_ranges_monotone :=
   apply bool_decide_pack;
@@ -185,7 +201,7 @@ Inductive has_ty : tm → ty → Prop :=
   | ty_val n σ f :
     0 ≤ n < 2 ^ (field_width σ f) →
     ⊢ bf_val n : val σ f
-  | ty_mask k σ f :
+  | ty_mask (k : Z) σ f :
     k = field_width σ f →
     ⊢ bf_mask k : val σ f
   | ty_nil_bv σ :
@@ -198,7 +214,7 @@ Inductive has_ty : tm → ty → Prop :=
     ⊢ t : bv σ →
     range_lt_head r (ranges t) →
     ⊢ bf_cons r x t : bv σ
-  | ty_cons_mv σ f r k t :
+  | ty_cons_mv σ f r (k : Z) t :
     recognize σ r = Some f →
     k = width r →
     ⊢ t : mv σ →

theories/mask_core/semantics.v

@@ -134,7 +134,6 @@ Proof.
   - auto_inv.
   - auto_inv. rewrite rc.bf_lor_mask_cons_r; try lia.
     eapply val_bounded; eauto.
-    erewrite recognize_spec; eauto.
   - rewrite rc.bf_lor_update_l; try lia. naive_solver.
   - rewrite rc.bf_lor_update_l; try lia. naive_solver.
   - rewrite rc.bf_lor_update_r; try lia. naive_solver.

theories/mask_core/total_merge.v

 From stdpp Require Import prelude sorting.
 From Coq Require Import ssreflect.
 
+Section Sorted.
+
+  Context {A : Type} (R : relation A) `{!Transitive R}.
+
+  Lemma Sorted_lookup_mono (l : list A) :
+    Sorted R l →
+    ∀ i j x y, l !! i = Some x → l !! j = Some y → i < j → R x y.
+  Proof.
+    induction 1 => i j x y Hi Hj Hlt //.
+    destruct i.
+    - simpl in Hi. inversion Hi; subst; clear Hi.
+      destruct j; [lia|]. simpl in Hj.
+      destruct l as [|b l]; first done. destruct j.
+      + simpl in Hj. inversion Hj; subst; clear Hj.
+        eapply HdRel_inv; eauto.
+      + etrans; first eapply HdRel_inv; eauto.
+        eapply (IHSorted 0 (S j)) => //. lia.
+    - simpl in Hi. destruct j; [lia|]. simpl in Hj.
+      have ? : i < j by lia. naive_solver.
+  Qed.
+
+  Lemma Sorted_last_max (l : list A) m :
+    Sorted R l →
+    last l = Some m →
+    ∀ x, x ∈ l → R x m ∨ x = m.
+  Proof.
+    intros ? Hm x Hx.
+    apply elem_of_list_lookup in Hx as [i Hi].
+    rewrite last_lookup in Hm.
+    have ? : (i < length l)%nat by apply lookup_lt_is_Some_1.
+    destruct (decide (i = Init.Nat.pred (length l))) as [->|].
+    - right. congruence.
+    - left. eapply Sorted_lookup_mono; eauto. lia.
+  Qed.
+
+End Sorted.
+
 Class TotalOrder {A : Type} (R : relation A) :=
   total_order : ∀ x y, x ≠ y → R x y ∨ R y x.
 
@@ -15,15 +52,7 @@ Global Instance nat_lt_total_order : TotalOrder lt := nat_total_order.
 Section total_merge.
 
   Context {A : Type} `{EqDecision A} (R : relation A) `{∀ x y, Decision (R x y)}.
-
-  Lemma Sorted_lookup_mono (l : list A) i j x y :
-    Sorted R l →
-    l !! i = Some x →
-    l !! j = Some y →
-    i < j →
-    R x y.
-  Admitted.
-
+  
   Fixpoint total_merge (l1 : list A) : list A → list A :=
     fix total_merge_aux l2 :=
     match l1, l2 with

theories/mask_core/typecheck.v

@@ -31,8 +31,8 @@ Proof.
   by apply Hb, range_eqb_spec.
 Qed.
 
-Fixpoint check_has_ty (t : tm) (τ : ty) : bool :=
-  match t, τ with
+Fixpoint check_has_ty (t' : tm) (τ : ty) : bool :=
+  match t', τ with
   | bf_val n, val σ f =>
     (* (0 <=? n) && (n <? 2 ^ (field_width σ f)) *)
     true
@@ -51,11 +51,14 @@ Fixpoint check_has_ty (t : tm) (τ : ty) : bool :=
     default false (
       f ← recognize σ r;
       Some (range_ltb_head r (ranges t)
-        && (width r =? k)
+        && (k =? width r)
         && check_has_ty t (mv σ))
     )
   | bf_slice r t, val σ f =>
-    (sig_ranges σ !!! f == r) && check_has_ty t (bv σ)
+    default false (
+      f' ← recognize σ r;
+      Some (Fin.eqb f' f && check_has_ty t (bv σ))
+    )
   | bf_update r x t, bv σ =>
     default false (
       f ← recognize σ r;
@@ -100,12 +103,6 @@ Fixpoint check_has_ty_conditions (t : tm) (τ : ty) : list Prop :=
   | _, _ => []
   end.
 
-Ltac destruct_option :=
-  match goal with
-  | |- context [ (?o ≫= _) ] =>
-    destruct o eqn:Heqn; simpl; try done
-  end.
-
 Lemma check_has_ty_conditions_mv_nil t σ :
   check_has_ty_conditions t (mv σ) = [].
 Proof. by destruct t. Qed.
@@ -115,16 +112,27 @@ Lemma check_has_ty_spec t τ :
   check_has_ty t τ = true →
   ⊢ t : τ.
 Proof.
-  (* induction t; destruct τ; try case_match.
-  all: simpl => //.
-  all: try destruct_option.
-  all: rewrite ?andb_true_iff ?bool_decide_eq_true ?range_ltb_head_spec ?range_eqb_spec ?Z.eqb_eq.
-  all: try case_match => //.
-  all: intros; repeat match goal with
-  | [ H : _ ∧ _ |- _ ] => destruct H as [? ?]
+  move : τ. induction t; destruct τ => //=.
+  all: try match goal with
+  | |- context [ (?o ≫= _) ] =>
+    destruct o eqn:Heqn; simpl; try done
   end.
-  all: repeat (econstructor; eauto) => //. *)
-Admitted.
+  all: repeat case_match => //=.
+  all: rewrite ?andb_true_iff ?range_ltb_head_spec ?range_eqb_spec ?Z.eqb_eq ?Nat.eqb_eq ?Fin.eqb_eq ?orb_true_iff.
+  all: rewrite ?Forall_app ?Forall_cons_iff ?Forall_singleton.
+  all: intros.
+  all: repeat match goal with
+  | [ H : _ ∧ _ |- _ ] => destruct H as [? ?]
+  | [ H : _ ∨ _ |- _ ] => destruct H as [?|?]
+  end => //; subst.
+  all: try by repeat (econstructor; eauto).
+  all: try have ? : Forall id (check_has_ty_conditions t1 (mv σ)) by rewrite check_has_ty_conditions_mv_nil.
+  all: try have ? : Forall id (check_has_ty_conditions t2 (mv σ)) by rewrite check_has_ty_conditions_mv_nil.
+  all: repeat (econstructor; eauto).
+  - apply subsume_mv_bv. eauto.
+  - by apply check_disjoint_spec.
+  - by apply check_disjoint_spec.
+Qed.
 
 Lemma has_ty_implies_check_has_ty_conditions t τ :
   ⊢ t : τ →