------------------------------------------------------------------------ -- Definitional interpreters can model systems with bounded space ------------------------------------------------------------------------ -- In "Reasoning on Divergent Computations with Coaxioms" Ancona, -- Dagnino and Zucca write the following: -- -- "To assess the applicability and generality of our approach much -- work is still needed. We are currently considering to apply -- coaxioms to other kinds of semantics; in particular, trace -- semantics seems particularly interesting for investigating -- whether our approach is suitable for formalizing and proving -- important safety properties of non terminating programs, as -- ensuring that a server will never try to use infinite resources. -- Other approaches based on definitional interpreters [Danielsson -- 2012], and the adoption of step counters [Amin and Rompf 2017; -- Ancona 2014; Ernst et al. 2006; Owens et al. 2016] seem to be -- appealing for proving type soundness properties with big-step -- semantics, and other results concerning program equivalence; -- however, it is not clear whether these solutions work well for -- other kinds of properties. For instance, if a program consists of -- an infinite loop that allocates new heap space at each step -- without releasing it, one would like to conclude that it will -- eventually crash even though a definitional interpreter returns -- timeout for all possible values of the step counter." -- -- This is an attempt to show that definitional interpreters can -- handle this situation. {-# OPTIONS --without-K --safe #-} module Bounded-space where open import Colist open import Equality.Propositional open import Prelude open import Tactic.By open import Nat equality-with-J open import Delay-monad open import Delay-monad.Bisimilarity as B hiding (reflexive; symmetric) open import Only-allocation ------------------------------------------------------------------------ -- Heaps -- Bounded heaps. (Only a size, plus a proof showing that the size is -- bounded.) record Heap (limit : ℕ) : Set where field size : ℕ bound : size ≤ limit open Heap public -- An empty heap. empty : ∀ {l} → Heap l empty = record { size = zero; bound = zero≤ _ } -- A full heap. full : ∀ l → Heap l full l = record { size = l; bound = ≤-refl } -- Reduces the heap's size by one. If the heap is empty, then it is -- returned unchanged. shrink : ∀ {l} → Heap l → Heap l shrink {l} h = record { size = pred (h .size) ; bound = pred (h .size) ≤⟨ pred≤ _ ⟩ h .size ≤⟨ h .bound ⟩∎ l ∎≤ } -- Increases the heap's size by one. If the heap already has the -- maximum size, then nothing is returned. grow : ∀ {l} → Heap l → Maybe (Heap l) grow {l} h with l ≤⊎> h .size ... | inj₁ _ = nothing ... | inj₂ h<l = just (record { size = suc (h .size) ; bound = h<l }) -- Lemmas related to grow. grow-full : ∀ {l} (h : Heap l) → h .size ≡ l → grow h ≡ nothing grow-full {l} h h≡l with l ≤⊎> h .size ... | inj₁ _ = refl ... | inj₂ h<l = ⊥-elim (+≮ 0 ( 1 + h .size ≤⟨ h<l ⟩ l ≡⟨ sym h≡l ⟩≤ h .size ∎≤)) grow-not-full : ∀ {l} (h : Heap l) → h .size < l → ∃ λ h′ → grow h ≡ just h′ × h′ .size ≡ 1 + h .size grow-not-full {l} h h<l with l ≤⊎> h .size ... | inj₂ _ = _ , refl , refl ... | inj₁ l≤h = ⊥-elim (+≮ 0 ( 1 + h .size ≤⟨ h<l ⟩ l ≤⟨ l≤h ⟩∎ h .size ∎≤)) ------------------------------------------------------------------------ -- Definitional interpreter -- One step of computation. step : ∀ {l} → Stmt → Heap l → Maybe (Heap l) step dealloc heap = just (shrink heap) step alloc heap = grow heap -- A crashing computation. crash : ∀ {i l} → Delay (Maybe (Heap l)) i crash = now nothing -- A definitional interpreter. ⟦_⟧ : ∀ {i l} → Program i → Heap l → Delay (Maybe (Heap l)) i ⟦ [] ⟧ heap = now (just heap) ⟦ s ∷ p ⟧ heap with step s heap ... | nothing = crash ... | just new-heap = later λ { .force → ⟦ p .force ⟧ new-heap } ------------------------------------------------------------------------ -- A program equivalence -- An equivalence relation that identifies programs that, given a -- sufficient amount of memory, behave identically (up to weak -- bisimilarity). infix 4 [_]_≃_ [_]_≃′_ [_]_≃_ : Size → Program ∞ → Program ∞ → Set [ i ] p ≃ q = ∃ λ c → ∀ l (h : Heap l) → c + h .size ≤ l → [ i ] ⟦ p ⟧ h ≈ ⟦ q ⟧ h [_]_≃′_ : Size → Program ∞ → Program ∞ → Set [ i ] p ≃′ q = ∃ λ c → ∀ l (h : Heap l) → c + h .size ≤ l → [ i ] ⟦ p ⟧ h ≈′ ⟦ q ⟧ h -- The relation is an equivalence relation. reflexive : ∀ {i} p → [ i ] p ≃ p reflexive _ = 0 , λ _ _ _ → B.reflexive _ symmetric : ∀ {i p q} → [ i ] p ≃ q → [ i ] q ≃ p symmetric = Σ-map id λ hyp l h c → B.symmetric (hyp l h c) transitive : ∀ {i p q r} → [ ∞ ] p ≃ q → [ ∞ ] q ≃ r → [ i ] p ≃ r transitive {p = p} {q} {r} (c₁ , p₁) (c₂ , p₂) = max c₁ c₂ , λ l h c → ⟦ p ⟧ h ≈⟨ p₁ l h (lemma₁ l h c) ⟩ ⟦ q ⟧ h ≈⟨ p₂ l h (lemma₂ l h c) ⟩∎ ⟦ r ⟧ h ∎ where lemma₁ = λ l h c → c₁ + h .size ≤⟨ ˡ≤max c₁ _ +-mono ≤-refl ⟩ max c₁ c₂ + h .size ≤⟨ c ⟩∎ l ∎≤ lemma₂ = λ l h c → c₂ + h .size ≤⟨ ʳ≤max c₁ _ +-mono ≤-refl ⟩ max c₁ c₂ + h .size ≤⟨ c ⟩∎ l ∎≤ -- The relation is compatible with respect to the program formers. []-cong : ∀ {i} → [ i ] [] ≃ [] []-cong = reflexive [] ∷-cong : ∀ {s p q i} → [ i ] p .force ≃′ q .force → [ i ] s ∷ p ≃ s ∷ q ∷-cong {dealloc} (c , p≈q) = c , λ l h c≤ → later λ { .force → p≈q l (shrink h) ( c + shrink h .size ≤⟨ ≤-refl {n = c} +-mono pred≤ _ ⟩ c + h .size ≤⟨ c≤ ⟩ l ∎≤) .force } ∷-cong {alloc} {p} {q} {i} (c , p≈q) = 1 + c , lemma where lemma : ∀ l (h : Heap l) → 1 + c + h .size ≤ l → [ i ] ⟦ alloc ∷ p ⟧ h ≈ ⟦ alloc ∷ q ⟧ h lemma l h 1+c≤ with l ≤⊎> h .size ... | inj₁ _ = now ... | inj₂ h<l = later λ { .force → p≈q l _ ( c + (1 + h .size) ≡⟨ +-assoc c ⟩≤ c + 1 + h .size ≡⟨ by (+-comm c) ⟩≤ 1 + c + h .size ≤⟨ 1+c≤ ⟩∎ l ∎≤) .force } ------------------------------------------------------------------------ -- Some examples -- The program bounded crashes when the heap is full. bounded-crash : ∀ {i l} (h : Heap l) → h .size ≡ l → [ i ] ⟦ bounded ⟧ h ≈ crash bounded-crash h h≡l rewrite grow-full h h≡l = now -- However, for smaller heaps the program loops. bounded-loop : ∀ {i l} (h : Heap l) → h .size < l → [ i ] ⟦ bounded ⟧ h ≈ never bounded-loop {l = l} h <l with grow h | grow-not-full h <l ... | .(just h′) | h′ , refl , refl = later λ { .force → later λ { .force → bounded-loop _ <l }} -- The program bounded₂ loops when there are at least two empty slots -- in the heap. bounded₂-loop : ∀ {i l} (h : Heap l) → 2 + h .size ≤ l → [ i ] ⟦ bounded₂ ⟧ h ≈ never bounded₂-loop {i} {l} h 2+h≤l with grow h | grow-not-full h (<→≤ 2+h≤l) ... | .(just h′) | h′ , refl , refl = later λ { .force → lemma } where lemma : [ i ] ⟦ force (tail bounded₂) ⟧ h′ ≈ never lemma with grow h′ | grow-not-full h′ 2+h≤l lemma | .(just h″) | h″ , refl , refl = later λ { .force → later λ { .force → later λ { .force → bounded₂-loop _ 2+h≤l }}} -- The program unbounded crashes for all heaps. unbounded-crash : ∀ {i l} (h : Heap l) → [ i ] ⟦ unbounded ⟧ h ≈ crash unbounded-crash {l = l} h = helper h (≤→≤↑ (h .bound)) where helper : ∀ {i} (h′ : Heap l) → size h′ ≤↑ l → [ i ] ⟦ unbounded ⟧ h′ ≈ crash helper h′ (≤↑-refl h′≡l) rewrite grow-full h′ h′≡l = now helper h′ (≤↑-step 1+h′≤l) with grow h′ | grow-not-full h′ (≤↑→≤ 1+h′≤l) ... | .(just h″) | h″ , refl , refl = laterˡ (helper h″ 1+h′≤l) -- The programs bounded and bounded₂ are ≃-equivalent. bounded≃bounded₂ : [ ∞ ] bounded ≃ bounded₂ bounded≃bounded₂ = 2 , λ l h 2+h≤l → ⟦ bounded ⟧ h ≈⟨ bounded-loop _ (<→≤ 2+h≤l) ⟩ never ≈⟨ B.symmetric (bounded₂-loop _ 2+h≤l) ⟩∎ ⟦ bounded₂ ⟧ h ∎ -- The programs bounded and unbounded are not ≃-equivalent. ¬bounded≃unbounded : ¬ [ ∞ ] bounded ≃ unbounded ¬bounded≃unbounded (c , c≈u) = now≉never ( crash ≈⟨ B.symmetric (unbounded-crash h) ⟩ ⟦ unbounded ⟧ h ≈⟨ B.symmetric (c≈u _ h (≤-refl +-mono zero≤ _)) ⟩ ⟦ bounded ⟧ h ≈⟨ bounded-loop h (m≤n+m _ _) ⟩∎ never ∎) where h : Heap (c + 1) h = record { size = 0 ; bound = zero≤ _ }