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⇒ρ)