Spec Language Design

open util/ordering[Time]

sig ShortCode {
  value: one String
}

sig LongURL {
  value: one String
}

sig Store {
  mapping: ShortCode -> lone LongURL,
  time: one Time
}

-- The store at each time step
fact traces {
  all t: Time - last |
    let t' = t.next |
      some op: Operation | op.pre = t and op.post = t'
}

-- Invariant: all stored URLs are valid
fact validURLs {
  all s: Store, c: ShortCode |
    c in s.mapping.LongURL implies isValidURI[s.mapping[c]]
}

pred isValidURI[u: LongURL] {
  -- abstract predicate; in Alloy we'd constrain the string set
  u.value in ValidURIStrings
}

-- Shorten operation
pred shorten[s, s': Store, url: LongURL, code: ShortCode] {
  -- precondition: code is fresh
  code not in s.mapping.LongURL
  -- postcondition: new mapping added
  s'.mapping = s.mapping + code -> url
  -- frame: nothing else changes
  isValidURI[url]
}

-- Resolve operation
pred resolve[s: Store, code: ShortCode, url: LongURL] {
  -- precondition: code exists
  code in s.mapping.LongURL
  -- postcondition: correct lookup
  url = s.mapping[code]
}

-- Alloy 6 temporal version (alternative)
one sig ActiveStore {
  var entries: ShortCode -> lone LongURL
}

fact invariantAlways {
  always all c: ShortCode, u: LongURL |
    c -> u in ActiveStore.entries implies isValidURI[u]
}

pred shorten_temporal[url: LongURL, code: ShortCode] {
  code not in ActiveStore.entries.LongURL
  ActiveStore.entries' = ActiveStore.entries + code -> url
}

------------------------------ MODULE UrlShortener ------------------------------
EXTENDS Strings, FiniteSets, TLC

CONSTANTS ShortCodeSet, LongURLSet, ValidURIs

VARIABLES store, created_at

TypeInvariant ==
  /\ store \in [ShortCodeSet -> LongURLSet \cup {NULL}]
  /\ created_at \in [ShortCodeSet -> Nat \cup {NULL}]

Init ==
  /\ store = [c \in ShortCodeSet |-> NULL]
  /\ created_at = [c \in ShortCodeSet |-> NULL]

\* Invariant: all stored URLs are valid
AllStoredURLsValid ==
  \A c \in ShortCodeSet :
    store[c] # NULL => store[c] \in ValidURIs

\* Shorten operation
Shorten(url, code) ==
  /\ url \in ValidURIs                          \* precondition
  /\ store[code] = NULL                         \* code is fresh
  /\ store' = [store EXCEPT ![code] = url]      \* update store
  /\ created_at' = [created_at EXCEPT ![code] = 1]
  /\ AllStoredURLsValid'                         \* invariant maintained

\* Resolve operation (no state change)
Resolve(code) ==
  /\ store[code] # NULL                         \* precondition: exists
  /\ UNCHANGED <<store, created_at>>            \* no mutation
  \* The "output" is store[code]

\* Next state relation
Next ==
  \/ \E url \in LongURLSet, code \in ShortCodeSet : Shorten(url, code)
  \/ \E code \in ShortCodeSet : Resolve(code)

\* Temporal specification
Spec == Init /\ [][Next]_<<store, created_at>>

\* Safety property
Safety == []AllStoredURLsValid
================================================================================

module UrlShortener {
  // Types
  type ShortCode = str
  type LongURL = str

  // State
  var store: ShortCode -> LongURL
  var created_at: ShortCode -> int

  // Pure helper
  pure def isValidURI(url: LongURL): bool = {
    url.length() > 0 and url.startsWith("http")
  }

  // Initial state
  action init = all {
    store' = Map(),
    created_at' = Map(),
  }

  // Shorten operation
  action shorten(url: LongURL, code: ShortCode): bool = all {
    isValidURI(url),
    not(store.has(code)),
    store' = store.put(code, url),
    created_at' = created_at.put(code, 0),
  }

  // Resolve operation
  action resolve(code: ShortCode): bool = all {
    store.has(code),
    store' = store,
    created_at' = created_at,
  }
  // The "output" would be store.get(code)

  // Invariant
  val allStoredURLsValid: bool =
    store.keys().forall(c => isValidURI(store.get(c)))

  // Temporal property
  temporal safety = always(allStoredURLsValid)

  // Step relation
  action step = any {
    nondet url = oneOf(Set("http://example.com"))
    nondet code = oneOf(Set("abc123"))
    shorten(url, code),
    nondet code = oneOf(store.keys())
    resolve(code),
  }
}

types
  ShortCode = seq of char
  inv sc == len sc >= 6 and len sc <= 10;

  LongURL = seq of char
  inv url == isValidURI(url);

state UrlShortener of
  store : map ShortCode to LongURL
  created_at : map ShortCode to nat
inv mk_UrlShortener(s, c) ==
  dom s = dom c and
  forall code in set dom s & isValidURI(s(code))
init s == s = mk_UrlShortener({|->}, {|->})
end

functions
  isValidURI: seq of char -> bool
  isValidURI(url) ==
    len url > 0 and url(1,...,4) = "http"

operations
  Shorten: LongURL ==> ShortCode
  Shorten(url) ==
    let code in set { generateCode() } in (
      store := store munion { code |-> url };
      created_at := created_at munion { code |-> 0 };
      return code
    )
  pre isValidURI(url)
  post url = store~(RESULT) and
       RESULT not in set dom store~ and
       card dom store = card dom store~ + 1;

  Resolve: ShortCode ==> LongURL
  Resolve(code) ==
    return store(code)
  pre code in set dom store
  post RESULT = store(code) and
       store = store~;

class ShortCode {
  var value: string
  ghost predicate Valid()
    reads this
  {
    6 <= |value| && |value| <= 10 &&
    forall i :: 0 <= i < |value| ==> IsAlphaNum(value[i])
  }
}

predicate IsValidURI(url: string) {
  |url| > 0 && url[..4] == "http"
}

class UrlShortener {
  var store: map<string, string>
  var created_at: map<string, int>

  ghost predicate Valid()
    reads this
  {
    (forall c :: c in store ==> IsValidURI(store[c])) &&
    store.Keys == created_at.Keys
  }

  constructor()
    ensures Valid()
    ensures store == map[]
  {
    store := map[];
    created_at := map[];
  }

  method Shorten(url: string) returns (code: string)
    requires IsValidURI(url)
    requires Valid()
    modifies this
    ensures Valid()
    ensures code !in old(store)
    ensures store == old(store)[code := url]
    ensures |store| == |old(store)| + 1
    ensures code in store && store[code] == url
  {
    code := GenerateCode();
    assume code !in store;  // would need real implementation
    store := store[code := url];
    created_at := created_at[code := 0];
  }

  method Resolve(code: string) returns (url: string)
    requires code in store
    requires Valid()
    ensures url == store[code]
    ensures store == old(store)
  {
    url := store[code];
  }
}

MACHINE UrlShortener

SETS
  SHORT_CODE; LONG_URL

CONSTANTS
  ValidURIs

PROPERTIES
  ValidURIs <: LONG_URL

VARIABLES
  store, created_at

INVARIANT
  store : SHORT_CODE +-> LONG_URL &     /* partial function */
  created_at : SHORT_CODE +-> NAT &
  dom(store) = dom(created_at) &
  ran(store) <: ValidURIs                /* all stored URLs valid */

INITIALISATION
  store := {} ||
  created_at := {}

EVENTS

  Shorten =
    ANY url, code WHERE
      url : ValidURIs &                  /* guard: valid URL */
      code : SHORT_CODE &
      code /: dom(store)                 /* guard: code is fresh */
    THEN
      store := store \/ {code |-> url} ||
      created_at := created_at \/ {code |-> 0}
    END;

  Resolve =
    ANY code WHERE
      code : dom(store)                  /* guard: code exists */
    THEN
      skip                               /* no state change */
    END
    /* output modeled as: store(code) */

END

-- Basic type declarations
[STRING]

-- Abbreviation definitions
ShortCode == { s: STRING | #s >= 6 /\ #s <= 10 }
LongURL == { s: STRING | IsValidURI(s) }

-- State schema
|-- UrlShortenerState ----------------------------------------
| store : ShortCode -|-> LongURL        -- partial function
| created_at : ShortCode -|-> DateTime
|--------------------------------------------------------------
| dom store = dom created_at
| ran store <: { u: LongURL | IsValidURI(u) }
|--------------------------------------------------------------

-- Initial state
|-- InitUrlShortener -----------------------------------------
| UrlShortenerState
|--------------------------------------------------------------
| store = {}
| created_at = {}
|--------------------------------------------------------------

-- Shorten operation
|-- Shorten --------------------------------------------------
| Delta UrlShortenerState               -- imports store, store'
| url? : LongURL                        -- input
| code! : ShortCode                     -- output
|--------------------------------------------------------------
| IsValidURI(url?)                      -- precondition
| code! \notin dom store                -- code is fresh
| store' = store \cup { code! |-> url?} -- update
| created_at' = created_at \cup { code! |-> now }
| #store' = #store + 1
|--------------------------------------------------------------

-- Resolve operation
|-- Resolve --------------------------------------------------
| Xi UrlShortenerState                  -- Xi = no state change
| code? : ShortCode                     -- input
| url! : LongURL                        -- output
|--------------------------------------------------------------
| code? \in dom store                   -- precondition
| url! = store(code?)                   -- output definition
|--------------------------------------------------------------

import "@typespec/http";
import "@typespec/rest";

using TypeSpec.Http;
using TypeSpec.Rest;

@doc("A short code identifier")
scalar ShortCode extends string;

@doc("A long URL")
scalar LongURL extends string;

model UrlMapping {
  @key code: ShortCode;
  url: LongURL;
  createdAt?: utcDateTime;
}

model ShortenRequest {
  url: LongURL;
}

model ShortenResponse {
  code: ShortCode;
  shortUrl: string;
}

@error
model ErrorResponse {
  code: int32;
  message: string;
}

@route("/")
namespace UrlShortener {

  @post
  @route("/shorten")
  op shorten(@body request: ShortenRequest):
    ShortenResponse | ErrorResponse;

  @get
  @route("/{code}")
  op resolve(@path code: ShortCode):
    { @statusCode statusCode: 302; @header location: string; }
    | ErrorResponse;

  @delete
  @route("/{code}")
  op remove(@path code: ShortCode):
    { @statusCode statusCode: 204; }
    | ErrorResponse;
}

// Note: TypeSpec has NO way to express:
// - store state
// - pre/postconditions
// - invariants
// - the relationship between shorten and resolve

$version: "2"

namespace com.example.urlshortener

resource UrlMapping {
    identifiers: { code: ShortCode }
    properties: { url: LongURL, createdAt: Timestamp }
    create: Shorten
    read: Resolve
    delete: Remove
}

@pattern("^[a-zA-Z0-9]{6,10}$")
string ShortCode

@pattern("^https?://.*$")
string LongURL

@http(method: "POST", uri: "/shorten")
operation Shorten {
    input := {
        @required
        url: LongURL
    }
    output := {
        @required
        code: ShortCode
        @required
        shortUrl: String
    }
    errors: [ValidationError, InternalError]
}

@readonly
@http(method: "GET", uri: "/{code}")
operation Resolve {
    input := {
        @required
        @httpLabel
        code: ShortCode
    }
    output := {
        @required
        url: LongURL
    }
    errors: [NotFoundError]
}

@idempotent
@http(method: "DELETE", uri: "/{code}")
operation Remove {
    input := {
        @required
        @httpLabel
        code: ShortCode
    }
    errors: [NotFoundError]
}

// Note: Smithy has NO way to express:
// - state transitions
// - pre/postconditions (only @required, @pattern)
// - invariants beyond simple shape constraints
// - the semantic meaning of operations

// P language version

type tShortenReq = (url: string);
type tShortenResp = (code: string, shortUrl: string);
type tResolveReq = (code: string);
type tResolveResp = (url: string);

event eShortenReq : tShortenReq;
event eShortenResp : tShortenResp;
event eResolveReq : tResolveReq;
event eResolveResp : tResolveResp;
event eError : string;

machine UrlShortenerService {
  var store: map[string, string];

  start state Ready {
    on eShortenReq do (req: tShortenReq) {
      if (!isValidURI(req.url)) {
        send client, eError, "invalid URL";
        return;
      }
      var code = generateCode();
      assert code !in store,
        "generated code already exists";
      store[code] = req.url;
      send client, eShortenResp,
        (code = code, shortUrl = format("/{0}", code));
    }

    on eResolveReq do (req: tResolveReq) {
      if (req.code !in store) {
        send client, eError, "not found";
        return;
      }
      send client, eResolveResp,
        (url = store[req.code]);
    }
  }
}

// Safety specification (monitor machine)
spec machine AllURLsValid observes eShortenReq, eShortenResp {
  start state Monitoring {
    on eShortenReq do (req: tShortenReq) {
      assert isValidURI(req.url),
        "invariant: all stored URLs must be valid";
    }
  }
}

(* ---- Lexical Grammar ---- *)

(* Identifiers *)
IDENT           = LETTER (LETTER | DIGIT | '_')* ;
UPPER_IDENT     = UPPER_LETTER (LETTER | DIGIT | '_')* ;
LOWER_IDENT     = LOWER_LETTER (LETTER | DIGIT | '_')* ;

LETTER          = 'a'..'z' | 'A'..'Z' ;
UPPER_LETTER    = 'A'..'Z' ;
LOWER_LETTER    = 'a'..'z' ;
DIGIT           = '0'..'9' ;

(* Literals *)
INT_LIT         = DIGIT+ ;
FLOAT_LIT       = DIGIT+ '.' DIGIT+ ;
STRING_LIT      = '"' (CHAR | ESCAPE)* '"' ;
BOOL_LIT        = 'true' | 'false' ;
CHAR            = <any Unicode except '"' and '\'> ;
ESCAPE          = '\' ('n' | 't' | 'r' | '\' | '"') ;
REGEX_LIT       = '/' (REGEX_CHAR)+ '/' ;
REGEX_CHAR      = <any Unicode except '/' and unescaped newline> ;

(* Keywords -- reserved, cannot be used as identifiers *)
KEYWORD         = 'service' | 'entity' | 'state' | 'operation'
                | 'input' | 'output' | 'requires' | 'ensures'
                | 'invariant' | 'fact' | 'conventions' | 'import'
                | 'module' | 'type' | 'enum' | 'transition'
                | 'one' | 'lone' | 'some' | 'set' | 'seq'
                | 'all' | 'no' | 'exists' | 'let' | 'in'
                | 'and' | 'or' | 'not' | 'implies' | 'iff'
                | 'if' | 'then' | 'else'
                | 'true' | 'false' | 'none'
                | 'pre' | 'where' | 'with' | 'the' | 'matches'
                | 'extends' | 'via' | 'when'
                | 'union' | 'intersect' | 'minus' | 'subset'
                | 'function' | 'predicate'
                | 'String' | 'Int' | 'Bool' | 'Float'
                | 'DateTime' | 'Duration'
                | 'Set' | 'Map' | 'Seq' | 'Option' ;

(* Operators *)
ARROW           = '->' ;
FAT_ARROW       = '=>' ;
PRIME           = "'" ;
DOT             = '.' ;
COMMA           = ',' ;
COLON           = ':' ;
PIPE            = '|' ;
HASH            = '#' ;
CARET           = '^' ;
AMPERSAND       = '&' ;
AT              = '@' ;
EQ              = '=' ;
NEQ             = '!=' ;
LT              = '<' ;
GT              = '>' ;
LTE             = '<=' ;
GTE             = '>=' ;
PLUS            = '+' ;
MINUS           = '-' ;
STAR            = '*' ;
SLASH           = '/' ;
LBRACE          = '{' ;
RBRACE          = '}' ;
LPAREN          = '(' ;
RPAREN          = ')' ;
LBRACKET        = '[' ;
RBRACKET        = ']' ;

(* Comments *)
LINE_COMMENT    = '//' <any>* NEWLINE ;
BLOCK_COMMENT   = '/*' <any>* '*/' ;

(* Whitespace -- ignored except as separator *)
WS              = (' ' | '\t' | '\r' | '\n')+ ;

(* ============================================================ *)
(* Top-Level Structure                                           *)
(* ============================================================ *)

spec_file       = { import_decl } service_decl ;

import_decl     = 'import' STRING_LIT ;

service_decl    = 'service' UPPER_IDENT '{'
                    { service_member }
                  '}' ;

service_member  = entity_decl
                | enum_decl
                | type_alias
                | state_decl
                | operation_decl
                | transition_decl
                | invariant_decl
                | fact_decl
                | function_decl
                | predicate_decl
                | convention_block
                ;

(* ============================================================ *)
(* Entity Declarations                                           *)
(* ============================================================ *)

entity_decl     = 'entity' UPPER_IDENT ['extends' UPPER_IDENT] '{'
                    { entity_member }
                  '}' ;

entity_member   = field_decl
                | entity_invariant
                ;

field_decl      = LOWER_IDENT ':' type_expr [field_constraint] ;

field_constraint = 'where' expr ;

entity_invariant = 'invariant' ':' expr ;

(* ============================================================ *)
(* Enum Declarations                                             *)
(* ============================================================ *)

enum_decl       = 'enum' UPPER_IDENT '{'
                    enum_value { ',' enum_value } [',']
                  '}' ;

enum_value      = UPPER_IDENT ;

(* ============================================================ *)
(* Type Aliases and Refinement Types                             *)
(* ============================================================ *)

type_alias      = 'type' UPPER_IDENT '=' type_expr ['where' expr] ;

(* ============================================================ *)
(* Type Expressions                                              *)
(* ============================================================ *)

(* Note: type_expr uses a base + suffix design to avoid left    *)
(* recursion. The relation arrow '->' is parsed as an optional  *)
(* suffix on a base type, not as a separate recursive rule.     *)

type_expr       = base_type [ '->' multiplicity base_type ] ;

base_type       = primitive_type
                | compound_type
                | option_type
                | UPPER_IDENT          (* entity, enum, or type alias ref *)
                ;

primitive_type  = 'String' | 'Int' | 'Bool' | 'Float'
                | 'DateTime' | 'Duration' ;

compound_type   = set_type | map_type | seq_type ;

set_type        = 'Set' '[' type_expr ']' ;

map_type        = 'Map' '[' type_expr ',' type_expr ']' ;

seq_type        = 'Seq' '[' type_expr ']' ;

option_type     = 'Option' '[' type_expr ']' ;

multiplicity    = 'one' | 'lone' | 'some' | 'set' ;

(* ============================================================ *)
(* State Declarations                                            *)
(* ============================================================ *)

state_decl      = 'state' '{'
                    { state_field }
                  '}' ;

state_field     = LOWER_IDENT ':' type_expr ;

(* ============================================================ *)
(* Operation Declarations                                        *)
(* ============================================================ *)

operation_decl  = 'operation' UPPER_IDENT '{'
                    [input_clause]
                    [output_clause]
                    [requires_clause]
                    [ensures_clause]
                  '}' ;

input_clause    = 'input' ':' param_list ;

output_clause   = 'output' ':' param_list ;

param_list      = param { ',' param } ;

param           = LOWER_IDENT ':' type_expr ;

requires_clause = 'requires' ':' expr_list ;

ensures_clause  = 'ensures' ':' expr_list ;

(* expr_list uses NEWLINE as separator. Within requires/ensures *)
(* blocks, each line is an independent expression; all lines    *)
(* are implicitly conjoined (AND'd). A NEWLINE is significant   *)
(* here: it separates consecutive expressions. Explicit 'and'   *)
(* within a single line still works for inline conjunction.     *)

expr_list       = expr { NEWLINE expr } ;

(* ============================================================ *)
(* Transition Declarations (State Machines)                      *)
(* ============================================================ *)

transition_decl = 'transition' UPPER_IDENT '{'
                    'entity' ':' UPPER_IDENT
                    'field' ':' LOWER_IDENT
                    { transition_rule }
                  '}' ;

transition_rule = enum_value '->' enum_value 'via' UPPER_IDENT
                  ['when' expr] ;

(* ============================================================ *)
(* Invariants and Facts                                          *)
(* ============================================================ *)

invariant_decl  = 'invariant' [LOWER_IDENT] ':' expr ;

fact_decl       = 'fact' [LOWER_IDENT] ':' expr ;

(* ============================================================ *)
(* User-Defined Functions and Predicates                         *)
(* ============================================================ *)

(* Functions return a typed value; predicates return Bool.       *)
(* Both are pure (no state mutation).                            *)

function_decl   = 'function' LOWER_IDENT '(' [param_list] ')'
                  ':' type_expr '=' expr ;

predicate_decl  = 'predicate' LOWER_IDENT '(' [param_list] ')'
                  '=' expr ;

(* ============================================================ *)
(* Convention Overrides                                           *)
(* ============================================================ *)

convention_block = 'conventions' '{'
                     { convention_rule }
                   '}' ;

convention_rule  = convention_target '.' convention_prop '=' convention_val ;

convention_target = UPPER_IDENT ;

convention_prop  = LOWER_IDENT
                 | LOWER_IDENT STRING_LIT   (* e.g., http_header "Location" *)
                 ;

convention_val   = STRING_LIT | INT_LIT | BOOL_LIT | expr ;

(* ============================================================ *)
(* Expressions                                                   *)
(* ============================================================ *)

(* Precedence from lowest (top) to highest (bottom).            *)
(* See section 2.4 for the full precedence table.               *)

expr            = or_expr ;

or_expr         = and_expr { 'or' and_expr } ;

and_expr        = not_expr { 'and' not_expr } ;

not_expr        = 'not' not_expr
                | implies_expr
                ;

implies_expr    = comparison_expr ['implies' comparison_expr]
                | comparison_expr ['iff' comparison_expr]
                ;

comparison_expr = set_op_expr { comp_op set_op_expr } ;

comp_op         = '=' | '!=' | '<' | '>' | '<=' | '>='
                | 'in' | 'not' 'in'
                | 'subset'                       (* A subset B *)
                | 'matches'                      (* s matches /regex/ *)
                ;

(* ---- Set-level infix operators ---- *)
(* These sit between comparison and additive so that             *)
(* 'A union B subset C' parses as '(A union B) subset C'.       *)

set_op_expr     = additive_expr
                  { ('union' | 'intersect' | 'minus') additive_expr } ;

additive_expr   = multiplicative_expr { ('+' | '-') multiplicative_expr } ;

multiplicative_expr = unary_expr { ('*' | '/') unary_expr } ;

unary_expr      = '#' unary_expr          (* cardinality *)
                | '-' unary_expr          (* negation *)
                | '^' unary_expr          (* transitive closure *)
                | with_expr
                ;

(* ---- 'with' record-update expression ---- *)
(* Parsed at a level between unary and postfix so that           *)
(*   pre(todos)[id] with { status = DONE }                      *)
(* parses as (pre(todos)[id]) with { status = DONE }.           *)

with_expr       = postfix_expr ['with' '{' field_assign
                    { ',' field_assign } '}'] ;

field_assign    = LOWER_IDENT '=' expr ;

(* ---- Postfix operators ---- *)

postfix_expr    = primary_expr { postfix_op } ;

postfix_op      = PRIME                   (* primed: store' *)
                | '.' LOWER_IDENT         (* field access *)
                | '[' expr ']'            (* indexing *)
                | '(' [arg_list] ')'      (* function call *)
                ;

arg_list        = expr { ',' expr } ;

(* ---- Primary expressions ---- *)

primary_expr    = INT_LIT
                | FLOAT_LIT
                | STRING_LIT
                | BOOL_LIT
                | REGEX_LIT
                | 'none'                          (* Option empty value *)
                | IDENT
                | 'pre' '(' IDENT ')'            (* pre-state reference *)
                | quantifier_expr
                | the_expr
                | some_wrap_expr
                | set_or_map_expr
                | sequence_literal
                | constructor_expr
                | lambda_expr
                | if_expr
                | let_expr
                | '(' expr ')'
                ;

(* ---- Quantifier expressions ---- *)
(* 'some' as quantifier: 'some x in S | P' -- uses 'in' and '|'. *)
(* Multi-variable: 'all x in A, y in B | P'.                     *)

quantifier_expr = quantifier quant_binding { ',' quant_binding }
                  '|' expr ;

quant_binding   = LOWER_IDENT 'in' expr ;

quantifier      = 'all' | 'some' | 'no' | 'exists' ;

(* ---- Disambiguation: some(expr) vs some x in ... ---- *)
(* 'some' followed by '(' is ambiguous. We resolve it by        *)
(* lookahead: if we see 'some' '(' expr ')' where the token     *)
(* after ')' is NOT 'in', it is an Option wrapper. If 'some'    *)
(* is followed by LOWER_IDENT 'in', it is a quantifier (handled *)
(* by quantifier_expr above). The dedicated some_wrap_expr rule *)
(* matches only the Option-wrapping case.                        *)

some_wrap_expr  = 'some' '(' expr ')' ;
  (* Constraint: must not be followed by 'in'; if the intent is *)
  (* a quantifier with parenthesized domain, use explicit form  *)
  (* 'some x in (S) | P'.                                       *)

(* ---- 'the' expression (definite description) ---- *)
(* Selects the unique element satisfying a predicate.            *)
(* Example: the s in sessions | sessions[s].access_token = t    *)

the_expr        = 'the' LOWER_IDENT 'in' expr '|' expr ;

(* ---- Lambda expressions ---- *)
(* Used in higher-order built-in calls like sum(coll, i => ...) *)

lambda_expr     = LOWER_IDENT '=>' expr ;

(* ---- Constructor expressions ---- *)
(* Creates an entity/record value: Name { field = val, ... }     *)

constructor_expr = UPPER_IDENT '{' field_assign { ',' field_assign } '}' ;

(* ---- Set, map, and relation literals ---- *)
(* We unify set literals, set comprehensions, and map/relation   *)
(* pair literals into a single rule with ordered alternatives.   *)

set_or_map_expr = '{' '}'                                   (* empty set/map *)
                | '{' LOWER_IDENT 'in' expr '|' expr '}'   (* set comprehension *)
                | '{' expr '->' expr
                    { ',' expr '->' expr } '}'              (* map/relation literal *)
                | '{' expr { ',' expr } '}'                 (* set literal *)
                ;

(* ---- Sequence literals ---- *)

sequence_literal = '[' ']'                                  (* empty sequence *)
                 | '[' expr { ',' expr } ']'                (* non-empty sequence *)
                 ;

(* ---- Conditional and let ---- *)

if_expr         = 'if' expr 'then' expr 'else' expr ;

let_expr        = 'let' LOWER_IDENT '=' expr 'in' expr ;

(* ============================================================ *)
(* Module System                                                 *)
(* ============================================================ *)

(* Files can import other spec files. The import makes all
   entities, types, and enums from the imported file available
   in the current scope. *)

(* Example:
     import "common/types.spec"
     import "auth/entities.spec"
*)

State = { field_name -> value | field_name in state_decl.fields }

operation Shorten {
  ensures:
    code not in pre(store)    // code was NOT in store before this operation
    store'[code] = url        // code IS in store after this operation
}

ensures:
  store'[code] = url          // post-state: code maps to url
  #store' = #store + 1        // post-size = pre-size + 1 (unprimed = pre-state)
  store' = store + {code -> url}  // post = pre + new mapping

all c in store | all d in store |
  (c != d) implies (store[c] != store[d])
// No two codes map to the same URL

{ c in store | store[c].startsWith("https") }
// The set of all codes whose URLs start with https

service UrlShortener {

  // --- Type Definitions ---

  type ShortCode = String where len(value) >= 6 and len(value) <= 10
                              and value matches /^[a-zA-Z0-9]+$/

  type LongURL = String where len(value) > 0 and isValidURI(value)

  type BaseURL = String where isValidURI(value)

  // --- Entities ---

  entity UrlMapping {
    code: ShortCode
    url: LongURL
    created_at: DateTime
    click_count: Int where value >= 0

    invariant: isValidURI(url)
  }

  // --- State ---

  state {
    store: ShortCode -> lone LongURL       // partial function
    metadata: ShortCode -> lone UrlMapping  // full entity lookup
    base_url: BaseURL                       // configuration
  }

  // --- Operations ---

  operation Shorten {
    input:  url: LongURL
    output: code: ShortCode, short_url: String

    requires:
      isValidURI(url)

    ensures:
      code not in pre(store)                  // code was fresh
      store' = pre(store) + {code -> url}     // mapping added
      short_url = base_url + "/" + code       // URL constructed
      #store' = #pre(store) + 1               // exactly one added
      metadata'[code].url = url               // entity synced
      metadata'[code].click_count = 0         // initialized
  }

  operation Resolve {
    input:  code: ShortCode
    output: url: LongURL

    requires:
      code in store

    ensures:
      url = store[code]                       // correct lookup
      store' = store                          // state unchanged
      metadata'[code].click_count =
        pre(metadata)[code].click_count + 1   // increment clicks
  }

  operation Delete {
    input: code: ShortCode

    requires:
      code in store

    ensures:
      code not in store'                      // removed
      code not in metadata'                   // entity removed
      #store' = #pre(store) - 1               // exactly one removed
  }

  operation ListAll {
    output: entries: Set[UrlMapping]

    requires:
      true                                    // no precondition

    ensures:
      entries = { m in metadata | true }      // all mappings
      store' = store                          // no mutation
  }

  // --- Global Invariants ---

  invariant allURLsValid:
    all c in store | isValidURI(store[c])

  invariant metadataConsistent:
    dom(store) = dom(metadata)

  invariant clickCountNonNegative:
    all c in metadata | metadata[c].click_count >= 0

  // --- Convention Overrides ---

  conventions {
    Shorten.http_method = "POST"
    Shorten.http_path = "/shorten"
    Shorten.http_status_success = 201

    Resolve.http_method = "GET"
    Resolve.http_path = "/{code}"
    Resolve.http_status_success = 302
    Resolve.http_header "Location" = output.url

    Delete.http_method = "DELETE"
    Delete.http_path = "/{code}"
    Delete.http_status_success = 204

    ListAll.http_method = "GET"
    ListAll.http_path = "/urls"
    ListAll.http_status_success = 200
  }
}

service TodoList {

  // --- Enums ---

  enum Status {
    TODO,
    IN_PROGRESS,
    DONE,
    ARCHIVED
  }

  enum Priority {
    LOW,
    MEDIUM,
    HIGH,
    URGENT
  }

  // --- Entities ---

  entity Todo {
    id: Int where value > 0
    title: String where len(value) >= 1 and len(value) <= 200
    description: Option[String]
    status: Status
    priority: Priority
    created_at: DateTime
    updated_at: DateTime
    completed_at: Option[DateTime]
    tags: Set[String]

    invariant: status = DONE implies completed_at != none
    invariant: status != DONE implies completed_at = none
    invariant: updated_at >= created_at
  }

  // --- State ---

  state {
    todos: Int -> lone Todo         // id to todo mapping
    next_id: Int                    // auto-increment counter
  }

  // --- State Machine ---

  transition TodoLifecycle {
    entity: Todo
    field: status

    TODO        -> IN_PROGRESS  via StartWork
    TODO        -> ARCHIVED     via Archive
    IN_PROGRESS -> DONE         via Complete
    IN_PROGRESS -> TODO         via PauseWork
    DONE        -> ARCHIVED     via Archive
    DONE        -> IN_PROGRESS  via Reopen     when updated_at > completed_at
  }

  // --- Operations ---

  operation CreateTodo {
    input:  title: String, description: Option[String],
            priority: Priority, tags: Set[String]
    output: todo: Todo

    requires:
      len(title) >= 1

    ensures:
      todo.id = pre(next_id)
      todo.title = title
      todo.description = description
      todo.status = TODO
      todo.priority = priority
      todo.tags = tags
      todo.completed_at = none
      next_id' = pre(next_id) + 1
      todos' = pre(todos) + {todo.id -> todo}
      #todos' = #pre(todos) + 1
  }

  operation GetTodo {
    input:  id: Int
    output: todo: Todo

    requires:
      id in todos

    ensures:
      todo = todos[id]
      todos' = todos
  }

  operation ListTodos {
    input:  status_filter: Option[Status],
            priority_filter: Option[Priority],
            tag_filter: Option[String]
    output: results: Seq[Todo]

    requires:
      true

    ensures:
      all t in results |
        t in ran(todos)
        and (status_filter = none or t.status = status_filter)
        and (priority_filter = none or t.priority = priority_filter)
        and (tag_filter = none or tag_filter in t.tags)
      todos' = todos
  }

  operation UpdateTodo {
    input:  id: Int, title: Option[String],
            description: Option[String], priority: Option[Priority],
            tags: Option[Set[String]]
    output: todo: Todo

    requires:
      id in todos

    ensures:
      todo.id = id
      title != none implies todo.title = title
      description != none implies todo.description = description
      priority != none implies todo.priority = priority
      tags != none implies todo.tags = tags
      title = none implies todo.title = pre(todos)[id].title
      todo.status = pre(todos)[id].status
      todo.updated_at >= pre(todos)[id].updated_at
      todos' = pre(todos) + {id -> todo}
  }

  operation StartWork {
    input: id: Int
    output: todo: Todo

    requires:
      id in todos
      todos[id].status = TODO

    ensures:
      todo = pre(todos)[id] with { status = IN_PROGRESS }
      todos' = pre(todos) + {id -> todo}
  }

  operation Complete {
    input: id: Int
    output: todo: Todo

    requires:
      id in todos
      todos[id].status = IN_PROGRESS

    ensures:
      todo = pre(todos)[id] with {
        status = DONE,
        completed_at = some(now())
      }
      todos' = pre(todos) + {id -> todo}
  }

  operation Reopen {
    input: id: Int
    output: todo: Todo

    requires:
      id in todos
      todos[id].status = DONE

    ensures:
      todo = pre(todos)[id] with {
        status = IN_PROGRESS,
        completed_at = none
      }
      todos' = pre(todos) + {id -> todo}
  }

  operation Archive {
    input: id: Int

    requires:
      id in todos
      todos[id].status in {TODO, DONE}

    ensures:
      todos'[id].status = ARCHIVED
      #todos' = #pre(todos)
  }

  operation DeleteTodo {
    input: id: Int

    requires:
      id in todos

    ensures:
      id not in todos'
      #todos' = #pre(todos) - 1
  }

  // --- Global Invariants ---

  invariant idsPositive:
    all id in todos | id > 0

  invariant nextIdMonotonic:
    next_id > 0

  invariant nextIdFresh:
    next_id not in todos

  invariant completedImpliesDone:
    all id in todos |
      todos[id].status = DONE iff todos[id].completed_at != none

  // --- Conventions ---

  conventions {
    CreateTodo.http_path = "/todos"
    CreateTodo.http_status_success = 201

    GetTodo.http_path = "/todos/{id}"
    ListTodos.http_path = "/todos"

    StartWork.http_method = "POST"
    StartWork.http_path = "/todos/{id}/start"

    Complete.http_method = "POST"
    Complete.http_path = "/todos/{id}/complete"

    Reopen.http_method = "POST"
    Reopen.http_path = "/todos/{id}/reopen"

    Archive.http_method = "POST"
    Archive.http_path = "/todos/{id}/archive"
  }
}

service AuthService {

  // --- Types ---

  type Email = String where value matches /^[^@]+@[^@]+\.[^@]+$/
  type PasswordHash = String where len(value) = 64   // SHA-256 hex
  type Token = String where len(value) = 128
  type UserId = Int where value > 0

  // --- Enums ---

  enum TokenType {
    ACCESS,
    REFRESH,
    RESET
  }

  // --- Entities ---

  entity User {
    id: UserId
    email: Email
    password_hash: PasswordHash
    display_name: String where len(value) >= 1 and len(value) <= 100
    created_at: DateTime
    last_login: Option[DateTime]
    is_active: Bool

    invariant: len(email) > 0
  }

  entity Session {
    id: Int where value > 0
    user_id: UserId
    access_token: Token
    refresh_token: Token
    access_expires_at: DateTime
    refresh_expires_at: DateTime
    created_at: DateTime
    is_revoked: Bool

    invariant: access_expires_at > created_at
    invariant: refresh_expires_at > access_expires_at
    invariant: access_token != refresh_token
  }

  entity LoginAttempt {
    email: Email
    timestamp: DateTime
    success: Bool
  }

  // --- State ---

  state {
    users: UserId -> lone User
    sessions: Int -> lone Session
    login_attempts: Seq[LoginAttempt]
    user_by_email: Email -> lone User          // index
    next_user_id: UserId
    next_session_id: Int
  }

  // --- Operations ---

  operation Register {
    input:  email: Email, password: String,
            display_name: String
    output: user: User

    requires:
      email not in user_by_email               // email unique
      len(password) >= 8                       // password policy
      len(display_name) >= 1

    ensures:
      user.id = pre(next_user_id)
      user.email = email
      user.password_hash = hash(password)
      user.display_name = display_name
      user.is_active = true
      user.last_login = none
      next_user_id' = pre(next_user_id) + 1
      users' = pre(users) + {user.id -> user}
      user_by_email' = pre(user_by_email) + {email -> user}
      #users' = #pre(users) + 1
  }

  operation Login {
    input:  email: Email, password: String
    output: session: Session

    requires:
      email in user_by_email
      user_by_email[email].is_active = true
      user_by_email[email].password_hash = hash(password)
      recentFailedAttempts(email) < 5          // rate limiting

    ensures:
      let user = user_by_email[email] in
        session.user_id = user.id
        and session.is_revoked = false
        and session.access_expires_at > now()
        and session.refresh_expires_at > session.access_expires_at
        and sessions' = pre(sessions) + {session.id -> session}
        and users'[user.id].last_login = some(now())
        and login_attempts' = pre(login_attempts)
             + [LoginAttempt { email = email,
                               timestamp = now(),
                               success = true }]
  }

  operation LoginFailed {
    input: email: Email

    requires:
      email in user_by_email
      user_by_email[email].password_hash != hash(input_password)

    ensures:
      sessions' = sessions
      users' = users
      login_attempts' = pre(login_attempts)
        + [LoginAttempt { email = email,
                          timestamp = now(),
                          success = false }]
  }

  operation RefreshToken {
    input:  refresh_token: Token
    output: new_session: Session

    requires:
      some s in sessions |
        sessions[s].refresh_token = refresh_token
        and sessions[s].is_revoked = false
        and sessions[s].refresh_expires_at > now()

    ensures:
      let old_session = (the s in sessions |
        sessions[s].refresh_token = refresh_token) in
        // Old session revoked
        sessions'[old_session].is_revoked = true
        // New session created
        and new_session.user_id = pre(sessions)[old_session].user_id
        and new_session.is_revoked = false
        and new_session.access_expires_at > now()
        and sessions' = pre(sessions)
             + {old_session -> pre(sessions)[old_session]
                  with { is_revoked = true }}
             + {new_session.id -> new_session}
  }

  operation RequestPasswordReset {
    input:  email: Email
    output: reset_token: Token

    requires:
      email in user_by_email
      user_by_email[email].is_active = true

    ensures:
      // A new session of type RESET is created
      // (modeled as a session with special properties)
      some s in sessions' |
        s not in pre(sessions)
        and sessions'[s].user_id = user_by_email[email].id
        and sessions'[s].access_expires_at > now()
      users' = users
  }

  operation ResetPassword {
    input:  reset_token: Token, new_password: String

    requires:
      some s in sessions |
        sessions[s].access_token = reset_token
        and sessions[s].is_revoked = false
        and sessions[s].access_expires_at > now()
      len(new_password) >= 8

    ensures:
      let s = (the s in sessions |
        sessions[s].access_token = reset_token) in
        let user_id = pre(sessions)[s].user_id in
          users'[user_id].password_hash = hash(new_password)
          and sessions'[s].is_revoked = true
  }

  operation Logout {
    input: access_token: Token

    requires:
      some s in sessions |
        sessions[s].access_token = access_token
        and sessions[s].is_revoked = false

    ensures:
      let s = (the s in sessions |
        sessions[s].access_token = access_token) in
        sessions'[s].is_revoked = true
        and users' = users
  }

  // --- Helper Functions ---

  fact recentFailedAttemptsDef:
    all email in dom(user_by_email) |
      recentFailedAttempts(email) =
        #{ a in login_attempts |
           a.email = email
           and a.success = false
           and a.timestamp > now() - minutes(15) }

  // --- Global Invariants ---

  invariant uniqueEmails:
    all u1 in users, u2 in users |
      u1 != u2 implies users[u1].email != users[u2].email

  invariant emailIndexConsistent:
    all email in user_by_email |
      user_by_email[email] in ran(users)
      and user_by_email[email].email = email

  invariant sessionBelongsToUser:
    all s in sessions |
      sessions[s].user_id in users

  invariant revokedSessionsStayRevoked:
    all s in sessions |
      pre(sessions)[s].is_revoked = true implies sessions'[s].is_revoked = true

  invariant accessTokensUnique:
    all s1 in sessions, s2 in sessions |
      s1 != s2 implies
        sessions[s1].access_token != sessions[s2].access_token

  invariant rateLimitEnforced:
    all email in user_by_email |
      recentFailedAttempts(email) < 5 or
        (no op: Login | op.input.email = email)

  // --- Conventions ---

  conventions {
    Register.http_path = "/auth/register"
    Register.http_status_success = 201

    Login.http_path = "/auth/login"
    Login.http_method = "POST"
    Login.http_status_success = 200

    RefreshToken.http_path = "/auth/refresh"
    RefreshToken.http_method = "POST"

    RequestPasswordReset.http_path = "/auth/password-reset"
    RequestPasswordReset.http_method = "POST"

    ResetPassword.http_path = "/auth/password-reset/confirm"
    ResetPassword.http_method = "POST"

    Logout.http_path = "/auth/logout"
    Logout.http_method = "POST"
    Logout.http_status_success = 204
  }
}

service OrderService {

  // --- Types ---

  type Money = Int where value >= 0           // cents
  type Quantity = Int where value > 0
  type SKU = String where len(value) >= 3 and len(value) <= 20
  type OrderId = Int where value > 0
  type CustomerId = Int where value > 0

  // --- Enums ---

  enum OrderStatus {
    DRAFT,
    PLACED,
    PAID,
    SHIPPED,
    DELIVERED,
    CANCELLED,
    RETURNED
  }

  enum PaymentStatus {
    PENDING,
    AUTHORIZED,
    CAPTURED,
    REFUNDED,
    FAILED
  }

  // --- Entities ---

  entity Product {
    sku: SKU
    name: String where len(value) >= 1
    price: Money
    description: Option[String]

    invariant: price > 0
  }

  entity LineItem {
    id: Int where value > 0
    product_sku: SKU
    quantity: Quantity
    unit_price: Money
    line_total: Money

    invariant: line_total = unit_price * quantity
    invariant: unit_price > 0
  }

  entity Order {
    id: OrderId
    customer_id: CustomerId
    status: OrderStatus
    items: Set[LineItem]
    subtotal: Money
    tax: Money
    total: Money
    created_at: DateTime
    updated_at: DateTime
    shipped_at: Option[DateTime]
    delivered_at: Option[DateTime]

    invariant: subtotal = sum(items, i => i.line_total)
    invariant: total = subtotal + tax
    invariant: #items > 0 implies total > 0
    invariant: status = SHIPPED implies shipped_at != none
    invariant: status = DELIVERED implies delivered_at != none
    invariant: delivered_at != none implies shipped_at != none
  }

  entity Payment {
    id: Int where value > 0
    order_id: OrderId
    amount: Money
    status: PaymentStatus
    created_at: DateTime

    invariant: amount > 0
  }

  entity InventoryEntry {
    sku: SKU
    available: Int where value >= 0
    reserved: Int where value >= 0

    invariant: available >= 0
    invariant: reserved >= 0
  }

  // --- State ---

  state {
    orders: OrderId -> lone Order
    products: SKU -> lone Product
    inventory: SKU -> lone InventoryEntry
    payments: Int -> lone Payment
    next_order_id: OrderId
    next_payment_id: Int
  }

  // --- State Machine ---

  transition OrderLifecycle {
    entity: Order
    field: status

    DRAFT      -> PLACED     via PlaceOrder
    DRAFT      -> CANCELLED  via CancelOrder
    PLACED     -> PAID       via RecordPayment     when paymentCaptured(order_id)
    PLACED     -> CANCELLED  via CancelOrder
    PAID       -> SHIPPED    via ShipOrder
    PAID       -> CANCELLED  via CancelOrder       when refundIssued(order_id)
    SHIPPED    -> DELIVERED  via ConfirmDelivery
    DELIVERED  -> RETURNED   via ProcessReturn      when withinReturnWindow(order_id)
  }

  // --- Operations ---

  operation CreateDraftOrder {
    input:  customer_id: CustomerId
    output: order: Order

    requires:
      true

    ensures:
      order.id = pre(next_order_id)
      order.customer_id = customer_id
      order.status = DRAFT
      order.items = {}
      order.subtotal = 0
      order.tax = 0
      order.total = 0
      next_order_id' = pre(next_order_id) + 1
      orders' = pre(orders) + {order.id -> order}
  }

  operation AddLineItem {
    input:  order_id: OrderId, sku: SKU, quantity: Quantity
    output: order: Order

    requires:
      order_id in orders
      orders[order_id].status = DRAFT
      sku in products
      sku in inventory
      inventory[sku].available >= quantity

    ensures:
      let product = products[sku] in
      let item = LineItem {
        product_sku = sku,
        quantity = quantity,
        unit_price = product.price,
        line_total = product.price * quantity
      } in
        order = pre(orders)[order_id] with {
          items = pre(orders)[order_id].items + {item},
          subtotal = pre(orders)[order_id].subtotal + item.line_total,
          total = pre(orders)[order_id].subtotal + item.line_total
                  + pre(orders)[order_id].tax
        }
        orders' = pre(orders) + {order_id -> order}
        // Reserve inventory
        inventory'[sku].reserved =
          pre(inventory)[sku].reserved + quantity
        inventory'[sku].available =
          pre(inventory)[sku].available - quantity
  }

  operation RemoveLineItem {
    input:  order_id: OrderId, item_id: Int
    output: order: Order

    requires:
      order_id in orders
      orders[order_id].status = DRAFT
      some i in orders[order_id].items | i.id = item_id

    ensures:
      let removed = (the i in pre(orders)[order_id].items |
                      i.id = item_id) in
        order = pre(orders)[order_id] with {
          items = pre(orders)[order_id].items - {removed},
          subtotal = pre(orders)[order_id].subtotal - removed.line_total,
          total = pre(orders)[order_id].subtotal - removed.line_total
                  + pre(orders)[order_id].tax
        }
        orders' = pre(orders) + {order_id -> order}
        // Release reserved inventory
        inventory'[removed.product_sku].reserved =
          pre(inventory)[removed.product_sku].reserved - removed.quantity
        inventory'[removed.product_sku].available =
          pre(inventory)[removed.product_sku].available + removed.quantity
  }

  operation PlaceOrder {
    input:  order_id: OrderId
    output: order: Order

    requires:
      order_id in orders
      orders[order_id].status = DRAFT
      #orders[order_id].items > 0

    ensures:
      order = pre(orders)[order_id] with { status = PLACED }
      orders' = pre(orders) + {order_id -> order}
      inventory' = inventory    // reservations stay
  }

  operation RecordPayment {
    input:  order_id: OrderId, amount: Money
    output: payment: Payment

    requires:
      order_id in orders
      orders[order_id].status = PLACED
      amount = orders[order_id].total

    ensures:
      payment.order_id = order_id
      payment.amount = amount
      payment.status = CAPTURED
      orders'[order_id].status = PAID
      payments' = pre(payments) + {payment.id -> payment}
      next_payment_id' = pre(next_payment_id) + 1
  }

  operation ShipOrder {
    input:  order_id: OrderId
    output: order: Order

    requires:
      order_id in orders
      orders[order_id].status = PAID

    ensures:
      order = pre(orders)[order_id] with {
        status = SHIPPED,
        shipped_at = some(now())
      }
      orders' = pre(orders) + {order_id -> order}
      // Committed inventory: reduce reserved count
      all item in order.items |
        inventory'[item.product_sku].reserved =
          pre(inventory)[item.product_sku].reserved - item.quantity
  }

  operation ConfirmDelivery {
    input:  order_id: OrderId
    output: order: Order

    requires:
      order_id in orders
      orders[order_id].status = SHIPPED

    ensures:
      order = pre(orders)[order_id] with {
        status = DELIVERED,
        delivered_at = some(now())
      }
      orders' = pre(orders) + {order_id -> order}
  }

  operation CancelOrder {
    input:  order_id: OrderId
    output: order: Order

    requires:
      order_id in orders
      orders[order_id].status in {DRAFT, PLACED, PAID}

    ensures:
      order = pre(orders)[order_id] with { status = CANCELLED }
      orders' = pre(orders) + {order_id -> order}
      // Release all reserved inventory
      all item in pre(orders)[order_id].items |
        inventory'[item.product_sku].available =
          pre(inventory)[item.product_sku].available + item.quantity
        and inventory'[item.product_sku].reserved =
          pre(inventory)[item.product_sku].reserved - item.quantity
      // Refund if paid
      orders[order_id].status = PAID implies
        some p in payments' |
          p not in pre(payments)
          and payments'[p].order_id = order_id
          and payments'[p].status = REFUNDED
  }

  operation ProcessReturn {
    input:  order_id: OrderId
    output: order: Order

    requires:
      order_id in orders
      orders[order_id].status = DELIVERED
      // Within 30-day return window
      orders[order_id].delivered_at != none
      now() - orders[order_id].delivered_at <= days(30)

    ensures:
      order = pre(orders)[order_id] with { status = RETURNED }
      orders' = pre(orders) + {order_id -> order}
      // Restore inventory
      all item in pre(orders)[order_id].items |
        inventory'[item.product_sku].available =
          pre(inventory)[item.product_sku].available + item.quantity
      // Issue refund
      some p in payments' |
        p not in pre(payments)
        and payments'[p].order_id = order_id
        and payments'[p].status = REFUNDED
        and payments'[p].amount = pre(orders)[order_id].total
  }

  operation GetOrder {
    input:  order_id: OrderId
    output: order: Order

    requires:
      order_id in orders

    ensures:
      order = orders[order_id]
      orders' = orders
  }

  operation ListOrders {
    input:  customer_id: Option[CustomerId],
            status_filter: Option[OrderStatus]
    output: results: Seq[Order]

    requires:
      true

    ensures:
      all o in results |
        o in ran(orders)
        and (customer_id = none or o.customer_id = customer_id)
        and (status_filter = none or o.status = status_filter)
      orders' = orders
  }

  // --- Global Invariants ---

  invariant orderTotalConsistency:
    all oid in orders |
      orders[oid].total =
        sum(orders[oid].items, i => i.line_total) + orders[oid].tax

  invariant lineItemTotalConsistency:
    all oid in orders |
      all item in orders[oid].items |
        item.line_total = item.unit_price * item.quantity

  invariant inventoryNonNegative:
    all sku in inventory |
      inventory[sku].available >= 0
      and inventory[sku].reserved >= 0

  invariant placedOrdersHaveItems:
    all oid in orders |
      orders[oid].status != DRAFT implies #orders[oid].items > 0

  invariant paidOrdersHavePayments:
    all oid in orders |
      orders[oid].status in {PAID, SHIPPED, DELIVERED} implies
        some pid in payments |
          payments[pid].order_id = oid
          and payments[pid].status = CAPTURED

  invariant cancelledPaidOrdersHaveRefunds:
    all oid in orders |
      orders[oid].status = CANCELLED implies
        (all pid in payments |
          payments[pid].order_id = oid and payments[pid].status = CAPTURED
          implies
          some rid in payments |
            payments[rid].order_id = oid and payments[rid].status = REFUNDED)

  invariant inventoryReservationsMatchOrders:
    all sku in inventory |
      inventory[sku].reserved =
        sum({ item in { oid in orders | orders[oid].status in {DRAFT, PLACED, PAID} } |
              some i in orders[item].items | i.product_sku = sku },
            order_id => sum(
              { i in orders[order_id].items | i.product_sku = sku },
              i => i.quantity))

  // --- Conventions ---

  conventions {
    CreateDraftOrder.http_path = "/orders"
    CreateDraftOrder.http_status_success = 201

    AddLineItem.http_method = "POST"
    AddLineItem.http_path = "/orders/{order_id}/items"
    AddLineItem.http_status_success = 201

    RemoveLineItem.http_method = "DELETE"
    RemoveLineItem.http_path = "/orders/{order_id}/items/{item_id}"

    PlaceOrder.http_method = "POST"
    PlaceOrder.http_path = "/orders/{order_id}/place"

    RecordPayment.http_method = "POST"
    RecordPayment.http_path = "/orders/{order_id}/payments"
    RecordPayment.http_status_success = 201

    ShipOrder.http_method = "POST"
    ShipOrder.http_path = "/orders/{order_id}/ship"

    ConfirmDelivery.http_method = "POST"
    ConfirmDelivery.http_path = "/orders/{order_id}/deliver"

    CancelOrder.http_method = "POST"
    CancelOrder.http_path = "/orders/{order_id}/cancel"

    ProcessReturn.http_method = "POST"
    ProcessReturn.http_path = "/orders/{order_id}/return"

    GetOrder.http_path = "/orders/{order_id}"
    ListOrders.http_path = "/orders"
  }
}

tags: Set[String]           // SQL: junction table or JSON array
                            // JSON: array (unique values enforced at app layer)

login_attempts: Seq[LoginAttempt]   // SQL: table with ordering column
                                    // JSON: array

settings: Map[String, String]       // SQL: key-value table or JSON column
                                    // JSON: object

description: Option[String]         // SQL: nullable column
                                    // JSON: field may be absent or null

entity Todo {
  id: Int where value > 0
  title: String where len(value) >= 1 and len(value) <= 200
  status: Status
  tags: Set[String]
}

CREATE TABLE todos (
  id INTEGER PRIMARY KEY CHECK (id > 0),
  title VARCHAR(200) NOT NULL CHECK (length(title) >= 1),
  status VARCHAR(20) NOT NULL CHECK (status IN ('TODO','IN_PROGRESS','DONE','ARCHIVED')),
  tags JSONB DEFAULT '[]'
);

state {
  store: ShortCode -> lone LongURL
}

Set[T]          -- for any type T
Map[K, V]       -- for any types K, V
Seq[T]          -- for any type T
Option[T]       -- for any type T

type ShortCode = String where len(value) >= 6 and len(value) <= 10
                            and value matches /^[a-zA-Z0-9]+$/

type Money = Int where value >= 0

type Percentage = Float where value >= 0.0 and value <= 100.0

type Email = String where value matches /^[^@]+@[^@]+\.[^@]+$/

error[E001]: Expected ':' after field name
  --> url_shortener.spec:12:15
   |
12 |     code ShortCode
   |          ^^^^^^^^^^ expected ':' here
   |
help: add a colon between the field name and type
   |
12 |     code: ShortCode
   |         +

error[E101]: Type mismatch in ensures clause
  --> url_shortener.spec:28:7
   |
28 |     code not in pre(store)
   |     ^^^^ expected ShortCode, found LongURL
   |
note: 'code' is declared as type LongURL in the output clause (line 24)
note: 'store' maps ShortCode -> LongURL, so membership test requires ShortCode
help: did you mean to check the output 'code' field? check the output type declaration

error[E201]: Multiplicity violation in ensures clause
  --> url_shortener.spec:30:7
   |
30 |     store'[code] = url1
31 |     store'[code] = url2
   |     ^^^^^^^^^^^^^^^^^^ 'store' has multiplicity 'lone' (at most one target per source)
   |     but postcondition assigns two different values for the same key
   |
note: store is declared as 'ShortCode -> lone LongURL' at line 18
note: 'lone' means each ShortCode maps to at most one LongURL

warning[W301]: Operation 'Resolve' may be unreachable
  --> url_shortener.spec:33:3
   |
33 |   operation Resolve {
   |   ^^^^^^^^^^^^^^^^^
   |
note: Resolve requires 'code in store' (line 37)
note: No operation in this service adds entries to 'store'
      (Shorten's ensures clause does not establish 'code in store' for arbitrary codes)
help: verify that at least one operation's postcondition establishes the precondition

error[E401]: Conflicting invariants detected
  --> order_service.spec:145:3
   |
145 |   invariant: all oid in orders | #orders[oid].items > 0
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
  --> order_service.spec:48:7
   |
48  |     order.items = {}      // CreateDraftOrder ensures empty items
   |     ^^^^^^^^^^^^^^^^
   |
note: Invariant on line 145 requires all orders to have at least one item
note: But CreateDraftOrder (line 42) creates orders with empty items
note: This means the invariant is violated immediately after CreateDraftOrder
help: Either weaken the invariant to exclude DRAFT orders:
   |
145 |   invariant: all oid in orders |
   |     orders[oid].status != DRAFT implies #orders[oid].items > 0
   |
      Or change CreateDraftOrder to require at least one item

warning[W501]: Incomplete frame condition in operation 'Shorten'
  --> url_shortener.spec:25:3
   |
25 |   operation Shorten {
   |   ^^^^^^^^^^^^^^^^^
   |
note: State has fields: store, metadata, base_url
note: Shorten's ensures clause mentions: store', metadata'
note: Shorten's ensures clause does NOT mention: base_url
help: If base_url should not change, add: base_url' = base_url
      If this omission is intentional, the checker assumes unchanged fields
      remain unchanged (closed-world assumption)

error[E601]: Postcondition may not be achievable
  --> url_shortener.spec:29:7
   |
29 |     #store' = #pre(store) + 2
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^
   |
note: Operation Shorten adds exactly one mapping (store' = pre(store) + {code -> url})
note: But the cardinality postcondition claims two entries were added
note: Counterexample: pre(store) = {}, after adding one mapping, #store' = 1, not 2
help: Did you mean #store' = #pre(store) + 1?

error[E701]: Invalid state transition
  --> todo_service.spec:62:7
   |
62 |     todo = pre(todos)[id] with { status = DONE }
   |                                          ^^^^
   |
note: Operation 'StartWork' transitions status from TODO
note: But DONE is not a valid target from TODO
note: Valid transitions from TODO: IN_PROGRESS (via StartWork), ARCHIVED (via Archive)
note: Defined in transition 'TodoLifecycle' at line 38
help: Did you mean status = IN_PROGRESS?

builtin entity Caller {
  id: Int
  role: Role           // enum defined per-service
  authenticated: Bool
  scopes: Set[String]  // OAuth-style scopes
}

operation CreatePost {
  input:  title: String, body: String
  output: post: Post

  requires:
    authenticated                         // shorthand for caller.authenticated = true
    len(title) >= 1

  ensures:
    post.author_id = caller.id
    posts' = pre(posts) + {post.id -> post}
}

enum Role { User, Moderator, Admin }

operation DeleteUser {
  input:  user_id: Int

  requires:
    authenticated
    caller.role in {Admin}                // only admins

  ensures:
    user_id not in users'
}

operation BanUser {
  input:  user_id: Int

  requires:
    authenticated
    caller.role in {Admin, Moderator}     // admins or moderators

  ensures:
    users'[user_id].banned = true
}

operation UpdatePost {
  input:  post_id: Int, body: String
  output: post: Post

  requires:
    authenticated
    post_id in posts
    caller.id = posts[post_id].author_id   // ownership check

  ensures:
    post.body = body
    posts' = pre(posts) + {post_id -> post}
}

operation ReadAnalytics {
  input:  report_id: Int
  output: report: AnalyticsReport

  requires:
    authenticated
    "analytics:read" in caller.scopes

  ensures:
    report = analytics[report_id]
}

entity Order {
  id: Int
  status: OrderStatus
  total: Float
  version: Int          // auto-incremented on each write
}

operation UpdateOrder {
  input:  order_id: Int, total: Float, expected_version: Int
  output: order: Order

  requires:
    order_id in orders
    orders[order_id].version = expected_version   // conflict detection

  ensures:
    order.total = total
    order.version = pre(orders)[order_id].version + 1
    orders' = pre(orders) + {order_id -> order}
}

effect PaymentGateway {
  action Charge {
    input:  amount: Float, currency: String, token: String
    output: charge_id: String, success: Bool

    ensures:
      success implies len(charge_id) > 0
  }
}

effect EmailService {
  action Send {
    input:  to: String, subject: String, body: String
    output: sent: Bool
  }
}

operation PlaceOrder {
  input:  order_id: Int, payment_token: String
  output: confirmation: OrderConfirmation
  uses:   PaymentGateway, EmailService

  requires:
    order_id in orders
    orders[order_id].status = Pending

  ensures:
    let charge = PaymentGateway.Charge(orders[order_id].total, "USD", payment_token)
    charge.success implies orders'[order_id].status = Confirmed
    not charge.success implies orders'[order_id].status = PaymentFailed
    charge.success implies EmailService.Send(customer_email, "Order Confirmed", ...)
}

operation Shorten {
  input:  url: LongURL
  output: code: ShortCode

  requires: isValidURI(url.value)

  ensures:
    code not in pre(store)             // code is fresh (existential: SOME code exists)
    store'[code] = url
    len(code.value) >= 6 and len(code.value) <= 10
}

ensures:
  order.created_at = now()                        // assigned at execution time
  order.created_at >= pre(orders)[last_id].created_at   // monotonic

ensures:
  post.id = max(dom(posts)) + 1    // next sequential ID
  post.id not in pre(posts)         // always fresh