Files

  • Verilog

    • Top

    Module TypeSystem

    From Stdlib Require Import Lists.List.
    From Stdlib Require Import PeanoNat.
    From Stdlib Require Import Arith.Compare_dec.
    From Stdlib Require Import Logic.Decidable.
    From Stdlib Require Export Lia.

    From Verilog Require Import Expr.
    From Verilog Require Import ExprPath.
    From Verilog Require Import Utils.

    Import ListNotations.
    Import Nat.

    Import Expr.
    Import ExprPath.
    Import Path.
    Import Utils.


    # Typing system definition In this module, we define our typing system and prove some of its properties.
    Module TypeSystem.

    ## Resizable Expressions This predicate characterizes the expressions that can be resized atomically, i.e., by changing only the root width annotation while leaving child widths unchanged. In the paper, this corresponds to the class of "atomically resizable expressions" used by the `Resize<==` rule.
      Variant Resizable : Expr -> Set :=
      | ResAtom : forall op, Resizable (EOperand op)
      | ResComp : forall lhs rhs, Resizable (EComp lhs rhs)
      | ResLogic : forall lhs rhs, Resizable (ELogic lhs rhs)
      | ResRed : forall e, Resizable (EReduction e)
      | ResAssign : forall lval arg, Resizable (EAssign lval arg)
      | ResConcat : forall args, Resizable (EConcat args)
      | ResRepl : forall amount arg, Resizable (ERepl amount arg)
      .


    ## Path-Function Combinators Typing judgments return a sizing function `f : path -> option nat` recording final widths of all valid subexpressions. These combinators correspond to the function operators introduced in the paper (Figure "function-operators").

    Build a singleton sizing function for a leaf: only the root path has a width.
      Definition Initial t : path -> option nat :=
        fun p =>
          match p with
          | [] => Some t
          | _ :: _ => None
          end
      .

    Replace the root width while preserving all strict subpaths. This is the function-level counterpart of atomic resizing.
      Definition ReplaceRoot t (f: path -> option nat) : path -> option nat :=
        fun p =>
          match p with
          | [] => Some t
          | _ :: _ => f p
          end
      .

    Combine two child sizing functions under a binary node. Child `0` is the left operand, child `1` is the right operand.
      Definition Binary t (f g: path -> option nat) : path -> option nat :=
        fun p =>
          match p with
          | [] => Some t
          | 0 :: p => f p
          | 1 :: p => g p
          | _ :: _ => None
          end
      .

    Combine one child sizing function under a unary node. Only child `0` is valid below the root.
      Definition Unary t (f: path -> option nat) : path -> option nat :=
        fun p =>
          match p with
          | [] => Some t
          | 0 :: p => f p
          | _ :: _ => None
          end
      .

    Combine three child sizing functions under a conditional node. Child order is condition (`0`), true branch (`1`), false branch (`2`).
      Definition Ternary t (f g h: path -> option nat) : path -> option nat :=
        fun p =>
          match p with
          | [] => Some t
          | 0 :: p => f p
          | 1 :: p => g p
          | 2 :: p => h p
          | _ :: _ => None
          end
      .

    Combine a list of child sizing functions under concatenation. Index `i` selects the `i`th argument.
      Definition Nary t (f_k: list (path -> option nat)) : path -> option nat :=
        fun p => match p with
               | [] => Some t
               | i :: p => match nth_error f_k i with
                           | Some f => f p
                           | None => None
                           end
               end
      .

      Reserved Notation "e '==>' t '-|' f" (at level 70).
      Reserved Notation "e '<==' t '-|' f" (at level 70).

    ## Bidirectional Judgments `synth` computes a self-determined width together with a full sizing function. `check` verifies an expression against a required width and records the resulting sizing function. These judgments implement the paper's core pair: - synthesis: `e ==> n` (written here `e ==> n -| f`), - checking: `e <== n` (written here `e <== n -| f`).
      Inductive synth : Expr -> nat -> (path -> option nat) -> Prop :=
      | AtomS : forall op f,
          f = Initial op ->
          EOperand op ==> op -| f

      | LBinOpS : forall a b t f fa fb,
          a ==> t -| fa ->
          b <== t -| fb ->
          f = Binary t fa fb ->
          EBinOp a b ==> t -| f

      | RBinOpS : forall a b t f fa fb,
          a <== t -| fa ->
          b ==> t -| fb ->
          f = Binary t fa fb ->
          EBinOp a b ==> t -| f

      | UnOpS : forall e t f fe,
          e ==> t -| fe ->
          f = Unary t fe ->
          EUnOp e ==> t -| f

      | LCompS : forall a b t f fa fb,
          a ==> t -| fa ->
          b <== t -| fb ->
          f = Binary 1 fa fb ->
          EComp a b ==> 1 -| f

      | RCompS : forall a b t f fa fb,
          a <== t -| fa ->
          b ==> t -| fb ->
          f = Binary 1 fa fb ->
          EComp a b ==> 1 -| f

      | LogicS : forall a b f ta tb fa fb,
          a ==> ta -| fa ->
          b ==> tb -| fb ->
          f = Binary 1 fa fb ->
          ELogic a b ==> 1 -| f

      | RedS : forall e t f fe,
          e ==> t -| fe ->
          f = Unary 1 fe ->
          EReduction e ==> 1 -| f

      | ShiftS : forall a b t f tb fa fb,
          a ==> t -| fa ->
          b ==> tb -| fb ->
          f = Binary t fa fb ->
          EShift a b ==> t -| f

      | LAssignS : forall lval e f fe,
          e <== lval -| fe ->
          f = Unary lval fe ->
          EAssign lval e ==> lval -| f

      | RAssignS : forall lval e f te fe,
          e ==> te -| fe ->
          lval < te ->
          f = Unary lval fe ->
          EAssign lval e ==> lval -| f

      | LCondS : forall e a b t f te fe fa fb,
          e ==> te -| fe ->
          a ==> t -| fa ->
          b <== t -| fb ->
          f = Ternary t fe fa fb ->
          ECond e a b ==> t -| f

      | RCondS : forall e a b t f te fe fa fb,
          e ==> te -| fe ->
          a <== t -| fa ->
          b ==> t -| fb ->
          f = Ternary t fe fa fb ->
          ECond e a b ==> t -| f

      | ConcatS : forall args t f ts fs,
          length args = length ts ->
          length args = length fs ->
          (forall n e te fe,
             nth_error args n = Some e ->
             nth_error ts n = Some te ->
             nth_error fs n = Some fe ->
             e ==> te -| fe) ->
          t = sum ts ->
          f = Nary t fs ->
          EConcat args ==> t -| f

      | ReplS : forall i e t f te fe,
          e ==> te -| fe ->
          t = i * te ->
          f = Unary t fe ->
          ERepl i e ==> t -| f

      where "e '==>' n '-|' f" := (synth e n f)

      with check : Expr -> nat -> (path -> option nat) -> Prop :=
      | ResizeC : forall e t f s fe,
          Resizable e ->
          e ==> s -| fe ->
          s <= t ->
          f = ReplaceRoot t fe ->
          e <== t -| f

      | BinOpC : forall a b t f fa fb,
          a <== t -| fa ->
          b <== t -| fb ->
          f = Binary t fa fb ->
          EBinOp a b <== t -| f

      | UnOpC : forall e t f fe,
          e <== t -| fe ->
          f = Unary t fe ->
          EUnOp e <== t -| f

      | ShiftC : forall a b t f tb fa fb,
          a <== t -| fa ->
          b ==> tb -| fb ->
          f = Binary t fa fb ->
          EShift a b <== t -| f

      | CondC : forall e a b t f te fe fa fb,
          e ==> te -| fe ->
          a <== t -| fa ->
          b <== t -| fb ->
          f = Ternary t fe fa fb ->
          ECond e a b <== t -| f

      where "e '<==' n '-|' f" := (check e n f)
      .

    Utility tactic that inverts synthesis/checking derivations and `Resizable` witnesses. Used throughout structural proofs on derivations.
      Ltac inv_ts :=
        match goal with
        | [ H: _ _ ==> _ -| _ |- _ ] => inv H; try inv_ts
        | [ H: _ _ <== _ -| _ |- _ ] => inv H; try inv_ts
        | [ H: Resizable _ |- _ ] => inv H
        end
      .

    Root soundness for synthesis: the root path `[]` always maps to the synthesized width.
      Lemma synth_root : forall e t f, e ==> t -| f -> f [] = Some t.
      Proof.
        intros. inv H; reflexivity.
      Qed.

    Root soundness for checking: the root path `[]` always maps to the checked width.
      Lemma check_root : forall e t f, e <== t -| f -> f [] = Some t.
      Proof.
        intros. inv H; reflexivity.
      Qed.

    Induction hypothesis schema for concatenation arguments. It states per-argument determinism (same synthesized width and function for two synthesis derivations of the same child).
      Definition concat_inj_hyp args :=
        forall (n : nat) (e : Expr),
          nth_error args n = Some e ->
          forall (t1 t2 : nat) (f1 f2 : path -> option nat),
            e ==> t1 -| f1 ->
            e ==> t2 -| f2 ->
            t1 = t2 /\ (forall p : path, f1 p = f2 p).

    Determinism of synthesized root width for concatenation, assuming per-argument determinism.
      Lemma concat_synth_inj_t: forall args f1 f2 t1 t2,
        concat_inj_hyp args -> EConcat args ==> t1 -| f1 -> EConcat args ==> t2 -| f2 ->
        t1 = t2.
      Proof.
        intros ? ? ? ? ? He H H0. inv H. inv H0.
        assert (Heqt: forall n t1 t2,
                   nth_error ts n = Some t1 -> nth_error ts0 n = Some t2 -> t1 = t2).
        - intros. repeat gen_nth. destruct (He _ _ H7 t1 t2 x1 x0); firstorder.
        - assert (Heql: ts = ts0). apply nth_ext with (d := 0) (d' := 0).
          rewrite H2 in *. assumption. intros. apply Heqt with (n := n).
          apply (nth_error_nth' _ _ H). rewrite <- H2 in H. rewrite H1 in H.
          apply (nth_error_nth' _ _ H). subst. reflexivity.
      Qed.

    Determinism of synthesized sizing function for concatenation, assuming per-argument determinism.
      Lemma concat_synth_inj_f: forall args t1 t2 f1 f2,
        concat_inj_hyp args -> EConcat args ==> t1 -| f1 -> EConcat args ==> t2 -| f2 ->
        forall p, f1 p = f2 p.
      Proof.
        intros ? ? ? ? ? He H H0.
        assert (Heq: t1 = t2) by apply (concat_synth_inj_t _ _ _ _ _ He H H0).
        inv H. inv H0. intros.
        assert (Heqf:
                 forall n f1 f2, nth_error fs n = Some f1 -> nth_error fs0 n = Some f2 ->
                                 forall p, f1 p = f2 p).
        { intros. repeat gen_nth. destruct (He _ _ H8 x2 x0 f1 f2); firstorder. }
        destruct p; try reflexivity. simpl. destruct (nth_error fs n) eqn:Hfs.
        - repeat gen_nth. rewrite H0. apply Heqf with (n := n); assumption.
        - destruct (nth_error fs0 n) eqn:Hfs0; try reflexivity. exfalso. repeat gen_nth.
          rewrite H1 in Hfs. discriminate Hfs.
      Qed.

    Pointwise monotonicity for concatenation follows from function determinism in this setting.
      Lemma concat_synth_order_f: forall args t1 t2 f1 f2,
        concat_inj_hyp args -> EConcat args ==> t1 -| f1 -> EConcat args ==> t2 -| f2 ->
        forall p, le_option_nat (f1 p) (f2 p).
      Proof.
        intros ? ? ? ? ? He H H0 p.
        assert (Heq: forall p, f1 p = f2 p) by apply (concat_synth_inj_f _ _ _ _ _ He H H0).
        rewrite Heq. reflexivity.
      Qed.

    Checking is upward closed. If an expression checks at width `t`, it also checks at any larger width. This is the operational form of "expressions can grow" used in the synthesis/checking correspondence proof.
      Theorem check_can_grow :
        forall e t f, e <== t -| f -> forall s, t <= s -> exists f', e <== s -| f'.
      Proof.
        Ltac _check_can_grow_tac :=
          match goal with
          | [ HRes: Resizable _, H: _ ==> ?x -| _, Hle: ?x <= ?y |- ?e <== ?z -| _ ] =>
              apply (ResizeC _ _ _ _ _ HRes H); try reflexivity;
              apply (le_trans x y z); eassumption
          | [ H: _ <== _ -| _ |- ex _ ] => inv H; eexists; _check_can_grow_tac
          end
        .
        induction e using Expr_ind; intros; try _check_can_grow_tac.
        - inv H. inv H1. edestruct IHe1; edestruct IHe2; try eassumption.
          eexists. econstructor; eassumption || reflexivity.
        - inv H. inv H1. edestruct IHe; try eassumption. eexists.
          econstructor; eassumption || reflexivity.
        - inv H. inv H1. edestruct IHe1; try eassumption. eexists.
          apply (ShiftC _ _ _ _ _ _ _ H H4). reflexivity.
        - inv H. inv H1. edestruct IHe2; edestruct IHe3; try eassumption.
          eexists. eapply (CondC _ _ _ _ _ _ _ _ _ H4); eassumption || reflexivity.
      Qed.

    Master structural lemma collecting key metatheory for one expression: - synthesis/checking order (`t <= s`), - synthesis determinism on widths, - determinism of sizing functions (synth/synth, check/check, synth/check), - pointwise monotonicity of sizing functions. In the paper, these components support the determinism and synthesis-checking correspondence results (Lemma 2 and Lemma 3).
      Lemma check_grow_synth_and_synth_inj :
        forall e,
        (forall t s f1 f2, e ==> t -| f1 -> e <== s -| f2 -> t <= s) /\
        (forall t1 t2 f1 f2, e ==> t1 -| f1 -> e ==> t2 -| f2 -> t1 = t2) /\
        (forall t f1 f2, e ==> t -| f1 -> e ==> t -| f2 -> forall p, f1 p = f2 p) /\
        (forall t f1 f2, e <== t -| f1 -> e <== t -| f2 -> forall p, f1 p = f2 p) /\
        (forall t f1 f2, e ==> t -| f1 -> e <== t -| f2 -> forall p, f1 p = f2 p) /\
        (forall t s f1 f2, e ==> t -| f1 -> e <== s -| f2 ->
                           forall p, le_option_nat (f1 p) (f2 p)) /\
        (forall t s f1 f2, e <== t -| f1 -> e <== s -| f2 -> t <= s ->
                           forall p, le_option_nat (f1 p) (f2 p)).
      Proof.
        Ltac _eq_gen_inj :=
          match goal with
          | [ A: ?e ==> ?t -| _, B: ?e ==> ?s -| _, H: forall _ _ _ _, _ -> _ -> _ = _ |- _ ] =>
              let Heq := fresh in assert (Heq: t = s) by apply (H _ _ _ _ A B);
                                  clear H; subst
          | [ A: ?e ==> ?t -| _, B: ?e <== ?s -| _, H: forall _ _ _ _, _ -> _ -> _ <= _ |- _ ] =>
              let Hlt := fresh in assert (Hlt: t <= s) by apply (H _ _ _ _ A B);
                                  clear H; try _eq_gen_inj; try lia
          | [ H: ?a <= ?b, P: ?b <= ?a |- _ ] =>
              let Heq := fresh in assert (Heq: a = b) by apply (le_antisymm _ _ H P);
                                  clear H; clear P; subst
          end
        .
        Ltac _tac_inj :=
          match goal with
          (* Values *)
          | [ |- _ = _ ] => _eq_gen_inj; auto
          | [ A: ?e ==> ?t -| _, B: ?e <== ?s -| _, H: forall _ _ _ _, _ -> _ -> _ <= _ |- ?t <= ?s ] =>
              apply (H _ _ _ _ A B)
          | [ A: ?e ==> ?t -| _, B: ?e ==> ?s -| _, H: forall _ _ _ _, _ -> _ -> _ = _ |- _ ] =>
              let Heq := fresh in assert (Heq: t = s) by apply (H _ _ _ _ A B);
                                  clear H; subst; auto; _tac_inj
          (* Functions *)
          (* - Synth & Check *)
          | [ A: ?e ==> ?t -| _, B: ?e <== ?t -| _,
                  H: forall _ _ _, _ -> _ -> forall _, _ = _ |- _ _ = _ _ ] =>
              apply (H _ _ _ A B) || symmetry; apply (H _ _ _ A B)
          (* Both synth *)
          | [ A: ?e ==> ?t -| _, B: ?e ==> ?t -| _,
                  H: forall _ _ _, _ -> _ -> forall _, _ = _ |- _ _ = _ _ ] =>
              try _eq_gen_inj; apply (H _ _ _ A B)
            (* Both check *)
          | [ A: ?e <== ?t -| ?f1, B: ?e <== ?t -| ?f2,
                  H: forall _ _ _, _ -> _ -> forall _, _ = _ |- ?f1 _ = ?f2 _ ] =>
              apply (H _ _ _ A B)
          | [ A: ?e ==> _ -| _, B: ?e <== _ -| _,
                  H: forall _ _ _ _, _ -> _ -> forall _, le_option_nat _ _
                                             |- le_option_nat _ _ ] =>
              apply (H _ _ _ _ A B)
          | [ A: ?e <== ?t -| _, B: ?e <== ?s -| _, C: ?t <= ?s,
                    H: forall _ _ _ _, _ -> _ -> _ -> forall _, le_option_nat _ _
                                                   |- le_option_nat _ _ ] =>
              apply (H _ _ _ _ A B C)
          | [ A: ?e ==> ?t -| _, B: ?e ==> ?t -| _,
                  H: forall _ _ _, _ -> _ -> forall _, _ = _ |- le_option_nat _ _ ] =>
              rewrite (H _ _ _ A B); reflexivity
          | [ A: ?e <== ?t -| _, B: ?e <== ?t -| _,
                  H: forall _ _ _, _ -> _ -> forall _, _ = _ |- le_option_nat _ _ ] =>
              rewrite (H _ _ _ A B); reflexivity
          | [ A: ?e ==> ?t -| _, B: ?e <== ?t -| _,
                  H: forall _ _ _, _ -> _ -> forall _, _ = _ |- le_option_nat _ _ ] =>
              rewrite (H _ _ _ A B); reflexivity
          | [ H: forall _ _, nth_error _ _ = Some _ -> _, G: nth_error _ _ = Some _ |- _ ] =>
              specialize (H _ _ G); repeat splitHyp; split; intros
          end
        .
        induction e using Expr_ind; repeat splitAnd; intros; repeat splitHyp;
        try (try (destruct p as [|[|[|[]]]]); inv_ts; simpl; repeat _eq_gen_inj;
             auto; try reflexivity; repeat _tac_inj; fail);
        assert (concat_inj_hyp args) by (unfold concat_inj_hyp; intros; repeat _tac_inj).
        - inv H1. assert _ by apply (concat_synth_inj_t _ _ _ _ _ H2 H0 H4).
          subst. assumption.
        - apply (concat_synth_inj_t _ _ _ _ _ H3 H1 H2).
        - apply (concat_synth_inj_f _ _ _ _ _ H4 H2 H3).
        - inv H3. inv H4. destruct p; simpl.
          + reflexivity.
          + apply (concat_synth_inj_f _ _ _ _ _ H5 H7 H9).
        - inv H5. destruct p; simpl.
          + apply (synth_root _ _ _ H4).
          + apply (concat_synth_inj_f _ _ _ _ _ H6 H4 H8).
        - inv H6. _eq_gen_inj. simpl. destruct p.
          + rewrite (synth_root _ _ _ H5). trivial.
          + apply (concat_synth_order_f _ _ _ _ _ H7 H5 H9).
        - inv H6. inv H7. _eq_gen_inj. simpl. destruct p.
          + assumption.
          + apply (concat_synth_order_f _ _ _ _ _ H9 H11 H13).
      Qed.


    If `e` synthesizes to `t` and checks at `s`, then `t <= s`. This is one direction of the paper's Synthesis-Checking Correspondence (Lemma 3).
      Theorem synth_check_order :
        forall e t s f1 f2, e ==> t -| f1 -> e <== s -| f2 -> t <= s.
      Proof.
        intros. destruct (check_grow_synth_and_synth_inj e). apply (H1 _ _ _ _ H H0).
      Qed.

    Determinism of synthesized width. Corresponds to part (1) of the paper's Derivation Determinism (Lemma 2).
      Theorem synth_inj :
        forall e t1 t2 f1 f2, e ==> t1 -| f1 -> e ==> t2 -| f2 -> t1 = t2.
      Proof.
        intros. destruct (check_grow_synth_and_synth_inj e).
        repeat splitHyp. apply (H2 _ _ _ _ H H0).
      Qed.

    Determinism of synthesized sizing function (up to extensional equality).
      Theorem synth_inj_f :
        forall e t1 t2 f1 f2, e ==> t1 -| f1 -> e ==> t2 -| f2 -> forall p, f1 p = f2 p.
      Proof.
        intros. destruct (check_grow_synth_and_synth_inj e).
        repeat splitHyp. rewrite (H2 _ _ _ _ H H0) in H. apply (H3 _ _ _ H H0).
      Qed.

    Agreement of synthesis and checking functions when target widths are equal.
      Theorem synth_check_inj_f :
        forall e t f1 f2, e ==> t -| f1 -> e <== t -| f2 -> forall p, f1 p = f2 p.
      Proof.
        intros. destruct (check_grow_synth_and_synth_inj e). firstorder.
      Qed.

    Determinism of checking sizing functions for a fixed target width. This corresponds to part (2) of paper Derivation Determinism (Lemma 2).
      Theorem check_inj_f :
        forall e t f1 f2, e <== t -| f1 -> e <== t -| f2 -> forall p, f1 p = f2 p.
      Proof.
        intros. destruct (check_grow_synth_and_synth_inj e). firstorder.
      Qed.

    Pointwise monotonicity from synthesis to checking: values recorded in synthesized paths do not exceed checked values.
      Theorem synth_check_order_f : forall e t s f1 f2,
        e ==> t -| f1 ->
        e <== s -| f2 ->
        forall p n1 n2,
          f1 p = Some n1 ->
          f2 p = Some n2 ->
          n1 <= n2.
      Proof.
        intros. destruct (check_grow_synth_and_synth_inj e). unfold le_option_nat in *.
        repeat splitHyp. apply (H8 _ _ _ _ H) with (p := p) in H0. rewrite H1 in H0.
        rewrite H2 in H0. assumption.
      Qed.

    Pointwise monotonicity between two checking derivations, assuming root width order.
      Theorem check_order_f : forall e t s f1 f2,
        e <== t -| f1 -> e <== s -| f2 -> t <= s ->
        forall p n1 n2, f1 p = Some n1 -> f2 p = Some n2 -> n1 <= n2.
      Proof.
        intros. destruct (check_grow_synth_and_synth_inj e). unfold le_option_nat in *.
        repeat splitHyp. apply (H10 _ _ _ _ H H0) with (p := p) in H1. rewrite H2 in H1.
        rewrite H3 in H1. assumption.
      Qed.

    From synthesis to checking at any larger width. Together with `synth_check_order`, this yields the iff in theorem `synth_check` below (paper Synthesis-Checking Correspondence, Lemma 3).
      Lemma synth_can_check :
        forall e t s f, e ==> t -| f -> t <= s -> exists g, e <== s -| g.
      Proof.
        induction e using Expr_ind; intros;
          try (eexists; eapply ResizeC with (s := t0);
               [constructor | eassumption | assumption | reflexivity]).
        - inv H.
          + destruct (IHe1 _ _ _ H3 H0). destruct (check_can_grow _ _ _ H4 _ H0).
            eexists. eapply BinOpC; eassumption || reflexivity.
          + destruct (IHe2 _ _ _ H4 H0). destruct (check_can_grow _ _ _ H3 _ H0).
            eexists. eapply BinOpC; eassumption || reflexivity.
        - inv H. destruct (IHe _ _ _ H2 H0). eexists.
          econstructor; eassumption || reflexivity.
        - inv H. destruct (IHe1 _ _ _ H3 H0). eexists. apply (ShiftC _ _ _ _ _ _ _ H H4).
          reflexivity.
        - inv H.
          + destruct (IHe2 _ _ _ H5 H0). destruct (check_can_grow _ _ _ H8 _ H0).
            eexists. apply (CondC _ _ _ _ _ _ _ _ _ H4 H H1). reflexivity.
          + destruct (IHe3 _ _ _ H8 H0). destruct (check_can_grow _ _ _ H5 _ H0).
            eexists. apply (CondC _ _ _ _ _ _ _ _ _ H4 H1 H). reflexivity.
      Qed.

    Synthesis-checking correspondence: an expression checks at width `s` iff `s` is at least its synthesized width. This is the formal counterpart of the paper's Synthesis-Checking Correspondence (Lemma 3).
      Theorem synth_check :
        forall e t f, e ==> t -| f -> forall s, t <= s <-> exists g, e <== s -| g.
      Proof.
        split; intros.
        - apply (synth_can_check _ _ _ _ H H0).
        - destruct H0. apply (synth_check_order _ _ _ _ _ H H0).
      Qed.

    Structural characterization of domains of sizing functions. For both synth and check, a path is valid in the expression iff the produced function is defined at that path.
      Lemma func_on_path : forall e,
        (forall t f, e ==> t -| f -> forall p, IsPath e p <-> exists n, f p = Some n) /\
        (forall t f, e <== t -| f -> forall p, IsPath e p <-> exists n, f p = Some n).
      Proof.
        Ltac _invHyp_fun_path :=
          match goal with
          | [ H: IsPath (_ _) _ |- _ ] => inv H
          | [ H: ex _ |- _ ] => inv H
          end
        .
        Ltac _tac_fun_path :=
          match goal with
          | [ H1: _ ==> _ -| _, H2: forall _ _, _ ==> _ -| _ -> _ |- _ ] =>
            try constructor; rewrite (H2 _ _ H1); eexists; eassumption
          | [ H1: _ <== _ -| _, H2: forall _ _, _ <== _ -| _ -> _ |- _ ] =>
              try constructor; rewrite (H2 _ _ H1); eexists; eassumption
          | [ |- IsPath _ [] ] => constructor
          end
        .
        induction e using Expr_ind; repeat split; intros; repeat splitHyp;
          inv_ts; repeat _invHyp_fun_path; try (try (eexists; reflexivity); firstorder);
          try (destruct p as [|[|[|[]]]]; simpl in *; discriminate H || inv H;
               _tac_fun_path).
        - destruct (H _ _ H2). repeat gen_nth. simpl. rewrite H7.
          assert (He: e ==> x0 -| x) by apply (H5 _ _ _ _ H2 H4 H7). firstorder.
        - destruct p; simpl in *; discriminate H0 || inv H0. constructor.
          destruct (nth_error fs n) eqn:Hnth. repeat gen_nth. econstructor. eassumption.
          destruct (H _ _ H0). apply (H5 _ _ _ _ H0 H1) in Hnth. _tac_fun_path.
          discriminate H2.
        - destruct (H _ _ H2). repeat gen_nth. simpl. rewrite H8.
          assert (He: e ==> x0 -| x) by apply (H7 _ _ _ _ H2 H6 H8). firstorder.
        - destruct p; simpl in *; discriminate H0 || inv H0. constructor.
          destruct (nth_error fs n) eqn:Hnth. repeat gen_nth. econstructor. eassumption.
          destruct (H _ _ H0). apply (H7 _ _ _ _ H0 H1) in Hnth. _tac_fun_path.
          discriminate H2.
      Qed.

    Specialization of `func_on_path` to synthesis derivations.
      Theorem synth_f_path :
        forall e t f, e ==> t -| f -> forall p, IsPath e p <-> exists n, f p = Some n.
      Proof.
        intros e. destruct (func_on_path e). assumption.
      Qed.


    Specialization of `func_on_path` to checking derivations.
      Theorem check_f_path :
        forall e t f, e <== t -| f -> forall p, IsPath e p <-> exists n, f p = Some n.
      Proof.
        intros e. destruct (func_on_path e). assumption.
      Qed.

    Subexpression decomposition of sizing functions. For any successful subexpression lookup `e @[p] = Some e'`, the derivation on `e` induces a derivation on `e'` whose function agrees with the parent function on all suffixes `p ++ k`. This is the technical core behind the paper's sub-expression correspondence lemmas.
      Lemma f_sub_exp : forall e,
        (forall t f,
           e ==> t -| f ->
           forall p e',
           e @[p] = Some e' ->
           exists t' f', (e' ==> t' -| f' \/ e' <== t' -| f') /\ forall k, f (p ++ k) = f' k)
        /\ (forall t f,
              e <== t -| f ->
              forall p e',
              e @[p] = Some e' ->
              exists t' f',
                (e' ==> t' -| f' \/ e' <== t' -| f') /\ forall k, f (p ++ k) = f' k).
      Proof.
        Ltac _inv_se_f :=
          match goal with
          | [ H: (_ _) @[ _ ] = _ |- _ ] => inv H
          end
        .
        induction e using Expr_ind; split; intros; repeat splitHyp;
          try (destruct p as [|[|[|[]]]]; _inv_se_f;
               try (exists t0; exists f; split; auto; intros; reflexivity);
               repeat inv_ts; firstorder; fail).
        - destruct p; _inv_se_f.
          + exists t0; exists f; split; auto; intros; reflexivity.
          + destruct (nth_error args n) eqn:Hnth; try congruence.
            specialize (H _ _ Hnth). destruct H as [Hs Hc].
            repeat inv_ts. repeat gen_nth. specialize (H4 _ _ _ _ Hnth H0 H).
            simpl. rewrite H. firstorder.
        - destruct p; _inv_se_f.
          + exists t0; exists f; split; auto; intros; reflexivity.
          + destruct (nth_error args n) eqn:Hnth; try congruence.
            specialize (H _ _ Hnth). destruct H as [Hs Hc].
            repeat inv_ts. repeat gen_nth. specialize (H6 _ _ _ _ Hnth H0 H).
            simpl. rewrite H. firstorder.
      Qed.

    Synthesis-side sub-expression correspondence. Matches the paper's Sub-expression Synthesis result (Lemma 4).
      Theorem synth_sub_expr : forall e t f p e',
        e ==> t -| f -> e @[p] = Some e' ->
        exists t' f', (e' ==> t' -| f' \/ e' <== t' -| f') /\ forall k, f (p ++ k) = f' k.
      Proof.
        intros. destruct (f_sub_exp e). firstorder.
      Qed.

    Checking-side sub-expression correspondence. Matches the paper's Sub-expression Checking result (Lemma 5).
      Theorem check_sub_expr : forall e t f p e',
        e <== t -| f -> e @[p] = Some e' ->
        exists t' f', (e' ==> t' -| f' \/ e' <== t' -| f') /\ forall k, f (p ++ k) = f' k.
      Proof.
        intros. destruct (f_sub_exp e). firstorder.
      Qed.

    Totality of synthesis: Every expression admits a synthesis derivation. This corresponds to part (1) of the paper's Universal Derivations (Lemma 1).
      Theorem always_synth : forall e, exists t f, e ==> t -| f.
      Proof.
        induction e using Expr_ind; repeat existsHyp;
          try (eexists; eexists; econstructor; eassumption || reflexivity).
        - destruct (max_dec_bis x1 x) as [[H1 H2]|[H1 H2]].
          + destruct (synth_can_check _ _ _ _ H H2).
            eexists; eexists; econstructor; eassumption || reflexivity.
          + destruct (synth_can_check _ _ _ _ H0 H2).
            eexists; eexists; econstructor; eassumption || reflexivity.
        - destruct (max_dec_bis x1 x) as [[H1 H2]|[H1 H2]].
          + destruct (synth_can_check _ _ _ _ H H2).
            eexists; eexists; econstructor; eassumption || reflexivity.
          + destruct (synth_can_check _ _ _ _ H0 H2).
            eexists; eexists; econstructor; eassumption || reflexivity.
        - destruct (le_gt_dec x op).
          + destruct (synth_can_check _ _ _ _ H l).
            eexists; eexists; econstructor; eassumption || reflexivity.
          + eexists; eexists; econstructor; eassumption || reflexivity.
        - destruct (max_dec_bis x1 x) as [[H2 H3]|[H2 H3]].
          + destruct (synth_can_check _ _ _ _ H H3).
            eexists; eexists; econstructor; eassumption || reflexivity.
          + destruct (synth_can_check _ _ _ _ H0 H3).
            eexists; eexists; econstructor; eassumption || reflexivity.
        - assert (Hfs: exists ts fs,
                     length args = length ts /\
                     length args = length fs /\
                     forall n e t f,
                    nth_error args n = Some e ->
                    nth_error ts n = Some t ->
                    nth_error fs n = Some f -> e ==> t -| f).
          + induction args.
            * exists []. exists []. repeat split. intros []; intros; discriminate H0.
            * destruct IHargs. intros. apply (H (S n) e H0). existsHyp.
              repeat splitHyp. destruct (H 0 a (Logic.eq_refl _)) as [t [f ?H]] .
              exists (t :: x). exists (f :: x0). repeat split; simpl; try congruence.
              intros. destruct n.
              -- inv H4. inv H5. inv H6. assumption.
              -- simpl in *. firstorder.
          + destruct Hfs as [ts [fs [H1 [H2 H3]]]].
            eexists; eexists; econstructor; eassumption || reflexivity.
      Qed.

    Totality of checking: Every expression checks against some width. This corresponds to part (2) of the paper's Universal Derivations(Lemma 1).
      Theorem always_check : forall e, exists t f, e <== t -| f.
      Proof.
        intros. destruct (always_synth e) as [t [f H]]. exists t.
        apply (synth_can_check _ _ _ _ H (le_refl _)).
      Qed.

    Auxiliary predicate used to state minimality: `P e s` means `e` checks at every width `t >= s`.
      Definition P e s := forall t, s <= t -> exists g, e <== t -| g.

    Minimality principle for synthesized widths. If `s` is the least lower bound of widths allowing checking, then `e` synthesizes at width `s`. This formalizes the paper's minimality statement (Theorem 1, "Synthesis as Minimal Width").
      Theorem synth_minimal_check :
        forall e s, P e s -> (forall u, P e u -> s <= u) -> exists f, e ==> s -| f.
      Proof.
        unfold P. intros. destruct always_synth with (e := e) as [t [f Hx]].
        assert (Heq: s = t).
        { apply le_antisymm.
          - apply H0. intros. rewrite <- synth_check; eassumption.
          - destruct (H s). reflexivity.
            rewrite synth_check; try eexists; eassumption.
        } subst. exists f. assumption.
      Qed.
    End TypeSystem.
    Generated by rocqnavi