lab14: init

lab14/typed-semantics.typ

@@ -0,0 +1,92 @@
+// ============================================================
+// 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>