// ============================================================
// Operational Semantics for BoolInt* Language — Typst version
// ============================================================
//
// ----- helper functions -------------------------------------

// Language keywords rendered in monospace
#let kw(body) = text(font: "DejaVu Sans Mono", size: 0.85em, body)

#let tr = kw[true]
#let fl = kw[false]
#let ife(e1, e2, e3) = [#kw[if] #e1 #kw[then] #e2 #kw[else] #e3]
#let suc(e) = [#kw[succ] #e]
#let prd(e) = [#kw[pred] #e]
#let sec(e) = [#kw[secret] #e]

// Security labels
#let lH = $upright(H)$
#let lL = $upright(L)$
#let ljoin = $union.sq$

// Labeled value: (v, ℓ)
#let lval(v, l) = $(#v, #l)$

// Big-step evaluation relation: e ⇓ (v, ℓ)
#let bstep(e, v) = $#e arrow.b.double #v$

// Rule name label in small-caps
#let rel(name) = text(size: 0.9em, smallcaps[\[#name\]])

// Big-step rule: fraction with name on the left
// premises (content), conclusion (content)
#let bsrule(name, premises, conclusion) = {
  grid(
    columns: (auto, auto),
    column-gutter: 1em,
    align: (right + horizon, left + horizon),
    rel(name), math.equation(block: true, numbering: none, math.frac(premises, conclusion)),
  )
  v(0.4em)
}

// Definition head: "e ::= ..." with label
#let mydefhead(lhs, label) = {
  grid(
    columns: (auto, auto),
    column-gutter: 1fr,
    [#lhs], emph(label),
  )
}

// Definition case: indented alternative with description
#let mydefcase(alt, desc) = {
  grid(
    columns: (2em, auto, auto),
    column-gutter: 1fr,
    [], [#alt], [#desc],
  )
}


// ----- Figure 2: big-step semantics -------------------------

#figure(
  box(width: 85%, inset: (left: 1em))[
    #set align(left)
    #text(weight: "bold")[Evaluation Rules:#h(1em)]#box(stroke: 0.5pt, inset: 4pt, $#bstep[$e$][$#lval[$v$][$ell$]$]$)

    #v(0.6em)

    #bsrule("B-Value", "", $#bstep[$v$][$#lval[$v$][$#lL$]$]$)

    #bsrule("B-Secret", $#bstep[$e$][$#lval[$v$][$ell$]$]$, $#bstep[#sec[$e$]][$#lval[$v$][$#lH$]$]$)

    #bsrule(
      "B-IfTrue",
      $#bstep[$e_1$][$#lval[$#tr$][$ell_1$]$] #h(2em) #bstep[$e_2$][$#lval[$v$][$ell_2$]$]$,
      $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$#lval[$v$][$ell_1 #ljoin ell_2$]$]$,
    )

    #bsrule(
      "B-IfFalse",
      $#bstep[$e_1$][$#lval[$#fl$][$ell_1$]$] #h(2em) #bstep[$e_3$][$#lval[$v$][$ell_3$]$]$,
      $#bstep[#ife[$e_1$][$e_2$][$e_3$]][$#lval[$v$][$ell_1 #ljoin ell_3$]$]$,
    )

    #bsrule("B-Succ", $#bstep[$e$][$#lval[$i$][$ell$]$]$, $#bstep[#suc[$e$]][$#lval[$i + 1$][$ell$]$]$)

    #bsrule("B-Pred", $#bstep[$e$][$#lval[$i$][$ell$]$]$, $#bstep[#prd[$e$]][$#lval[$i - 1$][$ell$]$]$)
  ],
  caption: [Big-step semantics for BoolInt\* with information flow],
) <fig:bigstep>