narrow (ternary sibling of the if-return optChain-compare rule)

examples/optChainDiscriminantTernary.def.lean

@@ -0,0 +1,28 @@
+/-
+  Generated by lsc from optChainDiscriminantTernary.ts
+  Do not edit — re-run `lsc gen` to regenerate.
+-/
+import «optChainDiscriminantTernary.types»
+
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+method textOr (e : Option Entry) (dflt : String) return (res : String)
+  ensures (match e with | .some _ => false | .none => true) → res = dflt
+  do
+    return Pure.textOr e dflt
+
+method textOrFlipped (e : Option Entry) (dflt : String) return (res : String)
+  ensures (match e with | .some _ => false | .none => true) → res = dflt
+  do
+    return Pure.textOrFlipped e dflt
+
+method bodyOr (r : Option Rec) (dflt : String) return (res : String)
+  ensures (match r with | .some _ => false | .none => true) → res = dflt
+  do
+    return Pure.bodyOr r dflt
+
+method firstText (e : Option Entry) (dflt : String) return (res : String)
+  ensures (match e with | .some _ => false | .none => true) → res = dflt
+  do
+    return Pure.firstText e dflt

examples/optChainDiscriminantTernary.dfy

@@ -0,0 +1,75 @@
+// Generated by lsc from optChainDiscriminantTernary.ts
+
+datatype Option<T> = None | Some(value: T)
+
+datatype Entry = msg(text: string) | sep
+
+datatype Rec = Rec(tag: string, body: string)
+
+function textOr(e: Option<Entry>, dflt: string): string
+{
+  var t := (match e { case Some(i_e_val) => (if i_e_val.msg? then Option.Some(i_e_val.text) else Option.None) case None => Option.None });
+  match t {
+    case Some(i_oc0_val) =>
+      i_oc0_val
+    case None =>
+      dflt
+  }
+}
+
+lemma textOr_ensures(e: Option<Entry>, dflt: string)
+  ensures ((match e { case Some(i_) => false case None => true }) ==> (textOr(e, dflt) == dflt))
+{
+}
+
+function textOrFlipped(e: Option<Entry>, dflt: string): string
+{
+  var t := (match e { case Some(i_e_val) => (if i_e_val.msg? then Option.Some(i_e_val.text) else Option.None) case None => Option.None });
+  match t {
+    case Some(i_oc1_val) =>
+      i_oc1_val
+    case None =>
+      dflt
+  }
+}
+
+lemma textOrFlipped_ensures(e: Option<Entry>, dflt: string)
+  ensures ((match e { case Some(i_) => false case None => true }) ==> (textOrFlipped(e, dflt) == dflt))
+{
+}
+
+function bodyOr(r: Option<Rec>, dflt: string): string
+{
+  var b := (match r { case Some(i_r_val) => (if (i_r_val.tag == "x") then Option.Some(i_r_val.body) else Option.None) case None => Option.None });
+  match b {
+    case Some(i_oc2_val) =>
+      i_oc2_val
+    case None =>
+      dflt
+  }
+}
+
+lemma bodyOr_ensures(r: Option<Rec>, dflt: string)
+  ensures ((match r { case Some(i_) => false case None => true }) ==> (bodyOr(r, dflt) == dflt))
+{
+}
+
+function firstText(e: Option<Entry>, dflt: string): string
+{
+  match e {
+    case Some(i_e_val) =>
+      match i_e_val {
+        case msg(i__e_val_text) =>
+          i__e_val_text
+        case sep =>
+          dflt
+      }
+    case None =>
+      dflt
+  }
+}
+
+lemma firstText_ensures(e: Option<Entry>, dflt: string)
+  ensures ((match e { case Some(i_) => false case None => true }) ==> (firstText(e, dflt) == dflt))
+{
+}

examples/optChainDiscriminantTernary.dfy.gen

@@ -0,0 +1,75 @@
+// Generated by lsc from optChainDiscriminantTernary.ts
+
+datatype Option<T> = None | Some(value: T)
+
+datatype Entry = msg(text: string) | sep
+
+datatype Rec = Rec(tag: string, body: string)
+
+function textOr(e: Option<Entry>, dflt: string): string
+{
+  var t := (match e { case Some(i_e_val) => (if i_e_val.msg? then Option.Some(i_e_val.text) else Option.None) case None => Option.None });
+  match t {
+    case Some(i_oc0_val) =>
+      i_oc0_val
+    case None =>
+      dflt
+  }
+}
+
+lemma textOr_ensures(e: Option<Entry>, dflt: string)
+  ensures ((match e { case Some(i_) => false case None => true }) ==> (textOr(e, dflt) == dflt))
+{
+}
+
+function textOrFlipped(e: Option<Entry>, dflt: string): string
+{
+  var t := (match e { case Some(i_e_val) => (if i_e_val.msg? then Option.Some(i_e_val.text) else Option.None) case None => Option.None });
+  match t {
+    case Some(i_oc1_val) =>
+      i_oc1_val
+    case None =>
+      dflt
+  }
+}
+
+lemma textOrFlipped_ensures(e: Option<Entry>, dflt: string)
+  ensures ((match e { case Some(i_) => false case None => true }) ==> (textOrFlipped(e, dflt) == dflt))
+{
+}
+
+function bodyOr(r: Option<Rec>, dflt: string): string
+{
+  var b := (match r { case Some(i_r_val) => (if (i_r_val.tag == "x") then Option.Some(i_r_val.body) else Option.None) case None => Option.None });
+  match b {
+    case Some(i_oc2_val) =>
+      i_oc2_val
+    case None =>
+      dflt
+  }
+}
+
+lemma bodyOr_ensures(r: Option<Rec>, dflt: string)
+  ensures ((match r { case Some(i_) => false case None => true }) ==> (bodyOr(r, dflt) == dflt))
+{
+}
+
+function firstText(e: Option<Entry>, dflt: string): string
+{
+  match e {
+    case Some(i_e_val) =>
+      match i_e_val {
+        case msg(i__e_val_text) =>
+          i__e_val_text
+        case sep =>
+          dflt
+      }
+    case None =>
+      dflt
+  }
+}
+
+lemma firstText_ensures(e: Option<Entry>, dflt: string)
+  ensures ((match e { case Some(i_) => false case None => true }) ==> (firstText(e, dflt) == dflt))
+{
+}

examples/optChainDiscriminantTernary.proof.lean

@@ -0,0 +1,27 @@
+import «optChainDiscriminantTernary.def»
+
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+-- Expression-bodied, so each method delegates to its `Pure.*` mirror; unfold it
+-- and split on the optional so the discriminant/field `match` in each arm
+-- reduces (mirrors truthiness.proof's optional cases).
+prove_correct textOr by
+  loom_goals_intro
+  loom_unfold
+  all_goals (cases e <;> simp_all [Pure.textOr])
+
+prove_correct textOrFlipped by
+  loom_goals_intro
+  loom_unfold
+  all_goals (cases e <;> simp_all [Pure.textOrFlipped])
+
+prove_correct bodyOr by
+  loom_goals_intro
+  loom_unfold
+  all_goals (cases r <;> simp_all [Pure.bodyOr])
+
+prove_correct firstText by
+  loom_goals_intro
+  loom_unfold
+  all_goals (cases e <;> simp_all [Pure.firstText])

examples/optChainDiscriminantTernary.ts

@@ -0,0 +1,44 @@
+/**
+ * `x?.disc === 'lit'` narrowing in expression position — the ternary sibling of
+ * the `if (x?.disc !== 'lit') return` statement rule (`ruleConditionalOptChainCompare`
+ * / `ruleEarlyReturnOptChainCompare`, sharing `parseOptChainLitCompare`). Covers
+ * optChain on either side, a discriminant vs. a plain field, and the `===`
+ * ternary and `!==` statement forms. Mirrors flue's `classifySubmissionState`
+ * (`assistantEntry?.type === 'message' ? assistantEntry.message : undefined`).
+ */
+
+type Entry = { kind: 'msg'; text: string } | { kind: 'sep' };
+type Rec = { tag: string; body: string };
+
+// `===` ternary, optChain on the left, discriminant field.
+export function textOr(e: Entry | undefined, dflt: string): string {
+  //@ verify
+  //@ ensures e === undefined ==> \result === dflt
+  const t = e?.kind === 'msg' ? e.text : undefined;
+  return t ?? dflt;
+}
+
+// optChain on the right (`'lit' === x?.disc`).
+export function textOrFlipped(e: Entry | undefined, dflt: string): string {
+  //@ verify
+  //@ ensures e === undefined ==> \result === dflt
+  const t = 'msg' === e?.kind ? e.text : undefined;
+  return t ?? dflt;
+}
+
+// Plain (non-discriminant) field on a record — the unwrapped guard stays a field
+// read, not a discriminant test.
+export function bodyOr(r: Rec | undefined, dflt: string): string {
+  //@ verify
+  //@ ensures r === undefined ==> \result === dflt
+  const b = r?.tag === 'x' ? r.body : undefined;
+  return b ?? dflt;
+}
+
+// `!==` statement form (early return) — exercises the shared helper's other arm.
+export function firstText(e: Entry | undefined, dflt: string): string {
+  //@ verify
+  //@ ensures e === undefined ==> \result === dflt
+  if (e?.kind !== 'msg') return dflt;
+  return e.text;
+}

examples/optChainDiscriminantTernary.types.lean

@@ -0,0 +1,53 @@
+/-
+  Generated by lsc — Lean types and pure function mirrors.
+-/
+import LemmaScript
+
+inductive Entry where
+  | msg (text : String) : Entry
+  | sep : Entry
+deriving Repr, Inhabited
+
+structure Rec where
+  tag : String
+  body : String
+deriving Repr, Inhabited, DecidableEq
+
+namespace Pure
+
+def textOr (e : Option Entry) (dflt : String) : String :=
+  let t := (match e with | .some _e_val => if (match _e_val with | .msg .. => true | _ => false) then Option.some (match _e_val with | .msg _v => _v | _ => (default : String)) else Option.none | .none => Option.none)
+  match t with
+  | .some _oc0_val =>
+    _oc0_val
+  | .none =>
+    dflt
+
+def textOrFlipped (e : Option Entry) (dflt : String) : String :=
+  let t := (match e with | .some _e_val => if (match _e_val with | .msg .. => true | _ => false) then Option.some (match _e_val with | .msg _v => _v | _ => (default : String)) else Option.none | .none => Option.none)
+  match t with
+  | .some _oc1_val =>
+    _oc1_val
+  | .none =>
+    dflt
+
+def bodyOr (r : Option Rec) (dflt : String) : String :=
+  let b := (match r with | .some _r_val => if _r_val.tag = "x" then Option.some _r_val.body else Option.none | .none => Option.none)
+  match b with
+  | .some _oc2_val =>
+    _oc2_val
+  | .none =>
+    dflt
+
+def firstText (e : Option Entry) (dflt : String) : String :=
+  match e with
+  | .some _e_val =>
+    match _e_val with
+    | .msg __e_val_text =>
+      __e_val_text
+    | .sep =>
+      dflt
+  | .none =>
+    dflt
+
+end Pure

lakefile.lean

@@ -135,6 +135,7 @@ lean_lib Examples where
     `«andChainStmt.types», `«andChainStmt.def»,
     `«nameClash.types», `«nameClash.def»,
     `«tuples.types», `«tuples.def», `«tuples.proof»,
-    `«forContinue.types», `«forContinue.def», `«forContinue.proof»
+    `«forContinue.types», `«forContinue.def», `«forContinue.proof»,
+    `«optChainDiscriminantTernary.types», `«optChainDiscriminantTernary.def», `«optChainDiscriminantTernary.proof»
   ]
   extraDepTargets := #[``downloadDependencies]