-- Programming Language Technology DAT151/DIT231 -- 2017-12-12 Agda -- From Dependent Types to Verified Compilation open import Relation.Binary.PropositionalEquality open ≡-Reasoning -- Example of a data type. data List (A : Set) : Set where [] : List A _∷_ : (x : A) (xs : List A) → List A -- Natural numbers in unary notation. data Nat : Set where zero : Nat suc : (n : Nat) → Nat {-# BUILTIN NATURAL Nat #-} -- NATURAL gives us decimal notation for Nat. five = suc 4 infixl 10 _+_ infixr 6 _∷_ _++_ -- Addition. _+_ : (n m : Nat) → Nat zero + m = m suc n + m = suc (n + m) plus-0 : ∀(n : Nat) → n + 0 ≡ n plus-0 zero = {!!} plus-0 (suc n) = {!!} -- Bounded numbers: Fin n = { m | n < m }. data Fin : Nat → Set where zero : {n : Nat} → Fin (suc n) suc : {n : Nat} (i : Fin n) → Fin (suc n) -- Example with hidden arguments. three : Fin 5 three = suc {4} (suc {3} (suc {2} (zero {1}))) -- Vectors (length-indexed lists). -- Vec : Set → Nat → Set data Vec (A : Set) : Nat → Set where [] : Vec A zero _∷_ : {n : Nat} (x : A) (xs : Vec A n) → Vec A (suc n) -- Reading an element of a vector. lookup : ∀{n A} (i : Fin n) (xs : Vec A n) → A lookup zero (x ∷ xs) = x lookup (suc i) (x ∷ xs) = lookup i xs -- Changing and element of a vector. update : ∀{n A} (i : Fin n) (x : A) (xs : Vec A n) → Vec A n update zero x (_ ∷ xs) = x ∷ xs update (suc i) x (y ∷ xs) = y ∷ update i x xs -- A partial formalization of JVM instructions and execution. StackSize = Nat -- Current stack size StoreSize = Nat -- Local variable store limit Addr = Fin -- Local variable address Word = Nat -- Word (should be 32bit signed int, but we use Nat here) -- JVM instructions. -- -- n = number of local variables -- m = stack size before instruction -- m' = stack size after instruction data Ins (n : StoreSize) : (m m' : StackSize) → Set where load : ∀{m} (a : Addr n) → Ins n m (1 + m) -- Load variable onto stack. store : ∀{m} (a : Addr n) → Ins n (1 + m) m -- Store top stack element into variable. add : ∀{m} → Ins n (2 + m) (1 + m) -- Add top stack elements. ldc : ∀{m} (w : Word) → Ins n m (1 + m) -- Load constant onto stack. pop : ∀{m} (w : Word) → Ins n (1 + m) m -- Remove top stack element. -- JVM machine state (simplified). record State (n : StoreSize) (m : StackSize) : Set where constructor state field V : Vec Word n S : Vec Word m open State -- Pushing a word onto the stack. push : ∀{n m} → Word → State n m → State n (suc m) push w (state V S) = state V (w ∷ S) -- Executing a JVM instruction. step : ∀{n m m'} (i : Ins n m m') (s : State n m) → State n m' step (load a) (state V S) = state V (lookup a V ∷ S) step (store a) (state V (w ∷ S)) = state (update a w V) S step add (state V (w ∷ v ∷ S)) = state V (v + w ∷ S) step (ldc w) (state V S) = state V (w ∷ S) step (pop w) (state V (_ ∷ S)) = state V S -- Instruction lists. -- Note that for instruction cons, the index "l" has to match. data Inss (n : StoreSize) (m : StackSize) : (m' : StackSize) → Set where [] : Inss n m m _∷_ : ∀{l k} (i : Ins n m l) (is : Inss n l k) → Inss n m k -- Concatenating instruction lists. _++_ : ∀{n m m' m''} → Inss n m m' → Inss n m' m'' → Inss n m m'' [] ++ is' = is' (i ∷ is) ++ is' = i ∷ (is ++ is') -- Lemma: Appending and empty list. ++-[] : ∀{n m m'} (i : Inss n m m') → i ++ [] ≡ i ++-[] = {!!} -- Lemma: Concatenation is associative. ++-assoc : ∀{n m m' m'' m'''} (is : Inss n m m') (is' : Inss n m' m'') (is'' : Inss n m'' m''') → (is ++ is') ++ is'' ≡ is ++ (is' ++ is'') ++-assoc = {!!} -- Executing a series of JVM instructions. steps : ∀{n m m'} (is : Inss n m m') (s : State n m) → State n m' steps [] s = s steps (i ∷ is) s = steps is (step i s) -- Executing a concatenation. steps-++ : ∀{n m m' m''} (is : Inss n m m') (is' : Inss n m' m'') (s : State n m) → steps (is ++ is') s ≡ steps is' (steps is s) steps-++ [] is' s = refl steps-++ (i ∷ is) is' s = steps-++ is is' (step i s) -- Expressions (Hutton's Razor only). data Exp : Set where num : (w : Word) → Exp plus : (e e' : Exp) → Exp -- Interpretation of expressions. eval : Exp → Word eval (num w) = w eval (plus e e') = eval e + eval e' -- Compilation of expressions. compile : ∀{n m} (e : Exp) → Inss n m (suc m) compile (num w) = ldc w ∷ [] compile (plus e e') = compile e ++ compile e' ++ add ∷ [] -- Compiler correctness. -- Lemma. -- Running the instructions for an expression e leaves the value of e on top of the stack, -- for a continuation to run from here. sound' : ∀{n m m'} (e : Exp) (s : State n m) (is : Inss n (suc m) m') → steps (compile e ++ is) s ≡ steps is (push (eval e) s) -- Case: number literals. sound' (num w) s is = steps-++ (ldc w ∷ []) is s -- Case: addition expression. sound' (plus e e') s is = begin steps ((compile e ++ compile e' ++ add ∷ []) ++ is) s ≡⟨ {!!} ⟩ steps (compile e ++ compile e' ++ (add ∷ []) ++ is) s ≡⟨ sound' e s (compile e' ++ (add ∷ []) ++ is) ⟩ steps (compile e' ++ (add ∷ []) ++ is) (push (eval e) s) ≡⟨ sound' e' (push (eval e) s) ((add ∷ []) ++ is) ⟩ steps ((add ∷ []) ++ is) (push (eval e') (push (eval e) s)) ≡⟨ steps-++ (add ∷ []) is (push (eval e') (push (eval e) s)) ⟩ steps is (push (eval e + eval e') s) ∎ -- Theorem. -- Running the instructions for an expression e leaves the value of e on top of the stack. sound : ∀{n m} (e : Exp) (s : State n m) → steps (compile e) s ≡ push (eval e) s sound {n} e s = begin steps (compile e) s ≡⟨ cong (λ z → steps z s) (sym (++-[] (compile e))) ⟩ steps (compile e ++ []) s ≡⟨ sound' e s [] ⟩ steps [] (push (eval e) s) ≡⟨⟩ push (eval e) s ∎