Rename 'a' to 'b' in fixedpoint algorithm proof

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Analysis/Forward.agda

@@ -0,0 +1,366 @@
+open import Language hiding (_[_])
+open import Lattice
+
+module Analysis.Forward
+    {L : Set} {h}
+    {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
+    (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
+    (≈ˡ-dec : IsDecidable _≈ˡ_) where
+
+open import Data.Empty using (⊥-elim)
+open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Data.Nat using (suc)
+open import Data.Product using (_×_; proj₁; proj₂; _,_)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith)
+open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
+open import Data.List.Relation.Unary.Any as Any using ()
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Unit using (⊤)
+open import Function using (_∘_; flip)
+import Chain
+
+open import Utils using (Pairwise; _⇒_; _∨_)
+import Lattice.FiniteValueMap
+
+open IsFiniteHeightLattice isFiniteHeightLatticeˡ
+    using ()
+    renaming
+        ( isLattice to isLatticeˡ
+        ; fixedHeight to fixedHeightˡ
+        ; _≼_ to _≼ˡ_
+        ; ≈-sym to ≈ˡ-sym
+        )
+
+module WithProg (prog : Program) where
+    open Program prog
+
+    -- The variable -> abstract value (e.g. sign) map is a finite value-map
+    -- with keys strings. Use a bundle to avoid explicitly specifying operators.
+    module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars
+    open VariableValuesFiniteMap
+        using ()
+        renaming
+            ( FiniteMap to VariableValues
+            ; isLattice to isLatticeᵛ
+            ; _≈_ to _≈ᵛ_
+            ; _⊔_ to _⊔ᵛ_
+            ; _≼_ to _≼ᵛ_
+            ; ≈₂-dec⇒≈-dec to ≈ˡ-dec⇒≈ᵛ-dec
+            ; _∈_ to _∈ᵛ_
+            ; _∈k_ to _∈kᵛ_
+            ; _updating_via_ to _updatingᵛ_via_
+            ; locate to locateᵛ
+            ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
+            ; ∈k-dec to ∈k-decᵛ
+            ; all-equal-keys to all-equal-keysᵛ
+            )
+        public
+    open IsLattice isLatticeᵛ
+        using ()
+        renaming
+            ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
+            ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
+            ; ⊔-idemp to ⊔ᵛ-idemp
+            )
+    open Lattice.FiniteValueMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ
+        using ()
+        renaming
+            ( Provenance-union to Provenance-unionᵐ
+            )
+    open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ
+        using ()
+        renaming
+            ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
+            ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
+            )
+
+    ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
+    joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
+    fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
+    ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
+
+    -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
+    module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
+    open StateVariablesFiniteMap
+        using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
+        renaming
+            ( FiniteMap to StateVariables
+            ; isLattice to isLatticeᵐ
+            ; _≈_ to _≈ᵐ_
+            ; _∈_ to _∈ᵐ_
+            ; _∈k_ to _∈kᵐ_
+            ; locate to locateᵐ
+            ; _≼_ to _≼ᵐ_
+            ; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec
+            ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
+            )
+        public
+    open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
+        using ()
+        renaming
+            ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
+            )
+    open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
+        using ()
+        renaming
+            ( ≈-sym to ≈ᵐ-sym
+            )
+
+    ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
+    fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
+
+    -- We now have our (state -> (variables -> value)) map.
+    -- Define a couple of helpers to retrieve values from it. Specifically,
+    -- since the State type is as specific as possible, it's always possible to
+    -- retrieve the variable values at each state.
+
+    states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
+    states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
+
+    variablesAt : State → StateVariables → VariableValues
+    variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
+
+    variablesAt-∈ : ∀ (s : State) (sv : StateVariables) → (s , variablesAt s sv) ∈ᵐ sv
+    variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv))
+
+    variablesAt-≈ : ∀ s sv₁ sv₂ → sv₁ ≈ᵐ sv₂ → variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
+    variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ =
+        m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂
+                               (states-in-Map s sv₁) (states-in-Map s sv₂)
+
+    -- build up the 'join' function, which follows from Exercise 4.26's
+    --
+    --    L₁ → (A → L₂)
+    --
+    -- Construction, with L₁ = (A → L₂), and f = id
+
+    joinForKey : State → StateVariables → VariableValues
+    joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
+
+    -- The per-key join is made up of map key accesses (which are monotonic)
+    -- and folds using the join operation (also monotonic)
+
+    joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
+    joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
+        foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
+                   (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
+                   (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
+
+    -- The name f' comes from the formulation of Exercise 4.26.
+    open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
+        renaming
+            ( f' to joinAll
+            ; f'-Monotonic to joinAll-Mono
+            ; f'-k∈ks-≡ to joinAll-k∈ks-≡
+            )
+
+    variablesAt-joinAll : ∀ (s : State) (sv : StateVariables) →
+                          variablesAt s (joinAll sv) ≡ joinForKey s sv
+    variablesAt-joinAll s sv
+        with (vs , s,vs∈usv) ← locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) =
+        joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
+
+    -- With 'join' in hand, we need to perform abstract evaluation.
+    module WithEvaluator (eval : Expr → VariableValues → L)
+                         (eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where
+
+        -- For a particular evaluation function, we need to perform an evaluation
+        -- for an assignment, and update the corresponding key. Use Exercise 4.26's
+        -- generalized update to set the single key's value.
+
+        private module _ (k : String) (e : Expr) where
+            open VariableValuesFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → eval-Mono e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
+                renaming
+                    ( f' to updateVariablesFromExpression
+                    ; f'-Monotonic to updateVariablesFromExpression-Mono
+                    ; f'-k∈ks-≡ to updateVariablesFromExpression-k∈ks-≡
+                    ; f'-k∉ks-backward to updateVariablesFromExpression-k∉ks-backward
+                    )
+                public
+
+        -- The per-state update function makes use of the single-key setter,
+        -- updateVariablesFromExpression, for the case where the statement
+        -- is an assignment.
+        --
+        -- This per-state function adjusts the variables in that state,
+        -- also monotonically; we derive the for-each-state update from
+        -- the Exercise 4.26 again.
+
+        updateVariablesFromStmt : BasicStmt → VariableValues → VariableValues
+        updateVariablesFromStmt (k ← e) vs = updateVariablesFromExpression k e vs
+        updateVariablesFromStmt noop vs = vs
+
+        updateVariablesFromStmt-Monoʳ : ∀ (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (updateVariablesFromStmt bs)
+        updateVariablesFromStmt-Monoʳ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
+        updateVariablesFromStmt-Monoʳ noop vs₁≼vs₂ = vs₁≼vs₂
+
+        updateVariablesForState : State → StateVariables → VariableValues
+        updateVariablesForState s sv =
+            foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s)
+
+        updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
+        updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =
+            let
+                bss = code s
+                (vs₁ , s,vs₁∈sv₁) = locateᵐ {s} {sv₁} (states-in-Map s sv₁)
+                (vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂)
+                vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂
+            in
+                foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
+                            (flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ
+                            vs₁≼vs₂
+
+        open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
+            renaming
+                ( f' to updateAll
+                ; f'-Monotonic to updateAll-Mono
+                ; f'-k∈ks-≡ to updateAll-k∈ks-≡
+                )
+
+        -- Finally, the whole analysis consists of getting the 'join'
+        -- of all incoming states, then applying the per-state evaluation
+        -- function. This is just a composition, and is trivially monotonic.
+
+        analyze : StateVariables → StateVariables
+        analyze = updateAll ∘ joinAll
+
+        analyze-Mono : Monotonic _≼ᵐ_ _≼ᵐ_ analyze
+        analyze-Mono {sv₁} {sv₂} sv₁≼sv₂ =
+            updateAll-Mono {joinAll sv₁} {joinAll sv₂}
+                           (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
+
+        -- The fixed point of the 'analyze' function is our final goal.
+        open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
+            using ()
+            renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
+            public
+
+        variablesAt-updateAll : ∀ (s : State) (sv : StateVariables) →
+                                variablesAt s (updateAll sv) ≡ updateVariablesForState s sv
+        variablesAt-updateAll s sv
+            with (vs , s,vs∈usv) ← locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) =
+            updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
+
+        module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
+            open LatticeInterpretation latticeInterpretationˡ
+                using ()
+                renaming
+                    ( ⟦_⟧ to ⟦_⟧ˡ
+                    ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
+                    ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
+                    )
+
+            ⟦_⟧ᵛ : VariableValues → Env → Set
+            ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
+
+            ⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ []
+            ⟦⊥ᵛ⟧ᵛ∅ _ ()
+
+            ⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ
+            ⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
+                            (m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ =
+                let
+                    (l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂
+                    ⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ
+                in
+                    ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
+
+            ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ
+            ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
+                with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂)))
+                     ← Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂
+                with ⟦vs₁⟧ρ∨⟦vs₂⟧ρ
+            ...   | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ))
+            ...   | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))
+
+            ⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} →
+                        ⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
+            ⟦⟧ᵛ-foldr {vs} {vs ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) =
+                ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₁ ⟦vs⟧ρ)
+            ⟦⟧ᵛ-foldr {vs} {vs' ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.there vs∈vss') =
+                ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
+                         (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
+
+            InterpretationValid : Set
+            InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
+
+            module WithValidity (interpretationValidˡ : InterpretationValid) where
+
+                updateVariablesFromStmt-matches : ∀ {bs vs ρ₁ ρ₂} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
+                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁
+                updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ₁ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
+                    with k ≟ˢ k' | k',v'∈ρ₂
+                ...   | yes refl | here _ v _
+                        rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
+                        interpretationValidˡ ρ,e⇒v ⟦vs⟧ρ₁
+                ...   | yes k≡k' | there _ _ _ _ _ k'≢k _ = ⊥-elim (k'≢k (sym k≡k'))
+                ...   | no k≢k' | here _ _ _ = ⊥-elim (k≢k' refl)
+                ...   | no k≢k'  | there _ _ _ _ _ _ k',v'∈ρ₁ =
+                        let
+                            k'∉[k] = (λ { (Any.here refl) → k≢k' refl })
+                            k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
+                        in
+                            ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁
+
+                updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
+                updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
+                updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
+                    updateVariablesFromStmt-fold-matches
+                        {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
+                        (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
+
+                updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
+                updateVariablesForState-matches =
+                    updateVariablesFromStmt-fold-matches
+
+                updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
+                updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
+                    rewrite variablesAt-updateAll s sv =
+                    updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
+
+
+                stepTrace : ∀ {s₁ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s₁ result ⟧ᵛ ρ₂
+                stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
+                        let
+                            -- I'd use rewrite, but Agda gets a memory overflow (?!).
+                            ⟦joinAll-result⟧ρ₁ =
+                                subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
+                                      (sym (variablesAt-joinAll s₁ result))
+                                      ⟦joinForKey-s₁⟧ρ₁
+                            ⟦analyze-result⟧ρ₂ =
+                                updateAll-matches {sv = joinAll result}
+                                                  ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
+                            analyze-result≈result =
+                                ≈ᵐ-sym {result} {updateAll (joinAll result)}
+                                       result≈analyze-result
+                            analyze-s₁≈s₁ =
+                                variablesAt-≈ s₁ (updateAll (joinAll result))
+                                                 result (analyze-result≈result)
+                        in
+                            ⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂
+
+                walkTrace : ∀ {s₁ s₂ ρ₁ ρ₂} → ⟦ joinForKey s₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
+                walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
+                    stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
+                walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
+                    let
+                        ⟦result-s₁⟧ρ =
+                            stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
+                        s₁∈incomingStates =
+                            []-∈ result (edge⇒incoming s₁→s₂)
+                                        (variablesAt-∈ s₁ result)
+                        ⟦joinForKey-s⟧ρ =
+                            ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
+                    in
+                        walkTrace ⟦joinForKey-s⟧ρ tr
+
+                joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
+                joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
+
+                ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
+                ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
+
+                analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
+                analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)

Analysis/Sign.agda

@@ -1,20 +1,20 @@
 module Analysis.Sign where
 
-open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Data.Integer as Int using (ℤ; +_; -[1+_])
-open import Data.Nat using (suc)
+open import Data.Nat as Nat using (ℕ; suc; zero)
-open import Data.Product using (_×_; proj₁; _,_)
+open import Data.Product using (Σ; proj₁; proj₂; _,_)
-open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Unit using (⊤; tt)
 open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
-open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary using (¬_; yes; no)
-open import Data.Unit using (⊤)
-open import Function using (_∘_)
 
 open import Language
 open import Lattice
-open import Utils using (Pairwise)
 open import Showable using (Showable; show)
-import Lattice.FiniteValueMap
+open import Utils using (_⇒_; _∧_; _∨_)
+import Analysis.Forward
 
 data Sign : Set where
     + : Sign
@@ -61,11 +61,11 @@ open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = s
 -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice.
 open AB.Plain 0ˢ using ()
     renaming
-        ( finiteHeightLattice to finiteHeightLatticeᵍ
+        ( isLattice to isLatticeᵍ
-        ; isLattice to isLatticeᵍ
         ; fixedHeight to fixedHeightᵍ
         ; _≼_ to _≼ᵍ_
         ; _⊔_ to _⊔ᵍ_
+        ; _⊓_ to _⊓ᵍ_
         )
 
 open IsLattice isLatticeᵍ using ()
@@ -111,199 +111,186 @@ minus [ 0ˢ ]ᵍ [ 0ˢ ]ᵍ = [ 0ˢ ]ᵍ
 postulate minus-Monoˡ : ∀ (s₂ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (λ s₁ → minus s₁ s₂)
 postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ_ (minus s₁)
 
+⟦_⟧ᵍ : SignLattice → Value → Set
+⟦_⟧ᵍ ⊥ᵍ _ = ⊥
+⟦_⟧ᵍ ⊤ᵍ _ = ⊤
+⟦_⟧ᵍ [ + ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ (+_ (suc n)))
+⟦_⟧ᵍ [ 0ˢ ]ᵍ v = v ≡ ↑ᶻ (+_ zero)
+⟦_⟧ᵍ [ - ]ᵍ v = Σ ℕ (λ n → v ≡ ↑ᶻ -[1+ n ])
+
+⟦⟧ᵍ-respects-≈ᵍ : ∀ {s₁ s₂ : SignLattice} → s₁ ≈ᵍ s₂ → ⟦ s₁ ⟧ᵍ ⇒ ⟦ s₂ ⟧ᵍ
+⟦⟧ᵍ-respects-≈ᵍ ≈ᵍ-⊥ᵍ-⊥ᵍ v bot = bot
+⟦⟧ᵍ-respects-≈ᵍ ≈ᵍ-⊤ᵍ-⊤ᵍ v top = top
+⟦⟧ᵍ-respects-≈ᵍ (≈ᵍ-lift { + } { + } refl) v proof = proof
+⟦⟧ᵍ-respects-≈ᵍ (≈ᵍ-lift { - } { - } refl) v proof = proof
+⟦⟧ᵍ-respects-≈ᵍ (≈ᵍ-lift { 0ˢ } { 0ˢ } refl) v proof = proof
+
+⟦⟧ᵍ-⊔ᵍ-∨ : ∀ {s₁ s₂ : SignLattice} → (⟦ s₁ ⟧ᵍ ∨ ⟦ s₂ ⟧ᵍ) ⇒ ⟦ s₁ ⊔ᵍ s₂ ⟧ᵍ
+⟦⟧ᵍ-⊔ᵍ-∨ {⊥ᵍ} x (inj₂ px₂) = px₂
+⟦⟧ᵍ-⊔ᵍ-∨ {⊤ᵍ} x _ = tt
+⟦⟧ᵍ-⊔ᵍ-∨ {[ s₁ ]ᵍ} {[ s₂ ]ᵍ} x px
+    with s₁ ≟ᵍ s₂
+...   | no _ = tt
+...   | yes refl
+        with px
+...       | inj₁ px₁ = px₁
+...       | inj₂ px₂ = px₂
+⟦⟧ᵍ-⊔ᵍ-∨ {[ s₁ ]ᵍ} {⊥ᵍ} x (inj₁ px₁) = px₁
+⟦⟧ᵍ-⊔ᵍ-∨ {[ s₁ ]ᵍ} {⊤ᵍ} x _ = tt
+
+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ˢ } { 0ˢ } +≢+ _ = ⊥-elim (+≢+ refl)
+s₁≢s₂⇒¬s₁∧s₂ { 0ˢ } { - } _ (refl , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { - } { + } _ ((n , refl) , (m , ()))
+s₁≢s₂⇒¬s₁∧s₂ { - } { 0ˢ } _ ((n , refl) , ())
+s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl)
+
+⟦⟧ᵍ-⊓ᵍ-∧ : ∀ {s₁ s₂ : SignLattice} → (⟦ s₁ ⟧ᵍ ∧ ⟦ s₂ ⟧ᵍ) ⇒ ⟦ s₁ ⊓ᵍ s₂ ⟧ᵍ
+⟦⟧ᵍ-⊓ᵍ-∧ {⊥ᵍ} x (bot , _) = bot
+⟦⟧ᵍ-⊓ᵍ-∧ {⊤ᵍ} x (_ , px₂) = px₂
+⟦⟧ᵍ-⊓ᵍ-∧ {[ s₁ ]ᵍ} {[ s₂ ]ᵍ} x (px₁ , px₂)
+    with s₁ ≟ᵍ s₂
+...   | no s₁≢s₂ = s₁≢s₂⇒¬s₁∧s₂ s₁≢s₂ (px₁ , px₂)
+...   | yes refl = px₁
+⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot
+⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁
+
+latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
+latticeInterpretationᵍ = record
+    { ⟦_⟧ = ⟦_⟧ᵍ
+    ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ
+    ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨
+    ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧
+    }
+
 module WithProg (prog : Program) where
     open Program prog
 
-    -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators.
+    module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog
-    module VariableSignsFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars
+    open ForwardWithProg
-    open VariableSignsFiniteMap
-        using ()
-        renaming
-            ( FiniteMap to VariableSigns
-            ; isLattice to isLatticeᵛ
-            ; _≈_ to _≈ᵛ_
-            ; _⊔_ to _⊔ᵛ_
-            ; _≼_ to _≼ᵛ_
-            ; ≈₂-dec⇒≈-dec to ≈ᵍ-dec⇒≈ᵛ-dec
-            ; _∈_ to _∈ᵛ_
-            ; _∈k_ to _∈kᵛ_
-            ; _updating_via_ to _updatingᵛ_via_
-            ; locate to locateᵛ
-            ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
-            )
-    open IsLattice isLatticeᵛ
-        using ()
-        renaming
-            ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
-            ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
-            ; ⊔-idemp to ⊔ᵛ-idemp
-            )
-    open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeᵍ vars-Unique ≈ᵍ-dec _ fixedHeightᵍ
-        using ()
-        renaming
-            ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
-            )
 
-    ≈ᵛ-dec = ≈ᵍ-dec⇒≈ᵛ-dec ≈ᵍ-dec
+    eval : ∀ (e : Expr) → VariableValues → SignLattice
-    joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
+    eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
-    fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
+    eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs)
-    ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
+    eval (` k) vs
+        with ∈k-decᵛ k (proj₁ (proj₁ vs))
+    ...   | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs)
+    ...   | no _ = ⊤ᵍ
+    eval (# 0) _ = [ 0ˢ ]ᵍ
+    eval (# (suc n')) _ = [ + ]ᵍ
 
-    -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in.
+    eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e)
-    module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
+    eval-Mono (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ =
-    open StateVariablesFiniteMap
-        using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
-        renaming
-            ( FiniteMap to StateVariables
-            ; isLattice to isLatticeᵐ
-            ; _∈k_ to _∈kᵐ_
-            ; locate to locateᵐ
-            ; _≼_ to _≼ᵐ_
-            ; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec
-            ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
-            )
-    open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
-        using ()
-        renaming
-            ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
-            )
-
-    ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
-    fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
-
-    -- build up the 'join' function, which follows from Exercise 4.26's
-    --
-    --    L₁ → (A → L₂)
-    --
-    -- Construction, with L₁ = (A → L₂), and f = id
-
-    joinForKey : State → StateVariables → VariableSigns
-    joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
-
-    -- The per-key join is made up of map key accesses (which are monotonic)
-    -- and folds using the join operation (also monotonic)
-
-    joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
-    joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
-        foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
-                   (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
-                   (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
-
-    -- The name f' comes from the formulation of Exercise 4.26.
-
-    open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
-        renaming
-            ( f' to joinAll
-            ; f'-Monotonic to joinAll-Mono
-            )
-
-    -- With 'join' in hand, we need to perform abstract evaluation.
-
-    vars-in-Map : ∀ (k : String) (vs : VariableSigns) →
-                  k ∈ˡ vars → k ∈kᵛ vs
-    vars-in-Map k vs@(m , kvs≡vars) k∈vars rewrite kvs≡vars = k∈vars
-
-    states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv
-    states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
-
-    eval : ∀ (e : Expr) → (∀ k → k ∈ᵉ e → k ∈ˡ vars) → VariableSigns → SignLattice
-    eval (e₁ + e₂) k∈e⇒k∈vars vs =
-        plus (eval e₁ (λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁)) vs)
-             (eval e₂ (λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂)) vs)
-    eval (e₁ - e₂) k∈e⇒k∈vars vs =
-        minus (eval e₁ (λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁)) vs)
-              (eval e₂ (λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂)) vs)
-    eval (` k) k∈e⇒k∈vars vs = proj₁ (locateᵛ {k} {vs} (vars-in-Map k vs (k∈e⇒k∈vars k here)))
-    eval (# 0) _ _ = [ 0ˢ ]ᵍ
-    eval (# (suc n')) _ _ = [ + ]ᵍ
-
-    eval-Mono : ∀ (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e k∈e⇒k∈vars)
-    eval-Mono (e₁ + e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
         let
             -- TODO: can this be done with less boilerplate?
-            k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁺₁ k∈e₁)
+            g₁vs₁ = eval e₁ vs₁
-            k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁺₂ k∈e₂)
+            g₂vs₁ = eval e₂ vs₁
-            g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁
+            g₁vs₂ = eval e₁ vs₂
-            g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁
+            g₂vs₂ = eval e₂ vs₂
-            g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂
-            g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂
         in
             ≼ᵍ-trans
                 {plus g₁vs₁ g₂vs₁} {plus g₁vs₂ g₂vs₁} {plus g₁vs₂ g₂vs₂}
-                (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ k∈e₁⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+                (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+                (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂))
-    eval-Mono (e₁ - e₂) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
+    eval-Mono (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ =
         let
             -- TODO: here too -- can this be done with less boilerplate?
-            k∈e₁⇒k∈vars = λ k k∈e₁ → k∈e⇒k∈vars k (in⁻₁ k∈e₁)
+            g₁vs₁ = eval e₁ vs₁
-            k∈e₂⇒k∈vars = λ k k∈e₂ → k∈e⇒k∈vars k (in⁻₂ k∈e₂)
+            g₂vs₁ = eval e₂ vs₁
-            g₁vs₁ = eval e₁ k∈e₁⇒k∈vars vs₁
+            g₁vs₂ = eval e₁ vs₂
-            g₂vs₁ = eval e₂ k∈e₂⇒k∈vars vs₁
+            g₂vs₂ = eval e₂ vs₂
-            g₁vs₂ = eval e₁ k∈e₁⇒k∈vars vs₂
-            g₂vs₂ = eval e₂ k∈e₂⇒k∈vars vs₂
         in
             ≼ᵍ-trans
                 {minus g₁vs₁ g₂vs₁} {minus g₁vs₂ g₂vs₁} {minus g₁vs₂ g₂vs₂}
-                (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ k∈e₁⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+                (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ {vs₁} {vs₂} vs₁≼vs₂))
-                (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ k∈e₂⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂))
+                (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂))
-    eval-Mono (` k) k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂ =
+    eval-Mono (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂
-        let
+        with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂
-            (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} (vars-in-Map k vs₁ (k∈e⇒k∈vars k here))
+    ...   | yes k∈kvs₁ | yes k∈kvs₂ =
-            (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} (vars-in-Map k vs₂ (k∈e⇒k∈vars k here))
-        in
-            m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
-    eval-Mono (# 0) _ _ = ≈ᵍ-refl
-    eval-Mono (# (suc n')) _ _ = ≈ᵍ-refl
-
-    private module _ (k : String) (e : Expr) (k∈e⇒k∈vars : ∀ k → k ∈ᵉ e → k ∈ˡ vars) where
-        open VariableSignsFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → eval e k∈e⇒k∈vars) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → eval-Mono e k∈e⇒k∈vars {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
-            renaming
-                ( f' to updateVariablesFromExpression
-                ; f'-Monotonic to updateVariablesFromExpression-Mono
-                )
-            public
-
-    updateVariablesForState : State → StateVariables → VariableSigns
-    updateVariablesForState s sv
-        -- More weirdness here. Apparently, capturing the with-equality proof
-        -- using 'in p' makes code that reasons about this function (below)
-        -- throw ill-typed with-abstraction errors. Instead, make use of the
-        -- fact that later with-clauses are generalized over earlier ones to
-        -- construct a specialization of vars-complete for (code s).
-        with code s | (λ k → vars-complete {k} s)
-    ...   | k ← e | k∈codes⇒k∈vars =
             let
-                (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv)
+                (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} k∈kvs₁
+                (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} k∈kvs₂
             in
-                updateVariablesFromExpression k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) vs
+                m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂
+    ...   | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁))
+    ...   | no k∉kvs₁ | yes k∈kvs₂ = ⊥-elim (k∉kvs₁ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₂ vs₁) k∈kvs₂))
+    ...   | no k∉kvs₁ | no k∉kvs₂ = IsLattice.≈-refl isLatticeᵍ
+    eval-Mono (# 0) _ = ≈ᵍ-refl
+    eval-Mono (# (suc n')) _ = ≈ᵍ-refl
 
-    updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
+    module ForwardWithEval = ForwardWithProg.WithEvaluator eval eval-Mono
-    updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂
+    open ForwardWithEval using (result)
-        with code s | (λ k → vars-complete {k} s)
-    ...   | k ← e | k∈codes⇒k∈vars =
-            let
-                (vs₁ , s,vs₁∈sv₁) = locateᵐ {s} {sv₁} (states-in-Map s sv₁)
-                (vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂)
-                vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂
-            in
-                updateVariablesFromExpression-Mono k e (λ k k∈e → k∈codes⇒k∈vars k (in←₂ k∈e)) {vs₁} {vs₂} vs₁≼vs₂
 
-    open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
+    -- For debugging purposes, print out the result.
-        renaming
+    output = show result
-            ( f' to updateAll
-            ; f'-Monotonic to updateAll-Mono
-            )
 
-    analyze : StateVariables → StateVariables
+    module ForwardWithInterp = ForwardWithEval.WithInterpretation latticeInterpretationᵍ
-    analyze = updateAll ∘ joinAll
+    open ForwardWithInterp using (⟦_⟧ᵛ; InterpretationValid)
 
-    analyze-Mono : Monotonic _≼ᵐ_ _≼ᵐ_ analyze
+    -- This should have fewer cases -- the same number as the actual 'plus' above.
-    analyze-Mono {sv₁} {sv₂} sv₁≼sv₂ = updateAll-Mono {joinAll sv₁} {joinAll sv₂} (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
+    -- 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
 
-    open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
+    -- Same for this one. It should be easier, but Agda won't simplify.
-        using ()
+    minus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᵍ (↑ᶻ z₁) → ⟦ g₂ ⟧ᵍ (↑ᶻ z₂) → ⟦ minus g₁ g₂ ⟧ᵍ (↑ᶻ (z₁ Int.- z₂))
-        renaming (aᶠ to signs)
+    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)
 
-    -- Debugging code: print the resulting map.
+    open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public
-    output = show signs

Chain.agda

@@ -10,7 +10,7 @@ open import Data.Nat using (ℕ; suc; _+_; _≤_)
 open import Data.Nat.Properties using (+-comm; m+1+n≰m)
 open import Data.Product using (_×_; Σ; _,_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
-open import Data.Empty using (⊥)
+open import Data.Empty as Empty using ()
 
 open IsEquivalence ≈-equiv
 
@@ -38,11 +38,16 @@ module _  where
     Bounded : ℕ → Set a
     Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound
 
-    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → ⊥
+    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → Empty.⊥
     Bounded-suc-n {a₁} {a₂} {n} bounded c = (m+1+n≰m n n+1≤n)
         where
             n+1≤n : n + 1 ≤ n
             n+1≤n rewrite (+-comm n 1) = bounded c
 
-    Height : ℕ → Set a
+    record Height (height : ℕ) : Set a where
-    Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)
+        field
+            ⊥ : A
+            ⊤ : A
+
+            longestChain : Chain ⊥ ⊤ height
+            bounded : Bounded height

Fixedpoint.agda

@@ -23,15 +23,21 @@ import Chain
 module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
 
 private
-    ⊥ᴬ : A
+    open ChainA.Height fixedHeight
-    ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
+        using ()
+        renaming
+            ( ⊥ to ⊥ᴬ
+            ; longestChain to longestChainᴬ
+            ; bounded to boundedᴬ
+            )
+
 
     ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
     ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
     ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
     ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
     ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
-    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
+    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
                     where
                         ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                         ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
@@ -45,7 +51,7 @@ private
     -- out, we have exceeded h steps, which shouldn't be possible.
 
     doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a)
-    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
+    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
     doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
         with ≈-dec a₂ (f a₂)
     ...   | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
@@ -67,15 +73,15 @@ aᶠ≈faᶠ : aᶠ ≈ f aᶠ
 aᶠ≈faᶠ = proj₂ fix
 
 private
-    stepPreservesLess : ∀ (g hᶜ : ℕ) (a₁ a₂ a : A) (a≈fa : a ≈ f a) (a₂≼a : a₂ ≼ a)
+    stepPreservesLess : ∀ (g hᶜ : ℕ) (a₁ a₂ b : A) (b≈fb : b ≈ f b) (a₂≼a : a₂ ≼ b)
                      (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h)
                      (a₂≼fa₂ : a₂ ≼ f a₂) →
-                     proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a
+                     proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ b
-    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
+    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
-    stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
+    stepPreservesLess (suc g') hᶜ a₁ a₂ b b≈fb a₂≼b c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
         with ≈-dec a₂ (f a₂)
-    ...   | yes _ = a₂≼a
+    ...   | yes _ = a₂≼b
-    ...   | no  _ = stepPreservesLess g' _ _ _ a a≈fa (≼-cong ≈-refl (≈-sym a≈fa) (Monotonicᶠ a₂≼a)) _ _ _
+    ...   | no  _ = stepPreservesLess g' _ _ _ b b≈fb (≼-cong ≈-refl (≈-sym b≈fb) (Monotonicᶠ a₂≼b)) _ _ _
 
 aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a
 aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))

Isomorphism.agda

@@ -38,8 +38,9 @@ module TransportFiniteHeight
     open IsEquivalence ≈₁-equiv using () renaming (≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
     open IsEquivalence ≈₂-equiv using () renaming (≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans)
 
-    open import Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
+    import Chain
-    open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
+    open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
+    open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
 
     private
         f-Injective : Injective _≈₁_ _≈₂_ f
@@ -65,10 +66,17 @@ module TransportFiniteHeight
     isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
     isFiniteHeightLattice =
         let
-            (((a₁ , a₂) , c) , bounded₁) = IsFiniteHeightLattice.fixedHeight fhlA
+            open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
+                using ()
+                renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
         in record
             { isLattice = lB
-            ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
+            ; fixedHeight = record
+                { ⊥ = f ⊥₁
+                ; ⊤ = f ⊤₁
+                ; longestChain = portChain₁ c
+                ; bounded = λ c' → bounded₁ (portChain₂ c')
+                }
             }
 
     finiteHeightLattice : FiniteHeightLattice B

Language.agda

@@ -1,175 +1,56 @@
 module Language where
 
-open import Data.Nat using (ℕ; suc; pred)
+open import Language.Base public
-open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Language.Semantics public
-open import Data.Product using (Σ; _,_; proj₁; proj₂)
+open import Language.Traces public
-open import Data.Vec using (Vec; foldr; lookup; _∷_)
+open import Language.Graphs public
-open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ)
+open import Language.Properties public
-open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
+
-open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.Fin using (Fin; suc; zero)
+open import Data.Fin.Properties as FinProp using (suc-injective)
+open import Data.List as List using (List; []; _∷_)
+open import Data.List.Membership.Propositional as ListMem using ()
+open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺)
 open import Data.List.Relation.Unary.Any as RelAny using ()
-open import Data.Fin using (Fin; suc; zero; fromℕ; inject₁) renaming (_≟_ to _≟ᶠ_)
+open import Data.Nat using (ℕ; suc)
-open import Data.Fin.Properties using (suc-injective)
+open import Data.Product using (_,_; Σ; proj₁; proj₂)
-open import Relation.Binary.PropositionalEquality using (cong; _≡_; refl)
+open import Data.Product.Properties as ProdProp using ()
+open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Relation.Nullary using (¬_)
-open import Function using (_∘_)
 
 open import Lattice
-open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs)
+open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs)
-
+open import Lattice.MapSet _≟ˢ_ using ()
-data Expr : Set where
-    _+_ : Expr → Expr → Expr
-    _-_ : Expr → Expr → Expr
-    `_ : String → Expr
-    #_ : ℕ → Expr
-
-data Stmt : Set where
-    _←_ : String → Expr → Stmt
-
-open import Lattice.MapSet _≟ˢ_
     renaming
         ( MapSet to StringSet
-        ; insert to insertˢ
         ; to-List to to-Listˢ
-        ; empty to emptyˢ
-        ; singleton to singletonˢ
-        ; _⊔_ to _⊔ˢ_
-        ; `_ to `ˢ_
-        ; _∈_ to _∈ˢ_
-        ; ⊔-preserves-∈k₁ to ⊔ˢ-preserves-∈k₁
-        ; ⊔-preserves-∈k₂ to ⊔ˢ-preserves-∈k₂
         )
 
-data _∈ᵉ_ : String → Expr → Set where
-    in⁺₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ + e₂)
-    in⁺₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ + e₂)
-    in⁻₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ - e₂)
-    in⁻₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ - e₂)
-    here : ∀ {k : String} → k ∈ᵉ (` k)
-
-data _∈ᵗ_ : String → Stmt → Set where
-    in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵗ (k ← e)
-    in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵗ (k' ← e)
-
-private
-    Expr-vars : Expr → StringSet
-    Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r
-    Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r
-    Expr-vars (` s) = singletonˢ s
-    Expr-vars (# _) = emptyˢ
-
-    ∈-Expr-vars⇒∈ : ∀ {k : String} (e : Expr) → k ∈ˢ (Expr-vars e) → k ∈ᵉ e
-    ∈-Expr-vars⇒∈ {k} (e₁ + e₂) k∈vs
-        with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs
-    ...   | in₁ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
-    ...   | in₂ _ (single k,tt∈vs₂) = (in⁺₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
-    ...   | bothᵘ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
-    ∈-Expr-vars⇒∈ {k} (e₁ - e₂) k∈vs
-        with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs
-    ...   | in₁ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
-    ...   | in₂ _ (single k,tt∈vs₂) = (in⁻₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
-    ...   | bothᵘ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
-    ∈-Expr-vars⇒∈ {k} (` k) (RelAny.here refl) = here
-
-    ∈⇒∈-Expr-vars : ∀ {k : String} {e : Expr} → k ∈ᵉ e → k ∈ˢ (Expr-vars e)
-    ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₁ k∈e₁) =
-        ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
-                         {m₂ = Expr-vars e₂}
-                         (∈⇒∈-Expr-vars k∈e₁)
-    ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₂ k∈e₂) =
-        ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
-                         {m₂ = Expr-vars e₂}
-                         (∈⇒∈-Expr-vars k∈e₂)
-    ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₁ k∈e₁) =
-        ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
-                         {m₂ = Expr-vars e₂}
-                         (∈⇒∈-Expr-vars k∈e₁)
-    ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₂ k∈e₂) =
-        ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
-                         {m₂ = Expr-vars e₂}
-                         (∈⇒∈-Expr-vars k∈e₂)
-    ∈⇒∈-Expr-vars here = RelAny.here refl
-
-    Stmt-vars : Stmt → StringSet
-    Stmt-vars (x ← e) = (singletonˢ x) ⊔ˢ (Expr-vars e)
-
-    ∈-Stmt-vars⇒∈ : ∀ {k : String} (s : Stmt) → k ∈ˢ (Stmt-vars s) → k ∈ᵗ s
-    ∈-Stmt-vars⇒∈ {k} (k' ← e) k∈vs
-        with Expr-Provenance k ((`ˢ (singletonˢ k')) ∪ (`ˢ (Expr-vars e))) k∈vs
-    ...   | in₁ (single (RelAny.here refl)) _ = in←₁
-    ...   | in₂ _ (single k,tt∈vs') = in←₂ (∈-Expr-vars⇒∈ e (forget k,tt∈vs'))
-    ...   | bothᵘ (single (RelAny.here refl)) _ = in←₁
-
-    ∈⇒∈-Stmt-vars : ∀ {k : String} {s : Stmt} → k ∈ᵗ s → k ∈ˢ (Stmt-vars s)
-    ∈⇒∈-Stmt-vars {k} {k ← e} in←₁ =
-        ⊔ˢ-preserves-∈k₁ {m₁ = singletonˢ k}
-                         {m₂ = Expr-vars e}
-                         (RelAny.here refl)
-    ∈⇒∈-Stmt-vars {k} {k' ← e} (in←₂ k∈e) =
-        ⊔ˢ-preserves-∈k₂ {m₁ = singletonˢ k'}
-                         {m₂ = Expr-vars e}
-                         (∈⇒∈-Expr-vars k∈e)
-
-    Stmts-vars : ∀ {n : ℕ} → Vec Stmt n → StringSet
-    Stmts-vars = foldr (λ n → StringSet)
-                       (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ
-
-    ∈-Stmts-vars⇒∈ : ∀ {n : ℕ} {k : String} (ss : Vec Stmt n) →
-                     k ∈ˢ (Stmts-vars ss) → Σ (Fin n) (λ f → k ∈ᵗ lookup ss f)
-    ∈-Stmts-vars⇒∈ {suc n'} {k} (s ∷ ss') k∈vss
-        with Expr-Provenance k ((`ˢ (Stmt-vars s)) ∪ (`ˢ (Stmts-vars ss'))) k∈vss
-    ...   | in₁ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
-    ...   | in₂ _ (single k,tt∈vss') =
-            let
-                (f' , k∈s') = ∈-Stmts-vars⇒∈ ss' (forget k,tt∈vss')
-            in
-                (suc f' , k∈s')
-    ...   | bothᵘ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
-
-    ∈⇒∈-Stmts-vars : ∀ {n : ℕ} {k : String} {ss : Vec Stmt n} {f : Fin n} →
-                     k ∈ᵗ lookup ss f → k ∈ˢ (Stmts-vars ss)
-    ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {zero} k∈s =
-        ⊔ˢ-preserves-∈k₁ {m₁ = Stmt-vars s}
-                         {m₂ = Stmts-vars ss'}
-                         (∈⇒∈-Stmt-vars k∈s)
-    ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {suc f'} k∈ss' =
-        ⊔ˢ-preserves-∈k₂ {m₁ = Stmt-vars s}
-                         {m₂ = Stmts-vars ss'}
-                         (∈⇒∈-Stmts-vars {n} {k} {ss'} {f'} k∈ss')
-
-    -- Creating a new number from a natural number can never create one
-    -- equal to one you get from weakening the bounds on another number.
-    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
-    z≢sf f ()
-
-    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
-    z≢mapsfs [] = []
-    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
-
-    indices : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    indices 0 = ([] , empty)
-    indices (suc n') =
-        let
-            (inds' , unids') = indices n'
-        in
-            ( zero ∷ mapˡ suc inds'
-            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-            )
-
-    indices-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ˡ (proj₁ (indices n))
-    indices-complete (suc n') zero = RelAny.here refl
-    indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f'))
-
-
--- For now, just represent the program and CFG as one type, without branching.
 record Program : Set where
     field
-        length : ℕ
+        rootStmt : Stmt
-        stmts : Vec Stmt length
+
+    graph : Graph
+    graph = wrap (buildCfg rootStmt)
+
+    State : Set
+    State = Graph.Index graph
+
+    initialState : State
+    initialState = proj₁ (wrap-input (buildCfg rootStmt))
+
+    finalState : State
+    finalState = proj₁ (wrap-output (buildCfg rootStmt))
+
+    trace : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → Trace {graph} initialState finalState [] ρ
+    trace {ρ} ∅,s⇒ρ
+        with MkEndToEndTrace idx₁ (RelAny.here refl) idx₂ (RelAny.here refl) tr
+             ← EndToEndTrace-wrap (buildCfg-sufficient ∅,s⇒ρ) = tr
 
     private
         vars-Set : StringSet
-        vars-Set = Stmts-vars stmts
+        vars-Set = Stmt-vars rootStmt
 
     vars : List String
     vars = to-Listˢ vars-Set
@@ -177,35 +58,36 @@ record Program : Set where
     vars-Unique : Unique vars
     vars-Unique = proj₂ vars-Set
 
-    State : Set
-    State = Fin length
-
     states : List State
-    states = proj₁ (indices length)
+    states = indices graph
 
-    states-complete : ∀ (s : State) → s ∈ˡ states
+    states-complete : ∀ (s : State) → s ListMem.∈ states
-    states-complete = indices-complete length
+    states-complete = indices-complete graph
 
     states-Unique : Unique states
-    states-Unique = proj₂ (indices length)
+    states-Unique = indices-Unique graph
 
-    code : State → Stmt
+    code : State → List BasicStmt
-    code = lookup stmts
+    code st = graph [ st ]
 
-    vars-complete : ∀ {k : String} (s : State) → k ∈ᵗ (code s) → k ∈ˡ vars
+    -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ListMem.∈ vars
-    vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
+    -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
 
     _≟_ : IsDecidable (_≡_ {_} {State})
-    _≟_ = _≟ᶠ_
+    _≟_ = FinProp._≟_
 
-    -- Computations for incoming and outgoing edges will have to change too
+    _≟ᵉ_ : IsDecidable (_≡_ {_} {Graph.Edge graph})
-    -- when we support branching etc.
+    _≟ᵉ_ = ProdProp.≡-dec _≟_ _≟_
+
+    open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)
 
     incoming : State → List State
-    incoming
+    incoming = predecessors graph
-        with length
+
-    ...   | 0 = (λ ())
+    initialState-pred-∅ : incoming initialState ≡ []
-    ...   | suc n' = (λ
+    initialState-pred-∅ =
-            { zero → []
+        wrap-preds-∅ (buildCfg rootStmt) initialState (RelAny.here refl)
-            ; (suc f') → (inject₁ f') ∷ []
+
-            })
+    edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
+                    s₁ ListMem.∈ (incoming s₂)
+    edge⇒incoming = edge⇒predecessor graph

Language/Base.agda

@@ -0,0 +1,145 @@
+module Language.Base where
+
+open import Data.List as List using (List)
+open import Data.Nat using (ℕ; suc)
+open import Data.Product using (Σ; _,_; proj₁)
+open import Data.String as String using (String)
+open import Data.Vec using (Vec; foldr; lookup)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+
+open import Lattice
+
+data Expr : Set where
+    _+_ : Expr → Expr → Expr
+    _-_ : Expr → Expr → Expr
+    `_ : String → Expr
+    #_ : ℕ → Expr
+
+data BasicStmt : Set where
+    _←_ : String → Expr → BasicStmt
+    noop : BasicStmt
+
+infixr 2 _then_
+infix 3 if_then_else_
+infix 3 while_repeat_
+data Stmt : Set where
+    ⟨_⟩ : BasicStmt → Stmt
+    _then_ : Stmt → Stmt → Stmt
+    if_then_else_ : Expr → Stmt → Stmt → Stmt
+    while_repeat_ : Expr → Stmt → Stmt
+
+data _∈ᵉ_ : String → Expr → Set where
+    in⁺₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ + e₂)
+    in⁺₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ + e₂)
+    in⁻₁ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₁ → k ∈ᵉ (e₁ - e₂)
+    in⁻₂ : ∀ {e₁ e₂ : Expr} {k : String} → k ∈ᵉ e₂ → k ∈ᵉ (e₁ - e₂)
+    here : ∀ {k : String} → k ∈ᵉ (` k)
+
+data _∈ᵇ_ : String → BasicStmt → Set where
+    in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵇ (k ← e)
+    in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵇ (k' ← e)
+
+open import Lattice.MapSet (String._≟_)
+    renaming
+        ( MapSet to StringSet
+        ; insert to insertˢ
+        ; empty to emptyˢ
+        ; singleton to singletonˢ
+        ; _⊔_ to _⊔ˢ_
+        ; `_ to `ˢ_
+        ; _∈_ to _∈ˢ_
+        ; ⊔-preserves-∈k₁ to ⊔ˢ-preserves-∈k₁
+        ; ⊔-preserves-∈k₂ to ⊔ˢ-preserves-∈k₂
+        )
+
+Expr-vars : Expr → StringSet
+Expr-vars (l + r) = Expr-vars l ⊔ˢ Expr-vars r
+Expr-vars (l - r) = Expr-vars l ⊔ˢ Expr-vars r
+Expr-vars (` s) = singletonˢ s
+Expr-vars (# _) = emptyˢ
+
+-- ∈-Expr-vars⇒∈ : ∀ {k : String} (e : Expr) → k ∈ˢ (Expr-vars e) → k ∈ᵉ e
+-- ∈-Expr-vars⇒∈ {k} (e₁ + e₂) k∈vs
+--     with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs
+-- ...   | in₁ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
+-- ...   | in₂ _ (single k,tt∈vs₂) = (in⁺₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
+-- ...   | bothᵘ (single k,tt∈vs₁) _ = (in⁺₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
+-- ∈-Expr-vars⇒∈ {k} (e₁ - e₂) k∈vs
+--     with Expr-Provenance k ((`ˢ (Expr-vars e₁)) ∪ (`ˢ (Expr-vars e₂))) k∈vs
+-- ...   | in₁ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
+-- ...   | in₂ _ (single k,tt∈vs₂) = (in⁻₂ (∈-Expr-vars⇒∈ e₂ (forget k,tt∈vs₂)))
+-- ...   | bothᵘ (single k,tt∈vs₁) _ = (in⁻₁ (∈-Expr-vars⇒∈ e₁ (forget k,tt∈vs₁)))
+-- ∈-Expr-vars⇒∈ {k} (` k) (RelAny.here refl) = here
+
+-- ∈⇒∈-Expr-vars : ∀ {k : String} {e : Expr} → k ∈ᵉ e → k ∈ˢ (Expr-vars e)
+-- ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₁ k∈e₁) =
+--     ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
+--                      {m₂ = Expr-vars e₂}
+--                      (∈⇒∈-Expr-vars k∈e₁)
+-- ∈⇒∈-Expr-vars {k} {e₁ + e₂} (in⁺₂ k∈e₂) =
+--     ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
+--                      {m₂ = Expr-vars e₂}
+--                      (∈⇒∈-Expr-vars k∈e₂)
+-- ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₁ k∈e₁) =
+--     ⊔ˢ-preserves-∈k₁ {m₁ = Expr-vars e₁}
+--                      {m₂ = Expr-vars e₂}
+--                      (∈⇒∈-Expr-vars k∈e₁)
+-- ∈⇒∈-Expr-vars {k} {e₁ - e₂} (in⁻₂ k∈e₂) =
+--     ⊔ˢ-preserves-∈k₂ {m₁ = Expr-vars e₁}
+--                      {m₂ = Expr-vars e₂}
+--                      (∈⇒∈-Expr-vars k∈e₂)
+-- ∈⇒∈-Expr-vars here = RelAny.here refl
+
+BasicStmt-vars : BasicStmt → StringSet
+BasicStmt-vars (x ← e) = (singletonˢ x) ⊔ˢ (Expr-vars e)
+BasicStmt-vars noop = emptyˢ
+
+Stmt-vars : Stmt → StringSet
+Stmt-vars ⟨ bs ⟩ = BasicStmt-vars bs
+Stmt-vars (s₁ then s₂) = (Stmt-vars s₁) ⊔ˢ (Stmt-vars s₂)
+Stmt-vars (if e then s₁ else s₂) = ((Expr-vars e) ⊔ˢ (Stmt-vars s₁)) ⊔ˢ (Stmt-vars s₂)
+Stmt-vars (while e repeat s) = (Expr-vars e) ⊔ˢ (Stmt-vars s)
+
+-- ∈-Stmt-vars⇒∈ : ∀ {k : String} (s : Stmt) → k ∈ˢ (Stmt-vars s) → k ∈ᵇ s
+-- ∈-Stmt-vars⇒∈ {k} (k' ← e) k∈vs
+--     with Expr-Provenance k ((`ˢ (singletonˢ k')) ∪ (`ˢ (Expr-vars e))) k∈vs
+-- ...   | in₁ (single (RelAny.here refl)) _ = in←₁
+-- ...   | in₂ _ (single k,tt∈vs') = in←₂ (∈-Expr-vars⇒∈ e (forget k,tt∈vs'))
+-- ...   | bothᵘ (single (RelAny.here refl)) _ = in←₁
+
+-- ∈⇒∈-Stmt-vars : ∀ {k : String} {s : Stmt} → k ∈ᵇ s → k ∈ˢ (Stmt-vars s)
+-- ∈⇒∈-Stmt-vars {k} {k ← e} in←₁ =
+--     ⊔ˢ-preserves-∈k₁ {m₁ = singletonˢ k}
+--                      {m₂ = Expr-vars e}
+--                      (RelAny.here refl)
+-- ∈⇒∈-Stmt-vars {k} {k' ← e} (in←₂ k∈e) =
+--     ⊔ˢ-preserves-∈k₂ {m₁ = singletonˢ k'}
+--                      {m₂ = Expr-vars e}
+--                      (∈⇒∈-Expr-vars k∈e)
+
+Stmts-vars : ∀ {n : ℕ} → Vec Stmt n → StringSet
+Stmts-vars = foldr (λ n → StringSet)
+                   (λ {k} stmt acc → (Stmt-vars stmt) ⊔ˢ acc) emptyˢ
+
+-- ∈-Stmts-vars⇒∈ : ∀ {n : ℕ} {k : String} (ss : Vec Stmt n) →
+--                  k ∈ˢ (Stmts-vars ss) → Σ (Fin n) (λ f → k ∈ᵇ lookup ss f)
+-- ∈-Stmts-vars⇒∈ {suc n'} {k} (s ∷ ss') k∈vss
+--     with Expr-Provenance k ((`ˢ (Stmt-vars s)) ∪ (`ˢ (Stmts-vars ss'))) k∈vss
+-- ...   | in₁ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
+-- ...   | in₂ _ (single k,tt∈vss') =
+--         let
+--             (f' , k∈s') = ∈-Stmts-vars⇒∈ ss' (forget k,tt∈vss')
+--         in
+--             (suc f' , k∈s')
+-- ...   | bothᵘ (single k,tt∈vs) _ = (zero , ∈-Stmt-vars⇒∈ s (forget k,tt∈vs))
+
+-- ∈⇒∈-Stmts-vars : ∀ {n : ℕ} {k : String} {ss : Vec Stmt n} {f : Fin n} →
+--                  k ∈ᵇ lookup ss f → k ∈ˢ (Stmts-vars ss)
+-- ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {zero} k∈s =
+--     ⊔ˢ-preserves-∈k₁ {m₁ = Stmt-vars s}
+--                      {m₂ = Stmts-vars ss'}
+--                      (∈⇒∈-Stmt-vars k∈s)
+-- ∈⇒∈-Stmts-vars {suc n} {k} {s ∷ ss'} {suc f'} k∈ss' =
+--     ⊔ˢ-preserves-∈k₂ {m₁ = Stmt-vars s}
+--                      {m₂ = Stmts-vars ss'}
+--                      (∈⇒∈-Stmts-vars {n} {k} {ss'} {f'} k∈ss')

Language/Graphs.agda

@@ -0,0 +1,174 @@
+module Language.Graphs where
+
+open import Language.Base using (Expr; Stmt; BasicStmt; ⟨_⟩; _then_; if_then_else_; while_repeat_)
+
+open import Data.Fin as Fin using (Fin; suc; zero)
+open import Data.Fin.Properties as FinProp using (suc-injective)
+open import Data.List as List using (List; []; _∷_)
+open import Data.List.Membership.Propositional as ListMem using ()
+open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺; ∈-filter⁻)
+open import Data.List.Relation.Unary.All using (All; []; _∷_)
+open import Data.List.Relation.Unary.Any as RelAny using ()
+open import Data.Nat as Nat using (ℕ; suc)
+open import Data.Nat.Properties using (+-assoc; +-comm)
+open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
+open import Data.Product.Properties as ProdProp using ()
+open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
+open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
+open import Relation.Nullary using (¬_)
+
+open import Lattice
+open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+
+record Graph : Set where
+    constructor MkGraph
+    field
+        size : ℕ
+
+    Index : Set
+    Index = Fin size
+
+    Edge : Set
+    Edge = Index × Index
+
+    field
+        nodes : Vec (List BasicStmt) size
+        edges : List Edge
+        inputs : List Index
+        outputs : List Index
+
+_↑ˡ_ : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n Nat.+ m) × Fin (n Nat.+ m))
+_↑ˡ_ (idx₁ , idx₂) m = (idx₁ Fin.↑ˡ m , idx₂ Fin.↑ˡ m)
+
+_↑ʳ_ : ∀ {m} n → (Fin m × Fin m) → Fin (n Nat.+ m) × Fin (n Nat.+ m)
+_↑ʳ_ n (idx₁ , idx₂) = (n Fin.↑ʳ idx₁ , n Fin.↑ʳ idx₂)
+
+_↑ˡⁱ_ : ∀ {n} → List (Fin n) → ∀ m → List (Fin (n Nat.+ m))
+_↑ˡⁱ_ l m = List.map (Fin._↑ˡ m) l
+
+_↑ʳⁱ_ : ∀ {m} n → List (Fin m) → List (Fin (n Nat.+ m))
+_↑ʳⁱ_ n l = List.map (n Fin.↑ʳ_) l
+
+_↑ˡᵉ_ : ∀ {n} → List (Fin n × Fin n) → ∀ m → List (Fin (n Nat.+ m) × Fin (n Nat.+ m))
+_↑ˡᵉ_ l m = List.map (_↑ˡ m) l
+
+_↑ʳᵉ_ : ∀ {m} n → List (Fin m × Fin m) → List (Fin (n Nat.+ m) × Fin (n Nat.+ m))
+_↑ʳᵉ_ n l = List.map (n ↑ʳ_) l
+
+infixr 5 _∙_
+_∙_ : Graph → Graph → Graph
+_∙_ g₁ g₂ = record
+    { size = Graph.size g₁ Nat.+ Graph.size g₂
+    ; nodes = Graph.nodes g₁ ++ Graph.nodes g₂
+    ; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++
+              (Graph.size g₁ ↑ʳᵉ Graph.edges g₂)
+    ; inputs = (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂) List.++
+               (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)
+    ; outputs = (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂) List.++
+                (Graph.size g₁ ↑ʳⁱ Graph.outputs g₂)
+    }
+
+infixr 5 _↦_
+_↦_ : Graph → Graph → Graph
+_↦_ g₁ g₂ = record
+    { size = Graph.size g₁ Nat.+ Graph.size g₂
+    ; nodes = Graph.nodes g₁ ++ Graph.nodes g₂
+    ; edges = (Graph.edges g₁ ↑ˡᵉ Graph.size g₂) List.++
+              (Graph.size g₁ ↑ʳᵉ Graph.edges g₂) List.++
+              (List.cartesianProduct (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
+                                     (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂))
+    ; inputs = Graph.inputs g₁ ↑ˡⁱ Graph.size g₂
+    ; outputs = Graph.size g₁ ↑ʳⁱ Graph.outputs g₂
+    }
+
+loop : Graph → Graph
+loop g = record
+    { size = 2 Nat.+ Graph.size g
+    ; nodes = [] ∷ [] ∷ Graph.nodes g
+    ; edges = (2 ↑ʳᵉ Graph.edges g) List.++
+              List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g) List.++
+              List.map (_, suc zero) (2 ↑ʳⁱ Graph.outputs g) List.++
+              ((suc zero , zero) ∷ (zero , suc zero) ∷ [])
+    ; inputs = zero ∷ []
+    ; outputs = (suc zero) ∷ []
+    }
+
+infixr 5 _skipto_
+_skipto_ : Graph → Graph → Graph
+_skipto_ g₁ g₂ = record (g₁ ∙ g₂)
+    { edges = Graph.edges (g₁ ∙ g₂) List.++
+              (List.cartesianProduct (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂)
+                                     (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂))
+    ; inputs = Graph.inputs g₁ ↑ˡⁱ Graph.size g₂
+    ; outputs = Graph.size g₁ ↑ʳⁱ Graph.inputs g₂
+    }
+
+_[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
+_[_] g idx = lookup (Graph.nodes g) idx
+
+singleton : List BasicStmt → Graph
+singleton bss = record
+    { size = 1
+    ; nodes = bss ∷ []
+    ; edges = []
+    ; inputs = zero ∷ []
+    ; outputs = zero ∷ []
+    }
+
+wrap : Graph → Graph
+wrap g = singleton [] ↦ g ↦ singleton []
+
+buildCfg : Stmt → Graph
+buildCfg ⟨ bs₁ ⟩ = singleton (bs₁ ∷ [])
+buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
+buildCfg (if _ then s₁ else s₂) = singleton [] ↦ (buildCfg s₁ ∙ buildCfg s₂) ↦ singleton []
+buildCfg (while _ repeat s) = loop (buildCfg s)
+
+private
+    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
+    z≢sf f ()
+
+    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
+    z≢mapsfs [] = []
+    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+    finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+    finValues 0 = ([] , Utils.empty)
+    finValues (suc n') =
+        let
+            (inds' , unids') = finValues n'
+        in
+            ( zero ∷ List.map suc inds'
+            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+            )
+
+    finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
+    finValues-complete (suc n') zero = RelAny.here refl
+    finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
+
+module _ (g : Graph) where
+    open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_)
+
+    indices : List (Graph.Index g)
+    indices = proj₁ (finValues (Graph.size g))
+
+    indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
+    indices-complete = finValues-complete (Graph.size g)
+
+    indices-Unique : Unique indices
+    indices-Unique = proj₂ (finValues (Graph.size g))
+
+    predecessors : (Graph.Index g) → List (Graph.Index g)
+    predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices
+
+    edge⇒predecessor : ∀ {idx₁ idx₂ : Graph.Index g} → (idx₁ , idx₂) ListMem.∈ (Graph.edges g) →
+                    idx₁ ListMem.∈ (predecessors idx₂)
+    edge⇒predecessor {idx₁} {idx₂} idx₁,idx₂∈es =
+        ∈-filter⁺ (λ idx' → (idx' , idx₂) ∈? (Graph.edges g))
+                  (indices-complete idx₁) idx₁,idx₂∈es
+
+    predecessor⇒edge : ∀ {idx₁ idx₂ : Graph.Index g} → idx₁ ListMem.∈ (predecessors idx₂) →
+                       (idx₁ , idx₂) ListMem.∈ (Graph.edges g)
+    predecessor⇒edge {idx₁} {idx₂} idx₁∈pred =
+        proj₂ (∈-filter⁻ (λ idx' → (idx' , idx₂) ∈? (Graph.edges g)) {v = idx₁} {xs = indices} idx₁∈pred )

Language/Properties.agda

@@ -0,0 +1,300 @@
+module Language.Properties where
+
+open import Language.Base
+open import Language.Semantics
+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.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 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₂)
+
+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)
+
+Trace-∙ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
+           Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →
+           Trace {g₁ ∙ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂
+Trace-∙ˡ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
+    rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
+    Trace-single ρ₁⇒ρ₂
+Trace-∙ˡ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
+    rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
+    Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (_↑ˡ Graph.size g₂) idx₁→idx))
+                    (Trace-∙ˡ tr')
+
+Trace-∙ʳ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₂} {ρ₁ ρ₂ : Env} →
+           Trace {g₂} idx₁ idx₂ ρ₁ ρ₂ →
+           Trace {g₁ ∙ g₂} (Graph.size g₁ Fin.↑ʳ idx₁) (Graph.size g₁ Fin.↑ʳ idx₂) ρ₁ ρ₂
+Trace-∙ʳ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
+    rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
+    Trace-single ρ₁⇒ρ₂
+Trace-∙ʳ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
+    rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
+    Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ _ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx))
+                    (Trace-∙ʳ tr')
+
+EndToEndTrace-∙ˡ : ∀ {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} →
+                   EndToEndTrace {g₁} ρ₁ ρ₂ →
+                   EndToEndTrace {g₁ ∙ g₂} ρ₁ ρ₂
+EndToEndTrace-∙ˡ {g₁} {g₂} etr = record
+    { idx₁ = EndToEndTrace.idx₁ etr Fin.↑ˡ Graph.size g₂
+    ; idx₁∈inputs = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂)
+                                                    (EndToEndTrace.idx₁∈inputs etr))
+    ; idx₂ = EndToEndTrace.idx₂ etr Fin.↑ˡ Graph.size g₂
+    ; idx₂∈outputs = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂)
+                                                    (EndToEndTrace.idx₂∈outputs etr))
+    ; trace = Trace-∙ˡ (EndToEndTrace.trace etr)
+    }
+
+EndToEndTrace-∙ʳ : ∀ {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} →
+           EndToEndTrace {g₂} ρ₁ ρ₂ →
+           EndToEndTrace {g₁ ∙ g₂} ρ₁ ρ₂
+EndToEndTrace-∙ʳ {g₁} {g₂} etr = record
+    { idx₁ = Graph.size g₁ Fin.↑ʳ EndToEndTrace.idx₁ etr
+    ; idx₁∈inputs = ListMemProp.∈-++⁺ʳ (Graph.inputs g₁ ↑ˡⁱ Graph.size g₂)
+                                       ((x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_)
+                                                     (EndToEndTrace.idx₁∈inputs etr)))
+    ; idx₂ = Graph.size g₁ Fin.↑ʳ EndToEndTrace.idx₂ etr
+    ; idx₂∈outputs = ListMemProp.∈-++⁺ʳ (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
+                                        ((x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_)
+                                                      (EndToEndTrace.idx₂∈outputs etr)))
+
+    ; trace = Trace-∙ʳ (EndToEndTrace.trace etr)
+    }
+
+Trace-↦ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
+           Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →
+           Trace {g₁ ↦ g₂} (idx₁ Fin.↑ˡ Graph.size g₂) (idx₂ Fin.↑ˡ Graph.size g₂) ρ₁ ρ₂
+Trace-↦ˡ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
+    rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
+    Trace-single ρ₁⇒ρ₂
+Trace-↦ˡ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
+    rewrite sym (lookup-++ˡ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
+    Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (_↑ˡ Graph.size g₂) idx₁→idx))
+                    (Trace-↦ˡ tr')
+
+Trace-↦ʳ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₂} {ρ₁ ρ₂ : Env} →
+           Trace {g₂} idx₁ idx₂ ρ₁ ρ₂ →
+           Trace {g₁ ↦ g₂} (Graph.size g₁ Fin.↑ʳ idx₁) (Graph.size g₁ Fin.↑ʳ idx₂) ρ₁ ρ₂
+Trace-↦ʳ {g₁} {g₂} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
+    rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
+    Trace-single ρ₁⇒ρ₂
+Trace-↦ʳ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
+    rewrite sym (lookup-++ʳ (Graph.nodes g₁) (Graph.nodes g₂) idx₁) =
+    Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ʳ (Graph.edges g₁ ↑ˡᵉ Graph.size g₂)
+                                        (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx)))
+                    (Trace-↦ʳ {g₁} {g₂} tr')
+
+loop-edge-groups : ∀ (g : Graph) → List (List (Graph.Edge (loop g)))
+loop-edge-groups g =
+    (2 ↑ʳᵉ Graph.edges g) ∷
+    (List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g)) ∷
+    (List.map (_, suc zero) (2 ↑ʳⁱ Graph.outputs g)) ∷
+    ((suc zero , zero) ∷ (zero , suc zero) ∷ []) ∷
+    []
+
+loop-edge-help : ∀ (g : Graph) {l : List (Graph.Edge (loop g))} {e : Graph.Edge (loop g)} →
+                 e ListMem.∈ l → l ListMem.∈ loop-edge-groups g →
+                 e ListMem.∈ Graph.edges (loop g)
+loop-edge-help g e∈l l∈ess = concat-∈ e∈l l∈ess
+
+Trace-loop : ∀ {g : Graph} {idx₁ idx₂ : Graph.Index g} {ρ₁ ρ₂ : Env} →
+             Trace {g} idx₁ idx₂ ρ₁ ρ₂ → Trace {loop g} (2 Fin.↑ʳ idx₁) (2 Fin.↑ʳ idx₂) ρ₁ ρ₂
+Trace-loop {g} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
+    rewrite sym (lookup-++ʳ (List.[] ∷ List.[] ∷ Vec.[]) (Graph.nodes g) idx₁) =
+    Trace-single ρ₁⇒ρ₂
+Trace-loop {g} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
+    rewrite sym (lookup-++ʳ (List.[] ∷ List.[] ∷ Vec.[]) (Graph.nodes g) idx₁) =
+    Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (2 ↑ʳ_) idx₁→idx))
+                    (Trace-loop {g} tr')
+
+EndToEndTrace-loop : ∀ {g : Graph} {ρ₁ ρ₂ : Env} →
+                     EndToEndTrace {g} ρ₁ ρ₂ → EndToEndTrace {loop g} ρ₁ ρ₂
+EndToEndTrace-loop {g} etr =
+    let
+        zero→idx₁' = x∈xs⇒fx∈fxs (zero ,_)
+                                 (x∈xs⇒fx∈fxs (2 Fin.↑ʳ_)
+                                              (EndToEndTrace.idx₁∈inputs etr))
+        zero→idx₁ = loop-edge-help g zero→idx₁' (there (here refl))
+        idx₂→suc' = x∈xs⇒fx∈fxs (_, suc zero)
+                               (x∈xs⇒fx∈fxs (2 Fin.↑ʳ_)
+                                            (EndToEndTrace.idx₂∈outputs etr))
+        idx₂→suc = loop-edge-help g idx₂→suc' (there (there (here refl)))
+    in
+        record
+            { idx₁ = zero
+            ; idx₁∈inputs = here refl
+            ; idx₂ = suc zero
+            ; idx₂∈outputs = here refl
+            ; trace =
+                Trace-single [] ++⟨ zero→idx₁ ⟩
+                Trace-loop {g} (EndToEndTrace.trace etr) ++⟨ idx₂→suc ⟩
+                Trace-single []
+            }
+
+EndToEndTrace-loop² : ∀ {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} →
+                      EndToEndTrace {loop g} ρ₁ ρ₂ →
+                      EndToEndTrace {loop g} ρ₂ ρ₃ →
+                      EndToEndTrace {loop g} ρ₁ ρ₃
+EndToEndTrace-loop² {g} (MkEndToEndTrace zero (here refl) (suc zero) (here refl) tr₁)
+                        (MkEndToEndTrace zero (here refl) (suc zero) (here refl) tr₂) =
+    let
+        suc→zero = loop-edge-help g (here refl)
+                                    (there (there (there (here refl))))
+    in
+        record
+            { idx₁ = zero
+            ; idx₁∈inputs = here refl
+            ; idx₂ = suc zero
+            ; idx₂∈outputs = here refl
+            ; trace = tr₁ ++⟨ suc→zero ⟩ tr₂
+            }
+
+EndToEndTrace-loop⁰ : ∀ {g : Graph} {ρ : Env} →
+                      EndToEndTrace {loop g} ρ ρ
+EndToEndTrace-loop⁰ {g} {ρ} =
+    let
+        zero→suc = loop-edge-help g (there (here refl))
+                                    (there (there (there (here refl))))
+    in
+        record
+            { idx₁ = zero
+            ; idx₁∈inputs = here refl
+            ; idx₂ = suc zero
+            ; idx₂∈outputs = here refl
+            ; trace = Trace-single [] ++⟨ zero→suc ⟩ Trace-single []
+            }
+
+infixr 5 _++_
+_++_ : ∀ {g₁ g₂ : Graph} {ρ₁ ρ₂ ρ₃ : Env} →
+       EndToEndTrace {g₁} ρ₁ ρ₂ → EndToEndTrace {g₂} ρ₂ ρ₃ →
+       EndToEndTrace {g₁ ↦ g₂} ρ₁ ρ₃
+_++_ {g₁} {g₂} etr₁ etr₂
+    = record
+        { idx₁ = EndToEndTrace.idx₁ etr₁ Fin.↑ˡ Graph.size g₂
+        ; idx₁∈inputs = x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂) (EndToEndTrace.idx₁∈inputs etr₁)
+        ; idx₂ = Graph.size g₁ Fin.↑ʳ EndToEndTrace.idx₂ etr₂
+        ; idx₂∈outputs = x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_) (EndToEndTrace.idx₂∈outputs etr₂)
+        ; trace =
+            let
+                o∈tr₁ = x∈xs⇒fx∈fxs (Fin._↑ˡ Graph.size g₂) (EndToEndTrace.idx₂∈outputs etr₁)
+                i∈tr₂ = x∈xs⇒fx∈fxs (Graph.size g₁ Fin.↑ʳ_) (EndToEndTrace.idx₁∈inputs etr₂)
+                oi∈es = ListMemProp.∈-++⁺ʳ (Graph.edges g₁ ↑ˡᵉ Graph.size g₂)
+                                           (ListMemProp.∈-++⁺ʳ (Graph.size g₁ ↑ʳᵉ Graph.edges g₂)
+                                                               (∈-cartesianProduct o∈tr₁ i∈tr₂))
+            in
+                (Trace-↦ˡ {g₁} {g₂} (EndToEndTrace.trace etr₁)) ++⟨ oi∈es ⟩
+                (Trace-↦ʳ {g₁} {g₂} (EndToEndTrace.trace etr₂))
+        }
+
+EndToEndTrace-singleton : ∀ {bss : List BasicStmt} {ρ₁ ρ₂ : Env} →
+                  ρ₁ , bss ⇒ᵇˢ ρ₂ → EndToEndTrace {singleton bss} ρ₁ ρ₂
+EndToEndTrace-singleton ρ₁⇒ρ₂ = record
+    { idx₁ = zero
+    ; idx₁∈inputs = here refl
+    ; idx₂ = zero
+    ; idx₂∈outputs = here refl
+    ; trace = Trace-single ρ₁⇒ρ₂
+    }
+
+EndToEndTrace-singleton[] : ∀ (ρ : Env) → EndToEndTrace {singleton []} ρ ρ
+EndToEndTrace-singleton[] env = EndToEndTrace-singleton []
+
+EndToEndTrace-wrap : ∀ {g : Graph} {ρ₁ ρ₂ : Env} →
+                     EndToEndTrace {g} ρ₁ ρ₂ → EndToEndTrace {wrap g} ρ₁ ρ₂
+EndToEndTrace-wrap {g} {ρ₁} {ρ₂} etr = EndToEndTrace-singleton[] ρ₁ ++ etr ++ EndToEndTrace-singleton[] ρ₂
+
+buildCfg-sufficient : ∀ {s : Stmt} {ρ₁ ρ₂ : Env} → ρ₁ , s ⇒ˢ ρ₂ →
+                      EndToEndTrace {buildCfg s} ρ₁ ρ₂
+buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) =
+    EndToEndTrace-singleton (ρ₁,bs⇒ρ₂ ∷ [])
+buildCfg-sufficient (⇒ˢ-then ρ₁ ρ₂ ρ₃ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) =
+    buildCfg-sufficient ρ₁,s₁⇒ρ₂ ++ buildCfg-sufficient ρ₂,s₂⇒ρ₃
+buildCfg-sufficient (⇒ˢ-if-true ρ₁ ρ₂ _ _ s₁ s₂ _ _ ρ₁,s₁⇒ρ₂) =
+    EndToEndTrace-singleton[] ρ₁ ++
+    (EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ₂)) ++
+    EndToEndTrace-singleton[] ρ₂
+buildCfg-sufficient (⇒ˢ-if-false ρ₁ ρ₂ _ s₁ s₂ _ ρ₁,s₂⇒ρ₂) =
+    EndToEndTrace-singleton[] ρ₁ ++
+    (EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)) ++
+    EndToEndTrace-singleton[] ρ₂
+buildCfg-sufficient (⇒ˢ-while-true ρ₁ ρ₂ ρ₃ _ _ s _ _ ρ₁,s⇒ρ₂ ρ₂,ws⇒ρ₃) =
+    EndToEndTrace-loop² {buildCfg s}
+                        (EndToEndTrace-loop {buildCfg s} (buildCfg-sufficient ρ₁,s⇒ρ₂))
+                        (buildCfg-sufficient ρ₂,ws⇒ρ₃)
+buildCfg-sufficient (⇒ˢ-while-false ρ _ s _) =
+    EndToEndTrace-loop⁰ {buildCfg s} {ρ}

Language/Semantics.agda

@@ -0,0 +1,73 @@
+module Language.Semantics where
+
+open import Language.Base
+
+open import Agda.Primitive using (lsuc)
+open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_)
+open import Data.Product using (_×_; _,_)
+open import Data.String using (String)
+open import Data.List as List using (List)
+open import Data.Nat using (ℕ)
+open import Relation.Nullary using (¬_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+open import Lattice
+open import Utils using (_⇒_; _∧_; _∨_)
+
+data Value : Set where
+    ↑ᶻ : ℤ → Value
+
+Env : Set
+Env = List (String × Value)
+
+data _∈_ : (String × Value) → Env → Set where
+    here : ∀ (s : String) (v : Value) (ρ : Env) → (s , v) ∈ ((s , v) List.∷ ρ)
+    there : ∀ (s s' : String) (v v' : Value) (ρ : Env) → ¬ (s ≡ s') → (s , v) ∈ ρ → (s , v) ∈ ((s' , v') List.∷ ρ)
+
+data _,_⇒ᵉ_ : Env → Expr → Value → Set where
+    ⇒ᵉ-ℕ : ∀ (ρ : Env) (n : ℕ) → ρ , (# n) ⇒ᵉ (↑ᶻ (+ n))
+    ⇒ᵉ-Var : ∀ (ρ : Env) (x : String) (v : Value) → (x , v) ∈ ρ → ρ , (` x) ⇒ᵉ v
+    ⇒ᵉ-+ : ∀ (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) →
+           ρ , e₁ ⇒ᵉ (↑ᶻ z₁) → ρ , e₂ ⇒ᵉ (↑ᶻ z₂) →
+           ρ , (e₁ + e₂) ⇒ᵉ (↑ᶻ (z₁ +ᶻ z₂))
+    ⇒ᵉ-- : ∀ (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) →
+           ρ , e₁ ⇒ᵉ (↑ᶻ z₁) → ρ , e₂ ⇒ᵉ (↑ᶻ z₂) →
+           ρ , (e₁ - e₂) ⇒ᵉ (↑ᶻ (z₁ -ᶻ z₂))
+
+data _,_⇒ᵇ_ : Env → BasicStmt → Env → Set where
+    ⇒ᵇ-noop : ∀ (ρ : Env) → ρ , noop ⇒ᵇ ρ
+    ⇒ᵇ-← : ∀ (ρ : Env) (x : String) (e : Expr) (v : Value) →
+           ρ , e ⇒ᵉ v → ρ , (x ← e) ⇒ᵇ ((x , v) List.∷ ρ)
+
+data _,_⇒ᵇˢ_ : Env → List BasicStmt → Env → Set where
+    [] : ∀ {ρ : Env} → ρ , List.[] ⇒ᵇˢ ρ
+    _∷_ : ∀ {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} →
+          ρ₁ , bs ⇒ᵇ ρ₂ → ρ₂ , bss ⇒ᵇˢ ρ₃ → ρ₁ , (bs List.∷ bss) ⇒ᵇˢ ρ₃
+
+data _,_⇒ˢ_ : Env → Stmt → Env → Set where
+    ⇒ˢ-⟨⟩ : ∀ (ρ₁ ρ₂ : Env) (bs : BasicStmt) →
+            ρ₁ , bs ⇒ᵇ ρ₂ → ρ₁ , ⟨ bs ⟩ ⇒ˢ ρ₂
+    ⇒ˢ-then : ∀ (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) →
+              ρ₁ , s₁ ⇒ˢ ρ₂ → ρ₂ , s₂ ⇒ˢ ρ₃ →
+              ρ₁ , (s₁ then s₂) ⇒ˢ ρ₃
+    ⇒ˢ-if-true : ∀ (ρ₁ ρ₂ : Env) (e : Expr) (z : ℤ) (s₁ s₂ : Stmt) →
+        ρ₁ , e ⇒ᵉ (↑ᶻ z) → ¬ z ≡ (+ 0) → ρ₁ , s₁ ⇒ˢ ρ₂ →
+        ρ₁ , (if e then s₁ else s₂) ⇒ˢ ρ₂
+    ⇒ˢ-if-false : ∀ (ρ₁ ρ₂ : Env) (e : Expr) (s₁ s₂ : Stmt) →
+        ρ₁ , e ⇒ᵉ (↑ᶻ (+ 0)) → ρ₁ , s₂ ⇒ˢ ρ₂ →
+        ρ₁ , (if e then s₁ else s₂) ⇒ˢ ρ₂
+    ⇒ˢ-while-true : ∀ (ρ₁ ρ₂ ρ₃ : Env) (e : Expr) (z : ℤ) (s : Stmt) →
+        ρ₁ , e ⇒ᵉ (↑ᶻ z) → ¬ z ≡ (+ 0) → ρ₁ , s ⇒ˢ ρ₂ → ρ₂ , (while e repeat s) ⇒ˢ ρ₃ →
+        ρ₁ , (while e repeat s) ⇒ˢ ρ₃
+    ⇒ˢ-while-false : ∀ (ρ : Env) (e : Expr) (s : Stmt) →
+        ρ , e ⇒ᵉ (↑ᶻ (+ 0)) →
+        ρ , (while e repeat s) ⇒ˢ ρ
+
+record LatticeInterpretation {l} {L : Set l} {_≈_ : L → L → Set l}
+                             {_⊔_ : L → L → L} {_⊓_ : L → L → L}
+                             (isLattice : IsLattice L _≈_ _⊔_ _⊓_) : Set (lsuc l) where
+    field
+        ⟦_⟧ : L → Value → Set
+        ⟦⟧-respects-≈ : ∀ {l₁ l₂ : L} → l₁ ≈ l₂ → ⟦ l₁ ⟧ ⇒ ⟦ l₂ ⟧
+        ⟦⟧-⊔-∨ : ∀ {l₁ l₂ : L} → (⟦ l₁ ⟧ ∨ ⟦ l₂ ⟧) ⇒ ⟦ l₁ ⊔ l₂ ⟧
+        ⟦⟧-⊓-∧ : ∀ {l₁ l₂ : L} → (⟦ l₁ ⟧ ∧ ⟦ l₂ ⟧) ⇒ ⟦ l₁ ⊓ l₂ ⟧

Language/Traces.agda

@@ -0,0 +1,36 @@
+module Language.Traces where
+
+open import Language.Base
+open import Language.Semantics using (Env; _,_⇒ᵇˢ_)
+open import Language.Graphs
+
+open import Data.Product using (_,_)
+open import Data.List.Membership.Propositional using (_∈_)
+
+module _ {g : Graph} where
+    open Graph g using (Index; edges; inputs; outputs)
+
+    data Trace : Index → Index → Env → Env → Set where
+        Trace-single : ∀ {ρ₁ ρ₂ : Env} {idx : Index} →
+                       ρ₁ , (g [ idx ]) ⇒ᵇˢ ρ₂ → Trace idx idx ρ₁ ρ₂
+        Trace-edge : ∀ {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : Index} →
+                     ρ₁ , (g [ idx₁ ]) ⇒ᵇˢ ρ₂ → (idx₁ , idx₂) ∈ edges →
+                     Trace idx₂ idx₃ ρ₂ ρ₃ → Trace idx₁ idx₃ ρ₁ ρ₃
+
+    infixr 5 _++⟨_⟩_
+    _++⟨_⟩_ : ∀ {idx₁ idx₂ idx₃ idx₄ : Index} {ρ₁ ρ₂ ρ₃ : Env} →
+           Trace idx₁ idx₂ ρ₁ ρ₂ → (idx₂ , idx₃) ∈ edges →
+           Trace idx₃ idx₄ ρ₂ ρ₃ → Trace idx₁ idx₄ ρ₁ ρ₃
+    _++⟨_⟩_ (Trace-single ρ₁⇒ρ₂) idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₂→idx₃ tr
+    _++⟨_⟩_ (Trace-edge ρ₁⇒ρ₂ idx₁→idx' tr') idx₂→idx₃ tr = Trace-edge ρ₁⇒ρ₂ idx₁→idx' (tr' ++⟨ idx₂→idx₃ ⟩ tr)
+
+    record EndToEndTrace (ρ₁ ρ₂ : Env) : Set where
+        constructor MkEndToEndTrace
+        field
+            idx₁ : Index
+            idx₁∈inputs : idx₁ ∈ inputs
+
+            idx₂ : Index
+            idx₂∈outputs : idx₂ ∈ outputs
+
+            trace : Trace idx₁ idx₂ ρ₁ ρ₂

Lattice.agda

@@ -137,7 +137,7 @@ module _ {a b} {A : Set a} {B : Set b}
     const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
     const-Mono x _ = ⊔₂-idemp x
 
-    open import Data.List as List using (List; foldr; _∷_)
+    open import Data.List as List using (List; foldr; foldl; _∷_)
     open import Utils using (Pairwise; _∷_)
 
     foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
@@ -150,6 +150,36 @@ module _ {a b} {A : Set a} {B : Set b}
         ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
                  (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
 
+    foldl-Mono : ∀ (l₁ l₂ : List A) (f : B → A → B) (b₁ b₂ : B) →
+                 Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
+                 (∀ a → Monotonic _≼₂_ _≼₂_ (λ b → f b a)) →
+                 (∀ b → Monotonic _≼₁_ _≼₂_ (f b)) →
+                 foldl f b₁ l₁ ≼₂ foldl f b₂ l₂
+    foldl-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
+    foldl-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
+        foldl-Mono xs ys f (f b₁ x) (f b₂ y) xs≼ys (≼₂-trans (f-Mono₁ x b₁≼b₂) (f-Mono₂ b₂ x≼y)) f-Mono₁ f-Mono₂
+
+module _ {a b} {A : Set a} {B : Set b}
+         {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
+         (lB : IsSemilattice B _≈₂_ _⊔₂_) where
+
+    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
+
+    open import Data.List as List using (List; foldr; foldl; _∷_)
+    open import Utils using (Pairwise; _∷_)
+
+    foldr-Mono' : ∀ (l : List A) (f : A → B → B) →
+                  (∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
+                  Monotonic _≼₂_ _≼₂_ (λ b → foldr f b l)
+    foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
+    foldr-Mono' (x ∷ xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂)
+
+    foldl-Mono' : ∀ (l : List A) (f : B → A → B) →
+                  (∀ b → Monotonic _≼₂_ _≼₂_ (λ a → f a b)) →
+                  Monotonic _≼₂_ _≼₂_ (λ b → foldl f b l)
+    foldl-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
+    foldl-Mono' (x ∷ xs) f f-Mono₁ b₁≼b₂ = foldl-Mono' xs f f-Mono₁ (f-Mono₁ x b₁≼b₂)
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)

Lattice/AboveBelow.agda

@@ -355,7 +355,12 @@ module Plain (x : A) where
         rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
 
     fixedHeight : IsLattice.FixedHeight isLattice 2
-    fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
+    fixedHeight = record
+        { ⊥ = ⊥
+        ; ⊤ = ⊤
+        ; longestChain = longestChain
+        ; bounded = isLongest
+        }
 
     isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record

Lattice/FiniteMap.agda

@@ -12,7 +12,7 @@ module Lattice.FiniteMap {a b : Level} {A : Set a} {B : Set b}
 
 open IsLattice lB using () renaming (_≼_ to _≼₂_)
 open import Lattice.Map ≡-dec-A lB as Map
-    using (Map; ⊔-equal-keys; ⊓-equal-keys; ∈k-dec)
+    using (Map; ⊔-equal-keys; ⊓-equal-keys)
     renaming
         ( _≈_ to _≈ᵐ_
         ; _⊔_ to _⊔ᵐ_
@@ -30,13 +30,21 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
         ; ≈-dec to ≈ᵐ-dec
         ; _[_] to _[_]ᵐ
+        ; []-∈ to []ᵐ-∈
         ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
+        ; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ to m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ
         ; locate to locateᵐ
         ; keys to keysᵐ
         ; _updating_via_ to _updatingᵐ_via_
         ; updating-via-keys-≡ to updatingᵐ-via-keys-≡
+        ; updating-via-k∈ks to updatingᵐ-via-k∈ks
+        ; updating-via-k∈ks-≡ to updatingᵐ-via-k∈ks-≡
+        ; updating-via-∈k-forward to updatingᵐ-via-∈k-forward
+        ; updating-via-k∉ks-forward to updatingᵐ-via-k∉ks-forward
+        ; updating-via-k∉ks-backward to updatingᵐ-via-k∉ks-backward
         ; f'-Monotonic to f'-Monotonicᵐ
         ; _≼_ to _≼ᵐ_
+        ; ∈k-dec to ∈k-decᵐ
         )
 open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
@@ -82,6 +90,10 @@ module WithKeys (ks : List A) where
     _∈k_ : A → FiniteMap → Set a
     _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
 
+    open Map using (forget) public
+
+    ∈k-dec = ∈k-decᵐ
+
     locate : ∀ {k : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm)
     locate {k} {fm = (m , _)} k∈kfm = locateᵐ {k} {m} k∈kfm
 
@@ -94,6 +106,10 @@ module WithKeys (ks : List A) where
     _[_] : FiniteMap → List A → List B
     _[_] (m₁ , _) ks = m₁ [ ks ]ᵐ
 
+    []-∈ : ∀ {k : A} {v : B} {ks' : List A} (fm : FiniteMap) →
+           k ∈ˡ ks' → (k , v) ∈ fm → v ∈ˡ (fm [ ks' ])
+    []-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks' 
+
     ≈-equiv : IsEquivalence FiniteMap _≈_
     ≈-equiv = record
         { ≈-refl =
@@ -149,6 +165,11 @@ module WithKeys (ks : List A) where
                         fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂
     m₁≼m₂⇒m₁[k]≼m₂[k] (m₁ , _) (m₂ , _) m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
 
+    m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (fm₁ fm₂ : FiniteMap) {k : A} →
+                             fm₁ ≈ fm₂ → ∀ (k∈kfm₁ : k ∈k fm₁) (k∈kfm₂ : k ∈k fm₂) →
+                             proj₁ (locate {fm = fm₁} k∈kfm₁) ≈₂ proj₁ (locate {fm = fm₂} k∈kfm₂)
+    m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ (m₁ , _) (m₂ , _) = m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ m₁ m₂
+
     module GeneralizedUpdate
              {l} {L : Set l}
              {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
@@ -168,6 +189,21 @@ module WithKeys (ks : List A) where
         f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
         f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
 
+        f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l)
+        f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)
+
+        f'-k∈ks : ∀ {k l} → k ∈ˡ ks → k ∈k (f' l) → (k , updater l k) ∈ (f' l)
+        f'-k∈ks {k} {l} = updatingᵐ-via-k∈ks (proj₁ (f l)) (updater l)
+
+        f'-k∈ks-≡ : ∀ {k v l} → k ∈ˡ ks → (k , v) ∈ (f' l) → v ≡ updater l k
+        f'-k∈ks-≡ {k} {v} {l} = updatingᵐ-via-k∈ks-≡ (proj₁ (f l)) (updater l)
+
+        f'-k∉ks-forward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f l) → (k , v) ∈ (f' l)
+        f'-k∉ks-forward {k} {v} {l} = updatingᵐ-via-k∉ks-forward (proj₁ (f l)) (updater l)
+
+        f'-k∉ks-backward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f' l) → (k , v) ∈ (f l)
+        f'-k∉ks-backward {k} {v} {l} = updatingᵐ-via-k∉ks-backward (proj₁ (f l)) (updater l)
+
     all-equal-keys : ∀ (fm₁ fm₂ : FiniteMap) → (Map.keys (proj₁ fm₁) ≡ Map.keys (proj₁ fm₂))
     all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)
 
@@ -182,7 +218,7 @@ module WithKeys (ks : List A) where
                           fm₁ ≼ fm₂ → Pairwise _≼₂_ (fm₁ [ ks' ]) (fm₂ [ ks' ])
     m₁≼m₂⇒m₁[ks]≼m₂[ks] _ _ [] _ = []
     m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁@(m₁ , km₁≡ks) fm₂@(m₂ , km₂≡ks) (k ∷ ks'') m₁≼m₂
-        with ∈k-dec k (proj₁ m₁) | ∈k-dec k (proj₁ m₂)
+        with ∈k-decᵐ k (proj₁ m₁) | ∈k-decᵐ k (proj₁ m₂)
     ...   | yes k∈km₁ | yes k∈km₂ =
             let
                 (v₁ , k,v₁∈m₁) = locateᵐ {m = m₁} k∈km₁

Lattice/FiniteValueMap.agda

@@ -28,11 +28,12 @@ open import Data.List.Relation.Unary.All using (All)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Relation.Nullary using (¬_)
 open import Isomorphism using (IsInverseˡ; IsInverseʳ)
+open import Chain using (Height)
 
 open import Lattice.Map ≡-dec-A lB
     using
         ( subset-impl
-        ; locate; forget
+        ; locate
         ; Map-functional
         ; Expr-Provenance
         ; Expr-Provenance-≡
@@ -104,6 +105,14 @@ module IterProdIsomorphism where
         _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
         _∈ᵐ_ {ks} = _∈_ ks
 
+    to-build : ∀ {b : B} {ks : List A} (uks : Unique ks) →
+               let fm = to uks (IP.build b tt (length ks))
+               in ∀ (k : A) (v : B) → (k , v) ∈ᵐ fm → v ≡ b
+    to-build {b} {k ∷ ks'} (push _ uks') k v (here refl) = refl
+    to-build {b} {k ∷ ks'} (push _ uks') k' v (there k',v∈m') =
+        to-build {ks = ks'} uks' k' v k',v∈m'
+
+
     -- The left inverse is: from (to x) = x
     from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
                       IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
@@ -153,6 +162,26 @@ module IterProdIsomorphism where
                                 fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
                         in (v'' , (v'≈v'' , there k',v''∈fm'₁))
 
+    FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set
+    FromBothMaps k v fm₁ fm₂ =
+        Σ (B × B)
+          (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
+
+    Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
+                       (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂
+    Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
+        with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
+    ...   | in₁ (single k,v∈m₁) k∉km₂
+            with k∈km₁ ← (forget k,v∈m₁)
+            rewrite trans ks₁≡ks (sym ks₂≡ks) =
+            ⊥-elim (k∉km₂ k∈km₁)
+    ...   | in₂ k∉km₁ (single k,v∈m₂)
+            with k∈km₂ ← (forget k,v∈m₂)
+            rewrite trans ks₁≡ks (sym ks₂≡ks) =
+            ⊥-elim (k∉km₁ k∈km₂)
+    ...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
+            ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
+
     private
         first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) →
                            Σ B (λ v → (k , v) ∈ᵐ fm)
@@ -204,26 +233,6 @@ module IterProdIsomorphism where
         k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
         k,v∈⇒k,v∈pop (m@(_ ∷ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm'
 
-        FromBothMaps : ∀ (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) → Set
-        FromBothMaps k v fm₁ fm₂ =
-            Σ (B × B)
-              (λ (v₁ , v₂) → ( (v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
-
-        Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
-                           (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂
-        Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
-            with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
-        ...   | in₁ (single k,v∈m₁) k∉km₂
-                with k∈km₁ ← (forget k,v∈m₁)
-                rewrite trans ks₁≡ks (sym ks₂≡ks) =
-                ⊥-elim (k∉km₂ k∈km₁)
-        ...   | in₂ k∉km₁ (single k,v∈m₂)
-                with k∈km₂ ← (forget k,v∈m₂)
-                rewrite trans ks₁≡ks (sym ks₂≡ks) =
-                ⊥-elim (k∉km₁ k∈km₂)
-        ...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
-                ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
-
         pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →
                       pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
         pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) =
@@ -407,3 +416,12 @@ module IterProdIsomorphism where
             (to-⊔-distr uks) (from-⊔-distr {ks})
             (from-to-inverseʳ uks) (from-to-inverseˡ uks)
             using (isFiniteHeightLattice; finiteHeightLattice) public
+
+        -- Helpful lemma: all entries of the 'bottom' map are assigned to bottom.
+
+        open Height (IsFiniteHeightLattice.fixedHeight isFiniteHeightLattice) using (⊥)
+
+        ⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB)
+        ⊥-contains-bottoms {k} {v} k,v∈⊥
+            rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ =
+            to-build uks k v k,v∈⊥

Lattice/IterProd.agda

@@ -11,9 +11,11 @@ module Lattice.IterProd {a} {A B : Set a}
     (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
 open import Agda.Primitive using (lsuc)
-open import Data.Nat using (ℕ; suc; _+_)
+open import Data.Nat using (ℕ; zero; suc; _+_)
-open import Data.Product using (_×_)
+open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
 open import Utils using (iterate)
+open import Chain using (Height)
 
 open IsLattice lA renaming (FixedHeight to FixedHeight₁)
 open IsLattice lB renaming (FixedHeight to FixedHeight₂)
@@ -30,31 +32,50 @@ IterProd k = iterate k (λ t → A × t) B
 -- that are built up by the two iterations. So, do everything in one iteration.
 -- This requires some odd code.
 
+build : A → B → (k : ℕ) → IterProd k
+build _ b zero = b
+build a b (suc s) = (a , build a b s)
+
 private
     record RequiredForFixedHeight : Set (lsuc a) where
-         field
+        field
             ≈₁-dec : IsDecidable _≈₁_
             ≈₂-dec : IsDecidable _≈₂_
             h₁ h₂ : ℕ
             fhA : FixedHeight₁ h₁
             fhB : FixedHeight₂ h₂
 
-    record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where
+        ⊥₁ : A
+        ⊥₁ = Height.⊥ fhA
+
+        ⊥₂ : B
+        ⊥₂ = Height.⊥ fhB
+
+        ⊥k : ∀ (k : ℕ) → IterProd k
+        ⊥k = build ⊥₁ ⊥₂
+
+    record IsFiniteHeightWithBotAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) (⊥ : A) : Set (lsuc a) where
         field
             height : ℕ
             fixedHeight : IsLattice.FixedHeight isLattice height
             ≈-dec : IsDecidable _≈_
 
-    record Everything (A : Set a) : Set (lsuc a) where
+            ⊥-correct : Height.⊥ fixedHeight ≡ ⊥
+
+    record Everything (k : ℕ) : Set (lsuc a) where
+        T = IterProd k
+
         field
-            _≈_ : A → A → Set a
+            _≈_ : T → T → Set a
-            _⊔_ : A → A → A
+            _⊔_ : T → T → T
-            _⊓_ : A → A → A
+            _⊓_ : T → T → T
 
-            isLattice : IsLattice A _≈_ _⊔_ _⊓_
+            isLattice : IsLattice T _≈_ _⊔_ _⊓_
-            isFiniteHeightIfSupported : RequiredForFixedHeight → IsFiniteHeightAndDecEq isLattice
+            isFiniteHeightIfSupported :
+                ∀ (req : RequiredForFixedHeight) →
+                IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)
 
-    everything : ∀ (k : ℕ) → Everything (IterProd k)
+    everything : ∀ (k : ℕ) → Everything k
     everything 0 = record
         { _≈_ = _≈₂_
         ; _⊔_ = _⊔₂_
@@ -64,6 +85,7 @@ private
             { height = RequiredForFixedHeight.h₂ req
             ; fixedHeight = RequiredForFixedHeight.fhB req
             ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
+            ; ⊥-correct = refl
             }
         }
     everything (suc k') = record
@@ -76,13 +98,16 @@ private
                 fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
             in
                 record
-                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
+                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
                     ; fixedHeight =
                         P.fixedHeight
-                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
+                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
-                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
+                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
-                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
+                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
-                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
+                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
+                    ; ⊥-correct =
+                        cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
+                             (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
                     }
         }
         where
@@ -121,16 +146,22 @@ module _ (k : ℕ) where
                 ; fhB = fhB
                 }
 
+        fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
+
         isFiniteHeightLattice = record
             { isLattice = isLattice
-            ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
+            ; fixedHeight = fixedHeight
             }
 
         finiteHeightLattice : FiniteHeightLattice (IterProd k)
         finiteHeightLattice = record
-            { height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
+            { height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
             ; _≈_ = _≈_
             ; _⊔_ = _⊔_
             ; _⊓_ = _⊓_
             ; isFiniteHeightLattice = isFiniteHeightLattice
             }
+
+        ⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
+        ⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required)
+

Lattice/Map.agda

@@ -1112,6 +1112,19 @@ _[_] m (k ∷ ks)
 ...   | yes k∈km = proj₁ (locate {m = m} k∈km) ∷ (m [ ks ])
 ...   | no _ = m [ ks ]
 
+[]-∈ : ∀ {k : A} {v : B} {ks : List A} (m : Map) →
+       (k , v) ∈ m → k ∈ˡ ks → v ∈ˡ (m [ ks ])
+[]-∈ {k} {v} {ks} m k,v∈m (here refl)
+    with ∈k-dec k (proj₁ m)
+...    | no k∉km = ⊥-elim (k∉km (forget k,v∈m))
+...    | yes k∈km
+         with (v' , k,v'∈m) ← locate {m = m} k∈km
+         rewrite Map-functional {m = m} k,v'∈m k,v∈m = here refl
+[]-∈ {k} {v} {k' ∷ ks'} m k,v∈m (there k∈ks')
+    with ∈k-dec k' (proj₁ m)
+...   | no _  = []-∈ m k,v∈m k∈ks'
+...   | yes _ = there ([]-∈ m k,v∈m k∈ks')
+
 m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (m₁ m₂ : Map) {k : A} {v₁ v₂ : B} →
                     m₁ ≼ m₂ → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → v₁ ≼₂ v₂
 m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
@@ -1129,3 +1142,12 @@ m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
         (v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
     in
         forget k,v'∈m₂
+
+m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : ∀ (m₁ m₂ : Map) {k : A} →
+                         m₁ ≈ m₂ → ∀ (k∈km₁ : k ∈k m₁) (k∈km₂ : k ∈k m₂) →
+                         proj₁ (locate {m = m₁} k∈km₁) ≈₂ proj₁ (locate {m = m₂} k∈km₂)
+m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ m₁ m₂ {k} (m₁⊆m₂ , m₂⊆m₁) k∈km₁ k∈km₂
+    with (v₁ , k,v₁∈m₁) ← locate {m = m₁} k∈km₁
+    with (v₂ , k,v₂∈m₂) ← locate {m = m₂} k∈km₂
+    with (v₂' , (v₁≈v₂' , k,v₂'∈m₂)) ← m₁⊆m₂ k v₁ k,v₁∈m₁
+    rewrite Map-functional {m = m₂} k,v₂∈m₂ k,v₂'∈m₂ = v₁≈v₂'

Lattice/Prod.agda

@@ -143,17 +143,8 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
         ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
         ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
 
-        amin : A
+        open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
-        amin = proj₁ (proj₁ (proj₁ fhA))
+        open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
-
-        amax : A
-        amax = proj₂ (proj₁ (proj₁ fhA))
-
-        bmin : B
-        bmin = proj₁ (proj₁ (proj₁ fhB))
-
-        bmax : B
-        bmax = proj₂ (proj₁ (proj₁ fhB))
 
         unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
         unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
@@ -172,15 +163,16 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                                      ))
 
     fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
-    fixedHeight =
+    fixedHeight = record
-      ( ( ((amin , bmin) , (amax , bmax))
+      { ⊥ = (⊥₁ , ⊥₂)
-        , concat
+      ; ⊤ = (⊤₁ , ⊤₂)
-            (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
+      ; longestChain = concat
-            (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
+            (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
-        )
+            (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
-      , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
+      ; bounded = λ a₁b₁a₂b₂ →
-                     in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
+            let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
-      )
+            in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
+      }
 
     isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record

Lattice/Unit.agda

@@ -108,7 +108,12 @@ private
     isLongest (done _) = z≤n
 
 fixedHeight : IsLattice.FixedHeight isLattice 0
-fixedHeight = (((tt , tt) , longestChain) , isLongest)
+fixedHeight = record
+    { ⊥ = tt
+    ; ⊤ = tt
+    ; longestChain = longestChain
+    ; bounded = isLongest
+    }
 
 isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
 isFiniteHeightLattice = record

Main.agda

@@ -1,3 +1,4 @@
+{-# OPTIONS --guardedness #-}
 module Main where
 
 open import Language
@@ -6,20 +7,37 @@ open import Data.Vec using (Vec; _∷_; [])
 open import IO
 open import Level using (0ℓ)
 
-testCode : Vec Stmt _
+testCode : Stmt
 testCode =
-    ("zero" ← (# 0)) ∷
+    ⟨ "zero" ← (# 0) ⟩ then
-    ("pos" ← ((` "zero") Expr.+ (# 1))) ∷
+    ⟨ "pos" ← ((` "zero") Expr.+ (# 1)) ⟩ then
-    ("neg" ← ((` "zero") Expr.- (# 1))) ∷
+    ⟨ "neg" ← ((` "zero") Expr.- (# 1)) ⟩ then
-    ("unknown" ← ((` "pos") Expr.+ (` "neg"))) ∷
+    ⟨ "unknown" ← ((` "pos") Expr.+ (` "neg")) ⟩
-    []
+
+testCodeCond₁ : Stmt
+testCodeCond₁ =
+    ⟨ "var" ← (# 1) ⟩ then
+    if (` "var") then (
+        ⟨ "var" ← ((` "var") Expr.+ (# 1)) ⟩
+    ) else (
+        ⟨ "var" ← ((` "var") Expr.- (# 1)) ⟩ then
+        ⟨ "var" ← (# 1) ⟩
+    )
+
+testCodeCond₂ : Stmt
+testCodeCond₂ =
+    ⟨ "var" ← (# 1) ⟩ then
+    if (` "var") then (
+        ⟨ "x" ← (# 1) ⟩
+    ) else (
+        ⟨ noop ⟩
+    )
 
 testProgram : Program
 testProgram = record
-    { length = _
+    { rootStmt = testCode
-    ; stmts = testCode
     }
 
-open WithProg testProgram using (output)
+open WithProg testProgram using (output; analyze-correct)
 
 main = run {0ℓ} (putStrLn output)

Utils.agda

@@ -1,14 +1,18 @@
 module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
+open import Data.Product as Prod using (_×_)
 open import Data.Nat using (ℕ; suc)
-open import Data.List using (List; []; _∷_; _++_) renaming (map to mapˡ)
+open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ)
 open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
 open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
 open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
+open import Data.Sum using (_⊎_)
 open import Function.Definitions using (Injective)
-open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
+open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Unary using (Decidable)
 
 data Unique {c} {C : Set c} : List C → Set c where
     empty : Unique []
@@ -68,3 +72,34 @@ data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List
     _∷_ : ∀ {x : A} {y : B} {xs : List A} {ys : List B} →
           P x y → Pairwise P xs ys →
           Pairwise P (x ∷ xs) (y ∷ ys)
+
+∈-cartesianProduct : ∀ {a b} {A : Set a} {B : Set b}
+                     {x : A} {xs : List A} {y : B} {ys : List B} →
+                     x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys
+∈-cartesianProduct {x = x} (here refl) y∈ys = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (x Prod.,_) y∈ys)
+∈-cartesianProduct {x = x} {xs = x' ∷ _} {ys = ys} (there x∈rest) y∈ys = ListMemProp.∈-++⁺ʳ (mapˡ (x' Prod.,_) ys) (∈-cartesianProduct x∈rest y∈ys)
+
+concat-∈ : ∀ {a} {A : Set a} {x : A} {l : List A} {ls : List (List A)} →
+           x ∈ l → l ∈ ls → x ∈ foldr _++_ [] ls
+concat-∈ x∈l (here refl) = ListMemProp.∈-++⁺ˡ x∈l
+concat-∈ {ls = l' ∷ ls'} x∈l (there l∈ls') = ListMemProp.∈-++⁺ʳ l' (concat-∈ x∈l l∈ls')
+
+filter-++ : ∀ {a p} {A : Set a} (l₁ l₂ : List A) {P : A → Set p} (P? : Decidable P) →
+            filter P? (l₁ ++ l₂) ≡ filter P? l₁ ++ filter P? l₂
+filter-++ [] l₂ P? = refl
+filter-++ (x ∷ xs) l₂ P?
+    with P? x
+...   | yes _ = cong (x ∷_) (filter-++ xs l₂ P?)
+...   | no _ = (filter-++ xs l₂ P?)
+
+_⇒_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
+      Set (a ⊔ℓ p₁ ⊔ℓ p₂)
+_⇒_ P Q = ∀ a → P a → Q a
+
+_∨_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
+      A → Set (p₁ ⊔ℓ p₂)
+_∨_ P Q a = P a ⊎ Q a
+
+_∧_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
+      A → Set (p₁ ⊔ℓ p₂)
+_∧_ P Q a = P a × Q a