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.

Cryptol.agda

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