Spec Verification Engine

entity ShortCode {
  value: String
  invariant: len(value) >= 6
}

state {
  store: ShortCode -> lone LongURL
}

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

  requires: isValidURI(url.value)

  ensures:
    store'[code] = url
    short_url = base_url + "/" + code.value
}

operation SetStatus {
  input: order_id: OrderId, status: Status
  ensures: orders'[order_id].status = status
}

operation FreezeOrder {
  input: order_id: OrderId
  ensures: orders'[order_id].status = FROZEN
           and all o in orders' | o.status != CANCELLED
}

state {
  items: Item -> lone Price
}

invariant: all i in items | items[i] > 100
invariant: all i in items | items[i] < 50

state {
  counter: Int
}

invariant: counter > 0

// No operation creates the initial state; counter defaults to 0.

state {
  assignments: Student -> one Course    // every student has exactly one course
}

operation Unenroll {
  input: s: Student
  ensures: s not in assignments'         // student has no course
}

operation Withdraw {
  input: account_id: AccountId, amount: Money

  requires: account_id in accounts

  ensures:
    accounts'[account_id].balance = accounts[account_id].balance - amount
}

operation CreateOrder { ... ensures: orders'[id].status = PENDING }
operation CancelOrder { ... requires: orders[id].status = PENDING ... }
operation ShipOrder   { ... requires: orders[id].status = PAID ... }

// Missing: no operation transitions from PENDING to PAID.

entity AuditLog {
  timestamp: DateTime
  action: String
  user: UserId
}

// No operation reads or writes AuditLog. It is dead specification.

state {
  cache: ShortCode -> lone LongURL
}

operation Resolve {
  input: code: ShortCode
  requires: code in cache           // reads cache
  ensures: url = cache[code]
}

// No operation ever writes to cache. It is always empty.
// Therefore: Resolve's requires clause is always false.

operation Transfer {
  input: from: AccountId, to: AccountId, amount: Money, memo: String

  requires: from in accounts and to in accounts and amount > 0
  ensures: ...
}

entity Receipt {
  order_id: OrderId
  total: Money
  issued_at: DateTime
}

// No operation has output: Receipt. The entity is defined but never emitted.

operation Refund {
  input: order_id: OrderId

  requires:
    orders[order_id].status = SHIPPED
    and orders[order_id].status = CANCELLED
}

state {
  archive: Document -> lone DateTime
}

operation ArchiveDocument {
  input: doc: Document
  requires: doc in archive              // BUG: should be doc NOT in archive
  ensures: archive'[doc] = now()
}

operation CreateOrder { ensures: orders'[id].status = PENDING }
operation PayOrder    { requires: status = PENDING, ensures: status' = PAID }
operation ShipOrder   { requires: status = PAID, ensures: status' = SHIPPED }
// SHIPPED is terminal -- no outgoing transitions. This is intentional.

operation HoldOrder   { requires: status = REVIEW, ensures: status' = HELD }
// HELD has no outgoing transitions AND no operation transitions INTO REVIEW.

state {
  discounts: Customer -> lone Percent
}

invariant: discounts = {}     // no customer ever has a discount

state {
  owner: Car -> one Person         // each car has exactly one owner
}

operation TransferOwnership {
  input: car: Car, new_owner: Person
  ensures: owner'[car] = {new_owner, old_owner}  // set of two people
}

entity Product {
  price: Money
  name: String
}

invariant: all p in products | p.price > p.name   // comparing Money to String

operation Checkout {
  input: cart_id: CartId
  ensures: receipt.total = carts[cart_id].total_price
}
// "receipt" is not declared as output.
// "total_price" is not a declared field of Cart.

invariant: all c in store' | isValidURI(store'[c].value)
// store' (post-state) has no meaning in a global invariant,
// which describes a static property of any reachable state.

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

  ensures:
    all c in store | store'[c] = store[c]    // frame: all EXISTING entries preserved
    store'[code] = url
    all x in store' | isValidURI(store'[x].value)  // uses x but also references code
}

operation Ping {
  input: none
  output: msg: String
  requires: true
  ensures: true          // does literally nothing observable
}

invariant: all c in store | c = c

operation Delete {
  input: code: ShortCode
  requires: true                    // accepts every input unconditionally
  ensures: code not in store'
}

operation GetUrl {
  input: code: ShortCode
  output: url: LongURL
  requires: code in store
  ensures: url = store[code] and store' = store
}

operation Resolve {
  input: code: ShortCode
  output: url: LongURL
  requires: code in store
  ensures: url = store[code] and store' = store
}

invariant: all c in store | len(c.value) >= 6
invariant: all c in store | len(c.value) >= 1

operation Resolve {
  input: code: ShortCode
  requires: code in store and len(code.value) >= 6

  ensures: url = store[code] and store' = store
}

; ============================================================
; URL Shortener Spec -> SMT-LIB2 Translation
; ============================================================

; --- Sorts ---
(declare-sort ShortCode 0)
(declare-sort LongURL 0)

; --- Entity field accessors ---
(declare-fun sc_value (ShortCode) String)
(declare-fun lu_value (LongURL) String)

; --- State: store is a partial function ShortCode -> LongURL ---
; We model the store as a set of ShortCode (the domain) plus a function
; for the mapping.
(declare-fun store_domain (ShortCode) Bool)          ; pre-state domain membership
(declare-fun store_map (ShortCode) LongURL)          ; pre-state mapping
(declare-fun store_domain_post (ShortCode) Bool)     ; post-state domain membership
(declare-fun store_map_post (ShortCode) LongURL)     ; post-state mapping

; --- Entity Invariants ---
; invariant: len(sc.value) >= 6 and len(sc.value) <= 10
(define-fun shortcode_inv ((c ShortCode)) Bool
  (and (>= (str.len (sc_value c)) 6)
       (<= (str.len (sc_value c)) 10)))

; invariant: sc.value matches /^[a-zA-Z0-9]+$/
(define-fun shortcode_alphanum ((c ShortCode)) Bool
  (str.in_re (sc_value c) (re.+ (re.union
    (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9")))))

; invariant: valid_uri(lu.value)
; We approximate valid_uri as: starts with "http://" or "https://"
(define-fun valid_uri ((u LongURL)) Bool
  (or (str.prefixof "http://" (lu_value u))
      (str.prefixof "https://" (lu_value u))))

; --- Global Invariant: all codes in store map to valid URIs ---
(declare-const global_inv_valid_urls Bool)
(assert (= global_inv_valid_urls
  (forall ((c ShortCode))
    (=> (store_domain c)
        (valid_uri (store_map c))))))

; --- Global Invariant: all codes in store satisfy entity invariants ---
(define-fun global_inv_codes () Bool
  (forall ((c ShortCode))
    (=> (store_domain c)
        (and (shortcode_inv c) (shortcode_alphanum c)))))

; --- Combined pre-state invariant ---
(define-fun all_invariants () Bool
  (and global_inv_valid_urls global_inv_codes))

; --- Combined post-state invariant ---
(define-fun all_invariants_post () Bool
  (and
    (forall ((c ShortCode))
      (=> (store_domain_post c)
          (valid_uri (store_map_post c))))
    (forall ((c ShortCode))
      (=> (store_domain_post c)
          (and (shortcode_inv c) (shortcode_alphanum c))))))

; ============================================================
; CHECK 1: Are the invariants satisfiable?
; ============================================================
; (push)
; (assert all_invariants)
; (check-sat)  ; expect SAT -- a valid state exists
; (pop)

; ============================================================
; CHECK 2: Does Shorten preserve invariants?
; ============================================================
; Operation Shorten:
;   input:  url: LongURL
;   output: code: ShortCode
;   requires: isValidURI(url)
;   ensures:  code not in pre(store)
;             store'[code] = url
;             for all other c: store'[c] = store[c]
;             code in store'

(declare-const input_url LongURL)
(declare-const output_code ShortCode)

; Pre-state invariants hold
(assert all_invariants)

; Precondition
(assert (valid_uri input_url))

; Postcondition: code was not in store
(assert (not (store_domain output_code)))

; Postcondition: store' = store + {output_code -> input_url}
(assert (store_domain_post output_code))
(assert (= (store_map_post output_code) input_url))

; Frame condition: everything else unchanged
(assert (forall ((c ShortCode))
  (=> (not (= c output_code))
      (and (= (store_domain_post c) (store_domain c))
           (= (store_map_post c) (store_map c))))))

; Now check: does the post-state invariant hold?
; We NEGATE the post-invariant and check for SAT.
; If SAT, the solver found a counterexample (invariant violation).
(assert (not all_invariants_post))

(check-sat)
; If SAT: VIOLATION FOUND. The model shows a counterexample.
;   The output_code might have sc_value of length < 6, violating shortcode_inv.
;   This is because the ensures clause does not constrain output_code's value length.
;
; If UNSAT: The operation provably preserves the invariant.

; (get-model)  ; in SAT case, shows the counterexample

; ============================================================
; CHECK 3: Does Resolve preserve invariants?
; ============================================================
; Resolve is read-only (store' = store), so it trivially preserves
; invariants. The check is:
;   all_invariants AND store' = store => all_invariants_post
; This is always UNSAT (when negated), confirming preservation.

; ============================================================
; CHECK 4: Does Delete preserve invariants?
; ============================================================
; Delete removes an entry. The frame is: store' = store - {code}.
; Since we only remove, and invariants are universally quantified
; over store contents, removing an entry preserves them. The check
; confirms this automatically.

sat
(model
  (define-fun output_code () ShortCode ShortCode!val!0)
  (define-fun sc_value ((x!0 ShortCode)) String
    (ite (= x!0 ShortCode!val!0) "ab" "abcdef"))
  (define-fun input_url () LongURL LongURL!val!0)
  (define-fun lu_value ((x!0 LongURL)) String
    "https://example.com")
)

-- ============================================================
-- URL Shortener Spec -> Alloy Translation
-- ============================================================

module UrlShortener

open util/ordering[State] as StateOrder

-- --- Entities ---

sig ShortCode {
  value: one Value
}

sig LongURL {
  url_value: one Value
}

-- Abstract value type (Alloy lacks native strings; we model lengths abstractly)
sig Value {
  length: one Int
}

-- --- State ---

sig State {
  store: ShortCode -> lone LongURL
}

-- --- Entity Invariants ---

-- All ShortCodes have value length between 6 and 10
fact ShortCodeInvariant {
  all c: ShortCode | c.value.length >= 6 and c.value.length <= 10
}

-- All LongURLs are "valid" (modeled as having positive length)
fact LongURLInvariant {
  all u: LongURL | u.url_value.length > 0
}

-- --- Global Invariants ---

-- All stored URLs are valid (subsumed by entity invariant, but stated explicitly)
fact GlobalValidURLs {
  all s: State, c: s.store.LongURL |
    let u = s.store[c] |
      u.url_value.length > 0
}

-- --- Initial State ---

fact InitialState {
  let s0 = StateOrder/first |
    no s0.store
}

-- --- Operations ---

-- Shorten: adds a new mapping
pred Shorten[s, s': State, url: LongURL, code: ShortCode] {
  -- Precondition: code is fresh
  code not in s.store.LongURL

  -- Postcondition: store gains exactly this mapping
  s'.store = s.store + code -> url

  -- Frame: nothing else changes (implicit in the equality above)
}

-- Resolve: reads a mapping (no state change)
pred Resolve[s, s': State, code: ShortCode, url: LongURL] {
  -- Precondition: code exists
  code in s.store.LongURL

  -- Postcondition: url is the stored value
  url = s.store[code]

  -- Frame: state unchanged
  s'.store = s.store
}

-- Delete: removes a mapping
pred Delete[s, s': State, code: ShortCode] {
  -- Precondition: code exists
  code in s.store.LongURL

  -- Postcondition: code removed
  s'.store = s.store - code -> s.store[code]
}

-- --- Transition System ---

fact Traces {
  all s: State - StateOrder/last |
    let s' = s.next |
      (some url: LongURL, code: ShortCode | Shorten[s, s', url, code])
      or
      (some code: ShortCode, url: LongURL | Resolve[s, s', code, url])
      or
      (some code: ShortCode | Delete[s, s', code])
}

-- ============================================================
-- Verification Commands
-- ============================================================

-- Check 1: Can a valid trace exist?
-- (Run finds an instance if one exists within bounds)
run TraceExists {} for 5 but 4 State, 5 ShortCode, 5 LongURL, 5 Value, 5 Int

-- Check 2: Does Shorten preserve the store integrity?
-- (Assert negation; if counterexample found, the property is violated)
assert ShortenPreservesIntegrity {
  all s, s': State, url: LongURL, code: ShortCode |
    Shorten[s, s', url, code] implies
      (all c: s'.store.LongURL | c.value.length >= 6)
}
check ShortenPreservesIntegrity for 5 but 4 State, 5 ShortCode, 5 LongURL, 5 Value, 6 Int

-- Check 3: No deadlocks (from any non-empty state, at least one op is enabled)
assert NoDeadlock {
  all s: State - StateOrder/last |
    (some url: LongURL, code: ShortCode | code not in s.store.LongURL)
    or
    (some code: ShortCode | code in s.store.LongURL)
}
check NoDeadlock for 5 but 4 State, 5 ShortCode, 5 LongURL, 5 Value, 6 Int

-- Check 4: Delete undoes Shorten
assert DeleteUndoesShorten {
  all s1, s2, s3: State, url: LongURL, code: ShortCode |
    (Shorten[s1, s2, url, code] and Delete[s2, s3, code])
      implies s3.store = s1.store
}
check DeleteUndoesShorten for 5 but 4 State, 5 ShortCode, 5 LongURL, 5 Value, 6 Int

Executing "Check ShortenPreservesIntegrity for 5"
   Solver=sat4j Bitwidth=6 MaxSeq=5 Symmetry=20
   12,345 vars. 678 primary vars. 23,456 clauses. 150ms.
   No counterexample found. Assertion may be valid.

Executing "Check ShortenPreservesIntegrity for 5"
   Solver=sat4j Bitwidth=6 MaxSeq=5 Symmetry=20
   12,345 vars. 678 primary vars. 23,456 clauses. 85ms.
   Counterexample found.

   State$0:
     store = { ShortCode$0 -> LongURL$0 }
   State$1:
     store = { ShortCode$0 -> LongURL$0, ShortCode$1 -> LongURL$1 }

   ShortCode$1.value = Value$2
   Value$2.length = 2          <-- VIOLATION: length 2 < 6

   Shorten[State$0, State$1, LongURL$1, ShortCode$1]

-- ============================================================
-- E-Commerce Order Service -> Alloy Translation
-- ============================================================

module OrderService

open util/ordering[State] as StateOrder

abstract sig OrderStatus {}
one sig PENDING, PAID, SHIPPED, DELIVERED, CANCELLED extends OrderStatus {}

sig OrderId {}
sig ProductId {}
sig CustomerId {}

sig OrderItem {
  product: one ProductId,
  quantity: one Int
} {
  quantity > 0
}

sig Order {
  id: one OrderId,
  customer: one CustomerId,
  items: set OrderItem,
  status: one OrderStatus,
  total: one Int
} {
  total >= 0
  #items > 0
}

sig State {
  orders: set Order,
  order_status: Order -> one OrderStatus,
  inventory: ProductId -> one Int
}

-- Inventory is never negative
fact InventoryNonNegative {
  all s: State, p: ProductId |
    let qty = s.inventory[p] |
      qty >= 0
}

-- Initial state: no orders, all inventory positive
fact InitialState {
  let s0 = StateOrder/first |
    no s0.orders
}

-- --- Operations ---

pred PlaceOrder[s, s': State, o: Order] {
  -- Pre: order not already placed
  o not in s.orders

  -- Pre: sufficient inventory for all items
  all item: o.items |
    s.inventory[item.product] >= item.quantity

  -- Post: order added with PENDING status
  s'.orders = s.orders + o
  s'.order_status = s.order_status ++ (o -> PENDING)

  -- Post: inventory decremented
  all p: ProductId |
    (some item: o.items | item.product = p)
      implies s'.inventory[p] = sub[s.inventory[p],
        (sum item: o.items & product.p | item.quantity)]
      else s'.inventory[p] = s.inventory[p]
}

pred CancelOrder[s, s': State, o: Order] {
  -- Pre: order exists and is PENDING
  o in s.orders
  s.order_status[o] = PENDING

  -- Post: status changed to CANCELLED
  s'.orders = s.orders
  s'.order_status = s.order_status ++ (o -> CANCELLED)

  -- Post: inventory restored
  all p: ProductId |
    (some item: o.items | item.product = p)
      implies s'.inventory[p] = add[s.inventory[p],
        (sum item: o.items & product.p | item.quantity)]
      else s'.inventory[p] = s.inventory[p]
}

pred PayOrder[s, s': State, o: Order] {
  o in s.orders
  s.order_status[o] = PENDING
  -- Post: order becomes PAID, everything else unchanged
  s'.orders = s.orders
  s'.order_status = s.order_status ++ (o -> PAID)
  s'.inventory = s.inventory
}

pred ShipOrder[s, s': State, o: Order] {
  o in s.orders
  s.order_status[o] = PAID
  s'.orders = s.orders
  s'.order_status = s.order_status ++ (o -> SHIPPED)
  s'.inventory = s.inventory
}

-- Verification: PlaceOrder preserves non-negative inventory
assert PlaceOrderPreservesInventory {
  all s, s': State, o: Order |
    PlaceOrder[s, s', o] implies
      (all p: ProductId | s'.inventory[p] >= 0)
}
check PlaceOrderPreservesInventory for 4 but 3 State, 4 Order, 3 ProductId, 5 Int

-- Verification: An order can go from PENDING to DELIVERED
-- (reachability -- run to see if a trace exists)
run CanDeliver {
  some s: State | some o: s.orders | o.status = DELIVERED
} for 6 but 5 State, 3 Order, 2 ProductId, 6 Int

// ============================================================
// Order State Machine -> Quint Translation
// ============================================================

module OrderStateMachine {

  // --- Types ---
  type OrderId = str
  type ProductId = str
  type CustomerId = str

  type OrderStatus =
    | PENDING
    | PAID
    | SHIPPED
    | DELIVERED
    | CANCELLED

  type OrderItem = {
    product: ProductId,
    quantity: int
  }

  type Order = {
    id: OrderId,
    customer: CustomerId,
    items: List[OrderItem],
    status: OrderStatus,
    total: int
  }

  // --- State ---
  var orders: OrderId -> Order
  var inventory: ProductId -> int

  // --- Initial state ---
  action init = all {
    orders' = Map(),
    inventory' = Map("prod1" -> 100, "prod2" -> 50, "prod3" -> 200),
  }

  // --- Operations ---

  action placeOrder(id: OrderId, customer: CustomerId, items: List[OrderItem], total: int): bool = all {
    not(orders.has(id)),
    items.length() > 0,
    total > 0,
    // Check inventory
    items.forall(item => inventory.get(item.product) >= item.quantity),
    // Update state
    orders' = orders.put(id, {
      id: id,
      customer: customer,
      items: items,
      status: PENDING,
      total: total
    }),
    // Decrement inventory
    inventory' = items.foldl(inventory, (inv, item) =>
      inv.put(item.product, inv.get(item.product) - item.quantity)
    ),
  }

  action payOrder(id: OrderId): bool = all {
    orders.has(id),
    orders.get(id).status == PENDING,
    orders' = orders.put(id, { ...orders.get(id), status: PAID }),
    inventory' = inventory,
  }

  action shipOrder(id: OrderId): bool = all {
    orders.has(id),
    orders.get(id).status == PAID,
    orders' = orders.put(id, { ...orders.get(id), status: SHIPPED }),
    inventory' = inventory,
  }

  action deliverOrder(id: OrderId): bool = all {
    orders.has(id),
    orders.get(id).status == SHIPPED,
    orders' = orders.put(id, { ...orders.get(id), status: DELIVERED }),
    inventory' = inventory,
  }

  action cancelOrder(id: OrderId): bool = all {
    orders.has(id),
    orders.get(id).status == PENDING,
    // Restore inventory
    val items = orders.get(id).items
    orders' = orders.put(id, { ...orders.get(id), status: CANCELLED }),
    inventory' = items.foldl(inventory, (inv, item) =>
      inv.put(item.product, inv.get(item.product) + item.quantity)
    ),
  }

  // --- Step: nondeterministic choice of operation ---
  action step = any {
    nondet id = oneOf(Set("o1", "o2", "o3"))
    nondet cust = oneOf(Set("c1", "c2"))
    nondet items = oneOf(Set(
      [{ product: "prod1", quantity: 1 }],
      [{ product: "prod2", quantity: 2 }],
    ))
    nondet total = oneOf(Set(10, 20, 50))
    placeOrder(id, cust, items, total),

    nondet id = oneOf(Set("o1", "o2", "o3"))
    payOrder(id),

    nondet id = oneOf(Set("o1", "o2", "o3"))
    shipOrder(id),

    nondet id = oneOf(Set("o1", "o2", "o3"))
    deliverOrder(id),

    nondet id = oneOf(Set("o1", "o2", "o3"))
    cancelOrder(id),
  }

  // ============================================================
  // Temporal Properties
  // ============================================================

  // Safety: inventory is never negative
  val inventoryNonNegative: bool =
    inventory.keys().forall(p => inventory.get(p) >= 0)

  // Safety: order status transitions are valid
  //   PENDING -> PAID, PENDING -> CANCELLED
  //   PAID -> SHIPPED
  //   SHIPPED -> DELIVERED
  // No backwards transitions
  val validTransitions: bool =
    orders.keys().forall(id =>
      val order = orders.get(id)
      order.status != DELIVERED or order.status != CANCELLED
      // (terminal states have no further transitions)
    )

  // Deadlock freedom: at least one operation is always enabled
  // (Either we can place a new order, or we can advance an existing one)
  temporal deadlockFree = always(enabled(step))

  // Liveness: every PENDING order is eventually PAID, DELIVERED, or CANCELLED
  // (requires fairness assumption on step)
  temporal eventualResolution =
    orders.keys().forall(id =>
      orders.get(id).status == PENDING implies
        eventually(
          orders.get(id).status == PAID or
          orders.get(id).status == DELIVERED or
          orders.get(id).status == CANCELLED
        )
    )

  // Ordering: an order must be PAID before it can be SHIPPED
  // Track payment history using an auxiliary variable
  var was_paid: OrderId -> bool

  // (In payOrder action, set was_paid' = was_paid.put(id, true))

  temporal payBeforeShip =
    always(orders.keys().forall(id =>
      orders.get(id).status == SHIPPED implies was_paid.get(id)
    ))
}

$ quint run OrderStateMachine.qnt --max-steps=20 --max-samples=10000

# Check safety invariant
$ quint verify OrderStateMachine.qnt --invariant=inventoryNonNegative --max-steps=15

[ok] inventoryNonNegative satisfied in 10000 traces (max depth 15).

# Check temporal property
$ quint verify OrderStateMachine.qnt --temporal=deadlockFree --max-steps=15

[ok] deadlockFree satisfied in 10000 traces (max depth 15).

# If a violation is found:
$ quint verify OrderStateMachine.qnt --invariant=inventoryNonNegative --max-steps=15

[violation] inventoryNonNegative violated after 3 steps.
Trace:
  State 0: { orders: {}, inventory: { "prod1": 1 } }
  Step 1 (placeOrder): { orders: { "o1": { status: PENDING, items: [{ product: "prod1", quantity: 1 }] } },
                         inventory: { "prod1": 0 } }
  Step 2 (placeOrder): FAILED -- inventory for "prod1" is 0, but quantity 1 requested
  // The precondition should prevent this, but if it doesn't, the invariant catches it.

// ============================================================
// URL Shortener -> Quint Translation
// ============================================================

module UrlShortener {

  type ShortCode = str
  type LongURL = str

  var store: ShortCode -> LongURL
  var created_at: ShortCode -> int  // timestamp as integer

  // --- Helpers ---
  pure def validCode(c: ShortCode): bool =
    c.length() >= 6 and c.length() <= 10

  pure def validUri(u: LongURL): bool =
    u.length() > 0  // simplified; real check would use regex

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

  // --- Operations ---

  action shorten(url: LongURL, code: ShortCode, timestamp: int): bool = all {
    // Precondition
    validUri(url),
    not(store.has(code)),
    validCode(code),
    // Postcondition
    store' = store.put(code, url),
    created_at' = created_at.put(code, timestamp),
  }

  action resolve(code: ShortCode): bool = all {
    // Precondition
    store.has(code),
    // Frame: no state change
    store' = store,
    created_at' = created_at,
  }

  action delete(code: ShortCode): bool = all {
    // Precondition
    store.has(code),
    // Postcondition
    store' = store.mapRemove(code),
    created_at' = created_at.mapRemove(code),
  }

  action step = any {
    nondet url = oneOf(Set("https://example.com", "https://test.org", "invalid"))
    nondet code = oneOf(Set("abcdef", "ghijkl", "ab", "mnopqrstuv"))
    nondet ts = oneOf(Set(1000, 2000, 3000))
    shorten(url, code, ts),

    nondet code = oneOf(Set("abcdef", "ghijkl", "ab"))
    resolve(code),

    nondet code = oneOf(Set("abcdef", "ghijkl"))
    delete(code),
  }

  // --- Invariants ---

  val allStoredUrlsValid: bool =
    store.keys().forall(c => validUri(store.get(c)))

  val allCodesValid: bool =
    store.keys().forall(c => validCode(c))

  val storeAndCreatedAtConsistent: bool =
    store.keys().forall(c => created_at.has(c)) and
    created_at.keys().forall(c => store.has(c))

  // Deadlock freedom: we can always do something
  // (we can always shorten with a fresh code, or resolve/delete existing ones,
  //  or at worst the store is empty and we can shorten)
  temporal alwaysProgress = always(enabled(step))
}

  Spec Source Text
       |
       v
  [Step 1] PARSING + IR Construction
       |
       v
  [Step 2] TYPE CHECKING (fast)
       |
       v
  [Step 3] CONSTRAINT SATISFIABILITY (moderate)
       |
       v
  [Step 4] INVARIANT PRESERVATION (moderate-slow)
       |
       v
  [Step 5] REACHABILITY ANALYSIS (slow)
       |
       v
  [Step 6] TEMPORAL PROPERTY CHECKING (slowest)
       |
       v
  Verification Report
       |
       v
  [Proceed to Code Generation or Report Errors]

ERROR: Parse error at line 12, column 5
  Expected: 'requires' or 'ensures'
  Found: 'guarantee'

  12 |    guarantee: code in store
            ^^^^^^^^^ Did you mean 'requires'?

ERROR: Type mismatch at line 35
  Expression: p.price > p.name
  Left operand:  p.price has type Money
  Right operand: p.name  has type String
  The '>' operator requires both operands to have the same ordered type.

ERROR: Unsatisfiable invariants at lines 15, 18

  Line 15: invariant: all i in items | items[i] > 100
  Line 18: invariant: all i in items | items[i] < 50

  These two invariants cannot be simultaneously satisfied.
  No valid state exists for the 'items' relation.

  Z3 proof core: the conjunction
    (forall x. f(x) > 100) AND (forall x. f(x) < 50)
  is unsatisfiable.

WARNING: Potentially unreachable operation 'ShipOrder' (line 45)

  ShipOrder requires: orders[id].status = PAID

  But no operation produces status = PAID.
  Available status transitions:
    CreateOrder -> PENDING
    CancelOrder: PENDING -> CANCELLED

  No path from PENDING to PAID was found within 10 steps.
  Consider adding a 'PayOrder' operation.

WARNING: Potential deadlock detected

  State: { orders: { "o1": { status: HELD } }, inventory: { ... } }

  No operation is enabled in this state:
    - PlaceOrder: disabled (requires order not in orders)
    - PayOrder: disabled (requires status = PENDING, but status = HELD)
    - ShipOrder: disabled (requires status = PAID)
    - CancelOrder: disabled (requires status = PENDING)

  The system reaches a state from which no further progress is possible.
  Trace to deadlock state:
    Step 0: init -> { orders: {} }
    Step 1: PlaceOrder("o1") -> { orders: { "o1": PENDING } }
    Step 2: HoldOrder("o1") -> { orders: { "o1": HELD } }
    Step 3: DEADLOCK -- no enabled operations

forall state, input, state', output:
  I(state)
  AND O.requires(input, state)
  AND O.ensures(input, state, state', output)
  => I(state')

EXISTS state, input, state', output:
  I(state)
  AND O.requires(input, state)
  AND O.ensures(input, state, state', output)
  AND NOT I(state')

entity LongURL {
  value: String
  invariant: isValidURI(value)
}

state {
  store: ShortCode -> lone LongURL
}

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

operation Shorten {
  input:  url: LongURL
  output: code: ShortCode, short_url: String
  requires: isValidURI(url.value)
  ensures:
    code not in pre(store)
    store'[code] = url
    all c in pre(store) | store'[c] = store[c]
    short_url = base_url + "/" + code.value
}

Assume:
  (A1) forall c in store. isValidURI(store[c].value)       -- invariant on pre-state
  (A2) isValidURI(url.value)                                 -- precondition
  (A3) code not in store                                    -- ensures: freshness
  (A4) store'[code] = url                                   -- ensures: insertion
  (A5) forall c in store. store'[c] = store[c]             -- ensures: frame

Prove:
  forall c in store'. isValidURI(store'[c].value)            -- invariant on post-state

(set-logic ALL)

(declare-sort ShortCode 0)
(declare-sort LongURL 0)

(declare-fun sc_value (ShortCode) String)
(declare-fun lu_value (LongURL) String)

; valid_uri approximation
(define-fun valid_uri ((u LongURL)) Bool
  (or (str.prefixof "http://" (lu_value u))
      (str.prefixof "https://" (lu_value u))))

; Pre-state
(declare-fun store_has (ShortCode) Bool)
(declare-fun store_get (ShortCode) LongURL)

; Post-state
(declare-fun store_has_post (ShortCode) Bool)
(declare-fun store_get_post (ShortCode) LongURL)

; Input and output
(declare-const url LongURL)
(declare-const code ShortCode)

; --- Assumptions ---

; (A1) Pre-state invariant
(assert (forall ((c ShortCode))
  (=> (store_has c) (valid_uri (store_get c)))))

; (A2) Precondition
(assert (valid_uri url))

; (A3) Freshness
(assert (not (store_has code)))

; (A4) Insertion
(assert (store_has_post code))
(assert (= (store_get_post code) url))

; (A5) Frame
(assert (forall ((c ShortCode))
  (=> (not (= c code))
      (and (= (store_has_post c) (store_has c))
           (=> (store_has c) (= (store_get_post c) (store_get c)))))))

; --- Negation of goal ---
; There exists some c in store' where valid_uri fails
(declare-const witness ShortCode)
(assert (store_has_post witness))
(assert (not (valid_uri (store_get_post witness))))

(check-sat)
; Expected: UNSAT (invariant is preserved)

entity Product { id: ProductId, name: String }

state {
  inventory: ProductId -> one Int
  orders: set Order
}

invariant: all p in inventory | inventory[p] >= 0

operation PlaceOrder {
  input: items: set OrderItem
  output: order_id: OrderId

  requires:
    #items > 0
    all item in items | item.product in inventory
    all item in items | inventory[item.product] >= item.quantity

  ensures:
    all item in items |
      inventory'[item.product] = inventory[item.product] - item.quantity
    all p not in (items.product) |
      inventory'[p] = inventory[p]
}

Assume:
  (A1) forall p in inventory. inventory[p] >= 0               -- pre-state invariant
  (A2) #items > 0                                              -- precondition
  (A3) forall item in items. item.product in inventory         -- precondition
  (A4) forall item in items. inventory[item.product] >= item.quantity  -- precondition
  (A5) forall item in items.
         inventory'[item.product] = inventory[item.product] - item.quantity  -- postcondition
  (A6) forall p not in items.product.
         inventory'[p] = inventory[p]                           -- frame

Prove:
  forall p in inventory'. inventory'[p] >= 0                   -- post-state invariant

ensures:
  all p in (items.product) |
    inventory'[p] = inventory[p] - sum(item.quantity for item in items if item.product = p)

requires:
  all p in (items.product) |
    inventory[p] >= sum(item.quantity for item in items if item.product = p)

(set-logic ALL)

(declare-sort ProductId 0)
(declare-sort OrderItem 0)

(declare-fun item_product (OrderItem) ProductId)
(declare-fun item_quantity (OrderItem) Int)

(declare-fun inventory (ProductId) Int)
(declare-fun inventory_post (ProductId) Int)

; Items set (modeled as two concrete items for bounded checking)
(declare-const item1 OrderItem)
(declare-const item2 OrderItem)

; (A1) Pre-state invariant
(assert (forall ((p ProductId)) (>= (inventory p) 0)))

; (A3) All item products are in inventory (trivially true for total function)

; (A4) Sufficient inventory
(assert (>= (inventory (item_product item1)) (item_quantity item1)))
(assert (>= (inventory (item_product item2)) (item_quantity item2)))
(assert (> (item_quantity item1) 0))
(assert (> (item_quantity item2) 0))

; (A5) Postcondition: decrement per item
; BUG: this does not aggregate when item1 and item2 have the same product
(assert (= (inventory_post (item_product item1))
           (- (inventory (item_product item1)) (item_quantity item1))))
(assert (= (inventory_post (item_product item2))
           (- (inventory (item_product item2)) (item_quantity item2))))

; (A6) Frame for other products
(assert (forall ((p ProductId))
  (=> (and (not (= p (item_product item1)))
           (not (= p (item_product item2))))
      (= (inventory_post p) (inventory p)))))

; --- Negation of post-invariant ---
(declare-const witness ProductId)
(assert (< (inventory_post witness) 0))

(check-sat)
; SAT when item1.product = item2.product and their quantities sum > inventory
; Counterexample: product = P, inventory[P] = 6, item1.qty = 4, item2.qty = 4
;   inventory_post[P] = 6 - 4 = 2 (from item1) BUT ALSO 6 - 4 = 2 (from item2)
;   Z3 finds the conflict: two assignments to inventory_post for same product

entity Todo {
  title: String
  done: Bool
  completed_at: optional DateTime
}

state {
  todos: TodoId -> one Todo
}

invariant: all t in todos |
  todos[t].done = true implies todos[t].completed_at != none

operation Complete {
  input: id: TodoId
  requires: id in todos and todos[id].done = false

  ensures:
    todos'[id].done = true
    todos'[id].title = todos[id].title
    all other in todos | other != id implies todos'[other] = todos[other]
}

Assume:
  (A1) forall t in todos. todos[t].done => todos[t].completed_at != none
  (A2) id in todos
  (A3) todos[id].done = false
  (A4) todos'[id].done = true
  (A5) todos'[id].title = todos[id].title
  (A6) forall other != id. todos'[other] = todos[other]

Prove:
  forall t in todos'. todos'[t].done => todos'[t].completed_at != none

ensures:
  todos'[id].done = true
  todos'[id].completed_at = now()        // MISSING -- this is the fix
  todos'[id].title = todos[id].title

method Shorten(store: map<ShortCode, LongURL>, url: LongURL)
  returns (code: ShortCode, store': map<ShortCode, LongURL>)
  requires forall c :: c in store ==> ValidUri(store[c])    // pre-invariant
  requires ValidUri(url)                                      // precondition
  ensures code !in old(store)                                 // freshness
  ensures store' == old(store)[code := url]                   // insertion
  ensures forall c :: c in store' ==> ValidUri(store'[c])    // post-invariant
{
  // Implementation synthesized by LLM
  code := GenerateFreshCode(store);
  store' := store[code := url];
}

operation MergeSort {
  input: list: List[Int]
  output: sorted: List[Int]

  requires: true
  ensures: is_sorted(sorted) and is_permutation(sorted, list)

  hint: "Use structural induction on list length. Split at midpoint."
  lemma: is_sorted(merge(a, b)) if is_sorted(a) and is_sorted(b)
}

operation CreateOrder  { ensures: status' = PENDING }
operation PayOrder     { requires: status = PENDING, ensures: status' = PAID }
operation ShipOrder    { requires: status = PAID, ensures: status' = SHIPPED }
operation DeliverOrder { requires: status = SHIPPED, ensures: status' = DELIVERED }
operation CancelOrder  { requires: status = PENDING, ensures: status' = CANCELLED }

operation CreateOrder  { ensures: status' = PENDING }
operation ShipOrder    { requires: status = PAID, ensures: status' = SHIPPED }
// Missing: no way to get from PENDING to PAID

PENDING -> PAID -> REVIEW

operation PayOrder    { requires: status = PENDING and amount > 0, ensures: status' = PAID }
operation CancelOrder { requires: status = PENDING, ensures: status' = CANCELLED }

States: { PENDING, PAID, SHIPPED, DELIVERED, CANCELLED }
Initial: PENDING
Terminal: { DELIVERED, CANCELLED }

Transitions:
  PENDING ---PayOrder---> PAID
  PENDING ---CancelOrder---> CANCELLED
  PAID ---ShipOrder---> SHIPPED
  SHIPPED ---DeliverOrder---> DELIVERED

Queue: [PENDING]
Visited: {}

Step 1: Visit PENDING. Neighbors: PAID, CANCELLED.
  Queue: [PAID, CANCELLED]. Visited: {PENDING}.

Step 2: Visit PAID. Neighbors: SHIPPED.
  Queue: [CANCELLED, SHIPPED]. Visited: {PENDING, PAID}.

Step 3: Visit CANCELLED. Neighbors: (none -- terminal).
  Queue: [SHIPPED]. Visited: {PENDING, PAID, CANCELLED}.

Step 4: Visit SHIPPED. Neighbors: DELIVERED.
  Queue: [DELIVERED]. Visited: {PENDING, PAID, CANCELLED, SHIPPED}.

Step 5: Visit DELIVERED. Neighbors: (none -- terminal).
  Queue: []. Visited: {PENDING, PAID, CANCELLED, SHIPPED, DELIVERED}.

Result: All 5 states reachable. PASS.

operation ReviewOrder {
  requires: status = PAID
  ensures: status' = REVIEW
}

PENDING -> PAID -> SHIPPED -> DELIVERED
              |        \
              +-> REVIEW (deadlock!)
              |
PENDING -> CANCELLED

ERROR: Invariant violation detected

  Invariant at line 42:
    invariant: all c in store | len(c.value) >= 6

  Violated by operation 'Shorten' at line 28:
    The postcondition allows store'[code] = url where code.value
    has no length constraint.

  Counterexample:
    Pre-state:  store = {}                          (empty, invariant trivially holds)
    Input:      url = LongURL { value: "https://example.com" }
    Output:     code = ShortCode { value: "ab" }    (length 2, violates invariant)
    Post-state: store = { ShortCode("ab") -> LongURL("https://example.com") }

  The post-state violates the invariant because code.value has length 2 < 6.

  Suggestion: Add constraint to Shorten's ensures clause:
    ensures:
      ...existing clauses...
  +   len(code.value) >= 6 and len(code.value) <= 10

WARNING: Operation 'ShipOrder' at line 67 may be unreachable

  ShipOrder requires:
    orders[id].status = PAID

  But no operation in the spec produces status = PAID.

  Defined status transitions:
    CreateOrder: (new) -> PENDING
    CancelOrder: PENDING -> CANCELLED

  There is no path from any reachable state to a state where
  orders[id].status = PAID.

  Checked: exhaustive BFS from initial state, depth 10, with
    up to 5 orders and 3 products. No reachable state enables ShipOrder.

  Suggestion: Add a 'PayOrder' operation:
    operation PayOrder {
      input: id: OrderId
      requires: orders[id].status = PENDING
      ensures: orders'[id].status = PAID
    }

ERROR: State machine deadlock detected

  State 'REVIEW' at line 34 has no outgoing transitions and
  is not marked as a terminal state.

  An order can reach REVIEW via:
    CreateOrder -> PENDING -> PayOrder -> PAID -> ReviewOrder -> REVIEW

  Once in REVIEW, no operation is enabled:
    PayOrder:     requires status = PENDING    (status is REVIEW)
    ShipOrder:    requires status = PAID       (status is REVIEW)
    CancelOrder:  requires status = PENDING    (status is REVIEW)
    DeliverOrder: requires status = SHIPPED    (status is REVIEW)

  Trace to deadlock:
    State 0: orders = {}
    Step 1:  CreateOrder("o1")  -> orders = { "o1": PENDING }
    Step 2:  PayOrder("o1")     -> orders = { "o1": PAID }
    Step 3:  ReviewOrder("o1")  -> orders = { "o1": REVIEW }
    DEADLOCK: no operation can fire.

  Suggestions:
    (a) Add transitions from REVIEW:
        operation ApproveOrder { requires: status = REVIEW, ensures: status' = PAID }
        operation RejectOrder  { requires: status = REVIEW, ensures: status' = CANCELLED }

    (b) Or mark REVIEW as a terminal state:
        terminal states: { DELIVERED, CANCELLED, REVIEW }

ERROR: Invariants are unsatisfiable -- no valid state can exist

  Invariant at line 15:
    invariant: all i in items | items[i].price > 100

  Invariant at line 18:
    invariant: all i in items | items[i].price < 50

  These invariants are contradictory: no value can be both > 100 and < 50.

  Proof:
    Assume items is non-empty (contains some item i).
    By line 15: items[i].price > 100
    By line 18: items[i].price < 50
    But 100 < 50 is false. Contradiction.

  Note: if items is always empty, the invariants hold vacuously.
  However, this means no item can ever be added to the service,
  rendering it useless.

  Suggestion: Review the invariant bounds. Perhaps one should be:
    invariant: all i in items | items[i].price > 50

WARNING: Missing state transition detected

  The state machine for Order.status has a gap:

  Reachable states: { PENDING, CANCELLED }
  Defined but unreachable states: { PAID, SHIPPED, DELIVERED }

  The gap is between PENDING and PAID -- no operation transitions
  from PENDING to PAID.

  Complete transition graph:
    PENDING --CancelOrder--> CANCELLED
    PAID    --ShipOrder-->   SHIPPED     (but PAID is unreachable)
    SHIPPED --DeliverOrder--> DELIVERED  (but SHIPPED is unreachable)

  The intended lifecycle appears to be:
    PENDING -> PAID -> SHIPPED -> DELIVERED
       |
       +-> CANCELLED

  Suggestion: Add:
    operation PayOrder {
      input: id: OrderId
      requires: orders[id].status = PENDING
      ensures: orders'[id].status = PAID
    }

ERROR: Type error at line 35

  Expression: p.price > p.name

  Left operand:  p.price : Money  (declared at line 8)
  Right operand: p.name  : String (declared at line 7)

  The '>' operator requires both operands to have the same ordered type.
  Money and String are incompatible.

  Did you mean one of:
    p.price > p.cost       (Money > Money)
    p.name  > p.category   (String > String, lexicographic)

from z3 import (
    DeclareSort, Function, BoolSort, IntSort, StringSort,
    ForAll, Exists, Implies, And, Or, Not, Solver, sat, unsat
)

class Z3SpecVerifier:
    def __init__(self, ir):
        self.ir = ir
        self.solver = Solver()
        self.solver.set("timeout", 30000)  # 30 seconds
        self.sorts = {}
        self.functions = {}

    def declare_entity(self, entity):
        """Declare an entity as an uninterpreted sort with field accessors."""
        sort = DeclareSort(entity.name)
        self.sorts[entity.name] = sort
        for field in entity.fields:
            field_sort = self._type_to_z3(field.type)
            func = Function(f"{entity.name}_{field.name}", sort, field_sort)
            self.functions[f"{entity.name}.{field.name}"] = func
        return sort

    def declare_state(self, state):
        """Declare state relations as functions."""
        for rel in state.relations:
            domain_sort = self.sorts[rel.domain_type]
            range_sort = self.sorts[rel.range_type]
            # Domain membership (is this key in the relation?)
            has_func = Function(f"{rel.name}_has", domain_sort, BoolSort())
            # Mapping function
            get_func = Function(f"{rel.name}_get", domain_sort, range_sort)
            self.functions[f"{rel.name}_has"] = has_func
            self.functions[f"{rel.name}_get"] = get_func

    def check_invariant_satisfiability(self, invariants):
        """Check if all invariants can be simultaneously satisfied."""
        self.solver.push()
        for inv in invariants:
            self.solver.add(self._translate_invariant(inv))
        result = self.solver.check()
        if result == unsat:
            core = self.solver.unsat_core()
            self.solver.pop()
            return VerificationResult(
                status="FAIL",
                message="Invariants are unsatisfiable",
                core=core
            )
        self.solver.pop()
        return VerificationResult(status="PASS")

    def check_invariant_preservation(self, operation, invariant):
        """Check if operation preserves invariant."""
        self.solver.push()

        # Assert pre-state invariant
        self.solver.add(self._translate_invariant(invariant, primed=False))

        # Assert precondition
        self.solver.add(self._translate_requires(operation))

        # Assert postcondition
        self.solver.add(self._translate_ensures(operation))

        # Assert negation of post-state invariant
        self.solver.add(Not(self._translate_invariant(invariant, primed=True)))

        result = self.solver.check()
        if result == sat:
            model = self.solver.model()
            self.solver.pop()
            return VerificationResult(
                status="FAIL",
                message=f"Operation '{operation.name}' may violate invariant",
                counterexample=self._extract_counterexample(model)
            )
        elif result == unsat:
            self.solver.pop()
            return VerificationResult(status="PASS")
        else:
            self.solver.pop()
            return VerificationResult(
                status="UNKNOWN",
                message="Verification timed out"
            )

    def _translate_invariant(self, invariant, primed=False):
        """Translate a spec invariant to a Z3 formula."""
        # Implementation depends on the IR expression AST.
        # Each node type (quantifier, comparison, field access, etc.)
        # maps to a Z3 construct.
        ...

    def _translate_requires(self, operation):
        """Translate operation precondition to Z3."""
        ...

    def _translate_ensures(self, operation):
        """Translate operation postcondition to Z3, with primed state variables."""
        ...

    def _extract_counterexample(self, model):
        """Extract a human-readable counterexample from a Z3 model."""
        ...

import subprocess
import tempfile
import os

class AlloySpecVerifier:
    ALLOY_JAR = "lib/alloy.jar"  # Path to Alloy JAR

    def __init__(self, ir):
        self.ir = ir

    def verify(self, checks):
        """Generate Alloy file, run checks, parse results."""
        alloy_source = self._generate_alloy(self.ir)

        with tempfile.NamedTemporaryFile(
            suffix=".als", mode="w", delete=False
        ) as f:
            f.write(alloy_source)
            als_path = f.name

        try:
            results = []
            for check in checks:
                result = self._run_check(als_path, check)
                results.append(result)
            return results
        finally:
            os.unlink(als_path)

    def _run_check(self, als_path, check_name):
        """Run a single Alloy check command."""
        # Use Alloy's CLI mode (available in Alloy 6+)
        cmd = [
            "java", "-cp", self.ALLOY_JAR,
            "edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler",
            als_path
        ]
        result = subprocess.run(
            cmd, capture_output=True, text=True, timeout=120
        )

        if "No counterexample found" in result.stdout:
            return VerificationResult(status="PASS", check=check_name)
        elif "Counterexample found" in result.stdout:
            return VerificationResult(
                status="FAIL",
                check=check_name,
                counterexample=self._parse_alloy_counterexample(result.stdout)
            )
        else:
            return VerificationResult(
                status="ERROR",
                message=result.stderr
            )

    def _generate_alloy(self, ir):
        """Translate IR to Alloy source code."""
        lines = []
        lines.append("module GeneratedSpec")
        lines.append("open util/ordering[State] as StateOrder")
        lines.append("")

        # Generate sigs for entities
        for entity in ir.entities:
            lines.append(f"sig {entity.name} {{")
            for i, field in enumerate(entity.fields):
                sep = "," if i < len(entity.fields) - 1 else ""
                alloy_type = self._type_to_alloy(field.type, field.multiplicity)
                lines.append(f"  {field.name}: {alloy_type}{sep}")
            lines.append("}")
            lines.append("")

        # Generate State sig
        lines.append("sig State {")
        for i, rel in enumerate(ir.state.relations):
            sep = "," if i < len(ir.state.relations) - 1 else ""
            lines.append(f"  {rel.name}: {rel.domain_type} -> "
                        f"{rel.multiplicity} {rel.range_type}{sep}")
        lines.append("}")
        lines.append("")

        # Generate facts for invariants
        for inv in ir.invariants:
            lines.append(f"fact {{ {self._invariant_to_alloy(inv)} }}")

        # Generate operation predicates
        for op in ir.operations:
            lines.append(self._operation_to_alloy(op))

        # Generate check commands
        for op in ir.operations:
            for inv in ir.invariants:
                lines.append(
                    self._generate_preservation_check(op, inv)
                )

        return "\n".join(lines)

import subprocess
import tempfile
import json

class QuintSpecVerifier:
    def __init__(self, ir):
        self.ir = ir

    def check_temporal(self, property_name, max_steps=15, max_samples=10000):
        """Generate Quint module, run verification, parse results."""
        quint_source = self._generate_quint(self.ir)

        with tempfile.NamedTemporaryFile(
            suffix=".qnt", mode="w", delete=False
        ) as f:
            f.write(quint_source)
            qnt_path = f.name

        try:
            cmd = [
                "npx", "quint", "verify",
                qnt_path,
                f"--invariant={property_name}",
                f"--max-steps={max_steps}",
                f"--max-samples={max_samples}",
            ]
            result = subprocess.run(
                cmd, capture_output=True, text=True, timeout=300
            )

            if result.returncode == 0:
                return VerificationResult(status="PASS")
            else:
                trace = self._parse_quint_trace(result.stdout)
                return VerificationResult(
                    status="FAIL",
                    counterexample=trace,
                    message=result.stdout
                )
        finally:
            os.unlink(qnt_path)

    def simulate(self, max_steps=20, num_traces=1000):
        """Run random simulation to explore state space."""
        quint_source = self._generate_quint(self.ir)

        with tempfile.NamedTemporaryFile(
            suffix=".qnt", mode="w", delete=False
        ) as f:
            f.write(quint_source)
            qnt_path = f.name

        try:
            cmd = [
                "npx", "quint", "run",
                qnt_path,
                f"--max-steps={max_steps}",
                f"--max-samples={num_traces}",
            ]
            result = subprocess.run(
                cmd, capture_output=True, text=True, timeout=300
            )
            return self._parse_simulation_results(result.stdout)
        finally:
            os.unlink(qnt_path)

    def _generate_quint(self, ir):
        """Translate IR to Quint source code."""
        lines = []
        module_name = ir.service_name.replace(" ", "")
        lines.append(f"module {module_name} {{")
        lines.append("")

        # Types
        for entity in ir.entities:
            fields = ", ".join(
                f"{f.name}: {self._type_to_quint(f.type)}"
                for f in entity.fields
            )
            lines.append(f"  type {entity.name} = {{ {fields} }}")

        # State variables
        for rel in ir.state.relations:
            qtype = self._relation_to_quint_type(rel)
            lines.append(f"  var {rel.name}: {qtype}")

        lines.append("")

        # Init action
        lines.append("  action init = all {")
        for rel in ir.state.relations:
            lines.append(f"    {rel.name}' = {self._default_value(rel)},")
        lines.append("  }")
        lines.append("")

        # Operations as actions
        for op in ir.operations:
            lines.append(self._operation_to_quint(op))

        # Step action (nondeterministic choice)
        lines.append("  action step = any {")
        for op in ir.operations:
            lines.append(f"    // {op.name}")
            lines.append(self._step_clause_for(op))
        lines.append("  }")
        lines.append("")

        # Invariants as val declarations
        for i, inv in enumerate(ir.invariants):
            lines.append(f"  val inv_{i}: bool = {self._invariant_to_quint(inv)}")

        lines.append("}")
        return "\n".join(lines)

import cats.effect.IO
import specrest.ir.{ServiceIR, Span}

enum DiagnosticLevel derives CanEqual: case Error, Warning

enum DiagnosticCategory derives CanEqual:
  case ContradictoryInvariants, UnsatisfiablePrecondition, UnreachableOperation,
       InvariantViolationByOperation, SolverTimeout, TranslatorLimitation, BackendError

enum CheckKind derives CanEqual: case Global, Requires, Enabled, Preservation, Temporal
enum CheckOutcome derives CanEqual: case Sat, Unsat, Unknown, Skipped
enum VerifierTool derives CanEqual: case Z3, Alloy

final case class Diagnostic(
    level: DiagnosticLevel,
    category: DiagnosticCategory,
    message: String,
    primarySpan: Option[Span],
    relatedSpans: List[(Span, String)],
    counterexample: Option[Counterexample],
    suggestion: Option[String],
    narrative: Option[String],
    coreSpans: List[Span]
)

final case class CheckResult(
    id: String,
    kind: CheckKind,
    tool: VerifierTool,
    operationName: Option[String],
    invariantName: Option[String],
    status: CheckOutcome,
    durationMs: Double,
    detail: Option[String],
    sourceSpans: List[Span],
    diagnostic: Option[Diagnostic]
)

final case class ConsistencyReport(checks: List[CheckResult], totalMs: Double, ok: Boolean)

object Consistency:
  def runConsistencyChecks(
      ir: ServiceIR,
      config: VerificationConfig,
      dump: Option[DumpSink] = None
  ): IO[ConsistencyReport] = ???  // see Consistency.scala

def test_unsatisfiable_invariants():
    spec = """
    service Test {
      entity Item { price: Int }
      state { items: ItemId -> one Item }
      invariant: all i in items | items[i].price > 100
      invariant: all i in items | items[i].price < 50
    }
    """
    ir = parse(spec)
    report = SpecVerifier(ir).verify()
    assert report.has_errors
    assert any("unsatisfiable" in r.message.lower() for r in report.errors)

def test_invariant_preservation_violation():
    spec = """
    service Test {
      entity Code { value: String, invariant: len(value) >= 6 }
      entity URL { value: String }
      state { store: Code -> lone URL }
      invariant: all c in store | len(c.value) >= 6
      operation Add {
        input: url: URL
        output: code: Code
        requires: true
        ensures: store'[code] = url
      }
    }
    """
    ir = parse(spec)
    report = SpecVerifier(ir).verify()
    assert report.has_errors
    assert any("preservation" in r.category.value or
               "violation" in r.message.lower()
               for r in report.errors)

def test_valid_spec_passes():
    spec = """
    service Test {
      entity Code { value: String, invariant: len(value) >= 6 }
      entity URL { value: String, invariant: len(value) > 0 }
      state { store: Code -> lone URL }
      invariant: all c in store | len(c.value) >= 6
      operation Add {
        input: url: URL
        output: code: Code
        requires: len(url.value) > 0
        ensures:
          len(code.value) >= 6
          store'[code] = url
          all c in pre(store) | store'[c] = store[c]
      }
    }
    """
    ir = parse(spec)
    report = SpecVerifier(ir).verify()
    assert not report.has_errors

def test_deadlock_detection():
    spec = """
    service Test {
      entity Order { status: Status }
      type Status = PENDING | REVIEW | DONE
      state { orders: OrderId -> one Order }
      operation Create {
        input: id: OrderId
        ensures: orders'[id].status = PENDING
      }
      operation Review {
        input: id: OrderId
        requires: orders[id].status = PENDING
        ensures: orders'[id].status = REVIEW
      }
      // REVIEW has no exit -- deadlock
    }
    """
    ir = parse(spec)
    report = SpecVerifier(ir).verify()
    assert any("deadlock" in r.message.lower() for r in report.results)

; ============================================================
; E-Commerce Order Service -> SMT-LIB2 Translation
; ============================================================

(set-logic ALL)

; --- Sorts ---
(declare-sort OrderId 0)
(declare-sort ProductId 0)
(declare-sort CustomerId 0)

; --- Order Status Enum ---
; Modeled as integer constants
(declare-datatypes ((OrderStatus 0))
  ((PENDING) (PAID) (SHIPPED) (DELIVERED) (CANCELLED)))

; --- Order Fields ---
(declare-fun order_customer (OrderId) CustomerId)
(declare-fun order_status (OrderId) OrderStatus)
(declare-fun order_total (OrderId) Int)

; --- State: orders set and inventory ---
(declare-fun order_exists (OrderId) Bool)            ; pre-state
(declare-fun order_exists_post (OrderId) Bool)       ; post-state
(declare-fun order_status_pre (OrderId) OrderStatus)
(declare-fun order_status_post (OrderId) OrderStatus)
(declare-fun order_total_pre (OrderId) Int)
(declare-fun order_total_post (OrderId) Int)

(declare-fun inventory (ProductId) Int)              ; pre-state
(declare-fun inventory_post (ProductId) Int)         ; post-state

; --- Item mapping: order -> product -> quantity ---
(declare-fun order_item_qty (OrderId ProductId) Int) ; quantity of product in order

; --- Invariant: inventory >= 0 ---
(define-fun inv_inventory_nonneg () Bool
  (forall ((p ProductId)) (>= (inventory p) 0)))

(define-fun inv_inventory_nonneg_post () Bool
  (forall ((p ProductId)) (>= (inventory_post p) 0)))

; --- Invariant: order total >= 0 ---
(define-fun inv_total_nonneg () Bool
  (forall ((o OrderId))
    (=> (order_exists o) (>= (order_total_pre o) 0))))

; ============================================================
; CHECK: PlaceOrder preserves inventory >= 0
; ============================================================

(declare-const new_order OrderId)
(declare-const product1 ProductId)

; Pre-state invariant
(assert (forall ((p ProductId)) (>= (inventory p) 0)))

; Precondition: order does not already exist
(assert (not (order_exists new_order)))

; Precondition: sufficient inventory
; (simplified: one product in the order)
(assert (> (order_item_qty new_order product1) 0))
(assert (>= (inventory product1) (order_item_qty new_order product1)))

; Postcondition: order exists in post-state
(assert (order_exists_post new_order))
(assert (= (order_status_post new_order) PENDING))

; Postcondition: inventory decremented for product1
(assert (= (inventory_post product1)
           (- (inventory product1) (order_item_qty new_order product1))))

; Frame: inventory unchanged for other products
(assert (forall ((p ProductId))
  (=> (not (= p product1))
      (= (inventory_post p) (inventory p)))))

; Negation of post-invariant
(assert (not (forall ((p ProductId)) (>= (inventory_post p) 0))))

(check-sat)
; Expected: UNSAT (precondition guarantees sufficient inventory)

; ============================================================
; CHECK: CancelOrder preserves inventory >= 0
; ============================================================
; (Cancel restores inventory, so if pre-inventory >= 0 and we add positive
;  quantities, post-inventory >= 0. Trivially preserves the invariant.)