Browse Source

Fix unsolved meta.

gas-move-test
Thomas Kerber 6 months ago
parent
commit
6042dec537
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
2 changed files with 7 additions and 4 deletions
  1. 0
    1
      Yggdrasil.agda
  2. 7
    3
      Yggdrasil/Security.agda

+ 0
- 1
Yggdrasil.agda View File

@@ -1 +0,0 @@
1
-module Yggdrasil where

+ 7
- 3
Yggdrasil/Security.agda View File

@@ -6,14 +6,14 @@ import Data.Rational.Literals as ℚLit
6 6
 import Data.Integer.Literals as ℤLit
7 7
 open import Data.List using (_∷_; []; map)
8 8
 open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
9
-open import Data.Nat using (ℕ; zero; suc; _≤_; _^_)
9
+open import Data.Nat using (ℕ; zero; suc; _≤_; _^_; _+_)
10 10
 open import Data.Integer using (ℤ)
11 11
 open import Data.Maybe using (Maybe) renaming (map to mmap)
12 12
 open import Data.Unit using (⊤; tt)
13 13
 open import Data.Rational using (ℚ)
14 14
 open import Function using (_∘_)
15 15
 open import Level using (Level; Lift; lift) renaming (suc to lsuc)
16
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
16
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong)
17 17
 open import Relation.Nullary.Decidable using (fromWitnessFalse)
18 18
 open import Yggdrasil.List using (_∈_; here; there; with-proof; map≡-implies-∈≡)
19 19
 open import Yggdrasil.World using (WorldType; WorldState; World; Oracle; Call; Strategy; Node; Action; weaken; call; call↓; _↑_; stnode; _∷_; []; ⌊exec⌋; _⊑_; Query; _∈↑_; abort; dist; _>>=_; call↯; query; path; _↑; strat)
@@ -111,9 +111,13 @@ Perfect : {ℓ : Level} → Challenge {ℓ} → Set (lsuc (lsuc ℓ))
111 111
 Perfect c = Adv[ c ]≤ 0
112 112
 
113 113
 private
114
+  +-≡0ˡ : ∀ {n m} → n + m ≡ 0 → n ≡ 0
115
+  +-≡0ˡ {zero} _ = refl
116
+  +-≡0ˡ {suc n} ()
117
+
114 118
   ^≢0 : ∀ {n m} → (suc n) ^ m ≢ 0
115 119
   ^≢0 {n} {zero} ()
116
-  ^≢0 {n} {suc m} ()
120
+  ^≢0 {n} {suc m} n^sm≡0 = ^≢0 {n} {m} (+-≡0ˡ n^sm≡0)
117 121
 
118 122
 Computational : {ℓ : Level} → ℕ → (ℕ → Challenge {ℓ}) → Set (lsuc (lsuc ℓ))
119 123
 Computational κ f = Adv[ f κ ]≤ (_÷_ 1 (2 ^ κ) {fromWitnessFalse (^≢0 {1} {κ})})

Loading…
Cancel
Save