From 9773ea404d41ce04489fd784947c7033a93be064 Mon Sep 17 00:00:00 2001
From: Aria Shrimpton <me@aria.rip>
Date: Mon, 26 Feb 2024 11:18:17 +0000
Subject: [PATCH] some more validation

---
 src/Wasm/Lists.agda      | 14 ++++++++------
 src/Wasm/Validation.agda | 20 +++++++++++++++-----
 2 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/src/Wasm/Lists.agda b/src/Wasm/Lists.agda
index c669088..e9dc4b6 100644
--- a/src/Wasm/Lists.agda
+++ b/src/Wasm/Lists.agda
@@ -3,6 +3,7 @@ module Wasm.Lists where
 
 open import Agda.Builtin.List
 open import Agda.Builtin.Nat as N
+open import Agda.Builtin.Equality
 open import Data.List using (length; lookup; take; drop; _++_)
 open import Data.Vec as V using (Vec; []; _∷_)
 open import Data.Fin using (Fin; suc; zero; toℕ)
@@ -45,21 +46,22 @@ _[_] : ∀ {T F} {Δ : List T} {t} → TypedList F Δ → Δ ∋ t → F t
 
 -- Target one or more entries at the top of a list
 data _∋*_ {T : Set} : List T → List T → Set where
-  count : ∀ {l : List T} → (n : Fin (N.suc (length l))) → l ∋* (take (toℕ n) l)
+  except : ∀ {Δ Φ : List T} → (bot : List T) → (Δ ≡ Φ ++ bot) → Δ ∋* Φ
 
 -- Discard that amount from the list
 discard : ∀ {T} {Δ φ : List T} → Δ ∋* φ → List T
-discard {Δ = Δ} (count n) = drop (toℕ n) Δ
+discard (except bot _) = bot
 
 -- Take the targeted region from a related typedstack
 take-vals : ∀ {T} {F : T → Set} {Δ φ : List T} → TypedList F Δ → Δ ∋* φ → TypedList F φ
-take-vals (x ∷ s) (count (suc n)) = x ∷ (take-vals s (count n))
-take-vals s (count zero) = []
+take-vals {φ = []} s (except _ refl) = []
+take-vals {φ = t ∷ ts} (s ∷ ss) (except bot refl) = s ∷ (take-vals ss (except bot refl))
 
 -- Discard the targeted region from a related typestack
 discard-vals : ∀ {T} {F : T → Set} {Δ φ : List T} → TypedList F Δ → (l : Δ ∋* φ) → TypedList F (discard l)
-discard-vals s (count zero) = s
-discard-vals (x ∷ xs) (count (suc n)) = discard-vals xs (count n)
+discard-vals {φ = []} s (except _ refl) = s
+discard-vals {φ = t ∷ ts} (_ ∷ s) (except bot refl) = discard-vals s (except bot refl)
+-- discard-vals (x ∷ xs) (count (suc n)) = discard-vals xs (count n)
 
 -- A vector with a related list of types
 data TypedVec : ∀ {T n} → (T → Set) → (Vec T n) → Set where
diff --git a/src/Wasm/Validation.agda b/src/Wasm/Validation.agda
index b0572e9..251c61c 100644
--- a/src/Wasm/Validation.agda
+++ b/src/Wasm/Validation.agda
@@ -13,7 +13,7 @@ open import Relation.Nullary using (Dec; yes; no)
 open import Data.Nat.Properties using (_<?_; suc-injective)
 open import Data.List using (map; _++_)
 open import Data.Vec using (Vec; []; _∷_; length; fromList; lookup)
-open import Data.Fin using (Fin; fromℕ<)
+open import Data.Fin using (Fin; suc; zero; fromℕ<)
 
 open import Wasm.Types
 open import Wasm.Configuration
@@ -103,6 +103,13 @@ getFuncType fts record { funcType = funcTypeIdx; localTypes = localTypes } = do
 
   ok record { args = args; ret = ret; locals = locals }
 
+checkStackTop : ∀ (Δ : ValStackTy) → (Φ : ValStackTy) → Result (Δ ∋* Φ)
+checkStackTop s [] = ok (except s refl)
+checkStackTop [] (x ∷ t) = err "stack was empty, but shouldnt have been"
+checkStackTop (x ∷ s) (y ∷ t) with valty-eq x y
+... | yes refl = (checkStackTop s t) >>= (λ{ (except bot refl) → ok (except bot refl) })
+... | no _ = err "wrong type"
+
 -- Validate that the given body runs in context Γ, and goes from stack `from` to `to`
 validateBody : ∀ {μ} {Γ : Context μ} → (from : ValStackTy) → (to : ValStackTy) → (List UT.Instruction) → Result (Γ ⊢ from ⟫ to)
 validateBody ss ts [] with valstackty-eq ss ts
@@ -114,8 +121,13 @@ validateBody ss ts (UT.I32Const n ∷ is) = validateBody (int l32 ∷ ss) ts is
 validateBody ss ts (UT.I64Const n ∷ is) = validateBody (int l64 ∷ ss) ts is >>= (ok ∘ (i-const (i64 n) then_))
 validateBody ss ts (UT.F32Const n ∷ is) = err "TODO: Float instructions"
 validateBody ss ts (UT.F64Const n ∷ is) = err "TODO: Float instructions"
-validateBody ss ts (UT.IUnOp x x₁ ∷ is) = err "TODO"
-validateBody ss ts (UT.IBinOp x x₁ ∷ is) = err "TODO"
+validateBody ss ts (UT.IUnOp s op ∷ is) with checkStackTop ss (int s ∷ [])
+... | err x = err x
+... | ok (except _ refl) = validateBody ss ts is >>= (ok ∘ (i-unop op then_))
+validateBody ss ts (UT.IBinOp s op ∷ is) = do
+  (except bot refl) <- checkStackTop ss (int s ∷ int s ∷ [])
+  rest <- validateBody (int s ∷ bot) ts is
+  ok (i-binop op then rest)
 validateBody ss ts (UT.I32Eqz ∷ is) = err "TODO"
 validateBody ss ts (UT.I64Eqz ∷ is) = err "TODO"
 validateBody ss ts (UT.IRelOp x x₁ ∷ is) = err "TODO"
@@ -213,5 +225,3 @@ instantiateModule m = do
   functions <- validateFunctions μ functions
   let store = record { functions = functions }
   ok (μ ,Σ store)
-
-{-# COMPILE GHC instantiateModule as instantiateModule #-}
-- 
2.51.2