4bf2dd38cd
git-subtree-dir: common-lean git-subtree-mainline:bd2e14214dgit-subtree-split:a0b719e170
97 lines
3.2 KiB
Text
97 lines
3.2 KiB
Text
/-!
|
||
# Common.Lang — cross-language abstraction.
|
||
|
||
A `BigStepLang` is a programming-language fragment with:
|
||
* a syntactic class of terms,
|
||
* a class of values,
|
||
* a state type carrying everything else (env, heap, etc.),
|
||
* a big-step relation `Eval : State → Term → Value → State → Prop`
|
||
saying "starting in state `s`, evaluating term `t` produces value
|
||
`v` and state `s'`",
|
||
* a determinism property (the relation is functional in `(v, s')`).
|
||
|
||
This generalises TGC's `BigStep : Heap → Env → Term → Value → Heap`
|
||
(with State := Heap × Env) and TOC's `BigStep : Env → Term → Value →
|
||
Env` (with State := Env). TSM uses small-step semantics and fits a
|
||
different class — see `SmallStepLang`.
|
||
|
||
The point of the abstraction: theorems about *any* deterministic
|
||
big-step language are stated and proved once, and apply to all
|
||
instances. -/
|
||
|
||
namespace Common
|
||
|
||
class BigStepLang where
|
||
Term : Type
|
||
Value : Type
|
||
State : Type
|
||
Eval : State → Term → Value → State → Prop
|
||
deterministic : ∀ {s : State} {t : Term} {v₁ v₂ : Value} {s₁ s₂ : State},
|
||
Eval s t v₁ s₁ → Eval s t v₂ s₂ → v₁ = v₂ ∧ s₁ = s₂
|
||
|
||
namespace BigStepLang
|
||
|
||
variable [L : BigStepLang]
|
||
|
||
/-- Result of an evaluation, when it exists, is unique. -/
|
||
theorem unique_value
|
||
{s : L.State} {t : L.Term} {v₁ v₂ : L.Value} {s₁ s₂ : L.State}
|
||
(h₁ : L.Eval s t v₁ s₁) (h₂ : L.Eval s t v₂ s₂) :
|
||
v₁ = v₂ :=
|
||
(L.deterministic h₁ h₂).1
|
||
|
||
theorem unique_state
|
||
{s : L.State} {t : L.Term} {v₁ v₂ : L.Value} {s₁ s₂ : L.State}
|
||
(h₁ : L.Eval s t v₁ s₁) (h₂ : L.Eval s t v₂ s₂) :
|
||
s₁ = s₂ :=
|
||
(L.deterministic h₁ h₂).2
|
||
|
||
end BigStepLang
|
||
|
||
/-! ## SmallStepLang — small-step semantics (e.g., TSM).
|
||
|
||
A `SmallStepLang` is structurally simpler: a state type and a step
|
||
function. Determinism is automatic since `step` is a function. -/
|
||
|
||
class SmallStepLang where
|
||
State : Type
|
||
step : State → Option State
|
||
|
||
namespace SmallStepLang
|
||
|
||
variable [L : SmallStepLang]
|
||
|
||
/-- Reflexive-transitive closure of `step`. -/
|
||
inductive MultiStep : L.State → L.State → Prop where
|
||
| refl (s : L.State) : MultiStep s s
|
||
| cons {s s' s'' : L.State}
|
||
(h₁ : L.step s = some s') (h₂ : MultiStep s' s'') :
|
||
MultiStep s s''
|
||
|
||
/-- Single-step is functional. -/
|
||
theorem step_deterministic {s s₁ s₂ : L.State}
|
||
(h₁ : L.step s = some s₁) (h₂ : L.step s = some s₂) :
|
||
s₁ = s₂ := by
|
||
rw [h₁] at h₂; exact Option.some.inj h₂
|
||
|
||
end SmallStepLang
|
||
|
||
/-! ## Compilation correctness — the substrate-projection theorem.
|
||
|
||
If `Source` is a `BigStepLang`, `Target` is either kind, and `compile`
|
||
maps source specs to target specs preserving evaluation, then the
|
||
compilation pipeline inherits determinism.
|
||
|
||
This is the categorical kernel of CompCert-style theorems. -/
|
||
|
||
structure CompileCorrect
|
||
(Source : BigStepLang)
|
||
(Target : Type) (TargetEval : Target → Source.Value → Prop)
|
||
(compile : Source.Term → Target) where
|
||
/-- Compilation preserves evaluation: source `Eval` implies target
|
||
`TargetEval` produces the same value. -/
|
||
preservation :
|
||
∀ {s : Source.State} {t : Source.Term} {v : Source.Value} {s' : Source.State},
|
||
Source.Eval s t v s' → TargetEval (compile t) v
|
||
|
||
end Common
|