Email

Fluent email builder with ordered typestate (LiquidJava ``Email`` demo). Acceptable construction order: new → set_from → add_to (+ optional set_subject) → set_body → build Phases (measure ``email_phase``): 1 empty · 2 sender set · 3 receivers · 4 body set The draft is linear: each step consumes the previous handle so you cannot skip stages or build twice.
Table of Contents

Types

EmailDraft

(type) linear
linear type EmailDraft

Functions

new_email

Start with an empty draft (phase 1).
def new_email (_ : Unit) : {e : EmailDraft | email_phase e = 1}

set_from

Record the sender (phase 1 → 2). Must be non-empty.
def set_from (sender : String | sender ≠ "") (1 e : EmailDraft | email_phase e = 1) : {out : EmailDraft | email_phase out = 2}

add_to

Add a recipient (phase 2 or 3 → 3). At least one ``add_to`` is required before ``set_body``.
def add_to (receiver : String | receiver ≠ "") (1 e : EmailDraft | email_phase e = 2 || email_phase e = 3) : {out : EmailDraft | email_phase out = 3}

set_subject

Optional subject; stays in phase 3.
def set_subject (subject : String) (1 e : EmailDraft | email_phase e = 3) : {out : EmailDraft | email_phase out = 3}

set_body

Set the body (phase 3 → 4).
def set_body (body : String | body ≠ "") (1 e : EmailDraft | email_phase e = 3) : {out : EmailDraft | email_phase out = 4}

build

Consume a complete draft and produce the rendered email text.
def build (1 e : EmailDraft | email_phase e = 4) : String

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

email_phase

uninterpreted
def email_phase : (e : EmailDraft) → Int