diff --git a/essay.lagda.md b/src/Essay.lagda.md similarity index 84% rename from essay.lagda.md rename to src/Essay.lagda.md index d675665..c5cbec6 100644 --- a/essay.lagda.md +++ b/src/Essay.lagda.md @@ -1,7 +1,7 @@ # Mechanisation of WebAssembly 1.0 (in Agda) ``` -module ExtraCredit where +module Essay where ``` @@ -620,57 +620,30 @@ A notable limitation here is that programs can end with at most one value on the We will use this constructor when we enter a block with a return type: ```agda - _,_⦂ˢ_ : ∀ {Γ Δ r r′} + _,_⦂_ : ∀ {Γ Δ r r′} → Frames r Γ - → Γ ⊢ Δ , r′ ⟫ ∅ +ʳ r + → Γ ⊢ Δ +ʳ r′ ⟫ ∅ +ʳ r → OpStack Δ ----------------------------- - → Frames (some r′) (Γ +ˡ some r′) + → Frames r′ (Γ +ˡ r′) ``` -Here, `r` is the type that the block which we are saving must return, and `r′` is the type we need to get before we can return to it. +Here, `r` is the return type of the block which we are saving, and `r′` is the return type we need before we can return to it. We store the 'continuation', which gets the return value, and will finish with whatever its previous frame expects. We also save the current state of the operand stack. -Unfortunately, we have to specify constructors for when there is a return type and when there isn't seperately, as Agda is unable to unify some constraints later if we don't. - - - -```agda - _,_⦂ⁿ_ : ∀ {Γ Δ r} - → Frames r Γ - → Γ ⊢ Δ ⟫ ∅ +ʳ r - → OpStack Δ - ----------------------- - → Frames none (Γ +ˡ none) -``` - -This definition is similar, but the stack will be unchanged once we come back. - Loop constructs must also store the inner body of the loop, since when we `br` to this label we will go back to the start of the inner body. When we finish the body normally, we will continue on with the second instruction list. Note that we need the next frame to return `some r`, but we add the label `none`, as we mentioned above. ```agda - _,_↬_⦂ˢ_ : ∀ {Γ Δ r r′} + _,_↬_⦂_ : ∀ {Γ Δ r r′} → Frames r Γ - → Γ +ˡ none ⊢ ∅ ⟫ ∅ , r′ -- Loop body - → Γ ⊢ Δ , r′ ⟫ ∅ +ʳ r -- Continuation + → Γ +ˡ none ⊢ ∅ ⟫ ∅ +ʳ r′ -- Loop body + → Γ ⊢ Δ +ʳ r′ ⟫ ∅ +ʳ r -- Continuation → OpStack Δ --------------------------- - → Frames (some r′) (Γ +ˡ none) - - _,_↬_⦂ⁿ_ : ∀ {Γ Δ r} - → Frames r Γ - → Γ +ˡ none ⊢ ∅ ⟫ ∅ - → Γ ⊢ Δ ⟫ ∅ +ʳ r - → OpStack Δ - ----------------------- - → Frames none (Γ +ˡ none) + → Frames r′ (Γ +ˡ none) ``` Now we define the current state of execution, referred to as a `Configuration` as in the specification. @@ -691,6 +664,10 @@ The last thing we need before we can define our reduction rules is the ability t This will be used when we call `br`, and must ascend the amount of frames specified, resuming that frame with the given return value and the new locals. ```agda + transplant-ret : ∀ {Δ Δ′ r} → OpStack (Δ +ʳ r) → OpStack Δ′ → OpStack (Δ′ +ʳ r) + transplant-ret {r = some _} (xs , x) m = m , x + transplant-ret {r = none} s m = m + br-unwind : ∀ {Γ Δ r v} → (Context.labels Γ) ∋ v -- Label/frame to unwind up to → OpStack (Δ +ʳ v) @@ -700,18 +677,14 @@ This will be used when we call `br`, and must ascend the amount of frames specif → Configuration -- Base cases - resume the top frame - br-unwind {v = some V} Z (_ , v) ls (ss , is ⦂ˢ s) = conf is (s , v) ls ss - br-unwind {v = none} Z _ ls (ss , is ⦂ⁿ s) = conf is s ls ss + br-unwind Z s ls (ss , is ⦂ s′) = conf is (transplant-ret s s′) ls ss -- For loops - go back to the start and don't remove the frame - br-unwind Z _ ls ss@(_ , start ↬ cont ⦂ˢ s) = conf start ∅ ls ss - br-unwind Z _ ls ss@(_ , start ↬ cont ⦂ⁿ s) = conf start ∅ ls ss + br-unwind Z _ ls ss@(_ , start ↬ cont ⦂ s) = conf start ∅ ls ss -- Recursive cases - br-unwind (S l) s ls (ss , _ ⦂ˢ _) = br-unwind l s ls ss - br-unwind (S l) s ls (ss , _ ⦂ⁿ _) = br-unwind l s ls ss - br-unwind (S l) s ls (ss , _ ↬ _ ⦂ˢ _) = br-unwind l s ls ss - br-unwind (S l) s ls (ss , _ ↬ _ ⦂ⁿ _) = br-unwind l s ls ss + br-unwind (S l) s ls (ss , _ ⦂ _) = br-unwind l s ls ss + br-unwind (S l) s ls (ss , _ ↬ _ ⦂ _) = br-unwind l s ls ss ``` @@ -803,63 +776,34 @@ As described above, when we enter a block we save the current state in our list We know that the inner instruction sequence will have the correct end state because of how we define our `block` instruction, but Agda needs us to spell it out anyway. ```agda - block-some : ∀ {Γ Δ r r′ s ls ss} - {is : Γ ⊢ Δ , r′ ⟫ ∅ +ʳ r} - {is′ : Γ +ˡ some r′ ⊢ ∅ ⟫ ∅ , r′} - ------------------------------------------- - → conf {Γ} {Δ} {r} (block is′ then is) s ls ss - —→ conf is′ ∅ ls (ss , is ⦂ˢ s) - - block-none : ∀ {Γ Δ r s ls ss} - {is : Γ ⊢ Δ ⟫ ∅ +ʳ r} - {is′ : Γ +ˡ none ⊢ ∅ ⟫ ∅} - ------------------------------------------- - → conf {Γ} {Δ} {r} (block is′ then is) s ls ss - —→ conf is′ ∅ ls (ss , is ⦂ⁿ s) - - loop-some : ∀ {Γ Δ r r′ s ls ss} - {is : Γ ⊢ Δ , r′ ⟫ ∅ +ʳ r} - {is′ : Γ +ˡ none ⊢ ∅ ⟫ ∅ , r′} - ------------------------------------------------------------ - → conf (loop is′ then is) s ls ss —→ conf is′ ∅ ls (ss , is′ ↬ is ⦂ˢ s) - - loop-none : ∀ {Γ Δ r s ls ss} - {is : Γ ⊢ Δ ⟫ ∅ +ʳ r} - {is′ : Γ +ˡ none ⊢ ∅ ⟫ ∅} - ------------------------------------------------------------ - → conf (loop is′ then is) s ls ss —→ conf is′ ∅ ls (ss , is′ ↬ is ⦂ⁿ s) - - ifᵀ-some : ∀ {Γ Δ n r r′ s ls ss} - {is : Γ ⊢ Δ , r′ ⟫ ∅ +ʳ r} - {ts : Γ +ˡ some r′ ⊢ ∅ ⟫ ∅ , r′} - {es : Γ +ˡ some r′ ⊢ ∅ ⟫ ∅ , r′} - ---------------------------------------------------------------------------- - → conf {Γ} {Δ , Number} {r} (if ts else es then is) (s , Number (suc n)) ls ss - —→ conf ts ∅ ls (ss , is ⦂ˢ s) - - ifᵀ-none : ∀ {Γ Δ n r s ls ss} - {is : Γ ⊢ Δ ⟫ ∅ +ʳ r} - {ts : Γ +ˡ none ⊢ ∅ ⟫ ∅} - {es : Γ +ˡ none ⊢ ∅ ⟫ ∅} - ---------------------------------------------------------------------------- - → conf {Γ} {Δ , Number} {r} (if ts else es then is) (s , Number (suc n)) ls ss - —→ conf ts ∅ ls (ss , is ⦂ⁿ s) - - ifꟳ-some : ∀ {Γ Δ r r′ s ls ss} - {is : Γ ⊢ Δ , r′ ⟫ ∅ +ʳ r} - {ts : Γ +ˡ some r′ ⊢ ∅ ⟫ ∅ , r′} - {es : Γ +ˡ some r′ ⊢ ∅ ⟫ ∅ , r′} - ------------------------------------------------------------------------- - → conf {Γ} {Δ , Number} {r} (if ts else es then is) (s , Number zero) ls ss - —→ conf es ∅ ls (ss , is ⦂ˢ s) - - ifꟳ-none : ∀ {Γ Δ r s ls ss} - {is : Γ ⊢ Δ ⟫ ∅ +ʳ r} - {ts : Γ +ˡ none ⊢ ∅ ⟫ ∅} - {es : Γ +ˡ none ⊢ ∅ ⟫ ∅} - ------------------------------------------------------------------------- - → conf {Γ} {Δ , Number} {r} (if ts else es then is) (s , Number zero) ls ss - —→ conf es ∅ ls (ss , is ⦂ⁿ s) + block : ∀ {Γ Δ r r′ s ls ss} + {is : Γ ⊢ Δ +ʳ r′ ⟫ ∅ +ʳ r} + {is′ : Γ +ˡ r′ ⊢ ∅ ⟫ ∅ +ʳ r′} + ------------------------------------------- + → conf {Γ} {Δ} {r} (block is′ then is) s ls ss + —→ conf is′ ∅ ls (ss , is ⦂ s) + + loop : ∀ {Γ Δ r r′ s ls ss} + {is : Γ ⊢ Δ +ʳ r′ ⟫ ∅ +ʳ r} + {is′ : Γ +ˡ none ⊢ ∅ ⟫ ∅ +ʳ r′} + ------------------------------------------------------------ + → conf (loop is′ then is) s ls ss —→ conf is′ ∅ ls (ss , is′ ↬ is ⦂ s) + + ifᵀ : ∀ {Γ Δ n r r′ s ls ss} + {is : Γ ⊢ Δ +ʳ r′ ⟫ ∅ +ʳ r} + {ts : Γ +ˡ r′ ⊢ ∅ ⟫ ∅ +ʳ r′} + {es : Γ +ˡ r′ ⊢ ∅ ⟫ ∅ +ʳ r′} + ---------------------------------------------------------------------------- + → conf {Γ} {Δ , Number} {r} (if ts else es then is) (s , Number (suc n)) ls ss + —→ conf ts ∅ ls (ss , is ⦂ s) + + ifꟳ : ∀ {Γ Δ r r′ s ls ss} + {is : Γ ⊢ Δ +ʳ r′ ⟫ ∅ +ʳ r} + {ts : Γ +ˡ r′ ⊢ ∅ ⟫ ∅ +ʳ r′} + {es : Γ +ˡ r′ ⊢ ∅ ⟫ ∅ +ʳ r′} + ------------------------------------------------------------------------- + → conf {Γ} {Δ , Number} {r} (if ts else es then is) (s , Number zero) ls ss + —→ conf es ∅ ls (ss , is ⦂ s) ``` `br` uses the `br-unwind` function defined above. @@ -919,25 +863,15 @@ Now we define our local instructions, which only affect the locals part of our c Finally, we need to be able to go back up to our previous frames once we've completed our current list of instructions. ```agda - ascend-some : ∀ {Γ V v ls Δ′ r′ cont s′ ss′} - -------------------------------------------------------------------- - → conf {Γ +ˡ some V} {∅ , V} {some V} done (∅ , v) ls (ss′ , cont ⦂ˢ s′) - —→ conf {Γ} {Δ′ , V} {r′} cont (s′ , v) ls ss′ - - ascend-none : ∀ {Γ ls Δ′ r′ s′ ss′ cont} - ------------------------------------------------------ - → conf {Γ +ˡ none} {∅} {none} done ∅ ls (ss′ , cont ⦂ⁿ s′) - —→ conf {Γ} {Δ′} {r′} cont s′ ls ss′ - - ascendˡ-some : ∀ {Γ V v ls Δ′ r′ s′ ss′ start cont} - -------------------------------------------------------------------------- - → conf {Γ +ˡ none} {∅ , V} {some V} done (∅ , v) ls (ss′ , start ↬ cont ⦂ˢ s′) - —→ conf {Γ} {Δ′ , V} {r′} cont (s′ , v) ls ss′ - - ascendˡ-none : ∀ {Γ ls Δ′ r′ s′ ss′ start cont} - -------------------------------------------------------------- - → conf {Γ +ˡ none} {∅} {none} done ∅ ls (ss′ , start ↬ cont ⦂ⁿ s′) - —→ conf {Γ} {Δ′} {r′} cont s′ ls ss′ + ascend : ∀ {Γ r ls Δ′ r′ cont s s′ ss′} + -------------------------------------------------------------------- + → conf {Γ +ˡ r} {∅ +ʳ r} {r} done s ls (ss′ , cont ⦂ s′) + —→ conf {Γ} {Δ′ +ʳ r} {r′} cont (transplant-ret s s′) ls ss′ + + ascendˡ : ∀ {Γ r ls Δ′ r′ s s′ ss′ start cont} + -------------------------------------------------------------------------- + → conf {Γ +ˡ none} {∅ +ʳ r} {r} done s ls (ss′ , start ↬ cont ⦂ s′) + —→ conf {Γ} {Δ′ +ʳ r} {r′} cont (transplant-ret s s′) ls ss′ ``` ## Progress @@ -994,18 +928,14 @@ For `op-test` and `op-rel` we must decide if `f x` is true ourselves. ``` -We must use different rules for loop and block depending on if there is a return value. +We may deliberately ascend up the frame stack: ```agda - progress (conf (block {r = some _} is′ then is) s _ ss) = step block-some - progress (conf (block {r = none} is′ then is) s _ ss) = step block-none - progress (conf (loop {r = some _} is′ then is) s _ ss) = step loop-some - progress (conf (loop {r = none} is′ then is) s _ ss) = step loop-none + progress (conf (block is′ then is) s _ ss) = step block + progress (conf (loop is′ then is) s _ ss) = step loop - progress (conf (if_else_ {r = some x} ts _ then is) (_ , Number (suc n)) _ ss) = step ifᵀ-some - progress (conf (if_else_ {r = none} ts _ then is) (_ , Number (suc n)) _ ss) = step ifᵀ-none - progress (conf (if_else_ {r = some x} _ fs then is) (_ , Number zero) _ ss) = step ifꟳ-some - progress (conf (if_else_ {r = none} _ fs then is) (_ , Number zero) _ ss) = step ifꟳ-none + progress (conf (if_else_ ts _ then is) (_ , Number (suc n)) _ ss) = step ifᵀ + progress (conf (if_else_ _ fs then is) (_ , Number zero) _ ss) = step ifꟳ progress (conf (br lbl then is) s _ ss) = step br progress (conf (br-if lbl then is) (_ , Number (suc _)) _ ss) = step br-ifᵀ @@ -1016,10 +946,8 @@ Finally, if we run out of instructions in the current frame we must try to use t Again, we know that we will have the return type when we need it thanks to the constraints in `Configuration`. ```agda - progress (conf done (∅ , v) _ (ss′ , is′ ⦂ˢ s′)) = step ascend-some - progress (conf done ∅ _ (ss′ , is′ ⦂ⁿ s′)) = step ascend-none - progress (conf done (∅ , v) _ (ss′ , ls ↬ is′ ⦂ˢ s′)) = step ascendˡ-some - progress (conf done ∅ _ (ss′ , ls ↬ is′ ⦂ⁿ s′)) = step ascendˡ-none + progress (conf done _ _ (ss′ , is′ ⦂ s′)) = step ascend + progress (conf done _ _ (ss′ , ls ↬ is′ ⦂ s′)) = step ascendˡ ``` We are only done when all instructions are executed, and we can't go up any more stack frames. @@ -1126,17 +1054,17 @@ Now we can evaluate the programs we defined earlier. (∅ , Number 0) ∅ ∅ - —→⟨ ifꟳ-some ⟩ + —→⟨ ifꟳ ⟩ conf (const 84 then done) ∅ ∅ - (∅ , done ⦂ˢ ∅) + (∅ , done ⦂ ∅) —→⟨ const ⟩ conf done (∅ , Number 84) ∅ - (∅ , done ⦂ˢ ∅) - —→⟨ ascend-some ⟩ + (∅ , done ⦂ ∅) + —→⟨ ascend ⟩ conf done (∅ , Number 84) ∅ @@ -1150,17 +1078,17 @@ Now we can evaluate the programs we defined earlier. (∅ , Number 1) ∅ ∅ - —→⟨ ifᵀ-some ⟩ + —→⟨ ifᵀ ⟩ conf (const 42 then done) ∅ ∅ - (∅ , done ⦂ˢ ∅) + (∅ , done ⦂ ∅) —→⟨ const ⟩ conf done (∅ , Number 42) ∅ - (∅ , done ⦂ˢ ∅) - —→⟨ ascend-some ⟩ + (∅ , done ⦂ ∅) + —→⟨ ascend ⟩ conf done (∅ , Number 42) ∅ @@ -1195,7 +1123,7 @@ Now we can evaluate the programs we defined earlier. op-binary (λ x y → x - y) then local-tee Z then br-if Z then done) then done) ∅ (∅ , Number 3) ∅ - —→⟨ loop-none ⟩ -- Loop 1 + —→⟨ loop ⟩ -- Loop 1 conf (local-get Z then const 1 then @@ -1205,7 +1133,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ local-get ⟩ conf (const 1 then @@ -1215,7 +1143,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ const ⟩ conf (op-binary (λ x y → x - y) then local-tee Z then br-if Z then done) @@ -1224,7 +1152,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ op-binary ⟩ conf (local-tee Z then br-if Z then done) (∅ , Number 2) (∅ , Number 3) @@ -1232,14 +1160,14 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ local-tee ⟩ conf (br-if Z then done) (∅ , Number 2) (∅ , Number 2) (∅ , local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ br-ifᵀ ⟩ -- Loop 2 conf (local-get Z then @@ -1250,7 +1178,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ local-get ⟩ conf (const 1 then @@ -1260,7 +1188,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ const ⟩ conf (op-binary (λ x y → x - y) then local-tee Z then br-if Z then done) @@ -1269,7 +1197,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ op-binary ⟩ conf (local-tee Z then br-if Z then done) (∅ , Number 1) (∅ , Number 2) @@ -1277,14 +1205,14 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ local-tee ⟩ conf (br-if Z then done) (∅ , Number 1) (∅ , Number 1) (∅ , local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ br-ifᵀ ⟩ -- Loop 3 conf (local-get Z then @@ -1295,7 +1223,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ local-get ⟩ conf (const 1 then @@ -1305,7 +1233,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ const ⟩ conf (op-binary (λ x y → x - y) then local-tee Z then br-if Z then done) @@ -1314,7 +1242,7 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ op-binary ⟩ conf (local-tee Z then br-if Z then done) (∅ , Number 0) (∅ , Number 1) @@ -1322,22 +1250,22 @@ Now we can evaluate the programs we defined earlier. local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ local-tee ⟩ conf (br-if Z then done) (∅ , Number 0) (∅ , Number 0) (∅ , local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) + ↬ done ⦂ ∅) —→⟨ br-ifꟳ ⟩ conf done ∅ (∅ , Number 0) (∅ , local-get Z then const 1 then op-binary (λ x y → x - y) then local-tee Z then br-if Z then done - ↬ done ⦂ⁿ ∅) - —→⟨ ascendˡ-none ⟩ + ↬ done ⦂ ∅) + —→⟨ ascendˡ ⟩ conf done ∅ (∅ , Number 0) ∅ ∎) _ = refl