Analysis/Forward.agda

@@ -356,6 +356,8 @@ module WithProg (prog : Program) where
                     in
                         walkTrace ⟦joinForKey-s⟧ρ tr
 
+                postulate initialState-pred-∅ : incoming initialState ≡ []
+
                 joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
                 joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
 

Analysis/Sign.agda

@@ -1,8 +1,8 @@
 module Analysis.Sign where
 
-open import Data.Integer as Int using (ℤ; +_; -[1+_])
-open import Data.Nat as Nat using (ℕ; suc; zero)
-open import Data.Product using (Σ; proj₁; proj₂; _,_)
+open import Data.Integer using (ℤ; +_; -[1+_])
+open import Data.Nat using (ℕ; suc; zero)
+open import Data.Product using (Σ; proj₁; _,_)
 open import Data.Sum using (inj₁; inj₂)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Unit using (⊤; tt)
@@ -115,7 +115,7 @@ postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ
 ⟦_⟧ᵍ ⊥ᵍ _ = ⊥
 ⟦_⟧ᵍ ⊤ᵍ _ = ⊤
 ⟦_⟧ᵍ [ + ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ (+_ (suc n)))
-⟦_⟧ᵍ [ 0ˢ ]ᵍ v = v ≡ ↑ᶻ (+_ zero)
+⟦_⟧ᵍ [ 0ˢ ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ (+_ zero))
 ⟦_⟧ᵍ [ - ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ -[1+ n ])
 
 ⟦⟧ᵍ-respects-≈ᵍ : ∀ {s₁ s₂ : SignLattice} → s₁ ≈ᵍ s₂ → ⟦ s₁ ⟧ᵍ ⇒ ⟦ s₂ ⟧ᵍ
@@ -141,12 +141,12 @@ postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ
 s₁≢s₂⇒¬s₁∧s₂ : ∀ {s₁ s₂ : Sign} → ¬ s₁ ≡ s₂ → ∀ {v} → ¬ ((⟦ [ s₁ ]ᵍ ⟧ᵍ ∧ ⟦ [ s₂ ]ᵍ ⟧ᵍ) v)
 s₁≢s₂⇒¬s₁∧s₂ { + } { + } +≢+ _ = ⊥-elim (+≢+ refl)
 s₁≢s₂⇒¬s₁∧s₂ { + } { - } _ ((n , refl) , (m , ()))
-s₁≢s₂⇒¬s₁∧s₂ { + } { 0ˢ } _ ((n , refl) , ())
-s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { + } _ (refl , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { + } { 0ˢ } _ ((n , refl) , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { + } _ ((n , refl) , (m , ()))
 s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { 0ˢ } +≢+ _ = ⊥-elim (+≢+ refl)
-s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { - } _ (refl , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { - } _ ((n , refl) , (m , ()))
 s₁≢s₂⇒¬s₁∧s₂ { - } { + } _ ((n , refl) , (m , ()))
-s₁≢s₂⇒¬s₁∧s₂ { - } { 0ˢ } _ ((n , refl) , ())
+s₁≢s₂⇒¬s₁∧s₂ { - } { 0ˢ } _ ((n , refl) , (m , ()))
 s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl)
 
 ⟦⟧ᵍ-⊓ᵍ-∧ : ∀ {s₁ s₂ : SignLattice} → (⟦ s₁ ⟧ᵍ ∧ ⟦ s₂ ⟧ᵍ) ⇒ ⟦ s₁ ⊓ᵍ s₂ ⟧ᵍ
@@ -222,75 +222,7 @@ module WithProg (prog : Program) where
     eval-Mono (# 0) _ = ≈ᵍ-refl
     eval-Mono (# (suc n')) _ = ≈ᵍ-refl
 
-    module ForwardWithEval = ForwardWithProg.WithEvaluator eval eval-Mono
-    open ForwardWithEval using (result)
+    open ForwardWithProg.WithEvaluator eval eval-Mono using (result)
 
     -- For debugging purposes, print out the result.
     output = show result
-
-    module ForwardWithInterp = ForwardWithEval.WithInterpretation latticeInterpretationᵍ
-    open ForwardWithInterp using (⟦_⟧ᵛ; InterpretationValid)
-
-    -- This should have fewer cases -- the same number as the actual 'plus' above.
-    -- But agda only simplifies on first argument, apparently, so we are stuck
-    -- listing them all.
-    plus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᵍ (↑ᶻ z₁) → ⟦ g₂ ⟧ᵍ (↑ᶻ z₂) → ⟦ plus g₁ g₂ ⟧ᵍ (↑ᶻ (z₁ Int.+ z₂))
-    plus-valid {⊥ᵍ} {_} ⊥ _ = ⊥
-    plus-valid {[ + ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥
-    plus-valid {[ - ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥
-    plus-valid {[ 0ˢ ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥
-    plus-valid {⊤ᵍ} {⊥ᵍ} _ ⊥ = ⊥
-    plus-valid {⊤ᵍ} {[ + ]ᵍ} _ _ = tt
-    plus-valid {⊤ᵍ} {[ - ]ᵍ} _ _ = tt
-    plus-valid {⊤ᵍ} {[ 0ˢ ]ᵍ} _ _ = tt
-    plus-valid {⊤ᵍ} {⊤ᵍ} _ _ = tt
-    plus-valid {[ + ]ᵍ} {[ + ]ᵍ} (n₁ , refl) (n₂ , refl) = (_ , refl)
-    plus-valid {[ + ]ᵍ} {[ - ]ᵍ} _ _ = tt
-    plus-valid {[ + ]ᵍ} {[ 0ˢ ]ᵍ} (n₁ , refl) refl = (_ , refl)
-    plus-valid {[ + ]ᵍ} {⊤ᵍ} _ _ = tt
-    plus-valid {[ - ]ᵍ} {[ + ]ᵍ} _ _ = tt
-    plus-valid {[ - ]ᵍ} {[ - ]ᵍ} (n₁ , refl) (n₂ , refl) = (_ , refl)
-    plus-valid {[ - ]ᵍ} {[ 0ˢ ]ᵍ} (n₁ , refl) refl = (_ , refl)
-    plus-valid {[ - ]ᵍ} {⊤ᵍ} _ _ = tt
-    plus-valid {[ 0ˢ ]ᵍ} {[ + ]ᵍ} refl (n₂ , refl) = (_ , refl)
-    plus-valid {[ 0ˢ ]ᵍ} {[ - ]ᵍ} refl (n₂ , refl) = (_ , refl)
-    plus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl
-    plus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt
-
-    -- Same for this one. It should be easier, but Agda won't simplify.
-    minus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᵍ (↑ᶻ z₁) → ⟦ g₂ ⟧ᵍ (↑ᶻ z₂) → ⟦ minus g₁ g₂ ⟧ᵍ (↑ᶻ (z₁ Int.- z₂))
-    minus-valid {⊥ᵍ} {_} ⊥ _ = ⊥
-    minus-valid {[ + ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥
-    minus-valid {[ - ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥
-    minus-valid {[ 0ˢ ]ᵍ} {⊥ᵍ} _ ⊥ = ⊥
-    minus-valid {⊤ᵍ} {⊥ᵍ} _ ⊥ = ⊥
-    minus-valid {⊤ᵍ} {[ + ]ᵍ} _ _ = tt
-    minus-valid {⊤ᵍ} {[ - ]ᵍ} _ _ = tt
-    minus-valid {⊤ᵍ} {[ 0ˢ ]ᵍ} _ _ = tt
-    minus-valid {⊤ᵍ} {⊤ᵍ} _ _ = tt
-    minus-valid {[ + ]ᵍ} {[ + ]ᵍ} _ _ = tt
-    minus-valid {[ + ]ᵍ} {[ - ]ᵍ} (n₁ , refl) (n₂ , refl) = (_ , refl)
-    minus-valid {[ + ]ᵍ} {[ 0ˢ ]ᵍ} (n₁ , refl) refl = (_ , refl)
-    minus-valid {[ + ]ᵍ} {⊤ᵍ} _ _ = tt
-    minus-valid {[ - ]ᵍ} {[ + ]ᵍ} (n₁ , refl) (n₂ , refl) = (_ , refl)
-    minus-valid {[ - ]ᵍ} {[ - ]ᵍ} _ _ = tt
-    minus-valid {[ - ]ᵍ} {[ 0ˢ ]ᵍ} (n₁ , refl) refl = (_ , refl)
-    minus-valid {[ - ]ᵍ} {⊤ᵍ} _ _ = tt
-    minus-valid {[ 0ˢ ]ᵍ} {[ + ]ᵍ} refl (n₂ , refl) = (_ , refl)
-    minus-valid {[ 0ˢ ]ᵍ} {[ - ]ᵍ} refl (n₂ , refl) = (_ , refl)
-    minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl
-    minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt
-
-    eval-Valid : InterpretationValid
-    eval-Valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
-        plus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
-    eval-Valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
-        minus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
-    eval-Valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
-        with ∈k-decᵛ x (proj₁ (proj₁ vs))
-    ...   | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ
-    ...   | no x∉kvs = tt
-    eval-Valid (⇒ᵉ-ℕ ρ 0) _ = refl
-    eval-Valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
-
-    open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public

Language.agda

@@ -84,10 +84,6 @@ record Program : Set where
     incoming : State → List State
     incoming = predecessors graph
 
-    initialState-pred-∅ : incoming initialState ≡ []
-    initialState-pred-∅ =
-        wrap-preds-∅ (buildCfg rootStmt) initialState (RelAny.here refl)
-
     edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
                     s₁ ListMem.∈ (incoming s₂)
     edge⇒incoming = edge⇒predecessor graph

Language/Properties.agda

@@ -6,84 +6,23 @@ open import Language.Graphs
 open import Language.Traces
 
 open import Data.Fin as Fin using (suc; zero)
-open import Data.Fin.Properties as FinProp using (suc-injective)
 open import Data.List as List using (List; _∷_; [])
-open import Data.List.Properties using (filter-none)
 open import Data.List.Relation.Unary.Any using (here; there)
-open import Data.List.Relation.Unary.All using (All; []; _∷_; map; tabulate)
 open import Data.List.Membership.Propositional as ListMem using ()
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
-open import Data.Nat as Nat using ()
-open import Data.Product using (Σ; _,_; _×_; proj₂)
-open import Data.Product.Properties as ProdProp using ()
-open import Data.Sum using (inj₁; inj₂)
+open import Data.Product using (Σ; _,_; _×_)
 open import Data.Vec as Vec using (_∷_)
 open import Data.Vec.Properties using (lookup-++ˡ; ++-identityʳ; lookup-++ʳ)
 open import Function using (_∘_)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; cong)
-open import Relation.Nullary using (¬_)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
 
 open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct; concat-∈)
 
--- All of the below helpers are to reason about what edges aren't included
--- when combinings graphs. The currenty most important use for this is proving
--- that the entry node has no incoming edges.
---
--- -------------- Begin ugly code to make this work ----------------
-↑-≢ : ∀ {n m} (f₁ : Fin.Fin n) (f₂ : Fin.Fin m) → ¬ (f₁ Fin.↑ˡ m) ≡ (n Fin.↑ʳ f₂)
-↑-≢ zero f₂ ()
-↑-≢ (suc f₁') f₂ f₁≡f₂ = ↑-≢ f₁' f₂ (suc-injective f₁≡f₂)
+wrap-input : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.inputs (wrap g) ≡ idx ∷ [])
+wrap-input g = (_ , refl)
 
-idx→f∉↑ʳᵉ : ∀ {n m} (idx : Fin.Fin (n Nat.+ m)) (f : Fin.Fin n) (es₂ : List (Fin.Fin m × Fin.Fin m)) → ¬ (idx , f Fin.↑ˡ m) ListMem.∈ (n ↑ʳᵉ es₂)
-idx→f∉↑ʳᵉ idx f ((idx₁ , idx₂) ∷ es') (here idx,f≡idx₁,idx₂) = ↑-≢ f idx₂ (cong proj₂ idx,f≡idx₁,idx₂)
-idx→f∉↑ʳᵉ idx f (_ ∷ es₂') (there idx→f∈es₂') = idx→f∉↑ʳᵉ idx f es₂' idx→f∈es₂'
-
-idx→f∉pair : ∀ {n m} (idx idx' : Fin.Fin (n Nat.+ m)) (f : Fin.Fin n) (inputs₂ : List (Fin.Fin m)) → ¬ (idx , f Fin.↑ˡ m) ListMem.∈ (List.map (idx' ,_) (n ↑ʳⁱ inputs₂))
-idx→f∉pair idx idx' f [] ()
-idx→f∉pair idx idx' f (input ∷ inputs') (here idx,f≡idx',input) = ↑-≢ f input (cong proj₂ idx,f≡idx',input)
-idx→f∉pair idx idx' f (_ ∷ inputs₂') (there idx,f∈inputs₂') = idx→f∉pair idx idx' f inputs₂' idx,f∈inputs₂'
-
-idx→f∉cart : ∀ {n m} (idx : Fin.Fin (n Nat.+ m)) (f : Fin.Fin n) (outputs₁ : List (Fin.Fin n)) (inputs₂ : List (Fin.Fin m)) → ¬ (idx , f Fin.↑ˡ m) ListMem.∈ (List.cartesianProduct (outputs₁ ↑ˡⁱ m) (n ↑ʳⁱ inputs₂))
-idx→f∉cart idx f [] inputs₂ ()
-idx→f∉cart {n} {m} idx f (output ∷ outputs₁') inputs₂ idx,f∈pair++cart
-    with ListMemProp.∈-++⁻ (List.map (output Fin.↑ˡ m ,_) (n ↑ʳⁱ inputs₂)) idx,f∈pair++cart
-...   | inj₁ idx,f∈pair = idx→f∉pair idx (output Fin.↑ˡ m) f inputs₂ idx,f∈pair
-...   | inj₂ idx,f∈cart = idx→f∉cart idx f outputs₁' inputs₂ idx,f∈cart
-
-help : let g₁ = singleton [] in
-       ∀ (g₂ : Graph) (idx₁ : Graph.Index g₁) (idx : Graph.Index (g₁ ↦ g₂)) →
-       ¬ (idx , idx₁ Fin.↑ˡ Graph.size g₂) ListMem.∈ ((Graph.size g₁ ↑ʳᵉ Graph.edges g₂) List.++
-                                                      (List.cartesianProduct (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
-                                                                             (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)))
-help g₂ idx₁ idx idx,idx₁∈g
-    with ListMemProp.∈-++⁻ (Graph.size (singleton []) ↑ʳᵉ Graph.edges g₂) idx,idx₁∈g
-...   | inj₁ idx,idx₁∈edges₂ = idx→f∉↑ʳᵉ idx idx₁ (Graph.edges g₂) idx,idx₁∈edges₂
-...   | inj₂ idx,idx₁∈cart = idx→f∉cart idx idx₁ (Graph.outputs (singleton [])) (Graph.inputs g₂) idx,idx₁∈cart
-
-helpAll : let g₁ = singleton [] in
-       ∀ (g₂ : Graph) (idx₁ : Graph.Index g₁) →
-       All (λ idx → ¬ (idx , idx₁ Fin.↑ˡ Graph.size g₂) ListMem.∈ ((Graph.size g₁ ↑ʳᵉ Graph.edges g₂) List.++
-                                                                   (List.cartesianProduct (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
-                                                                                          (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)))) (indices (g₁ ↦ g₂))
-helpAll g₂ idx₁ = tabulate (λ {idx} _ → help g₂ idx₁ idx)
-
-module _ (g : Graph) where
-    wrap-preds-∅ : (idx : Graph.Index (wrap g)) →
-                   idx ListMem.∈ Graph.inputs (wrap g) → predecessors (wrap g) idx ≡ []
-    wrap-preds-∅ zero (here refl) =
-        filter-none (λ idx' → (idx' , zero) ∈?
-                              (Graph.edges (wrap g)))
-                    (helpAll (g ↦ singleton []) zero)
-        where open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size (wrap g)}) (FinProp._≟_ {Graph.size (wrap g)})) using (_∈?_)
--- -------------- End ugly code to make this work ----------------
-
-
-module _ (g : Graph) where
-    wrap-input : Σ (Graph.Index (wrap g)) (λ idx → Graph.inputs (wrap g) ≡ idx ∷ [])
-    wrap-input = (_ , refl)
-
-    wrap-output : Σ (Graph.Index (wrap g)) (λ idx → Graph.outputs (wrap g) ≡ idx ∷ [])
-    wrap-output = (_ , refl)
+wrap-output : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.outputs (wrap g) ≡ idx ∷ [])
+wrap-output g = (_ , refl)
 
 Trace-∙ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
            Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →

Main.agda

@@ -37,6 +37,6 @@ testProgram = record
     { rootStmt = testCode
     }
 
-open WithProg testProgram using (output; analyze-correct)
+open WithProg testProgram using (output)
 
 main = run {0ℓ} (putStrLn output)