From 8afc84940bbd1be925e375782f74ba576ee7f284 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 15 Jun 2026 14:39:08 +0100 Subject: [PATCH 1/3] fix(formal/coq): repair Coq mechanization so the safety core actually checks The Coq formalization never compiled. Faults found and fixed: - `omega` (removed in Coq 8.12+) -> `lia`. - `value_eqb`/`phr_type_eqb` used a mutual `Fixpoint ... with` across phr_type and list, which Coq's guard checker rejects (not mutually inductive) -> rewritten with the nested-`fix` idiom. - `value_eqb_refl` invoked a nonexistent phr_value_rect P0/P1 eliminator -> two strong (nested) induction principles phr_type_ind'/phr_value_ind' added. - `phr_type_eq_dec`'s `decide equality` could not dispatch nested TRecord -> genuinely decidable now (this is the obligation that was unsound in Agda). - `preservation` was missing the T_List case, elided the record-field case, and lost the empty context in the EVar case -> reproved by induction on evaluation (keeps [] concrete); T_List via a list helper; field case closed by stating VT_Record over field_lookup. - `eval_deterministic` had a variable-name clash + miscalibrated bullets -> uniform IH-driven tactic. - `no_system_calls` was unsound (ELit (VString "system") satisfied it) and ill-typed (untyped existential) -> honest by-construction sandbox_no_call_form. - `totality` was malformed (Theorem ... with Fixpoint) and false as stated (no typing hypothesis) -> free_vars extracted; restated correctly and left as the lone explicit Admitted (termination, not yet mechanized, unused by core). Result: `coqc Phronesis.v` exits 0. `Print Assumptions` on preservation, eval_deterministic, type_safety, phr_type_eq_dec, subtype_trans, value_eqb_refl, literal_preservation, sandbox_no_call_form = "Closed under the global context" (axiom-free). SPDX header left unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) --- academic/formal-verification/coq/Phronesis.v | 462 +++++++++++-------- 1 file changed, 272 insertions(+), 190 deletions(-) diff --git a/academic/formal-verification/coq/Phronesis.v b/academic/formal-verification/coq/Phronesis.v index f7a3e81..1a2cbd1 100644 --- a/academic/formal-verification/coq/Phronesis.v +++ b/academic/formal-verification/coq/Phronesis.v @@ -9,7 +9,7 @@ Require Import Coq.Bool.Bool. Require Import Coq.Arith.Arith. Require Import Coq.Logic.Decidable. Require Import Coq.Program.Wf. -Require Import Coq.omega.Omega. +Require Import Lia. Import ListNotations. (** * 1. Types *) @@ -27,12 +27,97 @@ Inductive phr_type : Type := | TTop : phr_type | TBot : phr_type. -(** Type equality is decidable *) +(** A strong (nested) induction principle for [phr_type]. + + The auto-generated [phr_type_ind] gives NO induction hypothesis for the + elements of a [TRecord] field list (the recursion nests through [list] and + [prod], which are not part of [phr_type]'s inductive block). This principle + supplies a [Forall]-packaged IH for every field, and is reused below for + decidable equality. The list traversal is an explicit nested [fix] so the + guard checker accepts the recursive calls. *) +Fixpoint phr_type_ind' (P : phr_type -> Prop) + (HInt : P TInt) (HFloat : P TFloat) (HString : P TString) (HBool : P TBool) + (HIP : P TIP) (HDateTime : P TDateTime) + (HList : forall t, P t -> P (TList t)) + (HRecord : forall fs, Forall (fun p => P (snd p)) fs -> P (TRecord fs)) + (HNull : P TNull) (HTop : P TTop) (HBot : P TBot) + (t : phr_type) {struct t} : P t := + match t with + | TInt => HInt | TFloat => HFloat | TString => HString | TBool => HBool + | TIP => HIP | TDateTime => HDateTime + | TList a => HList a (phr_type_ind' P HInt HFloat HString HBool HIP HDateTime + HList HRecord HNull HTop HBot a) + | TRecord fs => HRecord fs + ((fix flds (l : list (string * phr_type)) : Forall (fun p => P (snd p)) l := + match l with + | [] => Forall_nil _ + | p :: l' => Forall_cons p + (phr_type_ind' P HInt HFloat HString HBool HIP HDateTime + HList HRecord HNull HTop HBot (snd p)) (flds l') + end) fs) + | TNull => HNull | TTop => HTop | TBot => HBot + end. + +(** Boolean type equality. + + [decide equality] cannot dispatch the nested [TRecord (list (string * + phr_type))] case, and a mutual [Fixpoint ... with] across [phr_type] and + [list] is rejected by Coq's guard checker (they are not mutually inductive). + We therefore use an explicit nested [fix] for the field list. *) +Fixpoint phr_type_eqb (t1 t2 : phr_type) {struct t1} : bool := + match t1, t2 with + | TList a, TList b => phr_type_eqb a b + | TRecord fs, TRecord gs => + (fix flds (xs ys : list (string * phr_type)) {struct xs} : bool := + match xs, ys with + | [], [] => true + | (f,a)::xs', (g,b)::ys' => + String.eqb f g && phr_type_eqb a b && flds xs' ys' + | _, _ => false + end) fs gs + | TInt, TInt => true | TFloat, TFloat => true | TString, TString => true + | TBool, TBool => true | TIP, TIP => true | TDateTime, TDateTime => true + | TNull, TNull => true | TTop, TTop => true | TBot, TBot => true + | _, _ => false + end. + +(** [phr_type_eqb] is reflexive. *) +Lemma phr_type_eqb_refl : forall t, phr_type_eqb t t = true. +Proof. + induction t using phr_type_ind'; simpl; try reflexivity. + - exact IHt. + - induction fs as [| p fs' IHfs]; simpl. + + reflexivity. + + inversion H; subst. destruct p as [f a]; simpl in *. + rewrite String.eqb_refl, H2. simpl. apply IHfs. exact H3. +Qed. + +(** [phr_type_eqb] reflects equality (soundness). *) +Lemma phr_type_eqb_true : forall t1 t2, phr_type_eqb t1 t2 = true -> t1 = t2. +Proof. + induction t1 using phr_type_ind'; intros t2 Heq; destruct t2; simpl in Heq; + try discriminate; try reflexivity. + - f_equal. + match goal with IH : forall u, phr_type_eqb ?a u = true -> ?a = u |- _ => + apply IH; exact Heq end. + - f_equal. + match goal with HF : Forall _ _ |- _ => rename HF into Hall end. + revert l Heq. + induction Hall as [| p fs' Hhd Htail IHfs]. + + intros [| q gs'] Heq; simpl in Heq; try discriminate. reflexivity. + + destruct p as [f a]. intros [| [g b] gs'] Heq; simpl in Heq; try discriminate. + apply andb_prop in Heq. destruct Heq as [Hh Htl]. + apply andb_prop in Hh. destruct Hh as [Hfg Hab]. + apply String.eqb_eq in Hfg. simpl in Hhd. apply Hhd in Hab. + apply IHfs in Htl. subst. reflexivity. +Qed. + +(** Type equality is decidable (derived from the reflective Boolean equality). *) Lemma phr_type_eq_dec : forall (t1 t2 : phr_type), {t1 = t2} + {t1 <> t2}. Proof. - decide equality. - - decide equality. apply String.string_dec. - - decide equality. apply String.string_dec. + intros t1 t2. destruct (phr_type_eqb t1 t2) eqn:E. + - left. apply phr_type_eqb_true. exact E. + - right. intro H. subst. rewrite phr_type_eqb_refl in E. discriminate. Defined. (** * 2. Values *) @@ -48,8 +133,42 @@ Inductive phr_value : Type := | VRecord : list (string * phr_value) -> phr_value | VNull : phr_value. -(** Value equality is decidable *) -Fixpoint value_eqb (v1 v2 : phr_value) : bool := +(** A strong (nested) induction principle for [phr_value] (cf. [phr_type_ind']); + supplies a [Forall]-packaged IH for [VList] elements and [VRecord] fields. *) +Fixpoint phr_value_ind' (P : phr_value -> Prop) + (HInt : forall z, P (VInt z)) (HFloat : forall z, P (VFloat z)) + (HString : forall s, P (VString s)) (HBool : forall b, P (VBool b)) + (HIP : forall a b c d, P (VIP a b c d)) (HDateTime : forall z, P (VDateTime z)) + (HList : forall vs, Forall P vs -> P (VList vs)) + (HRecord : forall fs, Forall (fun p => P (snd p)) fs -> P (VRecord fs)) + (HNull : P VNull) + (v : phr_value) {struct v} : P v := + match v with + | VInt z => HInt z | VFloat z => HFloat z | VString s => HString s + | VBool b => HBool b | VIP a b c d => HIP a b c d | VDateTime z => HDateTime z + | VList vs => HList vs + ((fix lst (l : list phr_value) : Forall P l := + match l with + | [] => Forall_nil _ + | x :: l' => Forall_cons x + (phr_value_ind' P HInt HFloat HString HBool HIP HDateTime + HList HRecord HNull x) (lst l') + end) vs) + | VRecord fs => HRecord fs + ((fix rcd (l : list (string * phr_value)) : Forall (fun p => P (snd p)) l := + match l with + | [] => Forall_nil _ + | p :: l' => Forall_cons p + (phr_value_ind' P HInt HFloat HString HBool HIP HDateTime + HList HRecord HNull (snd p)) (rcd l') + end) fs) + | VNull => HNull + end. + +(** Value equality is decidable (nested [fix] for the [VList]/[VRecord] + children, since a mutual [Fixpoint ... with] across [phr_value] and [list] + is rejected by Coq's guard checker). *) +Fixpoint value_eqb (v1 v2 : phr_value) {struct v1} : bool := match v1, v2 with | VInt n1, VInt n2 => Z.eqb n1 n2 | VFloat f1, VFloat f2 => Z.eqb f1 f2 @@ -58,40 +177,43 @@ Fixpoint value_eqb (v1 v2 : phr_value) : bool := | VIP a1 b1 c1 d1, VIP a2 b2 c2 d2 => Nat.eqb a1 a2 && Nat.eqb b1 b2 && Nat.eqb c1 c2 && Nat.eqb d1 d2 | VDateTime t1, VDateTime t2 => Z.eqb t1 t2 - | VList l1, VList l2 => list_eqb l1 l2 - | VRecord r1, VRecord r2 => record_eqb r1 r2 + | VList l1, VList l2 => + (fix lst (xs ys : list phr_value) {struct xs} : bool := + match xs, ys with + | [], [] => true + | x::xs', y::ys' => value_eqb x y && lst xs' ys' + | _, _ => false + end) l1 l2 + | VRecord r1, VRecord r2 => + (fix rcd (xs ys : list (string * phr_value)) {struct xs} : bool := + match xs, ys with + | [], [] => true + | (f,x)::xs', (g,y)::ys' => String.eqb f g && value_eqb x y && rcd xs' ys' + | _, _ => false + end) r1 r2 | VNull, VNull => true | _, _ => false - end -with list_eqb (l1 l2 : list phr_value) : bool := - match l1, l2 with - | [], [] => true - | v1 :: vs1, v2 :: vs2 => value_eqb v1 v2 && list_eqb vs1 vs2 - | _, _ => false - end -with record_eqb (r1 r2 : list (string * phr_value)) : bool := - match r1, r2 with - | [], [] => true - | (f1, v1) :: rest1, (f2, v2) :: rest2 => - String.eqb f1 f2 && value_eqb v1 v2 && record_eqb rest1 rest2 - | _, _ => false end. -(** value_eqb reflects equality *) +(** value_eqb reflects equality (reflexive direction). *) Lemma value_eqb_refl : forall v, value_eqb v v = true. Proof. - induction v using phr_value_rect with - (P0 := fun l => list_eqb l l = true) - (P1 := fun r => record_eqb r r = true); - simpl; auto. + induction v using phr_value_ind'; simpl; try reflexivity. - apply Z.eqb_refl. - apply Z.eqb_refl. - apply String.eqb_refl. - - destruct b; auto. - - rewrite !Nat.eqb_refl. simpl. auto. + - destruct b; reflexivity. + - rewrite !Nat.eqb_refl. reflexivity. - apply Z.eqb_refl. - - rewrite IHv, IHv0. auto. - - rewrite String.eqb_refl, IHv, IHv0. auto. + - match goal with HF : Forall _ _ |- _ => rename HF into Hall end. + simpl. induction Hall as [| x vs' Hhd Htl IHvs]. + + reflexivity. + + simpl. rewrite Hhd. simpl. exact IHvs. + - match goal with HF : Forall _ _ |- _ => rename HF into Hall end. + simpl. induction Hall as [| p fs' Hhd Htl IHfs]. + + reflexivity. + + destruct p as [f x]; simpl in *. rewrite String.eqb_refl, Hhd. simpl. + exact IHfs. Qed. (** * 3. Expressions *) @@ -174,7 +296,7 @@ Fixpoint expr_size (e : phr_expr) : nat := Lemma expr_size_pos : forall e, expr_size e >= 1. Proof. - induction e; simpl; omega. + induction e; simpl; lia. Qed. (** * 9. Typing Relation *) @@ -275,7 +397,7 @@ Inductive value_has_type : phr_value -> phr_type -> Prop := value_has_type (VList vs) (TList τ) | VT_Record : forall fields ftypes, (forall f τ, In (f, τ) ftypes -> - exists v, In (f, v) fields /\ value_has_type v τ) -> + exists v, field_lookup f fields = Some v /\ value_has_type v τ) -> value_has_type (VRecord fields) (TRecord ftypes). (** * 11. Evaluation Relation *) @@ -406,68 +528,66 @@ Qed. (** * 13. Type Safety: Preservation *) +(** List helper: zip per-element type-preservation with per-element typing. *) +Lemma literal_preservation_list : forall Γ vs τ, + Forall (fun w => forall Γ' τ', Γ' ⊢ (ELit w) ∈ τ' -> value_has_type w τ') vs -> + Forall (fun w => Γ ⊢ (ELit w) ∈ τ) vs -> + Forall (fun w => value_has_type w τ) vs. +Proof. + intros Γ vs. induction vs as [| w ws IHvs]; intros τ Hih Het. + - constructor. + - pose proof (Forall_inv Hih) as Hw. + pose proof (Forall_inv_tail Hih) as Hihs. + pose proof (Forall_inv Het) as Hwt. + pose proof (Forall_inv_tail Het) as Hets. + constructor. + + eapply Hw. exact Hwt. + + apply IHvs; assumption. +Qed. + +(** A well-typed literal value has the corresponding value type. Proved by the + strong value induction so the [VList] case can convert element typings. *) +Lemma literal_preservation : forall v Γ τ, + Γ ⊢ (ELit v) ∈ τ -> value_has_type v τ. +Proof. + intros v. induction v using phr_value_ind'; intros Γ τ Ht; inversion Ht; subst. + - constructor. (* VInt -> TInt *) + - constructor. (* VString -> TString *) + - constructor. (* VBool -> TBool *) + - constructor. (* VList vs -> TList τ0 *) + apply (literal_preservation_list Γ); assumption. + - constructor. (* VNull -> TNull *) +Qed. + +(** Preservation (type safety): a well-typed closed expression evaluates to a + value of its type. By induction on the evaluation derivation, which keeps + the typing context concrete ([]) so the [EVar] case is genuinely impossible. *) Theorem preservation : forall ρ e τ v, [] ⊢ e ∈ τ -> ρ ⊢ e ⇓ v -> value_has_type v τ. Proof. intros ρ e τ v Htype Heval. - generalize dependent v. - generalize dependent ρ. - induction Htype; intros ρ v Heval; inversion Heval; subst. - (* Literals *) - - constructor. - - constructor. - - constructor. - - constructor. - (* Variables - impossible in empty context *) - - simpl in H. discriminate. - (* Addition *) - - apply IHHtype1 in H3. apply IHHtype2 in H5. - inversion H3; subst. inversion H5; subst. - constructor. - (* Subtraction *) - - apply IHHtype1 in H3. apply IHHtype2 in H5. - inversion H3; subst. inversion H5; subst. - constructor. - (* Multiplication *) - - apply IHHtype1 in H3. apply IHHtype2 in H5. - inversion H3; subst. inversion H5; subst. - constructor. - (* And - true case *) - - apply IHHtype2 in H5. assumption. - (* And - false case *) - - constructor. - (* Or - true case *) - - constructor. - (* Or - false case *) - - apply IHHtype2 in H5. assumption. - (* Equality *) - - constructor. - (* Less than *) - - constructor. - (* Not *) - - constructor. - (* Negation *) - - constructor. - (* If true *) - - apply IHHtype2 in H5. assumption. - (* If false *) - - apply IHHtype3 in H5. assumption. - (* In *) - - constructor. - (* Field access - need to show field value has correct type *) - - apply IHHtype in H3. - inversion H3; subst. - (* From H: In (f, τ) fields (type-level fields) *) - (* From H4: field_lookup f fields0 = Some v (value-level fields) *) - (* Need: the record typing relates type-level and value-level *) - (* This requires a well-formedness condition on the value environment *) - (* For now, we assume the record is well-typed *) - destruct (H0 f τ H) as [v' [Hin Hvt]]. - (* Need to show v = v' - requires field_lookup determinism *) - (* This is a technical detail we elide *) - exact Hvt. + generalize dependent τ. + induction Heval; intros τ Htype; + try (inversion Htype; subst; now constructor). + - (* E_Lit *) eapply literal_preservation. exact Htype. + - (* E_Var: a variable is untypable in the empty context *) + inversion Htype; subst. + match goal with H : lookup _ [] = Some _ |- _ => simpl in H; discriminate H end. + - (* E_If_True *) inversion Htype; subst. apply IHHeval2. assumption. + - (* E_If_False *) inversion Htype; subst. apply IHHeval2. assumption. + - (* E_Field: the looked-up field value has the field's type *) + inversion Htype; subst. + match goal with Hrec : has_type [] ?ee (TRecord ?ff) |- _ => + specialize (IHHeval (TRecord ff) Hrec) end. + inversion IHHeval; subst. + match goal with + Hbody : forall f0 t, In (f0, t) ?ff -> _, + Hin : In (?f1, τ) ?ff |- _ => + destruct (Hbody f1 τ Hin) as [w [Hlk Hwt]] + end. + assert (v = w) by congruence. subst. exact Hwt. Qed. (** * 14. Evaluation is Deterministic *) @@ -479,58 +599,17 @@ Theorem eval_deterministic : forall ρ e v1 v2, Proof. intros ρ e v1 v2 H1. generalize dependent v2. - induction H1; intros v2 H2; inversion H2; subst; auto. - (* Literal *) - - reflexivity. - (* Variable *) - - rewrite H in H3. injection H3. auto. - (* Add *) - - apply IHeval1 in H4. apply IHeval2 in H6. - inversion H4; subst. inversion H6; subst. reflexivity. - (* Sub *) - - apply IHeval1 in H4. apply IHeval2 in H6. - inversion H4; subst. inversion H6; subst. reflexivity. - (* Mul *) - - apply IHeval1 in H4. apply IHeval2 in H6. - inversion H4; subst. inversion H6; subst. reflexivity. - (* And true *) - - apply IHeval1 in H4. inversion H4; subst. - apply IHeval2 in H6. assumption. - - apply IHeval1 in H4. inversion H4. - (* And false *) - - apply IHeval1 in H4. inversion H4. - - reflexivity. - (* Or true *) - - reflexivity. - - apply IHeval1 in H4. inversion H4. - (* Or false *) - - apply IHeval1 in H4. inversion H4. - - apply IHeval1 in H4. inversion H4; subst. - apply IHeval2 in H6. assumption. - (* Eq *) - - apply IHeval1 in H4. apply IHeval2 in H6. - subst. reflexivity. - (* Lt *) - - apply IHeval1 in H4. apply IHeval2 in H6. - inversion H4; subst. inversion H6; subst. reflexivity. - (* Not *) - - apply IHeval in H3. inversion H3; subst. reflexivity. - (* Neg *) - - apply IHeval in H3. inversion H3; subst. reflexivity. - (* If true *) - - apply IHeval1 in H5. inversion H5; subst. - apply IHeval2 in H7. assumption. - - apply IHeval1 in H5. inversion H5. - (* If false *) - - apply IHeval1 in H5. inversion H5. - - apply IHeval1 in H5. inversion H5; subst. - apply IHeval2 in H7. assumption. - (* In *) - - apply IHeval1 in H4. apply IHeval2 in H6. - subst. reflexivity. - (* Field *) - - apply IHeval in H4. inversion H4; subst. - rewrite H0 in H6. injection H6. auto. + (* For each evaluation rule of the first derivation, invert the second; then + resolve every shared subexpression by its induction hypothesis (which says + the subexpression evaluates to a unique value) and close by congruence. + Short-circuit boolean cases close because the IH forces a contradictory + guard value; the field case closes via field_lookup on equal records. *) + induction H1; intros vR H2; inversion H2; subst; + repeat match goal with + | [ IH : forall v, _ ⊢ ?e ⇓ v -> _ = v, Hv : _ ⊢ ?e ⇓ _ |- _ ] => + apply IH in Hv + end; + try reflexivity; try congruence. Qed. (** * 15. Termination *) @@ -551,12 +630,8 @@ Proof. - apply expr_size_pos. Qed. -(** All expressions can be evaluated (totality) *) -(** This follows from the absence of recursion and the structure of eval *) -Theorem totality : forall ρ e, - (forall x, In x (free_vars e) -> exists v, val_lookup x ρ = Some v) -> - exists v, ρ ⊢ e ⇓ v -with free_vars (e : phr_expr) : list string := +(** Free variables of an expression. *) +Fixpoint free_vars (e : phr_expr) : list string := match e with | ELit _ => [] | EVar x => [x] @@ -566,30 +641,28 @@ with free_vars (e : phr_expr) : list string := | EField e _ => free_vars e | EIn e1 e2 => free_vars e1 ++ free_vars e2 end. + +(** Totality / progress-to-a-value. + + NOTE (honesty): this is the one safety obligation in this file that is NOT + yet mechanized. It is stated here as an explicit [Admitted] obligation, not + a hidden gap. The ORIGINAL statement (closedness of the value environment + alone implies evaluation) is FALSE — e.g. [EBinOp OpAdd (ELit (VBool true)) + (ELit (VInt 1))] is closed but has no applicable evaluation rule. The + correct statement requires WELL-TYPEDNESS: a closed, well-typed expression + evaluates to a value (the language has no loops or recursion). The full + proof is an induction on the typing derivation using the canonical-forms + lemmas to pin each operand's value shape; it is left open here. + + Nothing below depends on [totality]; the safety core ([preservation], + [eval_deterministic], [type_safety], [phr_type_eq_dec], [subtype_trans], + [no_system_calls]) is fully proved and axiom-free. *) +Theorem totality : forall e τ ρ, + [] ⊢ e ∈ τ -> + (forall x, In x (free_vars e) -> exists v, val_lookup x ρ = Some v) -> + exists v, ρ ⊢ e ⇓ v. Proof. - (* Proof by induction on expression structure *) - intros ρ e Hclosed. - induction e. - (* Literal *) - - exists p. constructor. - (* Variable *) - - destruct (Hclosed s) as [v Hv]. - + simpl. left. reflexivity. - + exists v. constructor. assumption. - (* BinOp *) - - destruct IHe1 as [v1 Hv1]. - + intros x Hx. apply Hclosed. simpl. apply in_or_app. left. assumption. - + destruct IHe2 as [v2 Hv2]. - * intros x Hx. apply Hclosed. simpl. apply in_or_app. right. assumption. - * (* Need to case split on operator and value types *) - destruct b; destruct v1; destruct v2; try (exists VNull; constructor; fail). - (* Add *) - { exists (VInt (z + z0)). apply E_Add; assumption. } - (* Other cases similar - abbreviated *) - all: try (exists (VBool false); constructor; assumption). - (* Remaining cases follow similar pattern *) - all: try (exists VNull; constructor; fail). -Abort. (* Full proof is tedious but straightforward *) +Admitted. (** * 16. Type Safety Corollary *) @@ -598,22 +671,36 @@ Corollary type_safety : forall e τ ρ v, ρ ⊢ e ⇓ v -> value_has_type v τ. Proof. - apply preservation. + intros e τ ρ v Htype Heval. exact (preservation ρ e τ v Htype Heval). Qed. (** * 17. Sandbox Isolation *) -(** The grammar does not include system calls, file operations, or network operations. - This is enforced by construction: phr_expr has no such constructors. *) - -Theorem no_system_calls : forall e, - ~ exists f args, e = ELit (VString f) /\ - (f = "system"%string \/ f = "exec"%string \/ f = "shell"%string). +(** The grammar does not include system calls, file operations, or network + operations. This is enforced BY CONSTRUCTION: [phr_expr] is first-order and + has no application/call/IO constructor. + + NOTE (honesty): the previous [no_system_calls] statement was unsound — it + asserted that no expression equals [ELit (VString "system")], which is false + ([ELit (VString "system")] is a perfectly good inert string literal). The + sandbox guarantee is not "the string 'system' cannot appear" but "there is + no expression form that INVOKES anything". We capture that honestly below: + every expression is one of the seven inert forms, none of which is a call. *) + +Theorem sandbox_no_call_form : forall e : phr_expr, + (exists v, e = ELit v) \/ (exists x, e = EVar x) \/ + (exists o a b, e = EBinOp o a b) \/ (exists o a, e = EUnOp o a) \/ + (exists a b c, e = EIf a b c) \/ (exists a f, e = EField a f) \/ + (exists a b, e = EIn a b). Proof. - intros e [f [args [Heq Hf]]]. - destruct e; try discriminate. - injection Heq as Heq'. - destruct p; discriminate. + destruct e. + - left; eauto. + - right; left; eauto. + - right; right; left; eauto. + - right; right; right; left; eauto. + - right; right; right; right; left; eauto. + - right; right; right; right; right; left; eauto. + - right; right; right; right; right; right; eauto. Qed. (** * 18. Subtyping *) @@ -633,17 +720,12 @@ where "τ1 '<:' τ2" := (subtype τ1 τ2). Theorem subtype_trans : forall τ1 τ2 τ3, τ1 <: τ2 -> τ2 <: τ3 -> τ1 <: τ3. Proof. - intros τ1 τ2 τ3 H12 H23. - induction H12. + intros τ1 τ2 τ3 H12. generalize dependent τ3. + induction H12; intros τ3 H23. - assumption. - apply Sub_Bot. - - inversion H23; subst; try apply Sub_Top. - + apply Sub_Refl. - - inversion H23; subst. - + apply Sub_List. assumption. - + apply Sub_Bot. - + apply Sub_Top. - + apply Sub_List. apply IHsubtype. assumption. + - inversion H23; subst; apply Sub_Top. + - inversion H23; subst; eauto using Sub_List, Sub_Top. Qed. (** * 19. Summary *) From 174ecfdaee7d8f9a857ad088fbbc6f4386322f5c Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 15 Jun 2026 14:44:07 +0100 Subject: [PATCH 2/3] =?UTF-8?q?feat(formal/coq):=20discharge=20totality=20?= =?UTF-8?q?=E2=80=94=20Coq=20formalization=20now=20fully=20proved?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `totality` was the lone Admitted. Discharged as genuine progress-to-a-value: a well-typed closed expression always evaluates (the language has no loops or recursion). Proof is induction on the expression using the now-proved `preservation` + canonical value shapes to pin each operand; the value environment `ρ` is arbitrary because `[] ⊢ e ∈ τ` already forces closedness. The redundant `free_vars` hypothesis (and the previously-unsound free-vars-only statement) is dropped, since well-typedness in the empty context implies the expression is closed. Whole file now: `coqc Phronesis.v` exits 0 with NO Admitted/Abort/sorry, and `Print Assumptions totality` / `type_safety` = "Closed under the global context" (axiom-free). The mechanized safety story is complete: type safety (preservation), totality/progress, determinism, decidable type equality, subtyping transitivity, and by-construction sandbox isolation. Co-Authored-By: Claude Opus 4.8 (1M context) --- academic/formal-verification/coq/Phronesis.v | 108 ++++++++++++++++--- 1 file changed, 91 insertions(+), 17 deletions(-) diff --git a/academic/formal-verification/coq/Phronesis.v b/academic/formal-verification/coq/Phronesis.v index 1a2cbd1..50c5229 100644 --- a/academic/formal-verification/coq/Phronesis.v +++ b/academic/formal-verification/coq/Phronesis.v @@ -642,27 +642,101 @@ Fixpoint free_vars (e : phr_expr) : list string := | EIn e1 e2 => free_vars e1 ++ free_vars e2 end. -(** Totality / progress-to-a-value. +(** Totality / progress-to-a-value: a well-typed closed expression always + evaluates to a value (the language has no loops or recursion). - NOTE (honesty): this is the one safety obligation in this file that is NOT - yet mechanized. It is stated here as an explicit [Admitted] obligation, not - a hidden gap. The ORIGINAL statement (closedness of the value environment - alone implies evaluation) is FALSE — e.g. [EBinOp OpAdd (ELit (VBool true)) + NOTE: the ORIGINAL statement required only that the value environment cover + [free_vars e], which is FALSE — e.g. [EBinOp OpAdd (ELit (VBool true)) (ELit (VInt 1))] is closed but has no applicable evaluation rule. The - correct statement requires WELL-TYPEDNESS: a closed, well-typed expression - evaluates to a value (the language has no loops or recursion). The full - proof is an induction on the typing derivation using the canonical-forms - lemmas to pin each operand's value shape; it is left open here. - - Nothing below depends on [totality]; the safety core ([preservation], - [eval_deterministic], [type_safety], [phr_type_eq_dec], [subtype_trans], - [no_system_calls]) is fully proved and axiom-free. *) + correct hypothesis is WELL-TYPEDNESS; and since [[] ⊢ e ∈ τ] already forces + [e] to be closed (there is no binding form, so [EVar] is untypable here), + the value-environment hypothesis is redundant and dropped. The proof is an + induction on [e] that uses [preservation] + the canonical value shapes to + pin each operand. [ρ] is arbitrary precisely because [e] is closed. *) Theorem totality : forall e τ ρ, - [] ⊢ e ∈ τ -> - (forall x, In x (free_vars e) -> exists v, val_lookup x ρ = Some v) -> - exists v, ρ ⊢ e ⇓ v. + [] ⊢ e ∈ τ -> exists v, ρ ⊢ e ⇓ v. Proof. -Admitted. + intros e; induction e as + [ p | s | b e1 IHe1 e2 IHe2 | u e IHe + | e1 IHe1 e2 IHe2 e3 IHe3 | e IHe f | e1 IHe1 e2 IHe2 ]; + intros τ ρ Ht. + - (* ELit *) exists p. constructor. + - (* EVar: untypable in the empty context *) + inversion Ht; subst. + match goal with H : lookup _ [] = Some _ |- _ => simpl in H; discriminate H end. + - (* EBinOp: evaluate the left operand once, up front *) + inversion Ht; subst; + match goal with Ha : has_type [] e1 _ |- _ => + destruct (IHe1 _ ρ Ha) as [v1 Hv1]; + pose proof (preservation _ _ _ _ Ha Hv1) as T1 + end. + + (* Add *) match goal with Hb : has_type [] e2 _ |- _ => + destruct (IHe2 _ ρ Hb) as [v2 Hv2]; pose proof (preservation _ _ _ _ Hb Hv2) as T2 end; + inversion T1; subst; inversion T2; subst; eexists; apply E_Add; eassumption. + + (* Sub *) match goal with Hb : has_type [] e2 _ |- _ => + destruct (IHe2 _ ρ Hb) as [v2 Hv2]; pose proof (preservation _ _ _ _ Hb Hv2) as T2 end; + inversion T1; subst; inversion T2; subst; eexists; apply E_Sub; eassumption. + + (* Mul *) match goal with Hb : has_type [] e2 _ |- _ => + destruct (IHe2 _ ρ Hb) as [v2 Hv2]; pose proof (preservation _ _ _ _ Hb Hv2) as T2 end; + inversion T1; subst; inversion T2; subst; eexists; apply E_Mul; eassumption. + + (* And: short-circuit on the left guard *) + inversion T1; subst; + match goal with Hg : _ ⊢ e1 ⇓ VBool ?bb |- _ => destruct bb end. + * match goal with Hb : has_type [] e2 _ |- _ => + destruct (IHe2 _ ρ Hb) as [v2 Hv2]; pose proof (preservation _ _ _ _ Hb Hv2) as T2 end; + inversion T2; subst; eexists; apply E_And_True; eassumption. + * eexists; apply E_And_False; eassumption. + + (* Or: short-circuit on the left guard *) + inversion T1; subst; + match goal with Hg : _ ⊢ e1 ⇓ VBool ?bb |- _ => destruct bb end. + * eexists; apply E_Or_True; eassumption. + * match goal with Hb : has_type [] e2 _ |- _ => + destruct (IHe2 _ ρ Hb) as [v2 Hv2]; pose proof (preservation _ _ _ _ Hb Hv2) as T2 end; + inversion T2; subst; eexists; apply E_Or_False; eassumption. + + (* Eq: no value-shape constraint *) + match goal with Hb : has_type [] e2 _ |- _ => + destruct (IHe2 _ ρ Hb) as [v2 Hv2] end; + eexists; apply E_Eq; eassumption. + + (* Lt *) match goal with Hb : has_type [] e2 _ |- _ => + destruct (IHe2 _ ρ Hb) as [v2 Hv2]; pose proof (preservation _ _ _ _ Hb Hv2) as T2 end; + inversion T1; subst; inversion T2; subst; eexists; apply E_Lt; eassumption. + - (* EUnOp *) + inversion Ht; subst; + match goal with Ha : has_type [] e _ |- _ => + destruct (IHe _ ρ Ha) as [v Hv]; pose proof (preservation _ _ _ _ Ha Hv) as T end; + inversion T; subst. + + eexists; apply E_Not; eassumption. + + eexists; apply E_Neg; eassumption. + - (* EIf: branch on the guard value *) + inversion Ht; subst. + match goal with Hc : has_type [] e1 _ |- _ => + destruct (IHe1 _ ρ Hc) as [v1 Hv1]; pose proof (preservation _ _ _ _ Hc Hv1) as T1 end. + inversion T1; subst. + match goal with Hg : _ ⊢ e1 ⇓ VBool ?bb |- _ => destruct bb end. + + match goal with Ht2 : has_type [] e2 _ |- _ => + destruct (IHe2 _ ρ Ht2) as [v2 Hv2] end; exists v2; apply E_If_True; assumption. + + match goal with Ht3 : has_type [] e3 _ |- _ => + destruct (IHe3 _ ρ Ht3) as [v3 Hv3] end; exists v3; apply E_If_False; assumption. + - (* EField: the field exists in the (well-typed) record value *) + inversion Ht; subst. + match goal with Hr : has_type [] e (TRecord ?ff), Hin : In (f, τ) ?ff |- _ => + destruct (IHe _ ρ Hr) as [v Hv]; pose proof (preservation _ _ _ _ Hr Hv) as T; + inversion T; subst; + match goal with Hbody : forall a t, In (a, t) ff -> _ |- _ => + destruct (Hbody f τ Hin) as [w [Hlk Hwt]] + end + end. + exists w. eapply E_Field; eassumption. + - (* EIn: the right operand is a list value *) + inversion Ht; subst. + match goal with + Ha : has_type [] e1 _, Hb : has_type [] e2 (TList _) |- _ => + destruct (IHe1 _ ρ Ha) as [v1 Hv1]; + destruct (IHe2 _ ρ Hb) as [v2 Hv2]; + pose proof (preservation _ _ _ _ Hb Hv2) as T2 + end. + inversion T2; subst. eexists. apply E_In; eassumption. +Qed. (** * 16. Type Safety Corollary *) From 7fa39cddf7afbcdab6848c6862fa3d6921364641 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 15 Jun 2026 14:53:53 +0100 Subject: [PATCH 3/3] fix(formal/agda): make the intrinsic-typing formalization check under --safe --without-K MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Agda formalization never typechecked. Fixes: - Ctx's `_,_` clashed with Data.Product `_,_` (AmbiguousParseForApplication at the context-extension sites) -> renamed to `_,,_`. - Two `Data.Integer` imports listed names in both `using` and `renaming` (RepeatedNamesInImportDirective) and re-imported `_+_`, clashing with Data.Nat -> kept only the renamings. - `_≟ᵗ_` (decidable type equality) was UNSOUND: it omitted the TRecord case and used a single `_ ≟ᵗ _ = no (λ ())` catch-all, which --safe rejects ([ShouldBeEmpty]) since `TRecord fs ≡ TRecord gs` is inhabited by refl. Rewritten as a mutual decision with `_≟ᶠ_` over the field list; every same-head case is handled and the distinct-head pairs are enumerated. - `_<ᵛ_` parsed as `a ≤ᵇ (b ∧ …)` (fixity) and used `_≡ᵛ_` at an ambiguous type index -> parenthesised and indexed at TInt. - Added `{-# OPTIONS --safe --without-K #-}`. `agda Phronesis.agda` now exits 0 under --safe --without-K (no postulates, no holes, termination + positivity checked), so the intrinsic-typing "type safety is automatic" and "eval is total" claims now genuinely hold. SPDX header unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../formal-verification/agda/Phronesis.agda | 147 +++++++++++++++--- 1 file changed, 122 insertions(+), 25 deletions(-) diff --git a/academic/formal-verification/agda/Phronesis.agda b/academic/formal-verification/agda/Phronesis.agda index c832d95..2b3d490 100644 --- a/academic/formal-verification/agda/Phronesis.agda +++ b/academic/formal-verification/agda/Phronesis.agda @@ -2,6 +2,8 @@ -- Phronesis Formalization in Agda -- Intrinsically typed representation with dependent types +{-# OPTIONS --safe --without-K #-} + module Phronesis where open import Data.Nat using (ℕ; zero; suc; _+_; _≤_) @@ -35,20 +37,115 @@ data PhrType : Set where -- 2. Type Equality Decidability -- ═══════════════════════════════════════════════════════════════════════════ --- Decidable equality for types (needed for type checking) -_≟ᵗ_ : (τ₁ τ₂ : PhrType) → Dec (τ₁ ≡ τ₂) -TInt ≟ᵗ TInt = yes refl -TBool ≟ᵗ TBool = yes refl -TString ≟ᵗ TString = yes refl -TNull ≟ᵗ TNull = yes refl -TFloat ≟ᵗ TFloat = yes refl -TIP ≟ᵗ TIP = yes refl -TDateTime ≟ᵗ TDateTime = yes refl -TList τ₁ ≟ᵗ TList τ₂ with τ₁ ≟ᵗ τ₂ -... | yes refl = yes refl -... | no ¬p = no (λ { refl → ¬p refl }) --- ... other cases omitted for brevity -_ ≟ᵗ _ = no (λ ()) +-- Decidable equality for types (needed for type checking). +-- +-- TRecord nests through List (String × PhrType), so the field list is decided +-- mutually (_≟ᶠ_). EVERY same-head case — including TRecord — is handled +-- explicitly *above* the final catch-all, so the catch-all covers only +-- distinct-head pairs and `no (λ ())` is sound. (The previous version omitted +-- the TRecord case, which made the catch-all unsound: `TRecord fs ≡ TRecord gs` +-- is inhabited by `refl`, so `λ ()` did not typecheck under --safe.) +mutual + _≟ᵗ_ : (τ₁ τ₂ : PhrType) → Dec (τ₁ ≡ τ₂) + TInt ≟ᵗ TInt = yes refl + TBool ≟ᵗ TBool = yes refl + TString ≟ᵗ TString = yes refl + TNull ≟ᵗ TNull = yes refl + TFloat ≟ᵗ TFloat = yes refl + TIP ≟ᵗ TIP = yes refl + TDateTime ≟ᵗ TDateTime = yes refl + TList τ₁ ≟ᵗ TList τ₂ with τ₁ ≟ᵗ τ₂ + ... | yes refl = yes refl + ... | no ¬p = no (λ { refl → ¬p refl }) + TRecord fs ≟ᵗ TRecord gs with fs ≟ᶠ gs + ... | yes refl = yes refl + ... | no ¬p = no (λ { refl → ¬p refl }) + -- distinct-head pairs (all absurd; enumerated because Agda will not refine a + -- single `_ ≟ᵗ _` catch-all to the distinct-head cases under --safe): + TInt ≟ᵗ TFloat = no (λ ()) + TInt ≟ᵗ TString = no (λ ()) + TInt ≟ᵗ TBool = no (λ ()) + TInt ≟ᵗ TIP = no (λ ()) + TInt ≟ᵗ TDateTime = no (λ ()) + TInt ≟ᵗ TList _ = no (λ ()) + TInt ≟ᵗ TRecord _ = no (λ ()) + TInt ≟ᵗ TNull = no (λ ()) + TFloat ≟ᵗ TInt = no (λ ()) + TFloat ≟ᵗ TString = no (λ ()) + TFloat ≟ᵗ TBool = no (λ ()) + TFloat ≟ᵗ TIP = no (λ ()) + TFloat ≟ᵗ TDateTime = no (λ ()) + TFloat ≟ᵗ TList _ = no (λ ()) + TFloat ≟ᵗ TRecord _ = no (λ ()) + TFloat ≟ᵗ TNull = no (λ ()) + TString ≟ᵗ TInt = no (λ ()) + TString ≟ᵗ TFloat = no (λ ()) + TString ≟ᵗ TBool = no (λ ()) + TString ≟ᵗ TIP = no (λ ()) + TString ≟ᵗ TDateTime = no (λ ()) + TString ≟ᵗ TList _ = no (λ ()) + TString ≟ᵗ TRecord _ = no (λ ()) + TString ≟ᵗ TNull = no (λ ()) + TBool ≟ᵗ TInt = no (λ ()) + TBool ≟ᵗ TFloat = no (λ ()) + TBool ≟ᵗ TString = no (λ ()) + TBool ≟ᵗ TIP = no (λ ()) + TBool ≟ᵗ TDateTime = no (λ ()) + TBool ≟ᵗ TList _ = no (λ ()) + TBool ≟ᵗ TRecord _ = no (λ ()) + TBool ≟ᵗ TNull = no (λ ()) + TIP ≟ᵗ TInt = no (λ ()) + TIP ≟ᵗ TFloat = no (λ ()) + TIP ≟ᵗ TString = no (λ ()) + TIP ≟ᵗ TBool = no (λ ()) + TIP ≟ᵗ TDateTime = no (λ ()) + TIP ≟ᵗ TList _ = no (λ ()) + TIP ≟ᵗ TRecord _ = no (λ ()) + TIP ≟ᵗ TNull = no (λ ()) + TDateTime ≟ᵗ TInt = no (λ ()) + TDateTime ≟ᵗ TFloat = no (λ ()) + TDateTime ≟ᵗ TString = no (λ ()) + TDateTime ≟ᵗ TBool = no (λ ()) + TDateTime ≟ᵗ TIP = no (λ ()) + TDateTime ≟ᵗ TList _ = no (λ ()) + TDateTime ≟ᵗ TRecord _ = no (λ ()) + TDateTime ≟ᵗ TNull = no (λ ()) + TList _ ≟ᵗ TInt = no (λ ()) + TList _ ≟ᵗ TFloat = no (λ ()) + TList _ ≟ᵗ TString = no (λ ()) + TList _ ≟ᵗ TBool = no (λ ()) + TList _ ≟ᵗ TIP = no (λ ()) + TList _ ≟ᵗ TDateTime = no (λ ()) + TList _ ≟ᵗ TRecord _ = no (λ ()) + TList _ ≟ᵗ TNull = no (λ ()) + TRecord _ ≟ᵗ TInt = no (λ ()) + TRecord _ ≟ᵗ TFloat = no (λ ()) + TRecord _ ≟ᵗ TString = no (λ ()) + TRecord _ ≟ᵗ TBool = no (λ ()) + TRecord _ ≟ᵗ TIP = no (λ ()) + TRecord _ ≟ᵗ TDateTime = no (λ ()) + TRecord _ ≟ᵗ TList _ = no (λ ()) + TRecord _ ≟ᵗ TNull = no (λ ()) + TNull ≟ᵗ TInt = no (λ ()) + TNull ≟ᵗ TFloat = no (λ ()) + TNull ≟ᵗ TString = no (λ ()) + TNull ≟ᵗ TBool = no (λ ()) + TNull ≟ᵗ TIP = no (λ ()) + TNull ≟ᵗ TDateTime = no (λ ()) + TNull ≟ᵗ TList _ = no (λ ()) + TNull ≟ᵗ TRecord _ = no (λ ()) + + -- Decidable equality for record field lists. + _≟ᶠ_ : (fs gs : List (String × PhrType)) → Dec (fs ≡ gs) + [] ≟ᶠ [] = yes refl + [] ≟ᶠ (_ ∷ _) = no (λ ()) + (_ ∷ _) ≟ᶠ [] = no (λ ()) + ((s₁ , τ₁) ∷ fs) ≟ᶠ ((s₂ , τ₂) ∷ gs) + with Data.String._≟_ s₁ s₂ | τ₁ ≟ᵗ τ₂ | fs ≟ᶠ gs + ... | yes refl | yes refl | yes refl = yes refl + ... | no ¬p | _ | _ = no (λ { refl → ¬p refl }) + ... | _ | no ¬p | _ = no (λ { refl → ¬p refl }) + ... | _ | _ | no ¬p = no (λ { refl → ¬p refl }) -- ═══════════════════════════════════════════════════════════════════════════ -- 3. Semantic Domain (Values indexed by Type) @@ -72,15 +169,15 @@ _ ≟ᵗ _ = no (λ ()) -- ═══════════════════════════════════════════════════════════════════════════ data Ctx : Set where - ∅ : Ctx - _,_ : Ctx → String × PhrType → Ctx + ∅ : Ctx + _,,_ : Ctx → String × PhrType → Ctx -infixl 5 _,_ +infixl 5 _,,_ -- Variable lookup (de Bruijn style would be cleaner, but using names for clarity) data _∋_∶_ : Ctx → String → PhrType → Set where - here : ∀ {Γ x τ} → (Γ , (x , τ)) ∋ x ∶ τ - there : ∀ {Γ x y τ τ'} → Γ ∋ x ∶ τ → (Γ , (y , τ')) ∋ x ∶ τ + here : ∀ {Γ x τ} → (Γ ,, (x , τ)) ∋ x ∶ τ + there : ∀ {Γ x y τ τ'} → Γ ∋ x ∶ τ → (Γ ,, (y , τ')) ∋ x ∶ τ -- ═══════════════════════════════════════════════════════════════════════════ -- 5. Intrinsically Typed Expressions @@ -130,7 +227,7 @@ infix 5 _==ᵉ_ _<ᵉ_ data Env : Ctx → Set where ε : Env ∅ - _▷_ : ∀ {Γ x τ} → Env Γ → ⟦ τ ⟧ → Env (Γ , (x , τ)) + _▷_ : ∀ {Γ x τ} → Env Γ → ⟦ τ ⟧ → Env (Γ ,, (x , τ)) infixl 5 _▷_ @@ -143,12 +240,12 @@ lookupEnv (there x) (ρ ▷ _) = lookupEnv x ρ -- 7. Denotational Semantics (Evaluation) -- ═══════════════════════════════════════════════════════════════════════════ -open import Data.Integer using (_+_; _-_; _*_; _≤ᵇ_) renaming (_+_ to _+ℤ_; _-_ to _-ℤ_; _*_ to _*ℤ_) +open import Data.Integer using (_≤ᵇ_) renaming (_+_ to _+ℤ_; _-_ to _-ℤ_; _*_ to _*ℤ_) -- Value equality (for comparison operators) -- Implemented via decidable equality per type, not postulated. -open import Data.Integer using (_≟_) renaming (_≟_ to _≟ℤ_) +open import Data.Integer using () renaming (_≟_ to _≟ℤ_) open import Data.String using () renaming (_≟_ to _≟ˢ_) open import Data.Nat using () renaming (_≟_ to _≟ⁿ_) open import Data.Bool using () renaming (_≟_ to _≟ᵇ_) @@ -196,10 +293,10 @@ mutual eqRecord {[]} tt tt = true eqRecord {(_ , τ) ∷ fs} (v , vs) (w , ws) = _≡ᵛ_ v w ∧ eqRecord {fs} vs ws --- Integer less-than via the standard library ordering. +-- Integer less-than via the standard library ordering. The parentheses are +-- load-bearing (`_∧_` binds tighter than `_≤ᵇ_`); `_≡ᵛ_` is indexed at TInt. _<ᵛ_ : ℤ → ℤ → Bool -a <ᵛ b = a ≤ᵇ b ∧ not (a ≡ᵛ b) - where open import Data.Integer using (_≤ᵇ_) +a <ᵛ b = (a ≤ᵇ b) ∧ not (_≡ᵛ_ {TInt} a b) -- List membership via value equality. _∈ᵛ_ : ∀ {τ} → ⟦ τ ⟧ → List ⟦ τ ⟧ → Bool