cenary_proof.v

Require Coq.Lists.List.
Require Coq.Program.Basics. 

(* Utility Functions *)

Inductive Maybe (A : Type) : Type :=
  | Nothing : Maybe A
  | Just : A -> Maybe A.

Inductive stackValue : Set :=
  | IntegerValue : stackValue
  | AddressValue : stackValue
  | CharValue : stackValue.

Definition isAddrValue : stackValue -> bool :=
  fun v => match v with
  | AddressValue => true
  | _ => false
  end.

Definition instrAddable (l : stackValue) (r : stackValue) : bool :=
  match (l, r) with
  | (CharValue, _) => false
  | (_, CharValue) => false
  | _ => true
  end.

Definition compose {A B C} (g : B -> C) (f : A -> B) : A -> C :=
  fun x => g (f x).

(* Mimicking non-dependent applicatives here, even though this
   has nothing to do with actual applicatives
*)

Definition bind (A B : Type) (x : Maybe (A -> B)) (y : Maybe A) : Maybe B :=
  match (x, y) with
  | (Nothing _, _) => Nothing B
  | (_, Nothing _) => Nothing B
  | (Just _ f, Just _ v) => Just _ (f v)
  end.

Definition fish { A B C } (g : B -> Maybe C) (f : A -> Maybe B) : A -> Maybe C :=
  fun a => match f a with
    | Nothing _ => Nothing _
    | Just _ b => match g b with
      | Nothing _ => Nothing _
      | Just _ c => Just _ c
      end
    end.

Notation "A *> B" := (bind A B) (at level 80, right associativity).
Notation "A >=> B" := (fish A B) (at level 80, right associativity).
(* Stack Operations *)

Definition push32 (v : stackValue) (l : list stackValue) : Maybe (list stackValue) := Just _ (cons v l).

Definition pop (l : list stackValue) : Maybe (list stackValue) :=
  match l with
  | nil => Nothing _
  | cons x xs => Just _ xs
  end.

(* Store the element `stack[1]` at address `stack[0]` *)
Definition store' (l : list stackValue) : Maybe (list stackValue) :=
  match l with
  | cons AddressValue (cons IntegerValue xs) => Just _ xs
  | _ => Nothing _
  end.

(*
  Add the top 2 values on the stack.
  Addresses and integer values are inter-addable.
  We can add arbitrary values to addresses.
*)
Definition add (l : list stackValue) : Maybe (list stackValue) :=
  match l with
  | cons valueL (cons valueR xs) =>
    if instrAddable valueL valueR 
      then Just _ xs
      else Nothing _
  | _ => Nothing _
  end.

(* Load the value with the address on top of the stack from the memory. *)
Definition load' (l : list stackValue) : Maybe (list stackValue) :=
  match l with
  | cons AddressValue xs => Just _ xs
  | _ => Nothing _
  end.

(* Duplicate the value on top of the stack *)
Definition dup1 (l : list stackValue) : Maybe (list stackValue) :=
  match l with
  | cons x xs => Just _ (cons x (cons x xs))
  | _ => Nothing _
  end.

Definition sha3 (l : list stackValue): Maybe (list stackValue) :=
  match l with
  | cons x0 (cons x1 xs) =>
    if instrAddable x0 x1
      then Just _ xs
      else Nothing _ (* errorneous case *)
  | _ => Nothing _ (* errorneous case *)
  end.

(* My computation to test *)
Definition applyHashingFunction : list stackValue -> Maybe (list stackValue) :=
  (push32 AddressValue) >=>
  store' >=>
  push32 IntegerValue >=>
  push32 AddressValue >=>
  store' >=>
  push32 IntegerValue >=>
  push32 AddressValue >=>
  sha3.