Last active
June 14, 2016 17:50
-
-
Save beala/d9e95c17999e1cd4f2d9b8bddff7768a to your computer and use it in GitHub Desktop.
A runnable implementation of the "Cryptol view" from the "Power of Pi": http://www.cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf I also attempted to implement part of SHA-1.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open import Data.Vec hiding (take; drop; [_]; split) | |
open import Data.Nat using (_*_; ℕ; zero; suc; _+_) | |
open import Data.Fin using (Fin; _≤_; compare; toℕ) | |
open import Relation.Binary.Core using (_≡_; refl) | |
open import Relation.Binary.PropositionalEquality using (cong) | |
import Data.Bool.Base as B using (if_then_else_; Bool; _∧_; true; false) | |
-- A runnable implementation of the "Cryptol View" from "The Power of Pi" | |
-- by Nicolas Oury and Wouter Swierstra with an implementation of SHA-1 | |
-- Agda version 2.5.1 | |
-- Agda stdlib 0.12 | |
-- Custom implementation of Vec utility functions that are easier | |
-- than the stdlib's to prove properties over. | |
take : {A : Set} {m : ℕ} (n : ℕ) → Vec A (n + m) → Vec A n | |
take zero xs = [] | |
take (suc n) (x ∷ xs) = x ∷ take n xs | |
drop : {A : Set} {m : ℕ} (n : ℕ) → Vec A (n + m) → Vec A m | |
drop zero xs = xs | |
drop (suc n) (x ∷ xs) = drop n xs | |
split : {A : Set} → (n : ℕ) → (m : ℕ) → Vec A (m * n) → Vec (Vec A n) m | |
split n zero xs = [] | |
split n (suc m) xs = (take n xs) ∷ (split n m (drop n xs)) | |
-- The "not terribly interesting" lemmas elided in the paper. Took me several hours ;) | |
takeDropLemma : {A : Set} (n m : ℕ) → (xs : Vec A (n + m)) → ((take n xs) ++ (drop n xs)) ≡ xs | |
takeDropLemma zero m xs = refl | |
takeDropLemma (suc n) m (x ∷ xs) = cong (_∷_ x) (takeDropLemma n m xs) | |
splitConcatLemma : {A : Set}(n m : ℕ) → (xs : Vec A (m * n)) → concat (split n m xs) ≡ xs | |
splitConcatLemma zero zero [] = refl | |
splitConcatLemma zero (suc m) xs = splitConcatLemma zero m xs | |
splitConcatLemma (suc n) zero xs = splitConcatLemma n zero xs | |
splitConcatLemma (suc n) (suc m) (x ∷ xs) with concat (split (suc n) m (drop n xs)) | splitConcatLemma (suc n) m (drop n xs) | |
... | .(drop n xs) | refl = cong (_∷_ x) (takeDropLemma n (m * suc n) xs) | |
-- Finally the SplitView and view function that allow for custom pattern matching! | |
data SplitView {A : Set} : {n : ℕ} → (m : ℕ) → Vec A (m * n) → Set where | |
[_] : forall {m n} → (xss : Vec (Vec A n) m) → SplitView m (concat xss) | |
view : {A : Set} → (n : ℕ) → (m : ℕ) → (xs : Vec A (m * n)) → SplitView m xs | |
view n m xs with concat (split n m xs) | [ split n m xs ] | splitConcatLemma n m xs | |
view n m xs | .xs | v | refl = v | |
-- Definition of a bit vector to test the implementation on. | |
data Bit : Set where | |
I : Bit | |
O : Bit | |
Word : ℕ → Set | |
Word = Vec Bit | |
-- A function that uses the SplitView to swap the higher and | |
-- lower 4 bit chunks. | |
swab : Word 8 → Word 8 | |
swab xs with view 4 2 xs | |
swab ._ | [ a ∷ b ∷ [] ] = concat (b ∷ a ∷ []) | |
-- A unit test. | |
swabTest : swab (I ∷ I ∷ I ∷ I ∷ O ∷ O ∷ O ∷ O ∷ []) ≡ (O ∷ O ∷ O ∷ O ∷ I ∷ I ∷ I ∷ I ∷ []) | |
swabTest = refl | |
-- A proof! | |
swabProof : (a b c d e f g h : Bit) → swab (a ∷ b ∷ c ∷ d ∷ e ∷ f ∷ g ∷ h ∷ []) ≡ (e ∷ f ∷ g ∷ h ∷ a ∷ b ∷ c ∷ d ∷ []) | |
swabProof a b c d e f g h = refl | |
{------------------------------ | |
---Now lets implement SHA-1--- | |
------------------------------} | |
-- Some functions for working with bits. | |
and : Bit → Bit → Bit | |
and I I = I | |
and _ _ = O | |
xor : Bit → Bit → Bit | |
xor I O = I | |
xor O I = I | |
xor _ _ = O | |
not : Bit → Bit | |
not I = O | |
not O = I | |
infixl 5 _∧_ | |
_∧_ : {n : ℕ} → Word n → Word n → Word n | |
x ∧ y = zipWith and x y | |
infixl 5 _⊕_ | |
_⊕_ : {n : ℕ} → Word n → Word n → Word n | |
x ⊕ y = zipWith xor x y | |
¬ : {n : ℕ} → Word n → Word n | |
¬ = map not | |
-- Comparing Nats. Seems like these should exist, but I could | |
-- only find fancy proposition versions of these. | |
_:≤:_ : ℕ → ℕ → B.Bool | |
zero :≤: r = B.true | |
suc l :≤: zero = B.false | |
suc l :≤: suc r = l :≤: r | |
_≤_≤_ : ℕ → ℕ → ℕ → B.Bool | |
l ≤ n ≤ r = (l :≤: n) B.∧ (n :≤: r) | |
-- Goofy guard syntax | |
!_⇒_∙_ : {A : Set} → B.Bool → A → A → A | |
! cond ⇒ e ∙ else = B.if cond then e else else | |
-- *drum roll* | |
-- Something that I hope is not entirely unlike SHA-1 | |
sha1 : Fin 80 → Word 96 → Word 32 | |
sha1 t w with view 32 3 w | |
sha1 t ._ | [ x ∷ y ∷ z ∷ [] ] = | |
! 0 ≤ (toℕ t) ≤ 19 ⇒ (x ∧ y) ⊕ (¬ x ∧ z) ∙ -- Should ¬ or ∧ bind tighter?! | |
! 20 ≤ (toℕ t) ≤ 39 ⇒ x ⊕ y ⊕ z ∙ | |
! 40 ≤ (toℕ t) ≤ 59 ⇒ (x ∧ y) ⊕ (x ∧ z) ⊕ (y ∧ z) ∙ | |
x ⊕ y ⊕ z |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment