diff --git a/ocaml/.gitignore b/ocaml/.gitignore
new file mode 100644
index 00000000..fbfb0c56
--- /dev/null
+++ b/ocaml/.gitignore
@@ -0,0 +1,11 @@
+*~
+*.omc
+.omakedb
+.omakedb.lock
+*.vo
+*.glob
+*.cm[iox]
+*.o
+*.annot
+*.opt
+*.run
\ No newline at end of file
diff --git a/ocaml/OMakefile b/ocaml/OMakefile
new file mode 100644
index 00000000..496727d5
--- /dev/null
+++ b/ocaml/OMakefile
@@ -0,0 +1,8 @@
+NATIVE_ENABLED = true
+BYTE_ENABLED = true
+
+.PHONY: clean
+.SUBDIRS: ocaml proof
+
+clean:
+	rm -rf *.vo *.glob *~ *.omc .omakedb .omakedb.lock
diff --git a/ocaml/OMakeroot b/ocaml/OMakeroot
new file mode 100644
index 00000000..35c219da
--- /dev/null
+++ b/ocaml/OMakeroot
@@ -0,0 +1,45 @@
+########################################################################
+# Permission is hereby granted, free of charge, to any person
+# obtaining a copy of this file, to deal in the File without
+# restriction, including without limitation the rights to use,
+# copy, modify, merge, publish, distribute, sublicense, and/or
+# sell copies of the File, and to permit persons to whom the
+# File is furnished to do so, subject to the following condition:
+#
+# THE FILE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+# EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
+# OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+# IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+# DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR
+# OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE FILE OR
+# THE USE OR OTHER DEALINGS IN THE FILE.
+
+########################################################################
+# The standard OMakeroot file.
+# You will not normally need to modify this file.
+# By default, your changes should be placed in the
+# OMakefile in this directory.
+#
+# If you decide to modify this file, note that it uses exactly
+# the same syntax as the OMakefile.
+#
+
+#
+# Include the standard installed configuration files.
+# Any of these can be deleted if you are not using them,
+# but you probably want to keep the Common file.
+#
+open build/C
+open build/OCaml
+open build/LaTeX
+
+#
+# The command-line variables are defined *after* the
+# standard configuration has been loaded.
+#
+DefineCommandVars()
+
+#
+# Include the OMakefile in this directory.
+#
+.SUBDIRS: .
diff --git a/ocaml/README.markdown b/ocaml/README.markdown
new file mode 100644
index 00000000..26048134
--- /dev/null
+++ b/ocaml/README.markdown
@@ -0,0 +1,22 @@
+MsgPack for OCaml
+==============================
+
+OVERVIEW
+------------------------------
+MessagePack(http://msgpack.org)のOCaml版ライブラリです。
+シリアライズしたものをデシリアライズすると元にもどることがCoqによって保証されています。
+
+REQUIRE
+------------------------------
+* extlib http://code.google.com/p/ocaml-extlib/
+* Coq 8.3 http://coq.inria.fr
+
+BUILD & INSTALL
+------------------------------
+
+      $ omake
+      $ omake install
+
+DOCUMENT
+------------------------------
+http://mzp.github.com/msgpack-ocaml/refman
\ No newline at end of file
diff --git a/ocaml/bleis-hooks/commit-msg b/ocaml/bleis-hooks/commit-msg
new file mode 100755
index 00000000..38d4baf7
--- /dev/null
+++ b/ocaml/bleis-hooks/commit-msg
@@ -0,0 +1,14 @@
+#! /bin/sh
+
+if [ -n "${GIT_DIR}" ]; then
+    hooksdir="./${GIT_DIR}/hooks/"
+else
+    hooksdir="./"
+fi
+
+. "${hooksdir}common.sh"
+
+ticket="$(extractTicketId)"
+if [ -n "${ticket}" ]; then
+    appendMsgTo1stLine "$1" "${ticket}"
+fi
diff --git a/ocaml/bleis-hooks/common.sh b/ocaml/bleis-hooks/common.sh
new file mode 100755
index 00000000..556e74eb
--- /dev/null
+++ b/ocaml/bleis-hooks/common.sh
@@ -0,0 +1,60 @@
+#! /bin/sh
+
+getGitBranchName()
+{
+    branch="$(git symbolic-ref HEAD 2>/dev/null)" ||
+            "$(git describe --contains --all HEAD)"
+    echo ${branch##refs/heads/}
+}
+
+isOnMasterBranch()
+{
+    if [ "$(getGitBranchName)" = "master" ]; then
+        return 0
+    fi
+    return 1
+}
+
+appendMsgTo1stLine()
+{
+    mv $1 $1.$$
+    if [ -s "$1.$$" ]; then
+    if head -1 "$1.$$" | grep "$2" > /dev/null; then
+        cp "$1.$$" "$1"
+    else
+            sed '1s/$/ '"$2"'/' "$1.$$" > $1
+    fi
+    else
+        echo "$2" > "$1"
+    fi
+    rm -f $1.$$
+}
+
+extractTicketId()
+{
+    echo "$(getGitBranchName)" \
+    | awk 'BEGIN{ FS="[/]"}
+           $1 == "id" { printf "refs #%s", $2 }
+           $2 == "id" { printf "refs #%s", $3 }'
+}
+
+hasTicketId()
+{
+    first="$(git cat-file -p $1 \
+    | sed '1,/^$/d' | head -1 \
+    | sed '/.*refs #[0-9][0-9]*.*/!d')"
+
+    if [ -n "${first}" ]; then
+        echo "true"
+    else
+        echo "false"
+    fi
+}
+
+extractParents()
+{
+    parents="$(git cat-file -p $1 \
+    | grep '^parent [0-9a-f]\{40\}$')"
+    echo "${parents##parent }"
+}
+
diff --git a/ocaml/bleis-hooks/pre-commit b/ocaml/bleis-hooks/pre-commit
new file mode 100755
index 00000000..9b7766bc
--- /dev/null
+++ b/ocaml/bleis-hooks/pre-commit
@@ -0,0 +1,22 @@
+#! /bin/sh
+
+if [ -z "$(git branch)" ]; then
+    exit 0
+fi
+
+if [ -n "${GIT_DIR}" ]; then
+    hooksdir="./${GIT_DIR}/hooks/"
+else
+    hooksdir="./"
+fi
+
+. "${hooksdir}common.sh"
+
+isOnMasterBranch
+if [ $? -eq 0 ]; then
+    echo "can't commit on master branch."
+    echo "please commit on topic branch."
+    exit 1
+fi
+
+exit 0
diff --git a/ocaml/ocaml/.gitignore b/ocaml/ocaml/.gitignore
new file mode 100644
index 00000000..3425f3f1
--- /dev/null
+++ b/ocaml/ocaml/.gitignore
@@ -0,0 +1,4 @@
+runner
+doc
+msgpackCore.ml
+msgpackCore.mli
diff --git a/ocaml/ocaml/META b/ocaml/ocaml/META
new file mode 100644
index 00000000..1170b98f
--- /dev/null
+++ b/ocaml/ocaml/META
@@ -0,0 +1,6 @@
+name="msgpack"
+version="0.1.0"
+description="a library for MessagePack."
+requires="extlib, num"
+archive(byte)="msgpack.cmo"
+archive(native)="msgpack.cmx"
\ No newline at end of file
diff --git a/ocaml/ocaml/OMakefile b/ocaml/ocaml/OMakefile
new file mode 100644
index 00000000..47babc35
--- /dev/null
+++ b/ocaml/ocaml/OMakefile
@@ -0,0 +1,80 @@
+.PHONY: all clean check doc install
+
+# ------------------------------
+# camlp4
+# ------------------------------
+public.UseCamlp4(files) =
+	protected.CAMLP4CMO = $(addprefix $(ROOT)/camlp4/,$(addsuffix .cmo,$(files)))
+	OCAMLPPFLAGS+=-pp 'camlp4o $(CAMLP4CMO)'
+	OCAMLDEPFLAGS+=-pp 'camlp4o $(CAMLP4CMO)'
+	export
+	.SCANNER: scan-ocaml-%.ml: %.ml $(CAMLP4CMO)
+
+# ------------------------------
+# findlib
+# ------------------------------
+USE_OCAMLFIND = true
+
+if $(not $(OCAMLFIND_EXISTS))
+    eprintln('This project requires ocamlfind, but is was not found.')
+    eprintln('You need to install ocamlfind and run "omake --configure".')
+    exit 1
+
+OCAMLPACKS[] =
+	oUnit
+	extlib
+	num
+
+OCAML_WARN_FLAGS=$`(if $(equal $<,msgpackCore.ml),-annot,-w A -warn-error A ) #`
+OCAMLFLAGS=$(OCAML_WARN_FLAGS) -annot
+# ------------------------------
+# library
+# ------------------------------
+FILES[] =
+	pack
+	base
+	hList
+	msgpackCore
+	serialize
+	config
+
+msgpackCore.ml : ../proof/msgpackCore.ml
+	cp $^ $@
+
+msgpackCore.mli : ../proof/msgpackCore.mli
+	cp $^ $@
+
+# ------------------------------
+# test code
+# ------------------------------
+TEST_FILES[] =
+	packTest
+	serializeTest
+
+TEST_PROGRAM = runner
+
+# ------------------------------
+# build rule
+# ------------------------------
+PROGRAM = msgpack
+OCAMLLINK = $(OCAMLC)
+OCAMLOPTLINK = $(OCAMLOPT)
+OCAMLC   += -for-pack $(capitalize $(PROGRAM))
+OCAMLOPT += -for-pack $(capitalize $(PROGRAM))
+
+.DEFAULT: all
+
+all : $(OCamlPackage $(PROGRAM), $(FILES))
+
+check : $(OCamlProgram $(TEST_PROGRAM), $(TEST_FILES) $(FILES))
+	./$(TEST_PROGRAM)
+
+doc:
+	mkdir -p doc
+	ocamldoc -d doc -html msgpack.mli
+
+install:
+	ocamlfind install msgpack META msgpack.cmx msgpack.cmo
+
+clean:
+	rm -rf *.cm[iox] *.o *~ *.omc .omakedb .omakedb.lock *.cmxa *.a *.opt *.run *.annot runner msgpackCore.*
diff --git a/ocaml/ocaml/base.ml b/ocaml/ocaml/base.ml
new file mode 100644
index 00000000..e1ccdde5
--- /dev/null
+++ b/ocaml/ocaml/base.ml
@@ -0,0 +1,142 @@
+let (@@) f g = f g
+let (+>) f g = g f
+let ($) f g x = f (g x)
+let (!$) = Lazy.force
+external id : 'a -> 'a = "%identity"
+
+let uncurry f a b = f (a,b)
+let curry f (a,b) = f a b
+let flip f a b = f b a
+let const a _ = a
+
+let sure f =
+  function
+      Some x ->
+	Some (f x)
+    | None ->
+	None
+
+let option f x = try Some (f x) with Not_found -> None
+let maybe  f x = try `Val (f x) with e -> `Error e
+let tee f x = try ignore @@ f x; x with _ -> x
+
+type ('a,'b) either = Left of 'a | Right of 'b
+let left x = Left x
+let right x = Right x
+
+let failwithf fmt = Printf.kprintf (fun s () -> failwith s) fmt
+
+let lookup x xs = (option @@ List.assoc x) xs
+
+let string_of_list xs =
+  Printf.sprintf "[%s]"
+    @@ String.concat ";" xs
+
+let rec unfold f init =
+     match f init with
+	 Some (a, b) -> a :: unfold f b
+       | None        -> []
+
+let rec range a b =
+  if a >= b then
+    []
+  else
+    a::range (a+1) b
+
+let rec interperse delim =
+  function
+      []  -> []
+    | [x] -> [x]
+    | x::xs -> x::delim::interperse delim xs
+
+let map_accum_left f init xs =
+  let f (accum,ys) x =
+    let accum',y =
+      f accum x in
+      (accum',y::ys) in
+  let accum,ys =
+    List.fold_left f (init,[]) xs in
+    accum,List.rev ys
+
+let rec map_accum_right f init =
+  function
+      [] ->
+	init,[]
+    | x::xs ->
+	let (accum,ys) =
+	  map_accum_right f init xs in
+	let (accum,y) =
+	  f accum x in
+	  accum,y::ys
+
+let rec filter_map f =
+  function
+      x::xs ->
+	begin match f x with
+	    Some y -> y::filter_map f xs
+	  | None   -> filter_map f xs
+	end
+    | [] ->
+	[]
+
+let rec group_by f =
+  function
+      [] ->
+	[]
+    | x1::x2::xs when f x1 x2 ->
+	begin match group_by f @@ x2::xs with
+	    y::ys ->
+	      (x1::y)::ys
+	  | _ ->
+	      failwith "must not happen"
+	end
+    | x::xs ->
+	[x]::group_by f xs
+
+let index x xs =
+  let rec loop i = function
+      [] ->
+	raise Not_found
+    | y::ys ->
+	if x = y then
+	  i
+	else
+	  loop (i+1) ys in
+    loop 0 xs
+
+let string_of_char =
+  String.make 1
+
+let hex =
+  Printf.sprintf "0x%x"
+
+let open_out_with path f =
+  let ch =
+    open_out_bin path in
+    maybe f ch
+    +> tee (fun _ -> close_out ch)
+    +> function
+	`Val v ->  v
+      | `Error e -> raise e
+
+let open_in_with path f =
+  let ch =
+    open_in_bin path in
+    maybe f ch
+    +> tee (fun _ -> close_in ch)
+    +> function
+	`Val v ->  v
+      | `Error e -> raise e
+
+let forever f () =
+  while true do
+    f ()
+  done
+
+let undefined =  Obj.magic 42
+let undef     = undefined
+
+let p fmt = Printf.kprintf (fun s () -> print_endline s; flush stdout) fmt
+
+let ret x _ =
+  x
diff --git a/ocaml/ocaml/config.ml b/ocaml/ocaml/config.ml
new file mode 100644
index 00000000..9a6723a5
--- /dev/null
+++ b/ocaml/ocaml/config.ml
@@ -0,0 +1 @@
+let version = (1,0,0)
diff --git a/ocaml/ocaml/hList.ml b/ocaml/ocaml/hList.ml
new file mode 100644
index 00000000..732a6f10
--- /dev/null
+++ b/ocaml/ocaml/hList.ml
@@ -0,0 +1,191 @@
+open Base
+
+let rec last =
+  function
+      [] ->
+	invalid_arg "HList.last"
+    | [x] ->
+	x
+    | _::xs ->
+	last xs
+
+let init xs =
+  let rec init' ys =
+    function
+	[]  ->
+	  invalid_arg "HList.init"
+      |	[_] ->
+	  List.rev ys
+      | x::xs ->
+	  init' (x::ys) xs in
+    init' [] xs
+
+let null =
+  function
+      [] ->
+	true
+    | _ ->
+	false
+
+let fold_left1 f =
+  function
+      [] ->
+	invalid_arg "HList.fold_left1"
+    | x::xs ->
+	List.fold_left f x xs
+
+let rec fold_right1 f =
+  function
+      []    ->
+	invalid_arg "HList.fold_right1"
+    | [x]   ->
+	x
+    | x::xs ->
+	f x (fold_right1 f xs)
+
+let conj =
+  List.fold_left (&&) true
+
+let disj =
+  List.fold_left (||) false
+
+let sum =
+  List.fold_left (+) 0
+
+let product =
+  List.fold_left ( * ) 1
+
+let concat_map f xs =
+  List.fold_right ((@) $ f) xs []
+
+let maximum xs =
+  fold_left1 max xs
+
+let minimum xs =
+  fold_left1 min xs
+
+let rec scanl f y =
+  function
+      [] ->
+	[y]
+    | x::xs ->
+	y::scanl f (f y x) xs
+
+let scanl1 f =
+  function
+      [] ->
+	[]
+    | x::xs ->
+	scanl f x xs
+
+let rec scanr f z =
+  function
+      [] ->
+	[z]
+    | x::xs ->
+	match scanr f z xs with
+	    y::_ as yss ->
+	      (f x y) :: yss
+	  | _ ->
+	      failwith "must not happen"
+
+let scanr1 f =
+  function
+    [] ->
+      []
+  | x::xs ->
+      scanr f x xs
+
+let replicate n x =
+  let rec loop i ys =
+    if i = 0 then
+      ys
+    else
+      loop (i-1) (x::ys) in
+    loop n []
+
+let rec take n =
+  function
+      [] ->
+	[]
+    | x::xs ->
+	if n <= 0 then
+	  []
+	else
+	  x :: take (n - 1) xs
+
+let rec drop n =
+  function
+      [] ->
+	[]
+    | xs when n <= 0 ->
+	xs
+    | _::xs ->
+      drop (n-1) xs
+
+let rec splitAt n xs =
+  match n,xs with
+      0,_  | _,[] ->
+	[],xs
+    | _,y::ys ->
+	let p,q =
+	  splitAt (n-1) ys in
+	  y::p,q
+
+let rec takeWhile f =
+  function
+      x::xs when f x ->
+	x :: takeWhile f xs
+    | _ ->
+	[]
+
+let rec dropWhile f =
+  function
+      x::xs when f x ->
+	dropWhile f xs
+    | xs ->
+	xs
+
+let rec span f =
+  function
+      x::xs when f x ->
+	let ys,zs =
+	  span f xs in
+	  x::ys,zs
+    | xs ->
+	[],xs
+
+let break f =
+  span (not $ f)
+
+let rec zip_with f xs ys =
+  match xs,ys with
+      [],_ | _,[] ->
+	[]
+    | x::xs',y::ys' ->
+	(f x y)::zip_with f xs' ys'
+
+let rec zip_with3 f xs ys zs =
+  match xs,ys,zs with
+      [],_,_ | _,[],_ | _,_,[] ->
+	[]
+    | x::xs',y::ys',z::zs' ->
+	(f x y z)::zip_with3 f xs' ys' zs'
+
+let zip xs ys =
+  zip_with (fun x y -> (x,y)) xs ys
+
+let zip3 xs ys zs =
+  zip_with3 (fun x y z -> (x,y,z)) xs ys zs
+
+let unzip xs =
+  List.fold_right (fun (x,y) (xs,ys) -> (x::xs,y::ys)) xs ([],[])
+
+let unzip3 xs =
+  List.fold_right (fun (x,y,z) (xs,ys,zs) -> (x::xs,y::ys,z::zs)) xs ([],[],[])
+
+let lookup x xs =
+  try
+    Some (List.assoc x xs)
+  with Not_found ->
+    None
diff --git a/ocaml/ocaml/main.ml b/ocaml/ocaml/main.ml
new file mode 100644
index 00000000..f7c81958
--- /dev/null
+++ b/ocaml/ocaml/main.ml
@@ -0,0 +1,2 @@
+let _ =
+  print_endline "hello"
diff --git a/ocaml/ocaml/msgpack.mli b/ocaml/ocaml/msgpack.mli
new file mode 100644
index 00000000..cd227da5
--- /dev/null
+++ b/ocaml/ocaml/msgpack.mli
@@ -0,0 +1,46 @@
+(** MessagePack for OCaml *)
+
+(** Conversion MessagePack object between OCaml and Coq. *)
+module Pack : sig
+  (** exception when MesagePack object is invalid form *)
+  exception Not_conversion of string
+end
+
+(** MessagePack Serializer *)
+module Serialize : sig
+  (** MesagePack object. See also {{:http://redmine.msgpack.org/projects/msgpack/wiki/FormatSpec}MessagePack specification}. *)
+  type t =
+      [ `Bool of bool
+      | `Nil
+      | `PFixnum of int
+      | `NFixnum of int
+      | `Uint8 of int
+      | `Uint16 of int
+      | `Uint32 of int64
+      | `Uint64 of Big_int.big_int
+      | `Int8 of int
+      | `Int16 of int
+      | `Int32 of int32
+      | `Int64 of int64
+      | `Float of float
+      | `Double of float
+      | `FixRaw of char list
+      | `Raw16 of char list
+      | `Raw32 of char list
+      | `FixArray of t list
+      | `Array16 of t list
+      | `Array32 of t list
+      | `FixMap of (t * t) list
+      | `Map16 of (t * t) list
+      | `Map32 of (t * t) list ]
+
+  (**  [MessagePack.Serialize.deserialize_string str] deserialize MessagePack string [str] to MessagePack object. *)
+  val deserialize_string : string -> t
+
+  (**  [MessagePack.Serialize.serialize_string obj] serialize MessagePack object [obj] to MessagePack string. *)
+  val serialize_string   : t -> string
+end
+
+module Config : sig
+  val version : int * int * int
+end
diff --git a/ocaml/ocaml/pack.ml b/ocaml/ocaml/pack.ml
new file mode 100644
index 00000000..e70e96ee
--- /dev/null
+++ b/ocaml/ocaml/pack.ml
@@ -0,0 +1,206 @@
+open Base
+open MsgpackCore
+
+exception Not_conversion of string
+
+type t =
+  [ `Bool of bool
+  | `Nil
+  | `PFixnum of int
+  | `NFixnum of int
+  | `Uint8 of int
+  | `Uint16 of int
+  | `Uint32 of int64
+  | `Uint64 of Big_int.big_int
+  | `Int8 of int
+  | `Int16 of int
+  | `Int32 of int32
+  | `Int64 of int64
+  | `Float of float
+  | `Double of float
+  | `FixRaw of char list
+  | `Raw16 of char list
+  | `Raw32 of char list
+  | `FixArray of t list
+  | `Array16 of t list
+  | `Array32 of t list
+  | `FixMap of (t * t) list
+  | `Map16 of (t * t) list
+  | `Map32 of (t * t) list ]
+
+let ascii8 n =
+  Ascii(n land 0b0000_0001 <> 0,
+	n land 0b0000_0010 <> 0,
+	n land 0b0000_0100 <> 0,
+	n land 0b0000_1000 <> 0,
+	n land 0b0001_0000 <> 0,
+	n land 0b0010_0000 <> 0,
+	n land 0b0100_0000 <> 0,
+	n land 0b1000_0000 <> 0)
+
+let ascii8_of_char c =
+  c +> Char.code +> ascii8
+
+let ascii16 n =
+  (ascii8 (n lsr 8), ascii8 n)
+
+let ascii32 n =
+  (ascii16 (Int64.to_int (Int64.shift_right_logical n 16)),
+   ascii16 (Int64.to_int (Int64.logand n 0xFFFFL)))
+
+let ascii64 n =
+  let open Big_int in
+  let x =
+    shift_right_big_int n 32
+    +> int64_of_big_int
+    +> ascii32 in
+  let y =
+    and_big_int n (big_int_of_int64 0xFFFF_FFFFL)
+    +> int64_of_big_int
+    +> ascii32 in
+    (x, y)
+
+let ascii32_of_int32 n =
+  (ascii16 (Int32.to_int (Int32.shift_right_logical n 16)),
+   ascii16 (Int32.to_int n))
+
+let ascii64_of_int64 n =
+  (ascii32 (Int64.shift_right_logical n 32),
+   ascii32 n)
+
+let not_conversion msg =
+  raise @@ Not_conversion msg
+
+let rec pack = function
+    `Nil ->
+      Nil
+  | `Bool b ->
+      Bool b
+  | `PFixnum n ->
+      if 0 <= n && n < 128 then
+	PFixnum (ascii8 n)
+      else
+	not_conversion "pfixnum"
+  | `NFixnum n ->
+      if -32 <= n && n < 0 then
+	NFixnum (ascii8 n)
+      else
+	not_conversion "nfixnum"
+  | `Uint8 n ->
+      if 0 <= n && n <= 0xFF then
+	Uint8 (ascii8 n)
+      else
+	not_conversion "uint8"
+  | `Uint16 n ->
+      if 0 <= n && n <= 0xFF_FF then
+	Uint16 (ascii16 n)
+      else
+	not_conversion "uint16"
+  | `Uint32 n ->
+      if 0L <= n && n <= 0xFFFF_FFFFL then
+	Uint32 (ascii32 n)
+      else
+	not_conversion "uint32"
+  | `Uint64 n ->
+      let open Big_int in
+      let (<=%) = le_big_int in
+      let (<<)  = shift_left_big_int in
+      if zero_big_int <=% n && n <=%  (unit_big_int << 64) then
+	Uint64 (ascii64 n)
+      else
+	not_conversion "uint64"
+  | `Int8 n ->
+      if -127 <= n && n <= 128 then
+	Int8 (ascii8 n)
+      else
+	not_conversion "int8"
+  | `Int16 n ->
+      if -32767 <= n && n <= 32768 then
+	Int16 (ascii16 n)
+      else
+	not_conversion "int16"
+  | `Int32 n ->
+      Int32 (ascii16 (Int32.to_int (Int32.shift_right_logical n 16)),
+	     ascii16 (Int32.to_int n))
+  | `Int64 n ->
+      Int64 (ascii64_of_int64 n)
+  | `Float n ->
+      Float (ascii32_of_int32 @@ Int32.bits_of_float n)
+  | `Double n ->
+      Double (ascii64_of_int64 @@ Int64.bits_of_float n)
+  | `FixRaw cs ->
+      FixRaw (List.map ascii8_of_char cs)
+  | `Raw16 cs ->
+      Raw16 (List.map ascii8_of_char cs)
+  | `Raw32 cs ->
+      Raw32 (List.map ascii8_of_char cs)
+  | `FixArray xs ->
+      FixArray (List.map pack xs)
+  | `Array16 xs ->
+      Array16 (List.map pack xs)
+  | `Array32 xs ->
+      Array32 (List.map pack xs)
+  | `FixMap xs ->
+      FixMap (List.map (fun (x,y) -> (pack x, pack y)) xs)
+  | `Map16 xs ->
+      Map16 (List.map (fun (x,y) -> (pack x, pack y)) xs)
+  | `Map32 xs ->
+      Map32 (List.map (fun (x,y) -> (pack x, pack y)) xs)
+
+let of_ascii8 (Ascii(b1,b2,b3,b4,b5,b6,b7,b8)) =
+  List.fold_left (fun x y -> 2 * x + (if y then 1 else 0)) 0 [ b8; b7; b6; b5; b4; b3; b2; b1 ]
+
+let char_of_ascii8 c =
+  c +> of_ascii8 +> Char.chr
+
+let of_ascii16 (c1, c2) =
+  of_ascii8 c1 lsl 8 + of_ascii8 c2
+
+let of_ascii32 (c1,c2) =
+  let (+%) = Int64.add in
+  let (<<) = Int64.shift_left in
+    ((Int64.of_int (of_ascii16 c1)) << 16) +% Int64.of_int (of_ascii16 c2)
+
+let int32_of_ascii32 (c1,c2) =
+  let (+%) = Int32.add in
+  let (<<) = Int32.shift_left in
+    ((Int32.of_int @@ of_ascii16 c1) << 16) +% (Int32.of_int @@ of_ascii16 c2)
+
+let int64_of_ascii64 (c1,c2) =
+  let (+%) = Int64.add in
+  let (<<) = Int64.shift_left in
+    (of_ascii32 c1 << 32) +% (of_ascii32 c2)
+
+let of_ascii64 (c1, c2) =
+  let open Big_int in
+  let (+%) = add_big_int in
+  let (<<) = shift_left_big_int in
+    ((big_int_of_int64 @@ of_ascii32 c1) << 32) +% (big_int_of_int64 @@ of_ascii32 c2)
+
+let int width n =
+  (n lsl (Sys.word_size-width-1)) asr (Sys.word_size-width-1);;
+
+let rec unpack  = function
+  | Nil -> `Nil
+  | Bool b -> `Bool b
+  | PFixnum c -> `PFixnum (of_ascii8 c)
+  | NFixnum c -> `NFixnum (int 8 @@ of_ascii8 c)
+  | Uint8  c -> `Uint8  (of_ascii8 c)
+  | Uint16 c -> `Uint16 (of_ascii16 c)
+  | Uint32 c -> `Uint32 (of_ascii32 c)
+  | Uint64 c -> `Uint64 (of_ascii64 c)
+  | Int8   c -> `Int8  (int  8 @@ of_ascii8 c)
+  | Int16  c -> `Int16 (int 16 @@ of_ascii16 c)
+  | Int32  c -> `Int32 (int32_of_ascii32 c)
+  | Int64  c -> `Int64 (int64_of_ascii64 c)
+  | Float  c -> `Float (Int32.float_of_bits (int32_of_ascii32 c))
+  | Double c -> `Double (Int64.float_of_bits (int64_of_ascii64 c))
+  | FixRaw cs -> `FixRaw (List.map char_of_ascii8 cs)
+  | Raw16  cs -> `Raw16 (List.map char_of_ascii8 cs)
+  | Raw32  cs -> `Raw32 (List.map char_of_ascii8 cs)
+  | FixArray xs -> `FixArray (List.map unpack xs)
+  | Array16 xs -> `Array16 (List.map unpack xs)
+  | Array32 xs -> `Array32 (List.map unpack xs)
+  | FixMap  xs -> `FixMap (List.map (fun (x,y) -> (unpack x, unpack y)) xs)
+  | Map16  xs -> `Map16 (List.map (fun (x,y) -> (unpack x, unpack y)) xs)
+  | Map32  xs -> `Map32 (List.map (fun (x,y) -> (unpack x, unpack y)) xs)
diff --git a/ocaml/ocaml/pack.mli b/ocaml/ocaml/pack.mli
new file mode 100644
index 00000000..55c4c36a
--- /dev/null
+++ b/ocaml/ocaml/pack.mli
@@ -0,0 +1,32 @@
+exception Not_conversion of string
+
+type t =
+  [ `Bool of bool
+  | `Nil
+  | `PFixnum of int
+  | `NFixnum of int
+  | `Uint8 of int
+  | `Uint16 of int
+  | `Uint32 of int64
+  | `Uint64 of Big_int.big_int
+  | `Int8 of int
+  | `Int16 of int
+  | `Int32 of int32
+  | `Int64 of int64
+  | `Float of float
+  | `Double of float
+  | `FixRaw of char list
+  | `Raw16 of char list
+  | `Raw32 of char list
+  | `FixArray of t list
+  | `Array16 of t list
+  | `Array32 of t list
+  | `FixMap of (t * t) list
+  | `Map16 of (t * t) list
+  | `Map32 of (t * t) list ]
+
+val pack : t -> MsgpackCore.object0
+val unpack : MsgpackCore.object0 -> t
+
+val char_of_ascii8 : MsgpackCore.ascii -> char
+val ascii8_of_char : char -> MsgpackCore.ascii
diff --git a/ocaml/ocaml/packTest.ml b/ocaml/ocaml/packTest.ml
new file mode 100644
index 00000000..a68a711a
--- /dev/null
+++ b/ocaml/ocaml/packTest.ml
@@ -0,0 +1,175 @@
+open Base
+open OUnit
+open MsgpackCore
+open Pack
+open Printf
+
+let c0 =
+  Ascii (false,false,false,false,false,false,false,false)
+let c1 =
+  Ascii (true, false,false,false,false,false,false,false)
+let c255 =
+  Ascii (true,true,true,true,true,true,true,true)
+
+let valid = [
+  "nil",[
+    Nil, `Nil
+  ], [];
+  "bool",[
+    Bool true , `Bool true;
+    Bool false, `Bool false
+  ], [];
+  "pfixnum",[
+    PFixnum c0,`PFixnum 0;
+    PFixnum c1,`PFixnum 1;
+  ], [
+    `PFixnum 128;
+    `PFixnum (~-1);
+  ];
+  "nfixnum",[
+    NFixnum c255, `NFixnum ~-1;
+    NFixnum (Ascii (false,false,false,false,false,true,true,true)), `NFixnum ~-32
+  ],[
+    `NFixnum 0;
+    `NFixnum (~-33)
+  ];
+  "uint8", [
+    Uint8 c0, `Uint8 0;
+    Uint8 c1, `Uint8 1;
+    Uint8 c255, `Uint8 255
+  ],[
+    `Uint8 ~-1;
+    `Uint8 256
+  ];
+  "uint16", [
+    Uint16 (c0,c0), `Uint16 0;
+    Uint16 (c0,c1), `Uint16 1;
+    Uint16 (c1,c0), `Uint16 256;
+    Uint16 (c255,c255), `Uint16 65535;
+  ],[
+    `Uint16 ~-1;
+    `Uint16 65536
+  ];
+  "uint32", [
+    Uint32 ((c0,c0), (c0,c0)), `Uint32 0L;
+    Uint32 ((c255,c255), (c255,c255)), `Uint32 0xFFFF_FFFFL
+  ],[
+    `Uint32 (-1L);
+    `Uint32 0x1FFFF_FFFFL
+  ];
+  "uint64", [
+    Uint64 (((c0,c0), (c0,c0)),((c0,c0), (c0,c0))), `Uint64 Big_int.zero_big_int;
+    Uint64 (((c0,c0), (c0,c0)),((c0,c0), (c0,c1))), `Uint64 Big_int.unit_big_int;
+    Uint64 (((c255,c255), (c255,c255)),((c255,c255), (c255,c255))), `Uint64 (Big_int.big_int_of_string "18446744073709551615")
+  ],[
+    `Uint64 (Big_int.big_int_of_string "-1");
+    `Uint64 (Big_int.big_int_of_string "18446744073709551617")
+  ];
+  "int8", [
+    Int8 c0, `Int8 0;
+    Int8 c1, `Int8 1;
+    Int8 c255, `Int8 (~-1)
+  ],[
+    `Int8 129
+  ];
+  "int16", [
+    Int16 (c0,c0), `Int16 0;
+    Int16 (c0,c1), `Int16 1;
+    Int16 (c1,c0), `Int16 256;
+    Int16 (c255,c255), `Int16 ~-1;
+  ],[
+    `Int16 65536
+  ];
+  "int32", [
+    Int32 ((c0,c0), (c0,c0)), `Int32 0l;
+    Int32 ((c255,c255), (c255,c255)), `Int32 (-1l)
+  ],[];
+  "int64", [
+    Int64 (((c0,c0), (c0,c0)),((c0,c0), (c0,c0))), `Int64 0L;
+    Int64 (((c0,c0), (c0,c0)),((c0,c0), (c0,c1))), `Int64 1L;
+    Int64 (((c255,c255), (c255,c255)),((c255,c255), (c255,c255))), `Int64 (-1L)
+  ],[];
+  "float", [
+    Float ((c0,c0),(c0,c0)), `Float 0.0;
+    (* 0.5 = 3f_00_00_00 *)
+    Float ((Ascii (true,true,true,true,true,true,false,false),c0),(c0,c0)), `Float 0.5;
+  ], [];
+  "double", [
+    Double (((c0,c0),(c0,c0)),((c0,c0),(c0,c0))), `Double 0.0;
+    (* 0.5 = 3f_e0_00_00_00_00_00_00 *)
+    Double (((Ascii (true,true,true,true,true,true,false,false),
+	     Ascii (false,false,false,false,false,true,true,true)),
+	     (c0,c0)),
+	    ((c0,c0),(c0,c0))), `Double 0.5
+  ],[];
+  "fixraw", [
+    FixRaw [], `FixRaw [];
+    FixRaw [ c0 ], `FixRaw [ '\000'];
+    FixRaw [ c0; c1 ], `FixRaw [ '\000'; '\001'];
+  ],[];
+  "raw16", [
+    Raw16 [], `Raw16 [];
+    Raw16 [ c0 ], `Raw16 [ '\000'];
+    Raw16 [ c0; c1 ], `Raw16 [ '\000'; '\001'];
+  ], [];
+  "raw32", [
+    Raw32 [], `Raw32 [];
+    Raw32 [ c0 ], `Raw32 [ '\000'];
+    Raw32 [ c0; c1 ], `Raw32 [ '\000'; '\001'];
+  ], [];
+  "fixarray", [
+    FixArray [], `FixArray [];
+    FixArray [ PFixnum c0 ], `FixArray [`PFixnum 0 ];
+    FixArray [ FixArray [ PFixnum c0 ] ], `FixArray [`FixArray [ `PFixnum 0] ];
+  ], [];
+  "array16", [
+    Array16 [], `Array16 [];
+    Array16 [ PFixnum c0 ], `Array16 [`PFixnum 0 ];
+    Array16 [ Array16 [ PFixnum c0 ] ], `Array16 [`Array16 [ `PFixnum 0] ];
+  ], [];
+  "array32", [
+    Array32 [], `Array32 [];
+    Array32 [ PFixnum c0 ], `Array32 [`PFixnum 0 ];
+    Array32 [ Array32 [ PFixnum c0 ] ], `Array32 [`Array32 [ `PFixnum 0] ];
+  ], [];
+  "fixmap", [
+    FixMap [], `FixMap [];
+    FixMap [ PFixnum c0, PFixnum c1 ], `FixMap [`PFixnum 0, `PFixnum 1 ];
+  ], [];
+  "map16", [
+    Map16 [], `Map16 [];
+    Map16 [ PFixnum c0, PFixnum c1 ], `Map16 [`PFixnum 0, `PFixnum 1 ];
+  ], [];
+  "map32", [
+    Map32 [], `Map32 [];
+    Map32 [ PFixnum c0, PFixnum c1 ], `Map32 [`PFixnum 0, `PFixnum 1 ];
+  ], [];
+]
+
+
+let _ = begin "pack.ml" >::: [
+  "変換のテスト" >:::
+    valid +> HList.concat_map begin fun (name, ok, ng) ->
+       let xs =
+	 ok +> List.map begin fun (expect, actual) ->
+	   (sprintf "%sが変換できる" name) >:: (fun _ -> assert_equal expect (pack actual));
+	 end in
+       let ys =
+	 ng +> List.map begin fun actual ->
+	   (sprintf "%sのエラーチェック" name) >:: (fun _ -> assert_raises (Not_conversion name) (fun () -> pack actual))
+	 end in
+	 xs @ ys
+    end;
+  "復元のテスト" >:::
+    valid +> HList.concat_map begin fun (name, ok, _) ->
+      ok +> List.map begin fun (actual, expect) ->
+	(sprintf "%sが復元できる" name) >:: begin fun _ ->
+	  match expect, unpack actual with
+	      `Uint64 n1, `Uint64 n2 ->
+		assert_equal ~cmp:Big_int.eq_big_int n1 n2
+	    | x, y ->
+		assert_equal x y
+	end
+      end
+    end;
+] end +> run_test_tt_main
diff --git a/ocaml/ocaml/serialize.ml b/ocaml/ocaml/serialize.ml
new file mode 100644
index 00000000..e6e30d75
--- /dev/null
+++ b/ocaml/ocaml/serialize.ml
@@ -0,0 +1,20 @@
+open Base
+open ExtString
+
+type t = Pack.t
+
+let deserialize_string str =
+  str
+  +> String.explode
+  +> List.map Pack.ascii8_of_char
+  +> MsgpackCore.deserialize 0
+  +> List.hd
+  +> Pack.unpack
+
+let serialize_string obj =
+  obj
+  +> Pack.pack
+  +> MsgpackCore.serialize
+  +> List.map Pack.char_of_ascii8
+  +> String.implode
+
diff --git a/ocaml/ocaml/serialize.mli b/ocaml/ocaml/serialize.mli
new file mode 100644
index 00000000..69719e55
--- /dev/null
+++ b/ocaml/ocaml/serialize.mli
@@ -0,0 +1,4 @@
+type t = Pack.t
+
+val deserialize_string : string -> t
+val serialize_string   : t -> string
diff --git a/ocaml/ocaml/serializeTest.ml b/ocaml/ocaml/serializeTest.ml
new file mode 100644
index 00000000..32c8bab4
--- /dev/null
+++ b/ocaml/ocaml/serializeTest.ml
@@ -0,0 +1,16 @@
+open Base
+open OUnit
+open Serialize
+
+let _ = begin "serialize.ml" >::: [
+  "Rubyのライブラリとの互換テスト(deserialize)" >:: begin fun _ ->
+    (* [1,2,3].to_msgpack *)
+    assert_equal (`FixArray [`PFixnum 1; `PFixnum 2; `PFixnum 3]) @@
+      deserialize_string "\147\001\002\003"
+  end;
+  "Rubyのライブラリとの互換テスト(serialize)" >:: begin fun _ ->
+    assert_equal "\147\001\002\003" @@
+      serialize_string @@ `FixArray [`PFixnum 1; `PFixnum 2; `PFixnum 3]
+  end
+] end +> run_test_tt_main
+
diff --git a/ocaml/proof/.gitignore b/ocaml/proof/.gitignore
new file mode 100644
index 00000000..ffb82899
--- /dev/null
+++ b/ocaml/proof/.gitignore
@@ -0,0 +1,2 @@
+msgpackCore.ml
+msgpackCore.mli
diff --git a/ocaml/proof/CoqBuildRule b/ocaml/proof/CoqBuildRule
new file mode 100644
index 00000000..57be1c52
--- /dev/null
+++ b/ocaml/proof/CoqBuildRule
@@ -0,0 +1,14 @@
+public.COQC   = coqc
+public.COQC_FLAGS   =
+public.COQLIB = $(shell coqc -where)
+public.COQDEP = coqdep -w -coqlib $`(COQLIB) -I .
+
+public.CoqProof(files) =
+	vo=$(addsuffix .vo,$(files))
+	value $(vo)
+
+%.vo %.glob: %.v
+	$(COQC) $(COQC_FLAGS) $<
+
+.SCANNER: %.vo: %.v
+	$(COQDEP) $<
diff --git a/ocaml/proof/DeserializeImplement.v b/ocaml/proof/DeserializeImplement.v
new file mode 100644
index 00000000..f9e1f728
--- /dev/null
+++ b/ocaml/proof/DeserializeImplement.v
@@ -0,0 +1,630 @@
+Require Import Ascii List.
+Require Import ListUtil Object MultiByte Util SerializeSpec Pow SerializedList ProofUtil.
+
+Open Scope char_scope.
+
+Definition compact (xs : list object) : list ascii8 :=
+  List.flat_map (fun x => match x with
+                            FixRaw xs =>  xs
+                            | _ => []
+                          end)
+  xs.
+
+Fixpoint deserialize (n : nat) (xs : list ascii8) {struct xs} :=
+  match n with
+    | 0 =>
+      match xs with
+        | "192" :: ys =>
+          Nil::deserialize 0 ys
+        | "194" :: ys =>
+          Bool false :: deserialize 0 ys
+        | "195" :: ys =>
+          Bool true :: deserialize 0 ys
+        | Ascii b1 b2 b3 b4 b5 b6 b7 false :: ys =>
+          PFixnum (Ascii b1 b2 b3 b4 b5 b6 b7 false) :: deserialize 0 ys
+        | (Ascii b1 b2 b3 b4 b5 true true true) :: ys =>
+          NFixnum (Ascii b1 b2 b3 b4 b5 true true true) :: deserialize 0 ys
+        | "204" :: c1 :: ys =>
+          Uint8 c1 :: deserialize 0 ys
+        | "205" :: c1 :: c2 :: ys =>
+          Uint16 (c1, c2) :: deserialize 0 ys
+        | "206" :: c1 :: c2 :: c3 :: c4 :: ys =>
+          Uint32 ((c1, c2), (c3, c4)) :: deserialize 0 ys
+        | "207" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys =>
+          Uint64 (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys
+        | "208" :: c1 :: ys =>
+          Int8 c1 :: deserialize 0 ys
+        | "209" :: c1 :: c2 :: ys =>
+          Int16 (c1, c2) :: deserialize 0 ys
+        | "210" :: c1 :: c2 :: c3 :: c4 :: ys =>
+          Int32 ((c1, c2), (c3, c4)) :: deserialize 0 ys
+        | "211" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys =>
+          Int64 (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys
+        | "202" :: c1 :: c2 :: c3 :: c4 :: ys =>
+          Float ((c1,c2), (c3, c4)) :: deserialize 0 ys
+        | "203" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys =>
+          Double (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys
+        | Ascii b1 b2 b3 b4 b5 true false true :: ys =>
+          let n :=
+            nat_of_ascii8 (Ascii b1 b2 b3 b4 b5 false false false) in
+          let (zs, ws) :=
+            split_at n @@ deserialize n ys in
+            FixRaw (compact zs) :: ws
+        | "218" :: s1 :: s2 :: ys =>
+          let n :=
+            nat_of_ascii16 (s1,s2) in
+          let (zs, ws) :=
+            split_at n @@ deserialize n ys in
+            Raw16 (compact zs) :: ws
+        | "219" :: s1 :: s2 :: s3 :: s4 :: ys =>
+          let n :=
+            nat_of_ascii32 ((s1,s2),(s3,s4)) in
+          let (zs, ws) :=
+            split_at n @@ deserialize n ys in
+            Raw32 (compact zs) :: ws
+        | Ascii b1 b2 b3 b4 true false false true :: ys =>
+          let n :=
+            nat_of_ascii8 (Ascii b1 b2 b3 b4 false false false false) in
+          let (zs, ws) :=
+            split_at n @@ deserialize 0 ys in
+            FixArray zs :: ws
+        | "220" :: s1 :: s2 :: ys =>
+          let n :=
+            nat_of_ascii16 (s1,s2) in
+            let (zs, ws) :=
+              split_at n @@ deserialize 0 ys in
+              Array16 zs :: ws
+        | "221" :: s1 :: s2 :: s3 :: s4 :: ys =>
+          let n :=
+            nat_of_ascii32 ((s1, s2), (s3, s4)) in
+            let (zs, ws) :=
+              split_at n @@ deserialize 0 ys in
+              Array32 zs :: ws
+        | Ascii b1 b2 b3 b4 false false false true :: ys =>
+          let n :=
+            nat_of_ascii8 (Ascii b1 b2 b3 b4 false false false false) in
+            let (zs, ws) :=
+              split_at (2 * n) @@ deserialize 0 ys in
+              FixMap (pair zs) :: ws
+        | "222" :: s1 :: s2 :: ys =>
+          let n :=
+            nat_of_ascii16 (s1,s2) in
+            let (zs, ws) :=
+              split_at (2 * n) @@ deserialize 0 ys in
+              Map16 (pair zs) :: ws
+        | "223" :: s1 :: s2 :: s3 :: s4 :: ys =>
+          let n :=
+            nat_of_ascii32 ((s1, s2), (s3, s4)) in
+            let (zs, ws) :=
+              split_at (2 * n) @@ deserialize 0 ys in
+              Map32 (pair zs) :: ws
+        | _ =>
+          []
+      end
+    | S m =>
+      match xs with
+        | y::ys => FixRaw [ y ]::deserialize m ys
+        | _ => []
+      end
+  end.
+
+Definition DeserializeCorrect os bs :=
+  SerializedList os bs ->
+  deserialize 0 bs = os.
+
+Lemma correct_bot :
+  DeserializeCorrect [] [].
+Proof with auto.
+unfold DeserializeCorrect...
+Qed.
+
+Lemma correct_nil : forall os bs,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect (Nil :: os) ("192"::bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H0.
+apply H in H3.
+rewrite <- H3...
+Qed.
+
+Lemma correct_false: forall os bs,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Bool false) :: os) ("194"::bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H0.
+apply H in H3.
+rewrite <- H3...
+Qed.
+
+Lemma correct_true: forall os bs,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Bool true) :: os) ("195"::bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H0.
+apply H in H3.
+rewrite <- H3...
+Qed.
+
+Lemma correct_pfixnum: forall os bs x1 x2 x3 x4 x5 x6 x7,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))::os)
+                     ((Ascii x1 x2 x3 x4 x5 x6 x7 false)::bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H0.
+apply H in H2.
+rewrite <- H2.
+destruct x1,x2,x3,x4,x5,x6,x7; reflexivity.
+Qed.
+
+Lemma correct_nfixnum: forall os bs x1 x2 x3 x4 x5,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect
+     ((NFixnum   (Ascii x1 x2 x3 x4 x5 true true true))::os)
+     ((Ascii x1 x2 x3 x4 x5 true true true)::bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H0.
+apply H in H2.
+rewrite <- H2.
+destruct x1,x2,x3,x4,x5; reflexivity.
+Qed.
+
+Lemma correct_uint8 : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Uint8 c)::os) ("204"::list_of_ascii8 c ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H0.
+apply H in H2.
+rewrite <- H2...
+Qed.
+
+Lemma correct_uint16 : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Uint16 c)::os) ("205"::list_of_ascii16 c ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+destruct c.
+inversion H0.
+apply H in H2.
+rewrite <- H2...
+Qed.
+
+Lemma correct_uint32 : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Uint32 c)::os) ("206"::list_of_ascii32 c ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+destruct c.
+destruct a, a0.
+inversion H0.
+apply H in H2.
+rewrite <- H2...
+Qed.
+
+Lemma correct_uint64 : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Uint64 c)::os) ("207"::list_of_ascii64 c ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+destruct c.
+destruct a, a0.
+destruct a, a0, a1, a2.
+inversion H0.
+apply H in H2.
+rewrite <- H2...
+Qed.
+
+Lemma correct_int8 : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Int8 c)::os) ("208"::list_of_ascii8 c ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H0.
+apply H in H2.
+rewrite <- H2...
+Qed.
+
+Lemma correct_int16 : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Int16 c)::os) ("209"::list_of_ascii16 c ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+destruct c.
+inversion H0.
+apply H in H2.
+rewrite <- H2...
+Qed.
+
+Lemma correct_int32 : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Int32 c)::os) ("210"::list_of_ascii32 c ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+destruct c.
+destruct a, a0.
+inversion H0.
+apply H in H2.
+rewrite <- H2...
+Qed.
+
+Lemma correct_int64 : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Int64 c)::os) ("211"::list_of_ascii64 c ++ bs).
+Proof.
+unfold DeserializeCorrect.
+intros.
+destruct c.
+destruct a, a0.
+destruct a, a0, a1, a2.
+inversion H0.
+apply H in H2.
+rewrite <- H2.
+reflexivity.
+Qed.
+
+Lemma correct_float : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Float c)::os) ("202"::list_of_ascii32 c ++ bs).
+Proof.
+unfold DeserializeCorrect.
+intros.
+destruct c.
+destruct a, a0.
+inversion H0.
+apply H in H2.
+rewrite <- H2.
+reflexivity.
+Qed.
+
+Lemma correct_double : forall os bs c,
+  DeserializeCorrect os bs ->
+  DeserializeCorrect ((Double c)::os) ("203"::list_of_ascii64 c ++ bs).
+Proof.
+unfold DeserializeCorrect.
+intros.
+destruct c.
+destruct a, a0.
+destruct a, a0, a1, a2.
+inversion H0.
+apply H in H2.
+rewrite <- H2.
+reflexivity.
+Qed.
+
+Lemma deserialize_take_length: forall xs ys,
+  take (List.length xs) (deserialize (List.length xs) (xs ++ ys)) = List.map (fun x => FixRaw [ x ]) xs.
+Proof with auto.
+induction xs; [ reflexivity | intros ].
+simpl.
+rewrite IHxs...
+Qed.
+
+Lemma deserialize_drop_length: forall xs ys,
+  drop (List.length xs) (deserialize (List.length xs) (xs ++ ys)) = deserialize 0 ys.
+Proof with auto.
+induction xs; [ reflexivity | intros ].
+simpl.
+rewrite IHxs...
+Qed.
+
+Lemma compact_eq : forall xs,
+  compact (List.map (fun x => FixRaw [ x ]) xs) = xs.
+Proof with auto.
+induction xs; [ reflexivity | intros ].
+simpl.
+rewrite IHxs...
+Qed.
+
+Lemma correct_fixraw: forall os bs cs b1 b2 b3 b4 b5,
+ DeserializeCorrect os bs ->
+ Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (List.length cs) ->
+ List.length cs < pow 5 ->
+ DeserializeCorrect (FixRaw cs :: os) ((Ascii b1 b2 b3 b4 b5 true false true) :: cs ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H2.
+assert (bs0 = bs); [| rewrite_for bs0 ].
+ apply app_same in H11...
+apply H in H13.
+assert (length cs < pow 8).
+ transitivity (pow 5); auto.
+ apply pow_lt...
+destruct b1,b2,b3,b4,b5;
+  ((replace (deserialize 0 _ ) with
+    (let n := nat_of_ascii8 (ascii8_of_nat (length cs)) in
+     let (zs, ws) := split_at n @@ deserialize n (cs++bs) in
+     FixRaw (compact zs) :: ws));
+  [ unfold atat, split_at;
+    rewrite nat_ascii8_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, <- H13
+  | rewrite <- H7])...
+Qed.
+
+Lemma correct_raw16: forall os bs cs s1 s2,
+ DeserializeCorrect os bs ->
+ (s1, s2) = ascii16_of_nat (List.length cs) ->
+ List.length cs < pow 16 ->
+ DeserializeCorrect (Raw16 cs :: os) ("218" :: s1 :: s2 :: cs ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H2.
+assert (bs0 = bs); [| rewrite_for bs0 ].
+ apply app_same in H8...
+apply H in H10.
+change (deserialize 0 _ ) with
+  (let (zs, ws) :=
+    split_at (nat_of_ascii16 (s1,s2)) @@ deserialize (nat_of_ascii16 (s1,s2)) (cs++bs) in
+    Raw16 (compact zs) :: ws).
+unfold atat, split_at.
+rewrite H7, nat_ascii16_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, H10...
+Qed.
+
+Lemma correct_raw32: forall os bs cs s1 s2 s3 s4,
+  DeserializeCorrect os bs ->
+  ((s1, s2), (s3, s4)) = ascii32_of_nat (List.length cs) ->
+  List.length cs < pow 32 ->
+  DeserializeCorrect (Raw32 cs :: os) ("219" :: s1 :: s2 :: s3 :: s4 :: cs ++ bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H2.
+assert (bs0 = bs); [| rewrite_for bs0 ].
+ apply app_same in H10...
+apply H in H12.
+change (deserialize 0 _ ) with
+  (let (zs, ws) :=
+    split_at (nat_of_ascii32 ((s1,s2),(s3,s4))) @@ deserialize (nat_of_ascii32 ((s1,s2),(s3,s4))) (cs++bs) in
+    Raw32 (compact zs) :: ws).
+unfold atat, split_at.
+rewrite H7, nat_ascii32_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, H12...
+Qed.
+
+Lemma correct_fixarray : forall os bs n xs ys b1 b2 b3 b4,
+  DeserializeCorrect os bs ->
+  (xs, ys) = split_at n os ->
+  n < pow 4 ->
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat n ->
+  DeserializeCorrect (FixArray xs :: ys) (Ascii b1 b2 b3 b4 true false false true :: bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H3.
+assert (os = os0); [| rewrite_for os0 ].
+ apply split_at_soundness in H0.
+ apply split_at_soundness in H12.
+ rewrite H0, H12...
+apply H in H9.
+assert (n0 < pow 8).
+ transitivity (pow 4); auto.
+ apply pow_lt...
+destruct b1, b2, b3, b4;
+ (replace (deserialize 0 (_ :: bs)) with
+   (let (zs, ws) :=
+      split_at (nat_of_ascii8 (ascii8_of_nat n0)) @@ deserialize 0 bs
+    in
+      FixArray zs :: ws);
+   [ unfold atat; rewrite H9, nat_ascii8_embedding, <- H12 | rewrite <- H14])...
+Qed.
+
+Lemma correct_array16 : forall os bs n xs ys s1 s2 ,
+ DeserializeCorrect os bs ->
+ n < pow 16 ->
+ (s1, s2) = ascii16_of_nat n ->
+ (xs, ys) = split_at n os ->
+ DeserializeCorrect (Array16 xs :: ys) ("220" :: s1 :: s2 :: bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H3.
+assert (os = os0).
+ apply split_at_soundness in H2.
+ apply split_at_soundness in H10.
+ rewrite H2, H10...
+
+ rewrite_for os0.
+ apply H in H9.
+ assert ( n = nat_of_ascii16 (s1, s2)).
+  rewrite H1.
+  rewrite nat_ascii16_embedding...
+
+  simpl.
+  change (nat_of_ascii8 s1 * 256 + nat_of_ascii8 s2) with (nat_of_ascii16 (s1, s2)).
+  rewrite <- H13.
+  inversion H2.
+  rewrite <- H9...
+Qed.
+
+Lemma correct_array32: forall os bs n xs ys s1 s2 s3 s4,
+ DeserializeCorrect os bs ->
+ (xs, ys) = split_at n os ->
+ n < pow 32 ->
+ ((s1, s2), (s3, s4)) = ascii32_of_nat n ->
+ DeserializeCorrect (Array32 xs :: ys) ("221" :: s1 :: s2 :: s3 :: s4 :: bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H3.
+assert (os = os0).
+ apply split_at_soundness in H0.
+ apply split_at_soundness in H12.
+ rewrite H0, H12...
+
+ rewrite_for os0.
+ apply H in H9.
+ change (deserialize 0 ("221" :: s1 :: s2 :: s3 :: s4 :: bs)) with
+   (let (zs, ws) := split_at (nat_of_ascii32 (s1, s2, (s3, s4))) (deserialize 0 bs) in
+    Array32 zs :: ws).
+ rewrite H9, H14, nat_ascii32_embedding, <- H12...
+Qed.
+
+Lemma correct_fixmap: forall os bs n xs ys b1 b2 b3 b4,
+  DeserializeCorrect os bs ->
+  (xs, ys) = split_at (2 * n) os ->
+  length xs = 2 * n ->
+  n < pow 4 ->
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat n ->
+  DeserializeCorrect (FixMap (pair xs) :: ys) (Ascii b1 b2 b3 b4 false false false true :: bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H4.
+assert ( n < pow 8).
+ transitivity (pow 4); auto.
+ apply pow_lt...
+assert ( n0 < pow 8).
+ transitivity (pow 4); auto.
+ apply pow_lt...
+assert (n0 = n); [| rewrite_for n0 ].
+ rewrite H3 in H16.
+ apply ascii8_of_nat_eq in H16...
+assert (xs0 = xs); [| rewrite_for xs0 ].
+ rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto.
+ rewrite H5...
+assert (os0 = os); [| rewrite_for os0 ].
+ apply split_at_soundness in H0.
+ apply split_at_soundness in H13.
+ rewrite H0, H13...
+apply H in H11.
+destruct b1, b2, b3, b4;
+  (replace (deserialize 0 (_ :: bs)) with
+    (let (zs, ws) :=
+       split_at (2 * (nat_of_ascii8 (ascii8_of_nat n))) @@ deserialize 0 bs
+     in
+       FixMap (pair zs) :: ws);
+    [ unfold atat; rewrite nat_ascii8_embedding, H11, <- H13
+    | rewrite <- H16 ])...
+Qed.
+
+Lemma correct_map16: forall os bs n xs ys s1 s2,
+  DeserializeCorrect os bs ->
+  (xs, ys) = split_at (2 * n) os ->
+  length xs = 2 * n ->
+  n < pow 16 ->
+  (s1, s2) = ascii16_of_nat n ->
+  DeserializeCorrect (Map16 (pair xs) :: ys) ("222" :: s1 :: s2 :: bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H4.
+assert (n0 = n).
+ rewrite H3 in H14.
+ apply ascii16_of_nat_eq in H14...
+rewrite_for n0.
+assert (xs0 = xs).
+ rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto.
+ rewrite H5...
+rewrite_for xs0.
+assert (os0 = os).
+ apply split_at_soundness in H0.
+ apply split_at_soundness in H11.
+ rewrite H0, H11...
+rewrite_for os0.
+apply H in H10.
+change (deserialize 0 ("222" :: s1 :: s2 :: bs)) with
+  (let (zs, ws) := split_at (2 * nat_of_ascii16 (s1, s2)) @@ deserialize 0 bs in
+  Map16 (pair zs) :: ws).
+unfold atat.
+rewrite H10, H14, nat_ascii16_embedding, <- H11...
+Qed.
+
+Lemma correct_map32: forall os bs n xs ys s1 s2 s3 s4,
+  DeserializeCorrect os bs ->
+  (xs, ys) = split_at (2 * n) os ->
+  length xs = 2 * n ->
+  n < pow 32 ->
+  ((s1, s2), (s3, s4)) = ascii32_of_nat n ->
+  DeserializeCorrect (Map32 (pair xs) :: ys) ("223" :: s1 :: s2 :: s3 :: s4 :: bs).
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+inversion H4.
+assert (n0 = n); [| rewrite_for n0 ].
+ rewrite H3 in H16.
+ apply ascii32_of_nat_eq in H16...
+assert (xs0 = xs); [| rewrite_for xs0 ].
+ rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto.
+ rewrite H5...
+assert (os0 = os); [| rewrite_for os0 ].
+ apply split_at_soundness in H0.
+ apply split_at_soundness in H13.
+ rewrite H0, H13...
+apply H in H11.
+change (deserialize 0 ("223" :: s1 :: s2 :: s3 :: s4 :: bs)) with
+  (let (zs, ws) := split_at (2 * nat_of_ascii32 ((s1, s2),(s3,s4))) @@ deserialize 0 bs in
+    Map32 (pair zs) :: ws).
+unfold atat.
+rewrite H16, H11, nat_ascii32_embedding, <- H13...
+Qed.
+
+Lemma correct_intro : forall os bs,
+  (SerializedList os bs -> DeserializeCorrect os bs) ->
+  DeserializeCorrect os bs.
+Proof with auto.
+unfold DeserializeCorrect.
+intros.
+apply H in H0...
+Qed.
+
+Theorem deserialize_correct : forall os bs,
+  DeserializeCorrect os bs.
+Proof with auto.
+intros.
+apply correct_intro.
+intros.
+pattern os, bs.
+apply SerializedList_ind; intros; auto.
+ apply correct_bot...
+ apply correct_nil...
+ apply correct_true...
+ apply correct_false...
+ apply correct_pfixnum...
+ apply correct_nfixnum...
+ apply correct_uint8...
+ apply correct_uint16...
+ apply correct_uint32...
+ apply correct_uint64...
+ apply correct_int8...
+ apply correct_int16...
+ apply correct_int32...
+ apply correct_int64...
+ apply correct_float...
+ apply correct_double...
+ apply correct_fixraw...
+ simpl; apply correct_raw16...
+ simpl; apply correct_raw32...
+ apply correct_fixarray with (os:=os0) (n:=n)...
+ apply correct_array16 with (os:=os0) (n:=n)...
+ apply correct_array32 with (os:=os0) (n:=n)...
+ apply correct_fixmap with (os:=os0) (n:=n)...
+ apply correct_map16 with (os:=os0) (n:=n)...
+ apply correct_map32 with (os:=os0) (n:=n)...
+Qed.
+
+Lemma app_nil: forall A (xs : list A),
+  xs ++ [] = xs.
+Proof.
+induction xs.
+ reflexivity.
+simpl.
+rewrite IHxs.
+reflexivity.
+Qed.
+
diff --git a/ocaml/proof/ExtractUtil.v b/ocaml/proof/ExtractUtil.v
new file mode 100644
index 00000000..42fcbca4
--- /dev/null
+++ b/ocaml/proof/ExtractUtil.v
@@ -0,0 +1,95 @@
+Require Ascii.
+Require String.
+Require List.
+
+
+(* basic types for OCaml *)
+Parameter mlunit mlchar mlint mlstring : Set.
+
+(* unit *)
+Extract Constant mlunit => "unit".
+
+(* bool *)
+Extract Inductive bool => "bool" ["true" "false"].
+Extract Inductive sumbool => "bool" ["true" "false"].
+
+(* int *)
+Extract Constant mlint => "int".
+Parameter mlint_of_nat : nat -> mlint.
+Parameter nat_of_mlint : mlint -> nat.
+Extract Constant mlint_of_nat =>
+  "let rec iter = function O -> 0 | S p -> succ (iter p) in iter".
+Extract Constant nat_of_mlint =>
+  "let rec iter = function 0 -> O | n -> S (iter (pred n)) in iter".
+
+(* char *)
+Extract Constant mlchar => "char".
+Parameter mlchar_of_mlint : mlint -> mlchar.
+Parameter mlint_of_mlchar : mlchar -> mlint.
+Extract Constant mlchar_of_mlint => "char_of_int".
+Extract Constant mlint_of_mlchar => "int_of_char".
+
+(* list *)
+Extract Inductive list => "list" ["[]" "(::)"].
+
+(* option *)
+Extract Inductive option => "option" ["None" "Some"].
+
+(* string *)
+Extract Constant mlstring => "string".
+Extract Inductive String.string => "ascii list" ["[]" "(::)"].
+Parameter string_of_list : List.list Ascii.ascii -> String.string.
+Parameter list_of_string : String.string -> List.list Ascii.ascii.
+Extract Constant list_of_string => "(fun x -> x)".
+Extract Constant string_of_list => "(fun x -> x)".
+
+Parameter mlstring_of_list : forall {A:Type},
+  (A->mlchar) -> List.list A -> mlstring.
+Parameter list_of_mlstring : forall {A:Type},
+  (mlchar->A) -> mlstring -> List.list A.
+Extract Constant mlstring_of_list =>
+  "(fun f s -> String.concat """"
+     (List.map (fun x -> String.make 1 (f x)) s))".
+Extract Constant list_of_mlstring => "
+(fun f s ->
+  let rec explode_rec n =
+    if n >= String.length s then
+      []
+    else
+      f (String.get s n) :: explode_rec (succ n)
+  in
+  explode_rec 0)
+".
+
+Parameter mlstring_of_mlint : mlint -> mlstring.
+Extract Constant mlstring_of_mlint => "string_of_int".
+
+
+(* print to stdout *)
+Parameter print_mlstring : mlstring -> mlunit.
+Parameter println_mlstring : mlstring -> mlunit.
+Parameter prerr_mlstring : mlstring -> mlunit.
+Parameter prerrln_mlstring : mlstring -> mlunit.
+Parameter semicolon_flipped : forall {A:Type}, A -> mlunit -> A.
+Extract Constant semicolon_flipped => "(fun x f -> f; x)".
+Extract Constant print_mlstring => "print_string".
+Extract Constant println_mlstring => "print_endline".
+Extract Constant prerr_mlstring => "print_string".
+Extract Constant prerrln_mlstring => "print_endline".
+
+CoInductive llist (A: Type) : Type :=
+  LNil | LCons (x: A) (xs: llist A).
+
+Implicit Arguments LNil [A].
+Implicit Arguments LCons [A].
+
+Parameter get_contents_mlchars : llist mlchar.
+Extract Constant get_contents_mlchars => "
+ let rec iter store =
+   lazy
+     begin
+       try (LCons (input_char stdin, iter())) with
+       | End_of_file -> LNil
+     end
+ in
+ iter ()".
diff --git a/ocaml/proof/ListUtil.v b/ocaml/proof/ListUtil.v
new file mode 100644
index 00000000..22a82821
--- /dev/null
+++ b/ocaml/proof/ListUtil.v
@@ -0,0 +1,259 @@
+Require Import List Omega.
+
+Notation "[ ]" := nil : list_scope.
+Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.
+
+Lemma app_same : forall A (xs ys zs : list A),
+  xs ++  ys = xs ++ zs -> ys = zs.
+Proof.
+induction xs; intros; simpl in H.
+ auto.
+
+ inversion H.
+ apply IHxs in H1.
+ auto.
+Qed.
+Lemma length_lt_O: forall A (x : A) xs,
+  length (x::xs) > 0.
+Proof.
+intros.
+simpl.
+omega.
+Qed.
+
+Lemma length_inv: forall A (x y : A) xs ys,
+  length (x :: xs) = length (y :: ys) ->
+  length xs = length ys.
+Proof.
+intros.
+inversion H.
+auto.
+Qed.
+
+Hint Resolve length_lt_O.
+
+
+Fixpoint take {A} n (xs : list A) :=
+  match n, xs with
+    | O , _ => []
+    | _ , [] => []
+    | S m, x::xs =>
+      x::take m xs
+  end.
+
+Fixpoint drop {A} n (xs : list A) :=
+  match n, xs with
+    | O , _ => xs
+    | _ , [] => []
+    | S m, x::xs =>
+      drop m xs
+  end.
+
+Definition split_at {A} (n : nat) (xs : list A) : list A * list A :=
+  (take n xs, drop n xs).
+
+Lemma take_length : forall A ( xs ys : list A) n,
+  n = List.length xs ->
+  take n (xs ++ ys) = xs.
+Proof.
+induction xs; intros; simpl in *.
+ rewrite H.
+ reflexivity.
+
+ rewrite H.
+ simpl.
+ rewrite IHxs; auto.
+Qed.
+
+Lemma drop_length : forall A ( xs ys : list A) n,
+  n = List.length xs ->
+  drop n (xs ++ ys) = ys.
+Proof.
+induction xs; intros; simpl in *.
+ rewrite H.
+ reflexivity.
+
+ rewrite H.
+ simpl.
+ rewrite IHxs; auto.
+Qed.
+
+Lemma split_at_length : forall A (xs ys : list A),
+  (xs, ys) = split_at (length xs) (xs ++ ys).
+Proof.
+intros.
+unfold split_at.
+rewrite take_length, drop_length; auto.
+Qed.
+
+Lemma take_length_lt : forall A (xs ys : list A) n,
+  ys = take n xs ->
+  List.length ys <= n.
+Proof.
+induction xs; intros.
+ rewrite H.
+ destruct n; simpl; omega...
+
+ destruct n.
+  rewrite H.
+  simpl.
+  auto...
+
+  destruct ys; [ discriminate |].
+  inversion H.
+  rewrite <- H2.
+  apply IHxs in H2.
+  simpl.
+  omega...
+Qed.
+
+Lemma split_at_length_lt : forall A (xs ys zs : list A) n,
+  (xs, ys) = split_at n zs ->
+  List.length xs <= n.
+Proof.
+intros.
+unfold split_at in *.
+inversion H.
+apply (take_length_lt _ zs).
+reflexivity.
+Qed.
+
+Lemma split_at_soundness : forall A (xs ys zs : list A) n,
+  (ys,zs) = split_at n xs ->
+  xs = ys ++ zs.
+Proof.
+induction xs; induction n; intros; simpl;
+  try (inversion H; reflexivity).
+
+  unfold split_at in *.
+  simpl in H.
+  destruct ys.
+   inversion H.
+
+   rewrite (IHxs ys zs n); auto.
+    inversion H.
+    reflexivity.
+
+    inversion H.
+    reflexivity.
+Qed.
+
+Lemma take_nil : forall A n,
+  take n ([] : list A) = [].
+Proof.
+induction n; auto.
+Qed.
+
+Lemma take_drop_length : forall A ( xs ys : list A) n,
+  take n xs = ys ->
+  drop n xs = [ ] ->
+  xs  = ys.
+Proof.
+induction xs; intros; simpl in *.
+ rewrite take_nil in H.
+ assumption.
+
+ destruct n.
+  simpl in H0.
+  discriminate.
+
+  simpl in *.
+  destruct ys.
+   discriminate.
+
+   inversion H.
+   rewrite H3.
+   apply IHxs in H3; auto.
+   rewrite H3.
+   reflexivity.
+Qed.
+
+Fixpoint pair { A } ( xs : list A ) :=
+  match xs with
+    | [] => []
+    | [x] => []
+    | k :: v :: ys =>
+      (k, v) :: pair ys
+  end.
+
+Definition unpair {A} (xs : list (A * A)) :=
+  flat_map (fun x => [ fst x; snd x]) xs.
+
+Lemma pair_unpair : forall A ( xs : list ( A * A )),
+  pair (unpair xs) = xs.
+Proof.
+induction xs; intros; simpl; auto.
+rewrite IHxs.
+destruct a.
+simpl.
+reflexivity.
+Qed.
+
+Lemma unpair_pair : forall A n ( xs : list A),
+  List.length xs = 2 * n ->
+  unpair (pair xs) = xs.
+Proof.
+induction n; intros.
+ destruct xs; auto.
+ simpl in H.
+ discriminate.
+
+ destruct xs.
+  simpl in H.
+  discriminate...
+
+  destruct xs.
+   simpl in H.
+   assert (1 <> S (n + S (n + 0))); [ omega | contradiction ]...
+
+   replace (2 * S n) with (2 + 2 * n) in H; [| omega ].
+   simpl in *.
+   inversion H.
+   apply IHn in H1.
+   rewrite H1.
+   reflexivity.
+Qed.
+
+Lemma pair_length' : forall A n (xs : list A),
+  n = List.length (pair xs) ->
+  2 * n <= List.length xs.
+Proof.
+induction n; intros; simpl.
+ omega...
+
+ destruct xs; simpl in *; [ discriminate |].
+ destruct xs; simpl in *; [ discriminate |].
+ inversion H.
+ apply IHn in H1.
+ omega.
+Qed.
+
+
+Lemma pair_length : forall A (xs : list A),
+  2 * List.length (pair xs) <= List.length xs.
+Proof.
+intros.
+apply pair_length'.
+reflexivity.
+Qed.
+
+Lemma unpair_length : forall A ( xs : list (A * A)),
+  List.length (unpair xs) = 2 * List.length xs.
+Proof.
+induction xs; simpl; auto.
+rewrite IHxs.
+omega.
+Qed.
+
+Lemma unpair_split_at: forall A (x1 x2 : A) xs ys,
+  (unpair ((x1, x2) :: xs), ys) =
+  split_at (2 * length ((x1, x2) :: xs)) (x1 :: x2 :: unpair xs ++ ys).
+Proof.
+intros.
+replace (2 * (length ((x1,x2) :: xs))) with (length (unpair ((x1,x2)::xs))).
+ apply split_at_length.
+
+ simpl.
+ rewrite unpair_length.
+ omega.
+Qed.
\ No newline at end of file
diff --git a/ocaml/proof/Main.v b/ocaml/proof/Main.v
new file mode 100644
index 00000000..e189c802
--- /dev/null
+++ b/ocaml/proof/Main.v
@@ -0,0 +1,3 @@
+Require Import ExtrOcamlBasic ExtrOcamlIntConv ExtrOcamlNatInt.
+Require Import SerializeImplement DeserializeImplement.
+Extraction "msgpackCore.ml" serialize deserialize.
diff --git a/ocaml/proof/MultiByte.v b/ocaml/proof/MultiByte.v
new file mode 100644
index 00000000..3aa33416
--- /dev/null
+++ b/ocaml/proof/MultiByte.v
@@ -0,0 +1,334 @@
+(*
+   16bits,32bits,64bitsの定義。BigEndian。
+*)
+Require Import List Ascii NArith Omega Euclid.
+Require Import Pow.
+
+Open Scope char_scope.
+
+(* * 型の定義 *)
+Definition ascii8  : Set := ascii.
+Definition ascii16 : Set := (ascii8  * ascii8)%type.
+Definition ascii32 : Set := (ascii16 * ascii16)%type.
+Definition ascii64 : Set := (ascii32 * ascii32)%type.
+
+(** ** natとの相互変換 *)
+Definition nat_of_ascii8 :=
+  nat_of_ascii.
+
+Definition ascii8_of_nat :=
+  ascii_of_nat.
+
+Definition ascii16_of_nat (a : nat)  :=
+  let (q,r,_,_) := divmod a (pow 8) (pow_lt_O 8) in
+    (ascii8_of_nat q, ascii8_of_nat r).
+
+Definition nat_of_ascii16 (a : ascii16) :=
+  let (a1, a2) := a in
+    (nat_of_ascii8 a1) * (pow 8) + (nat_of_ascii8 a2).
+
+Definition ascii32_of_nat (a : nat)  :=
+  let (q,r,_,_) := divmod a (pow 16) (pow_lt_O 16) in
+    (ascii16_of_nat q, ascii16_of_nat r).
+
+Definition nat_of_ascii32 (a : ascii32) :=
+  let (a1, a2) := a in
+    (nat_of_ascii16 a1) * (pow 16) + (nat_of_ascii16 a2).
+
+Definition ascii64_of_nat (a : nat)  :=
+  let (q,r,_,_) := divmod a (pow 32) (pow_lt_O 32) in
+    (ascii32_of_nat q, ascii32_of_nat r).
+
+Definition nat_of_ascii64 (a : ascii64) :=
+  let (a1, a2) := a in
+    (nat_of_ascii32 a1) * (pow 32) + (nat_of_ascii32 a2).
+
+(** ** natに戻せることの証明 *)
+Lemma nat_ascii8_embedding : forall n,
+  n < pow 8 ->
+  nat_of_ascii8 (ascii8_of_nat n) = n.
+Proof.
+intros.
+unfold nat_of_ascii8,ascii8_of_nat.
+rewrite nat_ascii_embedding.
+ reflexivity.
+
+ simpl in H.
+ assumption.
+Qed.
+
+Lemma nat_ascii16_embedding : forall n,
+  n < pow 16 ->
+  nat_of_ascii16 (ascii16_of_nat n) = n.
+Proof.
+intros.
+unfold ascii16_of_nat, nat_of_ascii16.
+destruct divmod.
+rewrite (nat_ascii8_embedding q), (nat_ascii8_embedding r); try omega.
+apply divmod_lt_q with (t := 8) in e;
+  change (8+8) with 16; assumption.
+Qed.
+
+Lemma nat_ascii32_embedding : forall n,
+  n < pow 32 ->
+  nat_of_ascii32 (ascii32_of_nat n) = n.
+Proof.
+intros.
+unfold ascii32_of_nat, nat_of_ascii32.
+destruct divmod.
+rewrite (nat_ascii16_embedding q), (nat_ascii16_embedding r); try omega.
+apply divmod_lt_q with (t := 16) in e;
+  change (16+16) with 32; assumption.
+Qed.
+
+Lemma nat_ascii64_embedding : forall n,
+  n < pow 64 ->
+  nat_of_ascii64 (ascii64_of_nat n) = n.
+Proof.
+intros.
+unfold ascii64_of_nat, nat_of_ascii64.
+destruct divmod.
+rewrite (nat_ascii32_embedding q), (nat_ascii32_embedding r); try omega.
+apply divmod_lt_q with (t := 32) in e;
+  change (32+32) with 64; assumption.
+Qed.
+
+(** ** ascii8への変換 *)
+Definition list_of_ascii8  (x : ascii8) :=
+  x :: nil.
+
+Definition list_of_ascii16 (p : ascii16) :=
+  match p with
+    (x1,x2) => (list_of_ascii8 x1) ++ (list_of_ascii8 x2)
+  end.
+
+Definition list_of_ascii32 (p : ascii32) :=
+  match p with
+    (x1,x2) => (list_of_ascii16 x1) ++ (list_of_ascii16 x2)
+  end.
+
+Definition list_of_ascii64 (p : ascii64) :=
+  match p with
+    (x1,x2) => (list_of_ascii32 x1) ++ (list_of_ascii32 x2)
+  end.
+
+Lemma list_of_ascii8_eq : forall c1 c2,
+  list_of_ascii8 c1 = list_of_ascii8 c2 ->
+  c1 = c2.
+Proof.
+intros.
+unfold list_of_ascii8 in H.
+inversion H.
+reflexivity.
+Qed.
+
+Lemma list_of_ascii16_eq : forall c1 c2,
+  list_of_ascii16 c1 = list_of_ascii16 c2 ->
+  c1 = c2.
+Proof.
+intros.
+destruct c1; destruct c2.
+inversion H.
+reflexivity.
+Qed.
+
+Lemma list_of_ascii32_eq : forall c1 c2,
+  list_of_ascii32 c1 = list_of_ascii32 c2 ->
+  c1 = c2.
+Proof.
+intros.
+destruct c1; destruct c2.
+destruct a; destruct a0; destruct a1; destruct a2.
+inversion H.
+reflexivity.
+Qed.
+
+Lemma list_of_ascii64_eq : forall c1 c2,
+  list_of_ascii64 c1 = list_of_ascii64 c2 ->
+  c1 = c2.
+Proof.
+intros.
+destruct c1; destruct c2.
+destruct a; destruct a0; destruct a1; destruct a2.
+destruct a; destruct a3; destruct a0; destruct a4;
+destruct a1; destruct a5; destruct a2; destruct a6.
+inversion H.
+reflexivity.
+Qed.
+
+(** 0でないことの証明 *)
+Lemma ascii8_not_O: forall n,
+  0 < n < pow 8 ->
+  "000" <> ascii8_of_nat n.
+Proof.
+intros.
+destruct H.
+apply nat_ascii8_embedding in H0.
+destruct (ascii8_of_nat n).
+intro.
+destruct b; destruct b0; destruct b1; destruct b2; destruct b3; destruct b4; destruct b5; destruct b6; inversion H1.
+compute in H0.
+rewrite <- H0 in H.
+inversion H.
+Qed.
+
+Lemma ascii16_not_O: forall n,
+  0 < n < pow 16 ->
+  ("000","000") <> ascii16_of_nat n.
+Proof.
+intros.
+unfold ascii16_of_nat.
+destruct divmod.
+destruct H.
+intro.
+inversion H1.
+generalize e; intro.
+apply divmod_not_O in e; auto with pow.
+decompose [or] e.
+ apply ascii8_not_O in H3; auto.
+ apply divmod_lt_q with (t:=8) in e0; auto with pow.
+
+ apply ascii8_not_O in H4; auto with pow.
+Qed.
+
+Lemma ascii32_not_O: forall n,
+  0 < n < pow 32 ->
+  ("000","000",("000","000")) <> ascii32_of_nat n.
+Proof.
+intros.
+unfold ascii32_of_nat.
+destruct divmod.
+destruct H.
+intro.
+inversion H1.
+generalize e; intro.
+apply divmod_not_O in e.
+ decompose [or] e.
+ apply divmod_lt_q with (t:=16) in e0.
+  apply ascii16_not_O in H3.
+   contradiction.
+
+   split; assumption.
+
+   assumption.
+
+   exact H0.
+
+ apply ascii16_not_O in H4.
+  contradiction.
+
+   split; assumption.
+
+   assumption.
+
+ apply pow_lt_O.
+Qed.
+
+(* ** 2^n未満なら等価性が変らないことの証明 *)
+Lemma ascii8_of_nat_eq : forall n m,
+  n < pow 8 ->
+  m < pow 8 ->
+  ascii8_of_nat n = ascii8_of_nat m ->
+  n = m.
+Proof.
+intros.
+rewrite <- (nat_ascii8_embedding n), <- (nat_ascii8_embedding m), <- H1; auto.
+Qed.
+
+Lemma ascii16_of_nat_eq : forall n m,
+  n < pow 16 ->
+  m < pow 16 ->
+  ascii16_of_nat n = ascii16_of_nat m ->
+  n = m.
+Proof.
+intros.
+rewrite <- (nat_ascii16_embedding n), <- (nat_ascii16_embedding m), <- H1; auto.
+Qed.
+
+Lemma ascii32_of_nat_eq : forall n m,
+  n < pow 32 ->
+  m < pow 32 ->
+  ascii32_of_nat n = ascii32_of_nat m ->
+  n = m.
+Proof.
+intros.
+rewrite <- (nat_ascii32_embedding n), <- (nat_ascii32_embedding m), <- H1; auto.
+Qed.
+
+Lemma ascii8_of_nat_O:
+  "000" = ascii8_of_nat 0.
+Proof.
+compute.
+reflexivity.
+Qed.
+
+Lemma ascii16_of_nat_O:
+  ("000", "000") = ascii16_of_nat 0.
+Proof.
+unfold ascii16_of_nat.
+destruct divmod.
+apply divmod_O_pow in e.
+decompose [and] e.
+rewrite H, H0.
+rewrite <- ascii8_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma ascii32_of_nat_O:
+  (("000", "000"),("000","000")) = ascii32_of_nat 0.
+Proof.
+unfold ascii32_of_nat.
+destruct divmod.
+apply divmod_O_pow in e.
+decompose [and] e.
+rewrite H, H0.
+rewrite <- ascii16_of_nat_O.
+reflexivity.
+Qed.
+
+(* lengthが等しいことの証明 *)
+Lemma ascii8_length : forall c1 c2,
+  length (list_of_ascii8 c1) = length (list_of_ascii8 c2).
+Proof.
+auto.
+Qed.
+
+Lemma ascii16_length : forall c1 c2,
+  length (list_of_ascii16 c1) = length (list_of_ascii16 c2).
+Proof.
+destruct c1,c2.
+auto.
+Qed.
+
+Lemma ascii32_length : forall c1 c2,
+  length (list_of_ascii32 c1) = length (list_of_ascii32 c2).
+Proof.
+destruct c1 as [a1 a2] ,c2 as [a3 a4].
+destruct a1,a2,a3,a4.
+auto.
+Qed.
+
+Lemma ascii64_length : forall c1 c2,
+  length (list_of_ascii64 c1) = length (list_of_ascii64 c2).
+Proof.
+destruct c1 as [a1 a2] ,c2 as [a3 a4].
+destruct a1 as [b1 b2], a2 as [b3 b4], a3 as [b5 b6], a4 as [b7 b8].
+destruct b1,b2,b3,b4,b5,b6,b7,b8.
+auto.
+Qed.
+
+Lemma ascii5 : forall n b1 b2 b3 b4 b5 b6 b7 b8,
+  n < pow 5 ->
+  Ascii b1 b2 b3 b4 b5 b6 b7 b8 = ascii8_of_nat n ->
+  b6 = false /\ b7 = false /\ b8 = false.
+Proof.
+intros.
+simpl in H.
+do 32 (destruct n; [ inversion H0; auto | idtac]).
+do 32 (apply Lt.lt_S_n in H).
+inversion H.
+Qed.
+
+Hint Resolve ascii16_length ascii32_length ascii64_length
+  list_of_ascii8_eq list_of_ascii16_eq list_of_ascii32_eq list_of_ascii64_eq
+  : ascii.
\ No newline at end of file
diff --git a/ocaml/proof/OCamlBase.v b/ocaml/proof/OCamlBase.v
new file mode 100644
index 00000000..f5c0be5a
--- /dev/null
+++ b/ocaml/proof/OCamlBase.v
@@ -0,0 +1,8 @@
+Require Export String.
+Require Export List.
+Require Export ExtractUtil.
+Require Export Util.
+
+Open Scope string_scope.
+
+Notation "op ; x" := (semicolon_flipped x op) (at level 50).
diff --git a/ocaml/proof/OMakefile b/ocaml/proof/OMakefile
new file mode 100644
index 00000000..5ce19233
--- /dev/null
+++ b/ocaml/proof/OMakefile
@@ -0,0 +1,26 @@
+open CoqBuildRule
+.PHONY: all clean
+
+FILES[] =
+	Pow
+	MultiByte
+	ListUtil
+	Object
+	SerializeSpec
+	Prefix
+	Soundness
+	SerializeImplement
+	SerializedList
+	DeserializeImplement
+	OCamlBase
+	Util
+	ExtractUtil
+	Main
+
+.DEFAULT: all
+
+all: msgpackCore.ml msgpackCore.mli
+msgpackCore.ml msgpackCore.mli: $(CoqProof $(FILES))
+	echo "Proof complete"
+clean:
+	rm -rf *.vo *.glob *~ *.omc .omakedb .omakedb.lock *.cm[iox] *.annot *.o msgpackCore.ml msgpackCore.mli
diff --git a/ocaml/proof/Object.v b/ocaml/proof/Object.v
new file mode 100644
index 00000000..a80928e7
--- /dev/null
+++ b/ocaml/proof/Object.v
@@ -0,0 +1,122 @@
+(* -*- coding:utf-8 -*- *)
+Require Import List Ascii.
+Require Import Pow MultiByte ListUtil.
+
+Open Scope char_scope.
+
+(** MsgPackで使うオブジェクトの定義 *)
+Inductive object :=
+| Bool (_ : bool)
+| Nil
+| PFixnum (_ : ascii8)
+| NFixnum (_ : ascii8)
+| Uint8  (_ : ascii8)
+| Uint16 (_ : ascii16)
+| Uint32 (_ : ascii32)
+| Uint64 (_ : ascii64)
+| Int8   (_ : ascii8)
+| Int16  (_ : ascii16)
+| Int32  (_ : ascii32)
+| Int64  (_ : ascii64)
+| Float  (_ : ascii32)
+| Double (_ : ascii64)
+| FixRaw (_ : list ascii8)
+| Raw16  (_ : list ascii8)
+| Raw32  (_ : list ascii8)
+| FixArray ( _ : list object)
+| Array16  ( _ : list object)
+| Array32  ( _ : list object)
+| FixMap   ( _ : list (object * object)%type)
+| Map16    ( _ : list (object * object)%type)
+| Map32    ( _ : list (object * object)%type).
+
+(** 妥当なオブジェクトの定義 *)
+Inductive Valid : object -> Prop :=
+| VBool : forall b,
+  Valid (Bool b)
+| VPFixNum : forall n,
+  nat_of_ascii8 n < 128 -> Valid (PFixnum n)
+| VNFixNum : forall n,
+  (* 負の数を導入したくないので、補数表現を使う *)
+  223 < nat_of_ascii8 n /\ nat_of_ascii8 n < 256 -> Valid (NFixnum n)
+| VUint8  : forall c, Valid (Uint8 c)
+| VUint16 : forall c, Valid (Uint16 c)
+| VUint32 : forall c, Valid (Uint32 c)
+| VUint64 : forall c, Valid (Uint64 c)
+| VInt8   : forall c, Valid (Int8 c)
+| VInt16  : forall c, Valid (Int16 c)
+| VInt32  : forall c, Valid (Int32 c)
+| VInt64  : forall c, Valid (Int64 c)
+| VFloat  : forall c, Valid (Float c)
+| VDouble : forall c, Valid (Double c)
+| VFixRaw : forall xs,
+  length xs < pow 5 -> Valid (FixRaw xs)
+| VRaw16 : forall xs,
+  length xs < pow 16 -> Valid (Raw16 xs)
+| VRaw32 : forall xs,
+  length xs < pow 32 -> Valid (Raw32 xs)
+| VFixArrayNil :
+  Valid (FixArray [])
+| VFixArrayCons : forall x xs,
+  Valid x ->
+  Valid (FixArray xs) ->
+  length (x::xs) < pow 4 ->
+  Valid (FixArray (x::xs))
+| VArray16Nil :
+  Valid (Array16 [])
+| VArray16Cons: forall x xs,
+  Valid x ->
+  Valid (Array16 xs) ->
+  length (x::xs) < pow 16 ->
+  Valid (Array16 (x::xs))
+| VArray32Nil :
+  Valid (Array32 [])
+| VArray32Cons : forall x xs,
+  Valid x ->
+  Valid (Array32 xs) ->
+  length (x::xs) < pow 32 ->
+  Valid (Array32 (x::xs))
+| VFixMapNil:
+  Valid (FixMap [])
+| VFixMapCons : forall k v xs,
+  Valid k ->
+  Valid v ->
+  Valid (FixMap xs)  ->
+  length ((k,v)::xs) < pow 4 ->
+  Valid (FixMap ((k,v)::xs))
+| VMap16Nil :
+  Valid (Map16 [])
+| VMap16Cons : forall k v xs,
+  Valid k ->
+  Valid v ->
+  Valid (Map16 xs)  ->
+  length ((k,v)::xs) < pow 16 ->
+  Valid (Map16 ((k,v)::xs))
+| VMap32Nil :
+  Valid (Map32 [])
+| VMap32Cons : forall k v xs,
+  Valid k ->
+  Valid v ->
+  Valid (Map32 xs)  ->
+  length ((k,v)::xs) < pow 32 ->
+  Valid (Map32 ((k,v)::xs)).
+
+Lemma varray16_inv1: forall x xs,
+  Valid (Array16 (x::xs)) ->
+  ("000", "000") <> ascii16_of_nat (length (x :: xs)).
+Proof.
+intros.
+apply ascii16_not_O.
+split; [ apply length_lt_O | inversion H; auto ].
+Qed.
+
+Lemma varray16_inv2 : forall A (x y : A) xs ys,
+  pow 16 > length (x :: xs) ->
+  pow 16 > length (y :: ys) ->
+  ascii16_of_nat (length (x :: xs)) = ascii16_of_nat (length (y :: ys)) ->
+  ascii16_of_nat (length xs) = ascii16_of_nat (length ys).
+Proof.
+intros.
+apply ascii16_of_nat_eq in H1; auto.
+Qed.
+
diff --git a/ocaml/proof/Pow.v b/ocaml/proof/Pow.v
new file mode 100644
index 00000000..23c0666e
--- /dev/null
+++ b/ocaml/proof/Pow.v
@@ -0,0 +1,162 @@
+(**
+   算術演算関連の補題
+*)
+
+Require Import Omega NArith Euclid.
+
+(** ** 算術演算 *)
+Lemma mult_S_lt_reg_l :
+  forall n m p, 0 < n -> n * m < n * p -> m < p.
+Proof.
+intros.
+destruct n.
+ inversion H.
+
+elim (le_or_lt m p).
+ intro.
+ inversion H1.
+  rewrite H2 in H0.
+   elim (lt_irrefl _ H0).
+   omega.
+
+   intro.
+   apply (mult_S_lt_compat_l n _ _) in H1.
+   omega.
+Qed.
+
+Lemma plus_elim: forall p a b,
+  a + p < b -> a < b.
+Proof.
+intros.
+omega.
+Qed.
+
+(** ** pow *)
+Fixpoint pow (n : nat) :=
+  match n with
+    | 0 =>
+      1
+    | S n' =>
+      2 * pow n'
+  end.
+
+Lemma pow_lt_O : forall n,
+  0 < pow n.
+Proof.
+induction n; simpl; omega.
+Qed.
+
+Hint Resolve pow_lt_O.
+
+Lemma pow_add: forall n m,
+  pow n * pow m = pow (n + m).
+Proof.
+induction n; intros.
+ simpl in *.
+ omega.
+
+ simpl.
+ repeat rewrite plus_0_r.
+ rewrite <- IHn, mult_plus_distr_r.
+ reflexivity.
+Qed.
+
+(** ** divmod *)
+Definition divmod (n m : nat) (P : 0 < m) :=
+  eucl_dev m P n.
+
+Lemma divmod_lt_q : forall (n m q r s t: nat),
+  n < pow (s + t) ->
+  n = q * pow s + r ->
+  q < pow t.
+Proof.
+intros.
+rewrite H0 in H.
+apply plus_elim in H.
+rewrite <- pow_add, mult_comm in H.
+apply mult_S_lt_reg_l in H.
+ assumption.
+
+ apply pow_lt_O.
+Qed.
+
+Lemma divmod_not_O: forall n m q r,
+  0 < n ->
+  0 < m ->
+  n = q * m + r ->
+  0 < q \/ 0 < r.
+Proof.
+intros.
+rewrite H1 in H.
+destruct q.
+ simpl in H.
+ right.
+ assumption.
+
+ left.
+ omega.
+Qed.
+
+Lemma divmod_O: forall n q r,
+  0 = q * n + r ->
+  n <> 0 ->
+  q = 0 /\ r = 0.
+Proof.
+intros.
+destruct q; destruct n; destruct r; try omega.
+ simpl in H.
+ discriminate.
+
+ simpl in H.
+ discriminate.
+Qed.
+
+Lemma divmod_O_pow: forall n q r,
+  0 = q * pow n + r ->
+  q = 0 /\ r = 0.
+Proof.
+intros.
+apply (divmod_O (pow n) _ _); auto.
+intro.
+generalize (pow_lt_O n); intros.
+omega.
+Qed.
+
+Lemma plus_O : forall n,
+  n + 0 = n.
+Proof.
+Admitted.
+
+Lemma plus_double : forall n,
+  n < n + n.
+Admitted.
+
+Lemma pow_lt : forall n m,
+  n < m ->
+  pow n < pow m.
+Proof.
+induction n; induction m; simpl; intros.
+ inversion H.
+
+ destruct m; auto.
+ transitivity (pow (S m));
+   [ apply IHm | idtac];
+  omega.
+
+ inversion H.
+
+ simpl in IHm.
+ inversion H; simpl.
+  repeat (rewrite plus_O in *).
+  apply (Plus.plus_lt_compat_r O _).
+  transitivity (pow n); auto.
+  apply plus_double.
+
+  assert (S n < m); auto.
+  apply IHm in H2.
+  transitivity (pow m); auto.
+  rewrite plus_O.
+  apply plus_double.
+Qed.
+
+Hint Resolve pow_lt pow_lt_O: pow.
diff --git a/ocaml/proof/Prefix.v b/ocaml/proof/Prefix.v
new file mode 100644
index 00000000..d9e456f3
--- /dev/null
+++ b/ocaml/proof/Prefix.v
@@ -0,0 +1,674 @@
+Require Import List Ascii.
+Require Import ListUtil Object SerializeSpec MultiByte ProofUtil Pow.
+
+Definition Prefix obj1 x : Prop := forall obj2 y xs ys,
+  Serialized obj1 x ->
+  Serialized obj2 y ->
+  Valid obj1 ->
+  Valid obj2 ->
+  x ++ xs = y ++ ys ->
+  x = y.
+
+Ltac destruct_serialize obj y :=
+  match goal with
+    | [ H1 : _ ++ _ = y ++ _,
+        H2 : Serialized obj y |- _ ] =>
+    destruct y as [ | a ] ;
+      [ inversion H2 | inversion H1 ; rewrite_for a; inversion H2 ];
+      auto
+  end.
+
+(* 結果が1バイトになる変換 *)
+Ltac straight_forward :=
+  intros;
+  unfold Prefix;
+  intros obj2 y xs ys S1 S2 V1 V2 Happ;
+  destruct_serialize obj2 y.
+
+Lemma prefix_true :
+  Prefix (Bool true) ["195"].
+Proof.
+straight_forward.
+Qed.
+
+Lemma prefix_false :
+  Prefix (Bool false) ["194"].
+Proof.
+straight_forward.
+Qed.
+
+Lemma prefix_nil :
+  Prefix Nil ["192"].
+Proof.
+straight_forward.
+Qed.
+
+Lemma prefix_pfixnum: forall x1 x2 x3 x4 x5 x6 x7,
+  Prefix (PFixnum   (Ascii x1 x2 x3 x4 x5 x6 x7 false))
+         [Ascii x1 x2 x3 x4 x5 x6 x7 false].
+Proof.
+straight_forward.
+Qed.
+
+Lemma prefix_nfixnum : forall  x1 x2 x3 x4 x5,
+  Prefix (NFixnum   (Ascii x1 x2 x3 x4 x5 true true true))
+         [Ascii x1 x2 x3 x4 x5 true true true].
+Proof.
+straight_forward.
+Qed.
+
+(* 結果が固定長多バイトになる変換 *)
+Lemma prefix_same : forall A (x y xs ys : list A),
+  x ++ xs = y ++ ys ->
+  length x = length y ->
+  x = y.
+Proof.
+induction x; induction y; intros; auto.
+ simpl in H0.
+ discriminate.
+
+ simpl in H0.
+ discriminate.
+
+ inversion H.
+ inversion H0.
+ apply IHx in H3; auto.
+ rewrite_for y.
+ reflexivity.
+Qed.
+
+Ltac same_as_uint8 :=
+  unfold Prefix;
+  intros c obj2 y xs ys S1 S2 V1 V2 Happ;
+  destruct_serialize obj2 y;
+  rewrite_for y;
+  apply prefix_same in Happ; simpl;  auto with ascii.
+
+Lemma prefix_uint8 : forall c,
+  Prefix (Uint8 c) ("204"::list_of_ascii8 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_uint16: forall c,
+  Prefix (Uint16 c) ("205"::list_of_ascii16 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_uint32: forall c,
+  Prefix (Uint32 c) ("206"::list_of_ascii32 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_uint64 : forall c,
+  Prefix (Uint64 c) ("207"::list_of_ascii64 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_int8 : forall c,
+  Prefix (Int8 c) ("208"::list_of_ascii8 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_int16 : forall c,
+  Prefix (Int16 c) ("209"::list_of_ascii16 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_int32 : forall c,
+  Prefix (Int32 c) ("210"::list_of_ascii32 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_int64 : forall c,
+  Prefix (Int64 c) ("211"::list_of_ascii64 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_float : forall c,
+  Prefix (Float c) ("202"::list_of_ascii32 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma prefix_double : forall c,
+  Prefix (Double c) ("203"::list_of_ascii64 c).
+Proof.
+same_as_uint8.
+Qed.
+
+Lemma app_length_eq : forall A (xs ys zs ws : list A),
+  xs ++zs = ys ++ ws ->
+  length xs = length ys ->
+  xs = ys.
+Proof.
+induction xs; induction ys; simpl; intros; auto.
+ inversion H0.
+
+ inversion H0.
+
+ inversion H.
+ inversion H0.
+ assert (xs = ys); [| rewrite_for xs; auto].
+ apply (IHxs _ zs ws); auto.
+Qed.
+
+Lemma prefix_fixraw : forall cs b1 b2 b3 b4 b5,
+  Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
+  Prefix (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y.
+rewrite_for obj2.
+rewrite_for y.
+inversion H2.
+inversion H3.
+assert (cs = cs0); [| rewrite_for cs; auto ].
+apply (app_length_eq _ _ _ xs ys); auto.
+rewrite <- (nat_ascii8_embedding (length cs)),
+        <- (nat_ascii8_embedding (length cs0)).
+ rewrite <- H, <- H8.
+ reflexivity.
+
+ transitivity (pow 5); auto with pow.
+
+ transitivity (pow 5); auto with pow.
+Qed.
+
+Lemma prefix_raw16 : forall cs s1 s2,
+  (s1,s2) =  ascii16_of_nat (length cs) ->
+  Prefix (Raw16 cs) ("218"::s1::s2::cs).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y.
+rewrite_for obj2.
+rewrite_for y.
+inversion H2.
+inversion H3.
+inversion H7.
+assert (cs = cs0); [| rewrite_for cs; auto ].
+apply (app_length_eq _ _ _ xs ys); auto.
+rewrite <- (nat_ascii16_embedding (length cs)),
+        <- (nat_ascii16_embedding (length cs0)); auto.
+rewrite <- H, <- H8, H12, H13.
+reflexivity.
+Qed.
+
+Lemma prefix_raw32 : forall cs s1 s2 s3 s4,
+  ((s1,s2),(s3,s4)) =  ascii32_of_nat (length cs) ->
+  Prefix (Raw32 cs) ("219"::s1::s2::s3::s4::cs).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y.
+rewrite_for obj2.
+rewrite_for y.
+inversion H2.
+inversion H3.
+inversion H7.
+assert (cs = cs0); [| rewrite_for cs; auto ].
+apply (app_length_eq _ _ _ xs ys); auto.
+rewrite <- (nat_ascii32_embedding (length cs)),
+        <- (nat_ascii32_embedding (length cs0)); auto.
+rewrite <- H, <- H8, H12, H13, H14, H15.
+reflexivity.
+Qed.
+
+Lemma prefix_fixarray_nil:
+  Prefix (FixArray []) ["144"].
+Proof.
+straight_forward.
+apply ascii8_not_O in H7; [ contradiction |].
+rewrite_for obj2.
+inversion V2.
+split; [ simpl; omega |].
+transitivity (pow 4); [ exact H13 | apply pow_lt; auto ].
+Qed.
+
+Lemma  prefix_array16_nil:
+  Prefix (Array16 []) ["220"; "000"; "000"].
+Proof.
+unfold Prefix; intros.
+destruct_serialize obj2 y.
+rewrite_for obj2.
+rewrite_for y.
+inversion H3.
+rewrite <- H9, <- H11 in *.
+assert (("000", "000") <> ascii16_of_nat ((length (x::xs0)))); try contradiction.
+inversion H2.
+apply ascii16_not_O.
+split; auto.
+simpl.
+omega.
+Qed.
+
+Lemma  prefix_array32_nil:
+  Prefix (Array32 []) ["221"; "000"; "000";"000"; "000"].
+Proof.
+unfold Prefix; intros.
+destruct_serialize obj2 y.
+rewrite_for obj2.
+rewrite_for y.
+inversion H3.
+rewrite <- H9, <- H11, <- H12, <- H13 in *.
+assert (("000", "000",("000","000")) <> ascii32_of_nat ((length (x::xs0)))); try contradiction.
+inversion H2.
+apply ascii32_not_O.
+split; auto.
+simpl.
+omega.
+Qed.
+
+Lemma prefix_fixmap_nil:
+  Prefix (FixMap []) ["128"].
+Proof.
+unfold Prefix; intros.
+destruct_serialize obj2 y.
+rewrite_for obj2.
+apply ascii8_not_O in H12; [ contradiction |].
+inversion H2.
+split; [ simpl; omega |].
+transitivity (pow 4); [ exact H21 |].
+apply pow_lt.
+auto.
+Qed.
+
+Lemma prefix_map16_nil:
+  Prefix (Map16 []) ["222"; "000"; "000"].
+Proof.
+unfold Prefix; intros.
+destruct_serialize obj2 y.
+rewrite_for obj2.
+rewrite_for y.
+inversion H3.
+rewrite <- H10, <- H12 in *.
+assert (("000", "000") <> ascii16_of_nat ((length ((x1, x2)::xs0)))); try contradiction.
+inversion H2.
+apply ascii16_not_O.
+split.
+ simpl.
+ omega.
+
+ exact H19.
+Qed.
+
+Lemma prefix_map32_nil:
+  Prefix (Map32 []) ["223"; "000"; "000";"000"; "000"].
+Proof.
+unfold Prefix; intros.
+destruct_serialize obj2 y.
+rewrite_for obj2.
+rewrite_for y.
+inversion H3.
+rewrite <- H10, <- H12, <- H13, <- H14 in *.
+assert (("000", "000",("000","000")) <> ascii32_of_nat ((length ((x1, x2)::xs0)))); try contradiction.
+inversion H2.
+apply ascii32_not_O.
+split.
+ simpl.
+ omega.
+
+ exact H21.
+Qed.
+
+Lemma prefix_fixarray_cons: forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  Prefix x y ->
+  Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Prefix (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Prefix (FixArray (x :: xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y0; rewrite_for y0; rewrite_for obj2.
+ inversion H6.
+ rewrite_for b5.
+ rewrite_for b6.
+ rewrite_for b7.
+ rewrite_for b8.
+ apply ascii8_not_O in H0; [contradiction |].
+ split; [ simpl; omega |].
+ inversion H7.
+ transitivity (pow 4); [ exact H19 | apply pow_lt; auto].
+
+ assert (y ++ ys = y1 ++ ys1); [| rewrite_for (y++ys); reflexivity ].
+ generalize H12; intro Happ; clear H12.
+ rewrite <- (app_assoc y ys xs0), <- (app_assoc y1 ys1 ys0) in Happ.
+ inversion H7.
+ inversion H8.
+ apply (H2 x0 y1 (ys++xs0) (ys1++ys0))in H1; auto.
+ rewrite_for y1.
+ apply app_same in Happ.
+ apply (H4 (FixArray xs1) (Ascii b0 b9 b10 b11 true false false true :: ys1) xs0 ys0) in H3; auto.
+  inversion H3.
+  reflexivity.
+
+  simpl.
+  unfold ascii8 in *.
+  rewrite <- Happ.
+  rewrite H0 in H18.
+  apply ascii8_of_nat_eq in H18; [
+    | transitivity (pow 4); [| apply pow_lt]; auto
+    | transitivity (pow 4); [| apply pow_lt]; auto ].
+  simpl in H18.
+  inversion H18.
+  rewrite <- H28 in H16.
+  rewrite <- H16 in H.
+  inversion H.
+  reflexivity.
+Qed.
+
+Lemma prefix_array16_cons: forall x xs y ys s1 s2 t1 t2,
+  (t1, t2) = ascii16_of_nat (length xs) ->
+  (s1, s2) = ascii16_of_nat (length (x :: xs)) ->
+  Serialized x y ->
+  Prefix x y ->
+  Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
+  Prefix (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
+  Prefix (Array16 (x::xs)) ("220"::s1::s2::y ++ ys).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y0.
+ rewrite_for y0.
+ inversion H9.
+ rewrite_for s1.
+ rewrite_for s2.
+ apply ascii16_not_O in H0; [ contradiction |].
+ inversion H7.
+ split; [ simpl; omega | exact H17 ].
+
+ rewrite_for y0.
+ rewrite_for obj2.
+ inversion H9.
+ rewrite_for s0.
+ rewrite_for s3.
+ assert( y++ ys = y1 ++ ys1); [| rewrite_for (y++ys); reflexivity ].
+ rewrite <- (app_assoc y ys xs0), <- (app_assoc y1 ys1 ys0) in H18.
+ inversion H7.
+ inversion H8.
+ apply (H2 x0 y1 (ys++xs0) (ys1++ys0))in H1; auto.
+ rewrite_for y1.
+ apply app_same in H18.
+ apply (H4 (Array16 xs1)  ("220" :: t0 :: t3 :: ys1) xs0 ys0) in H3; auto.
+  inversion H3.
+  reflexivity.
+
+  simpl.
+  unfold ascii8 in *.
+  rewrite <- H18.
+  rewrite H0 in H13.
+  apply ascii16_of_nat_eq in H13; auto.
+  simpl in H13.
+  inversion H13.
+  rewrite <- H26 in H11.
+  rewrite <- H11 in H.
+  inversion H.
+  reflexivity.
+Qed.
+
+Lemma prefix_array32_cons: forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
+  (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
+  (s1, s2, (s3, s4)) = ascii32_of_nat (length (x :: xs)) ->
+  Serialized x y ->
+  Prefix x y ->
+  Serialized (Array32 xs) ("221" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Prefix (Array32 xs) ("221" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Prefix (Array32 (x :: xs)) ("221" :: s1 :: s2 :: s3 :: s4 :: y ++ ys).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y0;
+ rewrite_for y0; rewrite_for obj2; inversion H9.
+ rewrite_for s1.
+ rewrite_for s2.
+ rewrite_for s3.
+ rewrite_for s4.
+ apply ascii32_not_O in H0; [ contradiction |].
+ inversion H7.
+ split; [ simpl; omega | exact H15 ].
+
+ rewrite_for s0.
+ rewrite_for s5.
+ rewrite_for s6.
+ rewrite_for s7.
+ assert( y++ ys = y1 ++ ys1); [| rewrite_for (y++ys); reflexivity ].
+ rewrite <- (app_assoc y ys xs0), <- (app_assoc y1 ys1 ys0) in H20.
+ inversion H7.
+ inversion H8.
+ apply (H2 x0 y1 (ys++xs0) (ys1++ys0)) in H1; auto.
+ rewrite_for y1.
+ apply app_same in H20.
+ apply (H4 (Array32 xs1)  ("221" :: t0 :: t5 :: t6 :: t7 :: ys1) xs0 ys0) in H3; auto.
+  inversion H3.
+  reflexivity.
+
+  simpl.
+  unfold ascii8 in *.
+  rewrite <- H20.
+  rewrite H0 in H13.
+  apply ascii32_of_nat_eq in H13; auto.
+  simpl in H13.
+  inversion H13.
+  rewrite <- H26 in H11.
+  rewrite <- H11 in H.
+  inversion H.
+  reflexivity.
+Qed.
+
+Lemma prefix_fixmap_cons: forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
+  Serialized x1 y1 -> Prefix x1 y1 ->
+  Serialized x2 y2 -> Prefix x2 y2 ->
+  Serialized (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
+  Prefix (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
+  Prefix (FixMap ((x1, x2) :: xs)) (Ascii b5 b6 b7 b8 false false false true :: y1 ++ y2 ++ ys).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y; rewrite_for y; rewrite_for obj2.
+ rewrite_for b5.
+ rewrite_for b6.
+ rewrite_for b7.
+ rewrite_for b8.
+ apply ascii8_not_O in H0; [ contradiction |].
+ split; [ simpl; omega |].
+ inversion H9.
+ transitivity (pow 4); auto.
+ apply pow_lt.
+ auto.
+
+assert (y1 ++ y2 ++ ys = y0 ++ y3 ++ ys1); [| rewrite_for (y1 ++ y2 ++ ys); reflexivity ].
+generalize H14; intro Happ; clear H14.
+replace ((y1 ++ y2 ++ ys) ++ xs0) with (y1 ++ y2 ++ ys ++ xs0) in Happ;
+  [| repeat (rewrite app_assoc); reflexivity ].
+replace ((y0 ++ y3 ++ ys1) ++ ys0) with (y0 ++ y3 ++ ys1 ++ ys0) in Happ;
+  [| repeat (rewrite app_assoc); reflexivity ].
+inversion H9.
+inversion H10.
+apply (H2 x0 y0 (y2 ++ ys ++ xs0) (y3 ++ ys1 ++ ys0))in H1; auto.
+rewrite_for y1.
+apply app_same in Happ.
+apply (H4 x3 y3 (ys ++ xs0) (ys1 ++ ys0)) in H3; auto.
+rewrite_for y3.
+apply app_same in Happ.
+apply (H6 (FixMap xs1) (Ascii b0 b9 b10 b11 false false false true :: ys1) xs0 ys0) in H5; auto.
+ inversion H5.
+ reflexivity.
+
+ simpl.
+ unfold ascii8 in *.
+ rewrite <- Happ.
+ rewrite H0 in H20.
+  apply ascii8_of_nat_eq in H20; [
+    | transitivity (pow 4); [| apply pow_lt]; auto
+    | transitivity (pow 4); [| apply pow_lt]; auto ].
+ simpl in H20.
+ inversion H20.
+ rewrite H3 in H.
+ rewrite <- H19 in H.
+ inversion H.
+ reflexivity.
+Qed.
+
+Lemma prefix_map16_cons: forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
+  (t1, t2) = ascii16_of_nat (length xs) ->
+  (s1, s2) = ascii16_of_nat (length ((x1, x2) :: xs)) ->
+  Serialized x1 y1 ->
+  Prefix x1 y1 ->
+  Serialized x2 y2 ->
+  Prefix x2 y2 ->
+  Serialized (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
+  Prefix (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
+  Prefix (Map16 ((x1, x2) :: xs)) ("222" :: s1 :: s2 :: y1 ++ y2 ++ ys).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y; rewrite_for y; rewrite_for obj2.
+ inversion H11.
+ rewrite_for s1.
+ rewrite_for s2.
+ apply ascii16_not_O in H0; [ contradiction |].
+ inversion H9.
+ split; [ simpl; omega | exact H20 ].
+
+ inversion H14.
+ rewrite_for s1.
+ rewrite_for s2.
+ assert( y1 ++ y2 ++ ys = y0 ++ y3  ++ ys1); [| rewrite_for (y1 ++ y2 ++ ys); reflexivity ].
+ replace ((y1 ++ y2 ++ ys) ++ xs0) with (y1 ++ y2 ++ ys ++ xs0) in H21;
+   [| repeat (rewrite app_assoc); reflexivity ].
+ replace ((y0 ++ y3 ++ ys1) ++ ys0) with (y0 ++ y3 ++ ys1 ++ ys0) in H21;
+   [| repeat (rewrite app_assoc); reflexivity ].
+ inversion H9.
+ inversion H10.
+ apply (H2 x0 y0 (y2 ++ ys ++ xs0) (y3 ++ ys1 ++ ys0))in H1; auto.
+ rewrite_for y1.
+ apply app_same in H21.
+ apply (H4 x3 y3 (ys ++ xs0) (ys1 ++ ys0)) in H3; auto.
+ rewrite_for y3.
+ apply app_same in H21.
+ apply (H6 (Map16 xs1) ("222" :: t0 :: t3 :: ys1) xs0 ys0) in H5; auto.
+  inversion H5.
+  reflexivity.
+
+  simpl.
+  unfold ascii8 in *.
+  rewrite <- H21.
+  rewrite H0 in H15.
+  apply ascii16_of_nat_eq in H15; auto.
+  simpl in H15.
+  inversion H15.
+  rewrite H3 in H.
+  rewrite <- H13 in H.
+  inversion H.
+  reflexivity.
+Qed.
+
+Lemma prefix_map32_cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
+  (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
+  (s1, s2, (s3, s4)) = ascii32_of_nat (length ((x1, x2) :: xs)) ->
+  Serialized x1 y1 ->
+  Prefix x1 y1 ->
+  Serialized x2 y2 ->
+  Prefix x2 y2 ->
+  Serialized (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Prefix (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Prefix (Map32 ((x1, x2) :: xs)) ("223" :: s1 :: s2 :: s3 :: s4 :: y1 ++ y2 ++ ys).
+Proof.
+unfold Prefix.
+intros.
+destruct_serialize obj2 y; rewrite_for y; rewrite_for obj2.
+ inversion H11.
+ rewrite_for s1.
+ rewrite_for s2.
+ rewrite_for s3.
+ rewrite_for s4.
+ apply ascii32_not_O in H0; [ contradiction |].
+ inversion H9.
+ split; [ simpl; omega | exact H20 ].
+
+ inversion H14.
+ rewrite_for s1.
+ rewrite_for s2.
+ rewrite_for s3.
+ rewrite_for s4.
+ generalize H23; intro Happ; clear H23.
+ assert( y1 ++ y2 ++ ys = y0 ++ y3  ++ ys1); [| rewrite_for (y1 ++ y2 ++ ys); reflexivity ].
+ replace ((y1 ++ y2 ++ ys) ++ xs0) with (y1 ++ y2 ++ ys ++ xs0) in Happ;
+   [| repeat (rewrite app_assoc); reflexivity ].
+ replace ((y0 ++ y3 ++ ys1) ++ ys0) with (y0 ++ y3 ++ ys1 ++ ys0) in Happ;
+   [| repeat (rewrite app_assoc); reflexivity ].
+ inversion H9.
+ inversion H10.
+ apply (H2 x0 y0 (y2 ++ ys ++ xs0) (y3 ++ ys1 ++ ys0)) in H1; auto.
+ rewrite_for y1.
+ apply app_same in Happ.
+ apply (H4 x3 y3 (ys ++ xs0) (ys1 ++ ys0)) in H3; auto.
+ rewrite_for y3.
+ apply app_same in Happ.
+ apply (H6 (Map32 xs1) ("223" :: t0 :: t5 :: t6 :: t7 :: ys1) xs0 ys0) in H5; auto.
+  inversion H5.
+  reflexivity.
+
+  simpl.
+  unfold ascii8 in *.
+  rewrite <- Happ.
+  rewrite H0 in H15.
+  apply ascii32_of_nat_eq in H15; auto.
+  simpl in H15.
+  inversion H15.
+  rewrite H3 in H.
+  rewrite <- H13 in H.
+  inversion H.
+  reflexivity.
+Qed.
+
+Hint Resolve
+  prefix_true prefix_false
+  prefix_nil prefix_pfixnum prefix_nfixnum
+  prefix_uint8 prefix_uint16 prefix_uint32 prefix_uint64
+  prefix_int8  prefix_int16  prefix_int32  prefix_int64
+  prefix_float prefix_double
+  prefix_raw16 prefix_raw32
+  prefix_fixarray_nil prefix_array16_nil prefix_array32_nil
+  prefix_fixmap_nil prefix_map16_nil prefix_map32_nil
+  : prefix.
+
+Lemma prefix_intro: forall obj x,
+  (Serialized obj x -> Prefix obj x)->
+  Prefix obj x.
+Proof.
+unfold Prefix.
+intros.
+apply H with (xs:=xs) (ys:=ys) in H1; auto.
+Qed.
+
+Lemma prefix : forall obj1 x,
+  Prefix obj1 x.
+Proof.
+intros.
+apply prefix_intro.
+intro.
+pattern obj1,x.
+apply Serialized_ind; intros; auto with prefix.
+ apply prefix_fixraw; auto.
+ apply prefix_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply prefix_array16_cons with (t1:=t1) (t2:=t2); auto.
+ apply prefix_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+ apply prefix_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply prefix_map16_cons with (t1:=t1) (t2:=t2); auto.
+ apply prefix_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+Qed.
diff --git a/ocaml/proof/ProofUtil.v b/ocaml/proof/ProofUtil.v
new file mode 100644
index 00000000..191544e6
--- /dev/null
+++ b/ocaml/proof/ProofUtil.v
@@ -0,0 +1,5 @@
+Ltac rewrite_for x :=
+  match goal with
+    | [ H : x = _ |- _ ] => rewrite H in *; clear H
+    | [ H : _ = x |- _ ] => rewrite <- H in *; clear H
+  end.
\ No newline at end of file
diff --git a/ocaml/proof/SerializeImplement.v b/ocaml/proof/SerializeImplement.v
new file mode 100644
index 00000000..0bfd6ddf
--- /dev/null
+++ b/ocaml/proof/SerializeImplement.v
@@ -0,0 +1,465 @@
+Require Import Ascii List.
+Require Import ListUtil Object MultiByte Util SerializeSpec ProofUtil.
+
+Open Scope char_scope.
+
+Fixpoint serialize (obj : object) : list ascii8 :=
+  match obj with
+    | Nil        => [ "192" ]
+    | Bool false => [ "194" ]
+    | Bool true  => [ "195" ]
+    | PFixnum (Ascii b1 b2 b3 b4 b5 b6 b7 _) =>
+      [ Ascii b1 b2 b3 b4 b5 b6 b7 false ]
+    | NFixnum (Ascii b1 b2 b3 b4 b5 _ _ _) =>
+      [ Ascii b1 b2 b3 b4 b5 true true true ]
+    | Uint8  c => "204"::list_of_ascii8 c
+    | Uint16 c => "205"::list_of_ascii16 c
+    | Uint32 c => "206"::list_of_ascii32 c
+    | Uint64 c => "207"::list_of_ascii64 c
+    | Int8   c => "208"::list_of_ascii8 c
+    | Int16  c => "209"::list_of_ascii16 c
+    | Int32  c => "210"::list_of_ascii32 c
+    | Int64  c => "211"::list_of_ascii64 c
+    | Float  c => "202"::list_of_ascii32 c
+    | Double c => "203"::list_of_ascii64 c
+    | FixRaw xs =>
+      match ascii8_of_nat @@ length xs with
+        | Ascii b1 b2 b3 b4 b5 _ _ _ =>
+          (Ascii b1 b2 b3 b4 b5 true false true)::xs
+      end
+    | Raw16 xs =>
+      let (s1,s2) :=
+        ascii16_of_nat @@ length xs
+      in
+        "218"::s1::s2::xs
+    | Raw32 xs =>
+      match ascii32_of_nat @@ length xs with
+        | ((s1,s2),(s3,s4)) =>
+          "219"::s1::s2::s3::s4::xs
+      end
+    | FixArray xs =>
+      let ys :=
+        flat_map serialize xs
+      in
+      match ascii8_of_nat @@ length xs with
+        | Ascii b1 b2 b3 b4 _ _ _ _ =>
+          (Ascii b1 b2 b3 b4 true false false true)::ys
+      end
+    | Array16 xs =>
+      let ys :=
+        flat_map serialize xs
+      in
+      let (s1, s2) :=
+        ascii16_of_nat (length  xs)
+      in
+        "220"::s1::s2::ys
+    | Array32 xs =>
+      let ys :=
+        flat_map serialize xs
+      in
+      match ascii32_of_nat @@ length xs with
+        | ((s1,s2),(s3,s4)) =>
+         "221"::s1::s2::s3::s4::ys
+      end
+    | FixMap xs =>
+      let ys :=
+        flat_map (fun p => serialize (fst p) ++ serialize (snd p)) xs
+      in
+      match ascii8_of_nat @@ length xs with
+        | Ascii b1 b2 b3 b4 _ _ _ _ =>
+          (Ascii b1 b2 b3 b4 false false false true)::ys
+      end
+    | Map16 xs =>
+      let ys :=
+        flat_map (fun p => serialize (fst p) ++ serialize (snd p)) xs
+      in
+      let (s1, s2) :=
+        ascii16_of_nat (length  xs)
+      in
+        "222"::s1::s2::ys
+    | Map32 xs =>
+      let ys :=
+        flat_map (fun p => serialize (fst p) ++ serialize (snd p)) xs
+      in
+      match ascii32_of_nat @@ length xs with
+        | ((s1,s2),(s3,s4)) =>
+         "223"::s1::s2::s3::s4::ys
+      end
+  end.
+
+Definition Correct obj xs :=
+  Serialized obj xs ->
+  serialize obj = xs.
+
+Ltac straitfoward :=
+  unfold Correct;
+  intros;
+  simpl;
+  reflexivity.
+
+Lemma correct_nil:
+  Correct Nil ["192"].
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_false:
+  Correct (Bool false) ["194"].
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_true:
+  Correct (Bool true) ["195"].
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_pfixnum: forall x1 x2 x3 x4 x5 x6 x7,
+  Correct (PFixnum   (Ascii x1 x2 x3 x4 x5 x6 x7 false))
+          [Ascii x1 x2 x3 x4 x5 x6 x7 false].
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_nfixnum: forall x1 x2 x3 x4 x5,
+  Correct (NFixnum   (Ascii x1 x2 x3 x4 x5 true true true))
+          [Ascii x1 x2 x3 x4 x5 true true true].
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_uint8 : forall c,
+  Correct (Uint8 c) ("204"::list_of_ascii8 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_uint16 : forall c,
+  Correct (Uint16 c) ("205"::list_of_ascii16 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_uint32 : forall c,
+  Correct (Uint32 c) ("206"::list_of_ascii32 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_uint64 : forall c,
+  Correct (Uint64 c) ("207"::list_of_ascii64 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_int8 : forall c,
+  Correct (Int8 c) ("208"::list_of_ascii8 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_int16 : forall c,
+  Correct (Int16 c) ("209"::list_of_ascii16 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_int32 : forall c,
+  Correct (Int32 c) ("210"::list_of_ascii32 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_int64 : forall c,
+  Correct (Int64 c) ("211"::list_of_ascii64 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_float : forall c,
+  Correct (Float c) ("202"::list_of_ascii32 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_double : forall c,
+  Correct (Double c) ("203"::list_of_ascii64 c).
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_fixraw : forall cs b1 b2 b3 b4 b5,
+  Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
+  Correct (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs).
+Proof.
+unfold Correct.
+intros.
+inversion H0.
+simpl.
+unfold atat.
+rewrite_for (ascii8_of_nat (length cs)).
+reflexivity.
+Qed.
+
+Lemma correct_raw16: forall cs s1 s2,
+  (s1,s2) =  ascii16_of_nat (length cs) ->
+  Correct (Raw16 cs) ("218"::s1::s2::cs).
+Proof.
+unfold Correct.
+intros.
+inversion H0.
+simpl.
+unfold atat.
+rewrite_for (ascii16_of_nat (length cs)).
+reflexivity.
+Qed.
+
+Lemma correct_raw32 : forall cs s1 s2 s3 s4,
+  ((s1,s2),(s3,s4)) =  ascii32_of_nat (length cs) ->
+  Correct (Raw32 cs) ("219"::s1::s2::s3::s4::cs).
+Proof.
+unfold Correct.
+intros.
+inversion H0.
+simpl.
+unfold atat.
+rewrite_for (ascii32_of_nat (length cs)).
+reflexivity.
+Qed.
+
+Lemma correct_fixarray_nil :
+  Correct (FixArray []) ["144"].
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_array16_nil :
+  Correct (Array16 []) ["220"; "000"; "000"].
+Proof.
+unfold Correct.
+intros.
+simpl.
+rewrite <- ascii16_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma correct_array32_nil:
+  Correct (Array32 []) ["221"; "000"; "000";"000"; "000"].
+Proof.
+unfold Correct.
+intros.
+simpl.
+unfold atat.
+rewrite <- ascii32_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma correct_fixmap_nil:
+  Correct (FixMap []) ["128"].
+Proof.
+straitfoward.
+Qed.
+
+Lemma correct_map16_nil:
+  Correct (Map16 []) ["222"; "000"; "000"].
+Proof.
+unfold Correct.
+intros.
+simpl.
+rewrite <- ascii16_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma correct_map32_nil:
+  Correct (Map32 []) ["223"; "000"; "000";"000"; "000"].
+Proof.
+unfold Correct.
+intros.
+simpl.
+unfold atat.
+rewrite <- ascii32_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma correct_fixarray_cons: forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  Correct x y ->
+  Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Correct (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Correct (FixArray (x :: xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys).
+Proof.
+unfold Correct.
+intros.
+simpl in *.
+unfold atat in *.
+rewrite_for (ascii8_of_nat (S (length xs))).
+apply H2 in H1.
+apply H4 in H3.
+rewrite_for (ascii8_of_nat (length xs)).
+rewrite_for y.
+inversion H3.
+reflexivity.
+Qed.
+
+Lemma correct_array16_cons: forall x xs t1 t2 s1 s2 y ys,
+  (t1, t2) = ascii16_of_nat (length xs) ->
+  (s1, s2) = ascii16_of_nat (length (x :: xs)) ->
+  Serialized x y ->
+  (Serialized x y -> Correct x y) ->
+  Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
+  (Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
+    Correct (Array16 xs) ("220" :: t1 :: t2 :: ys)) ->
+  Correct (Array16 (x :: xs)) ("220" :: s1 :: s2 :: y ++ ys).
+Proof.
+unfold Correct.
+intros.
+simpl in *.
+rewrite_for (ascii16_of_nat (S (length xs))).
+apply H2 in H1; auto.
+apply H4 in H3; auto.
+rewrite_for (ascii16_of_nat (length xs)).
+rewrite_for y.
+inversion H3.
+reflexivity.
+Qed.
+
+Lemma correct_array32_cons: forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
+  ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
+  ((s1,s2),(s3,s4)) = ascii32_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  (Serialized x y -> Correct x y) ->
+  Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
+  (Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) -> Correct (Array32 xs) ("221"::t1::t2::t3::t4::ys)) ->
+  Correct (Array32 (x::xs)) ("221"::s1::s2::s3::s4::y ++ ys).
+Proof.
+unfold Correct.
+intros.
+simpl in *.
+unfold atat in *.
+rewrite_for (ascii32_of_nat (S (length xs))).
+apply H2 in H1; auto.
+apply H4 in H3; auto.
+rewrite_for (ascii32_of_nat (length xs)).
+rewrite_for y.
+inversion H3.
+reflexivity.
+Qed.
+
+Lemma correct_fixmap_cons: forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
+  Serialized x1 y1 -> Correct x1 y1 ->
+  Serialized x2 y2 -> Correct x2 y2 ->
+  Serialized (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
+  Correct (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
+  Correct (FixMap ((x1, x2) :: xs)) (Ascii b5 b6 b7 b8 false false false true :: y1 ++ y2 ++ ys).
+Proof.
+unfold Correct.
+intros.
+simpl in *.
+unfold atat in *.
+rewrite_for (ascii8_of_nat (S (length xs))).
+apply H2 in H1.
+apply H4 in H3.
+apply H6 in H5.
+rewrite_for (ascii8_of_nat (length xs)).
+rewrite_for y1.
+rewrite_for y2.
+inversion H5.
+rewrite <- app_assoc.
+reflexivity.
+Qed.
+
+Lemma correct_map16_cons: forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
+  (t1, t2) = ascii16_of_nat (length xs) ->
+  (s1, s2) = ascii16_of_nat (length ((x1, x2) :: xs)) ->
+  Serialized x1 y1 ->
+  Correct x1 y1 ->
+  Serialized x2 y2 ->
+  Correct x2 y2 ->
+  Serialized (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
+  Correct (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
+  Correct (Map16 ((x1, x2) :: xs)) ("222" :: s1 :: s2 :: y1 ++ y2 ++ ys).
+Proof.
+unfold Correct.
+intros.
+simpl in *.
+rewrite_for (ascii16_of_nat (S (length xs))).
+apply H2 in H1.
+apply H4 in H3.
+apply H6 in H5.
+rewrite_for (ascii16_of_nat (length xs)).
+rewrite_for y1.
+rewrite_for y2.
+inversion H5.
+rewrite <- app_assoc.
+reflexivity.
+Qed.
+
+Lemma correct_map32_cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
+  (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
+  (s1, s2, (s3, s4)) = ascii32_of_nat (length ((x1, x2) :: xs)) ->
+  Serialized x1 y1 ->
+  Correct x1 y1 ->
+  Serialized x2 y2 ->
+  Correct x2 y2 ->
+  Serialized (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Correct (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Correct (Map32 ((x1, x2) :: xs)) ("223" :: s1 :: s2 :: s3 :: s4 :: y1 ++ y2 ++ ys).
+Proof.
+unfold Correct.
+intros.
+simpl in *.
+unfold atat in *.
+rewrite_for (ascii32_of_nat (S (length xs))).
+apply H2 in H1.
+apply H4 in H3.
+apply H6 in H5.
+rewrite_for (ascii32_of_nat (length xs)).
+rewrite_for y1.
+rewrite_for y2.
+inversion H5.
+rewrite <- app_assoc.
+reflexivity.
+Qed.
+
+Lemma correct_intro : forall obj xs,
+  (Serialized obj xs -> Correct obj xs) ->
+  Correct obj xs.
+Proof.
+unfold Correct.
+intros.
+apply H in H0; auto.
+Qed.
+
+Hint Resolve
+  correct_true correct_false
+  correct_nil correct_pfixnum correct_nfixnum
+  correct_uint8 correct_uint16 correct_uint32 correct_uint64
+  correct_int8  correct_int16  correct_int32  correct_int64
+  correct_float correct_double
+  correct_raw16 correct_raw32
+  correct_fixarray_nil correct_array16_nil correct_array32_nil
+  correct_fixmap_nil correct_map16_nil correct_map32_nil
+  : correct.
+
+
+Theorem serialize_correct : forall obj xs,
+  Correct obj xs.
+Proof.
+intros.
+apply correct_intro.
+intro.
+pattern obj,xs.
+apply Serialized_ind; intros; auto with correct.
+ apply correct_fixraw; auto.
+ apply correct_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply correct_array16_cons with (t1:=t1) (t2:=t2); auto.
+ apply correct_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+ apply correct_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply correct_map16_cons with (t1:=t1) (t2:=t2); auto.
+ apply correct_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+Qed.
diff --git a/ocaml/proof/SerializeSpec.v b/ocaml/proof/SerializeSpec.v
new file mode 100644
index 00000000..a071c62a
--- /dev/null
+++ b/ocaml/proof/SerializeSpec.v
@@ -0,0 +1,99 @@
+Require Import List Ascii.
+Require Import MultiByte Object ListUtil.
+
+Open Scope list_scope.
+Open Scope char_scope.
+
+Inductive Serialized : object -> list ascii8 -> Prop :=
+| SNil :
+  Serialized Nil ["192"]
+| STrue :
+  Serialized (Bool true)  ["195"]
+| SFalse :
+  Serialized (Bool false) ["194"]
+| SPFixnum : forall x1 x2 x3 x4 x5 x6 x7,
+  Serialized (PFixnum   (Ascii x1 x2 x3 x4 x5 x6 x7 false))
+             [Ascii x1 x2 x3 x4 x5 x6 x7 false]
+| SNFixnum : forall  x1 x2 x3 x4 x5,
+  Serialized (NFixnum   (Ascii x1 x2 x3 x4 x5 true true true))
+             [Ascii x1 x2 x3 x4 x5 true true true]
+| SUint8 : forall c,
+  Serialized (Uint8 c) ("204"::list_of_ascii8 c)
+| SUint16 : forall c,
+  Serialized (Uint16 c) ("205"::list_of_ascii16 c)
+| SUint32 : forall c,
+  Serialized (Uint32 c) ("206"::list_of_ascii32 c)
+| SUint64 : forall c,
+  Serialized (Uint64 c) ("207"::list_of_ascii64 c)
+| SInt8 : forall c,
+  Serialized (Int8 c) ("208"::list_of_ascii8 c)
+| SInt16 : forall c,
+  Serialized (Int16 c) ("209"::list_of_ascii16 c)
+| SInt32 : forall c,
+  Serialized (Int32 c) ("210"::list_of_ascii32 c)
+| SInt64 : forall c,
+  Serialized (Int64 c) ("211"::list_of_ascii64 c)
+| SFloat : forall c,
+  Serialized (Float c) ("202"::list_of_ascii32 c)
+| SDouble : forall c,
+  Serialized (Double c) ("203"::list_of_ascii64 c)
+| SFixRaw : forall cs b1 b2 b3 b4 b5,
+  Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
+  Serialized (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs)
+| SRaw16 : forall cs s1 s2,
+  (s1,s2) =  ascii16_of_nat (length cs) ->
+  Serialized (Raw16 cs) ("218"::s1::s2::cs)
+| SRaw32 : forall cs s1 s2 s3 s4,
+  ((s1,s2),(s3,s4)) =  ascii32_of_nat (length cs) ->
+   Serialized (Raw32 cs) ("219"::s1::s2::s3::s4::cs)
+| SFixArrayNil :
+  Serialized (FixArray []) ["144"]
+| SFixArrayCons : forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Serialized (FixArray (x::xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys)
+| SArray16Nil :
+  Serialized (Array16 []) ["220"; "000"; "000"]
+| SArray16Cons : forall x xs y ys s1 s2 t1 t2,
+  (t1,t2) = ascii16_of_nat (length xs) ->
+  (s1,s2) = ascii16_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  Serialized (Array16 xs) ("220"::t1::t2::ys) ->
+  Serialized (Array16 (x::xs)) ("220"::s1::s2::y ++ ys)
+| SArray32Nil :
+  Serialized (Array32 []) ["221"; "000"; "000";"000"; "000"]
+| SArray32Cons : forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
+  ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
+  ((s1,s2),(s3,s4)) = ascii32_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
+  Serialized (Array32 (x::xs)) ("221"::s1::s2::s3::s4::y ++ ys)
+| SFixMapNil :
+  Serialized (FixMap []) ["128"]
+| SFixMapCons : forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
+  Serialized x1 y1 ->
+  Serialized x2 y2 ->
+  Serialized (FixMap xs) ((Ascii b1 b2 b3 b4 false false false true)::ys) ->
+  Serialized (FixMap ((x1,x2)::xs)) ((Ascii b5 b6 b7 b8 false false false true)::y1 ++ y2  ++ ys)
+| SMap16Nil :
+  Serialized (Map16 []) ["222"; "000"; "000"]
+| SMap16Cons : forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
+  (t1,t2) = ascii16_of_nat (length xs) ->
+  (s1,s2) = ascii16_of_nat (length ((x1,x2)::xs)) ->
+  Serialized x1 y1 ->
+  Serialized x2 y2 ->
+  Serialized (Map16 xs) ("222"::t1::t2::ys) ->
+  Serialized (Map16 ((x1,x2)::xs)) ("222"::s1::s2::y1 ++ y2 ++ ys)
+| SMap32Nil :
+  Serialized (Map32 []) ["223"; "000"; "000";"000"; "000"]
+| SMap32Cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
+  ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
+  ((s1,s2),(s3,s4)) = ascii32_of_nat (length ((x1,x2)::xs)) ->
+  Serialized x1 y1 ->
+  Serialized x2 y2 ->
+  Serialized (Map32 xs) ("223"::t1::t2::t3::t4::ys) ->
+  Serialized (Map32 ((x1,x2)::xs)) ("223"::s1::s2::s3::s4::y1 ++ y2 ++ ys).
diff --git a/ocaml/proof/SerializedList.v b/ocaml/proof/SerializedList.v
new file mode 100644
index 00000000..e2da9e5f
--- /dev/null
+++ b/ocaml/proof/SerializedList.v
@@ -0,0 +1,521 @@
+Require Import Ascii List.
+Require Import ListUtil Object MultiByte Util SerializeSpec Pow.
+
+Open Scope char_scope.
+
+Definition lift P (o : object) (b : list ascii) := forall os bs,
+  P os bs -> P (o::os) (b ++ bs).
+
+Inductive SerializedList : list object -> list ascii8 -> Prop :=
+| SLbot :
+  SerializedList [] []
+| SLNil:
+  lift SerializedList Nil ["192"]
+| SLTrue :
+  lift SerializedList (Bool true)  ["195"]
+| SLFalse :
+  lift SerializedList (Bool false) ["194"]
+| SLPFixnum : forall x1 x2 x3 x4 x5 x6 x7,
+  lift SerializedList (PFixnum   (Ascii x1 x2 x3 x4 x5 x6 x7 false))
+                      [Ascii x1 x2 x3 x4 x5 x6 x7 false]
+| SLNFixnum : forall  x1 x2 x3 x4 x5,
+  lift SerializedList (NFixnum   (Ascii x1 x2 x3 x4 x5 true true true))
+                      [Ascii x1 x2 x3 x4 x5 true true true]
+| SLUint8 : forall c,
+  lift SerializedList (Uint8 c) ("204" :: list_of_ascii8 c)
+| SLUint16 : forall c,
+  lift SerializedList (Uint16 c) ("205" :: list_of_ascii16 c)
+| SLUint32 : forall c,
+  lift SerializedList (Uint32 c) ("206" :: list_of_ascii32 c)
+| SLUint64 : forall c,
+  lift SerializedList (Uint64 c) ("207" :: list_of_ascii64 c)
+| SLInt8 : forall c,
+  lift SerializedList (Int8 c) ("208" :: list_of_ascii8 c)
+| SLInt16 : forall c,
+  lift SerializedList (Int16 c) ("209" :: list_of_ascii16 c)
+| SLInt32 : forall c,
+  lift SerializedList (Int32 c) ("210" :: list_of_ascii32 c)
+| SLInt64 : forall c,
+  lift SerializedList (Int64 c) ("211" :: list_of_ascii64 c)
+| SLFloat : forall c,
+  lift SerializedList (Float c) ("202" :: list_of_ascii32 c)
+| SLDouble : forall c,
+  lift SerializedList (Double c) ("203" :: list_of_ascii64 c)
+| SLFixRaw : forall cs b1 b2 b3 b4 b5,
+  Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
+  List.length cs < pow 5 ->
+  lift SerializedList (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true) :: cs)
+| SLRaw16 : forall cs s1 s2,
+  (s1,s2) =  ascii16_of_nat (length cs) ->
+  List.length cs < pow 16 ->
+  lift SerializedList (Raw16 cs) ("218" :: s1 :: s2 :: cs)
+| SLRaw32 : forall cs s1 s2 s3 s4,
+  ((s1,s2),(s3,s4)) =  ascii32_of_nat (length cs) ->
+  List.length cs < pow 32 ->
+   lift SerializedList (Raw32 cs) ("219" :: s1 :: s2 :: s3 :: s4 :: cs)
+| SLFixArray : forall os n b1 b2 b3 b4 xs ys bs,
+  SerializedList os bs ->
+  (xs,ys) = split_at n os ->
+  n < pow 4 ->
+  (Ascii b1 b2 b3 b4 false false false false) = ascii8_of_nat n ->
+  SerializedList ((FixArray xs) :: ys) ((Ascii b1 b2 b3 b4 true false false true) :: bs)
+| SLArray16 : forall os n xs ys bs s1 s2,
+  SerializedList os bs ->
+  (xs,ys) = split_at n os ->
+  n < pow 16 ->
+  (s1,s2) = ascii16_of_nat n ->
+  SerializedList ((Array16 xs)::ys) ("220" :: s1 :: s2 :: bs)
+| SLArray32 : forall os n xs ys bs s1 s2 s3 s4,
+  SerializedList os bs ->
+  (xs,ys) = split_at n os ->
+  n < pow 32 ->
+  ((s1,s2),(s3,s4)) = ascii32_of_nat n ->
+  SerializedList ((Array32 xs)::ys) ("221" :: s1 :: s2 :: s3 :: s4 :: bs)
+| SLFixMap : forall os n b1 b2 b3 b4 xs ys bs,
+  SerializedList os bs ->
+  (xs,ys) = split_at (2 * n) os ->
+  List.length xs = 2 * n ->
+  n < pow 4 ->
+  (Ascii b1 b2 b3 b4 false false false false) = ascii8_of_nat n ->
+  SerializedList ((FixMap (pair xs)) :: ys) ((Ascii b1 b2 b3 b4 false false false true) :: bs)
+| SLMap16 : forall os n xs ys bs s1 s2,
+  SerializedList os bs ->
+  (xs,ys) = split_at (2 * n) os ->
+  List.length xs = 2 * n ->
+  n < pow 16 ->
+  (s1,s2) = ascii16_of_nat n ->
+  SerializedList ((Map16 (pair xs))::ys) ("222" :: s1 :: s2 :: bs)
+| SLMap32 : forall os n xs ys bs s1 s2 s3 s4,
+  SerializedList os bs ->
+  (xs,ys) = split_at (2 * n) os ->
+  List.length xs = 2 * n ->
+  n < pow 32 ->
+  ((s1,s2),(s3,s4)) = ascii32_of_nat n ->
+  SerializedList ((Map32 (pair xs))::ys) ("223" :: s1 :: s2 :: s3 :: s4 :: bs).
+
+Lemma app_cons: forall A (xs ys zs : list A) x,
+  x :: (xs ++ ys) ++ zs = x :: (xs ++ ys ++ zs).
+Proof.
+induction xs; intros; simpl; auto.
+rewrite (IHxs ys zs a).
+reflexivity.
+Qed.
+
+Definition Soundness o bs := forall os bs',
+  Serialized o bs ->
+  Valid o ->
+  SerializedList os bs' ->
+  SerializedList (o :: os) (bs ++ bs').
+
+Ltac straitfoward P :=
+ intros;
+ unfold Soundness;
+ intros os bs' Hs Hv Hsl;
+ apply P;
+ auto.
+
+Lemma soundness_nil:
+  Soundness Nil ["192"].
+Proof.
+straitfoward SLNil.
+Qed.
+
+Lemma soundness_false:
+  Soundness (Bool false) ["194"].
+Proof.
+straitfoward SLFalse.
+Qed.
+
+Lemma soundness_true:
+  Soundness (Bool true) ["195"].
+Proof.
+straitfoward SLTrue.
+Qed.
+
+Lemma soundness_pfixnum: forall x1 x2 x3 x4 x5 x6 x7,
+  Soundness (PFixnum   (Ascii x1 x2 x3 x4 x5 x6 x7 false))
+          [Ascii x1 x2 x3 x4 x5 x6 x7 false].
+Proof.
+straitfoward SLPFixnum.
+Qed.
+
+Lemma soundness_nfixnum: forall x1 x2 x3 x4 x5,
+  Soundness (NFixnum   (Ascii x1 x2 x3 x4 x5 true true true))
+          [Ascii x1 x2 x3 x4 x5 true true true].
+Proof.
+straitfoward SLNFixnum.
+Qed.
+
+Lemma soundness_uint8 : forall c,
+  Soundness (Uint8 c) ("204"::list_of_ascii8 c).
+Proof.
+straitfoward SLUint8.
+Qed.
+
+Lemma soundness_uint16 : forall c,
+  Soundness (Uint16 c) ("205"::list_of_ascii16 c).
+Proof.
+straitfoward SLUint16.
+Qed.
+
+Lemma soundness_uint32 : forall c,
+  Soundness (Uint32 c) ("206"::list_of_ascii32 c).
+Proof.
+straitfoward SLUint32.
+Qed.
+
+Lemma soundness_uint64 : forall c,
+  Soundness (Uint64 c) ("207"::list_of_ascii64 c).
+Proof.
+straitfoward SLUint64.
+Qed.
+
+Lemma soundness_int8 : forall c,
+  Soundness (Int8 c) ("208"::list_of_ascii8 c).
+Proof.
+straitfoward SLInt8.
+Qed.
+
+Lemma soundness_int16 : forall c,
+  Soundness (Int16 c) ("209"::list_of_ascii16 c).
+Proof.
+straitfoward SLInt16.
+Qed.
+
+Lemma soundness_int32 : forall c,
+  Soundness (Int32 c) ("210"::list_of_ascii32 c).
+Proof.
+straitfoward SLInt32.
+Qed.
+
+Lemma soundness_int64 : forall c,
+  Soundness (Int64 c) ("211"::list_of_ascii64 c).
+Proof.
+straitfoward SLInt64.
+Qed.
+
+Lemma soundness_float : forall c,
+  Soundness (Float c) ("202"::list_of_ascii32 c).
+Proof.
+straitfoward SLFloat.
+Qed.
+
+Lemma soundness_double : forall c,
+  Soundness (Double c) ("203"::list_of_ascii64 c).
+Proof.
+straitfoward SLDouble.
+Qed.
+
+Lemma soundness_fixraw : forall cs b1 b2 b3 b4 b5,
+  Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
+  Soundness (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs).
+Proof.
+straitfoward SLFixRaw.
+inversion Hv.
+assumption.
+Qed.
+
+Lemma soundness_raw16: forall cs s1 s2,
+  (s1,s2) =  ascii16_of_nat (length cs) ->
+  Soundness (Raw16 cs) ("218"::s1::s2::cs).
+Proof.
+straitfoward SLRaw16.
+inversion Hv.
+assumption.
+Qed.
+
+Lemma soundness_raw32 : forall cs s1 s2 s3 s4,
+  ((s1,s2),(s3,s4)) =  ascii32_of_nat (length cs) ->
+  Soundness (Raw32 cs) ("219"::s1::s2::s3::s4::cs).
+Proof.
+straitfoward SLRaw32.
+inversion Hv.
+assumption.
+Qed.
+
+Lemma soundness_fixarray_nil :
+  Soundness (FixArray []) ["144"].
+Proof.
+unfold Soundness.
+intros.
+apply (SLFixArray os 0); auto.
+Qed.
+
+Lemma soundness_array16_nil :
+  Soundness (Array16 []) ["220"; "000"; "000"].
+Proof.
+unfold Soundness.
+intros.
+apply (SLArray16 os 0 _ _ bs' "000" "000"); auto.
+rewrite <- ascii16_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma soundness_array32_nil:
+  Soundness (Array32 []) ["221"; "000"; "000";"000"; "000"].
+Proof.
+unfold Soundness.
+intros.
+apply (SLArray32 os 0 _ _ bs' "000" "000" "000" "000"); auto.
+rewrite <- ascii32_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma soundness_fixmap_nil:
+  Soundness (FixMap []) ["128"].
+Proof.
+unfold Soundness.
+intros.
+apply (SLFixMap os 0 _ _ _ _ [] _ bs'); auto.
+Qed.
+
+Lemma soundness_map16_nil:
+  Soundness (Map16 []) ["222"; "000"; "000"].
+Proof.
+unfold Soundness.
+intros.
+apply (SLMap16 os 0 [] _ bs' "000" "000"); auto.
+rewrite <- ascii16_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma soundness_map32_nil:
+  Soundness (Map32 []) ["223"; "000"; "000";"000"; "000"].
+Proof.
+unfold Soundness.
+intros.
+apply (SLMap32 os 0 [] _ bs' "000" "000" "000" "000"); auto.
+rewrite <- ascii32_of_nat_O.
+reflexivity.
+Qed.
+
+Lemma soundness_fixarray_cons: forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  Soundness x y ->
+  Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Soundness (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Soundness (FixArray (x :: xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys).
+Proof.
+unfold Soundness.
+intros.
+simpl.
+rewrite app_cons.
+inversion H6.
+apply (SLFixArray (x::(xs++os)) (length (x::xs))); auto.
+ apply (H2 (xs++os) (ys++bs')) in H1; auto.
+ apply (H4 os bs') in H3; auto.
+ inversion H3.
+ apply split_at_soundness in H21.
+ rewrite H21 in *.
+ assumption.
+
+ apply split_at_length.
+Qed.
+
+Lemma soundness_array16_cons: forall x xs t1 t2 s1 s2 y ys,
+  (t1, t2) = ascii16_of_nat (length xs) ->
+  (s1, s2) = ascii16_of_nat (length (x :: xs)) ->
+  Serialized x y ->
+  Soundness x y ->
+  Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
+  Soundness (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
+  Soundness (Array16 (x :: xs)) ("220" :: s1 :: s2 :: y ++ ys).
+Proof.
+unfold Soundness.
+intros.
+simpl.
+rewrite app_cons.
+inversion H6.
+apply (SLArray16 (x::(xs++os)) (length (x::xs))); auto.
+ apply (H2 (xs++os) (ys++bs')) in H1; auto.
+ apply (H4 os bs') in H3; auto.
+ inversion H3.
+ apply split_at_soundness in H19.
+ rewrite H19 in *.
+ assumption.
+
+ apply split_at_length.
+Qed.
+
+Lemma soundness_array32_cons: forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
+  ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
+  ((s1,s2),(s3,s4)) = ascii32_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  Soundness x y ->
+  Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
+  Soundness (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
+  Soundness (Array32 (x::xs)) ("221"::s1::s2::s3::s4::y ++ ys).
+Proof.
+unfold Soundness.
+intros.
+simpl.
+rewrite app_cons.
+inversion H6.
+apply (SLArray32 (x::(xs++os)) (length (x::xs))); auto.
+ apply (H2 (xs++os) (ys++bs')) in H1; auto.
+ apply (H4 os bs') in H3; auto.
+ inversion H3.
+ apply split_at_soundness in H21.
+ rewrite H21 in *.
+ assumption.
+
+ apply split_at_length.
+Qed.
+
+
+Lemma soundness_fixmap_cons: forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
+  Serialized x1 y1 -> Soundness x1 y1 ->
+  Serialized x2 y2 -> Soundness x2 y2 ->
+  Serialized (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
+  Soundness (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
+  Soundness (FixMap ((x1, x2) :: xs)) (Ascii b5 b6 b7 b8 false false false true :: y1 ++ y2 ++ ys).
+Proof with auto.
+unfold Soundness.
+intros.
+simpl.
+rewrite app_cons.
+rewrite <- app_assoc.
+rewrite <- (pair_unpair _ ( (x1, x2) :: xs )).
+inversion H8.
+apply (SLFixMap (x1::x2::unpair xs++os)  (length ((x1,x2)::xs))); auto.
+ apply (H2 ( x2 :: unpair xs ++ os ) ( y2 ++ ys ++ bs' )) in H1; auto.
+ apply (H4 ( unpair xs ++ os) ( ys ++ bs')) in H3; auto.
+ apply (H6 os bs') in H5; auto.
+ inversion H5.
+ rewrite (unpair_pair _ n); auto.
+ apply split_at_soundness in H25.
+ rewrite <- H25...
+
+ apply unpair_split_at.
+
+ apply unpair_length.
+Qed.
+
+Lemma soundness_map16_cons: forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
+  (t1, t2) = ascii16_of_nat (length xs) ->
+  (s1, s2) = ascii16_of_nat (length ((x1, x2) :: xs)) ->
+  Serialized x1 y1 ->
+  Soundness x1 y1 ->
+  Serialized x2 y2 ->
+  Soundness x2 y2 ->
+  Serialized (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
+  Soundness (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
+  Soundness (Map16 ((x1, x2) :: xs)) ("222" :: s1 :: s2 :: y1 ++ y2 ++ ys).
+Proof with auto.
+unfold Soundness.
+intros.
+simpl.
+rewrite app_cons.
+rewrite <- app_assoc.
+rewrite <- (pair_unpair _ ( (x1, x2) :: xs )).
+inversion H8.
+apply (SLMap16 (x1::x2::unpair xs++os)  (length ((x1,x2)::xs))); auto.
+ apply (H2 ( x2 :: unpair xs ++ os ) ( y2 ++ ys ++ bs' )) in H1; auto.
+ apply (H4 ( unpair xs ++ os) ( ys ++ bs')) in H3; auto.
+ apply (H6 os bs') in H5; auto.
+ inversion H5.
+ rewrite (unpair_pair _ n); auto.
+ apply split_at_soundness in H23.
+ rewrite <- H23...
+
+ apply unpair_split_at.
+
+ apply unpair_length.
+Qed.
+
+Lemma soundness_map32_cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
+  (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
+  (s1, s2, (s3, s4)) = ascii32_of_nat (length ((x1, x2) :: xs)) ->
+  Serialized x1 y1 ->
+  Soundness x1 y1 ->
+  Serialized x2 y2 ->
+  Soundness x2 y2 ->
+  Serialized (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Soundness (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Soundness (Map32 ((x1, x2) :: xs)) ("223" :: s1 :: s2 :: s3 :: s4 :: y1 ++ y2 ++ ys).
+Proof with auto.
+unfold Soundness.
+intros.
+simpl.
+rewrite app_cons.
+rewrite <- app_assoc.
+rewrite <- (pair_unpair _ ( (x1, x2) :: xs )).
+inversion H8.
+apply (SLMap32 (x1::x2::unpair xs++os)  (length ((x1,x2)::xs))); auto.
+ apply (H2 ( x2 :: unpair xs ++ os ) ( y2 ++ ys ++ bs' )) in H1; auto.
+ apply (H4 ( unpair xs ++ os) ( ys ++ bs')) in H3; auto.
+ apply (H6 os bs') in H5; auto.
+ inversion H5.
+ rewrite (unpair_pair _ n); auto.
+ apply split_at_soundness in H25.
+ rewrite <- H25...
+
+ apply unpair_split_at.
+
+ apply unpair_length.
+Qed.
+
+Lemma soundness_intro : forall obj xs,
+  (Serialized obj xs -> Soundness obj xs) ->
+  Soundness obj xs.
+Proof.
+unfold Soundness.
+intros.
+eapply H in H0; auto.
+apply H0.
+auto.
+Qed.
+
+Hint Resolve
+  soundness_true soundness_false
+  soundness_nil soundness_pfixnum soundness_nfixnum
+  soundness_uint8 soundness_uint16 soundness_uint32 soundness_uint64
+  soundness_int8  soundness_int16  soundness_int32  soundness_int64
+  soundness_float soundness_double
+  soundness_raw16 soundness_raw32
+  soundness_fixarray_nil soundness_array16_nil soundness_array32_nil
+  soundness_fixmap_nil soundness_map16_nil soundness_map32_nil
+  : soundness.
+
+
+Theorem serialize_soundness : forall obj xs,
+  Soundness obj xs.
+Proof.
+intros.
+apply soundness_intro.
+intro.
+pattern obj,xs.
+apply Serialized_ind; intros; auto with soundness.
+ apply soundness_fixraw; auto.
+ apply soundness_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply soundness_array16_cons with (t1:=t1) (t2:=t2); auto.
+ apply soundness_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+ apply soundness_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply soundness_map16_cons with (t1:=t1) (t2:=t2); auto.
+ apply soundness_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+Qed.
+
+Lemma sl_soundness: forall o os bs bs',
+  Serialized o bs ->
+  Valid o ->
+  SerializedList os bs' ->
+  SerializedList (o :: os) (bs ++ bs').
+Proof.
+intros.
+apply soundness_intro; auto.
+intro.
+pattern o, bs.
+apply Serialized_ind; intros; auto with soundness.
+ apply soundness_fixraw; auto.
+ apply soundness_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply soundness_array16_cons with (t1:=t1) (t2:=t2); auto.
+ apply soundness_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+ apply soundness_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply soundness_map16_cons with (t1:=t1) (t2:=t2); auto.
+ apply soundness_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+Qed.
+
diff --git a/ocaml/proof/Soundness.v b/ocaml/proof/Soundness.v
new file mode 100644
index 00000000..a3072e80
--- /dev/null
+++ b/ocaml/proof/Soundness.v
@@ -0,0 +1,623 @@
+Require Import Ascii.
+Require Import ListUtil Object MultiByte SerializeSpec Prefix ProofUtil Pow.
+
+Definition Soundness obj1 x : Prop := forall obj2,
+  Serialized obj1 x ->
+  Serialized obj2 x ->
+  Valid obj1 ->
+  Valid obj2 ->
+  obj1 = obj2.
+
+Ltac straightfoward :=
+  intros;
+  unfold Soundness;
+  intros obj2 Hs1 Hs2 V1 V2;
+  inversion Hs2;
+  reflexivity.
+
+Lemma  soundness_nil:
+  Soundness Nil ["192"].
+Proof.
+straightfoward.
+Qed.
+
+Lemma soundness_true :
+  Soundness (Bool true) ["195"].
+Proof.
+straightfoward.
+Qed.
+
+Lemma soundness_false :
+  Soundness (Bool false) ["194"].
+Proof.
+straightfoward.
+Qed.
+
+Lemma soundness_pfixnum: forall x1 x2 x3 x4 x5 x6 x7,
+  Soundness (PFixnum   (Ascii x1 x2 x3 x4 x5 x6 x7 false))
+            [Ascii x1 x2 x3 x4 x5 x6 x7 false].
+Proof.
+straightfoward.
+Qed.
+
+Lemma soundness_nfixnum: forall x1 x2 x3 x4 x5,
+  Soundness (NFixnum   (Ascii x1 x2 x3 x4 x5 true true true))
+            [Ascii x1 x2 x3 x4 x5 true true true].
+Proof.
+straightfoward.
+Qed.
+
+Lemma soundness_uint8 : forall c,
+  Soundness (Uint8 c) ("204"::list_of_ascii8 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+rewrite_for obj2.
+auto.
+Qed.
+
+Lemma soundness_uint16 : forall c,
+  Soundness (Uint16 c) ("205"::list_of_ascii16 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_uint32 : forall c,
+  Soundness (Uint32 c) ("206"::list_of_ascii32 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_uint64 : forall c,
+  Soundness (Uint64 c) ("207"::list_of_ascii64 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_int8 : forall c,
+  Soundness (Int8 c) ("208"::list_of_ascii8 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_int16 : forall c,
+  Soundness (Int16 c) ("209"::list_of_ascii16 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_int32 : forall c,
+  Soundness (Int32 c) ("210"::list_of_ascii32 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_int64 : forall c,
+  Soundness (Int64 c) ("211"::list_of_ascii64 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_float : forall c,
+  Soundness (Float c) ("202"::list_of_ascii32 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_double : forall c,
+  Soundness (Double c) ("203"::list_of_ascii64 c).
+Proof.
+intros.
+unfold Soundness.
+intros obj2 Hs1 Hs2 V1 V2.
+inversion Hs2.
+assert (c = c0); [| rewrite_for c ]; auto with ascii.
+Qed.
+
+Lemma soundness_fixraw : forall cs b1 b2 b3 b4 b5,
+  Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (length cs) ->
+  Soundness (FixRaw cs) ((Ascii b1 b2 b3 b4 b5 true false true)::cs).
+Proof.
+straightfoward.
+Qed.
+
+Lemma soundness_raw16: forall cs s1 s2,
+  (s1,s2) =  ascii16_of_nat (length cs) ->
+  Soundness (Raw16 cs) ("218"::s1::s2::cs).
+Proof.
+straightfoward.
+Qed.
+
+Lemma soundness_raw32 : forall cs s1 s2 s3 s4,
+  ((s1,s2),(s3,s4)) =  ascii32_of_nat (length cs) ->
+  Soundness (Raw32 cs) ("219"::s1::s2::s3::s4::cs).
+Proof.
+straightfoward.
+Qed.
+
+Lemma soundness_fixarray_nil :
+  Soundness (FixArray []) ["144"].
+Proof.
+unfold Soundness.
+intros.
+inversion H0; auto.
+apply ascii8_not_O in H10; [ contradiction |].
+split; [ simpl; omega |].
+rewrite_for obj2.
+inversion H2.
+transitivity (pow 4); [ assumption |].
+apply pow_lt.
+auto.
+Qed.
+
+Lemma soundness_array16_nil :
+  Soundness (Array16 []) ["220"; "000"; "000"].
+Proof.
+unfold Soundness.
+intros.
+inversion H0; auto.
+apply ascii16_not_O in H8; [ contradiction |].
+split; [ simpl; omega |].
+rewrite_for obj2.
+inversion H2.
+assumption.
+Qed.
+
+Lemma soundness_array32_nil:
+  Soundness (Array32 []) ["221"; "000"; "000";"000"; "000"].
+Proof.
+unfold Soundness.
+intros.
+inversion H0; auto.
+apply ascii32_not_O in H10; [ contradiction |].
+split; [ simpl; omega |].
+rewrite_for obj2.
+inversion H2.
+assumption.
+Qed.
+
+Lemma soundness_fixmap_nil:
+  Soundness (FixMap []) ["128"].
+Proof.
+unfold Soundness.
+intros.
+inversion H0; auto.
+apply ascii8_not_O in H10; [ contradiction |].
+split; [ simpl; omega |].
+rewrite_for obj2.
+inversion H2.
+transitivity (pow 4); [ assumption |].
+apply pow_lt.
+auto.
+Qed.
+
+Lemma soundness_map16_nil:
+  Soundness (Map16 []) ["222"; "000"; "000"].
+Proof.
+unfold Soundness.
+intros.
+inversion H0; auto.
+apply ascii16_not_O in H7; [ contradiction |].
+split; [ simpl; omega |].
+rewrite_for obj2.
+inversion H2.
+assumption.
+Qed.
+
+Lemma soundness_map32_nil:
+  Soundness (Map32 []) ["223"; "000"; "000";"000"; "000"].
+Proof.
+unfold Soundness.
+intros.
+inversion H0; auto.
+apply ascii32_not_O in H10; [ contradiction |].
+split; [ simpl; omega |].
+rewrite_for obj2.
+inversion H2.
+assumption.
+Qed.
+
+Lemma soundness_fixarray_cons: forall x xs y ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  Soundness x y ->
+  Serialized (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Soundness (FixArray xs) ((Ascii b1 b2 b3 b4 true false false true)::ys) ->
+  Soundness (FixArray (x :: xs)) ((Ascii b5 b6 b7 b8 true false false true)::y ++ ys).
+Proof.
+unfold Soundness.
+intros.
+inversion H6.
+ rewrite_for b5.
+ rewrite_for b6.
+ rewrite_for b7.
+ rewrite_for b8.
+ apply ascii8_not_O in H0; [ contradiction |].
+ split; [ simpl; omega |].
+ inversion H7.
+ transitivity (pow 4); [| apply pow_lt ]; auto.
+
+ rewrite_for obj2.
+ inversion H7.
+ inversion H8.
+ assert (y = y0).
+  generalize prefix.
+  unfold Prefix.
+  intro Hprefix.
+  apply (Hprefix x _ x0 _ ys ys0); auto.
+
+  rewrite_for y0.
+  apply H2 with (obj2:=x0) in H1; auto.
+  apply app_same in H15.
+  apply H4 with (obj2:=(FixArray xs0)) in H3; auto.
+   inversion H3.
+   rewrite H1.
+   reflexivity.
+
+   rewrite H16 in H0.
+   apply ascii8_of_nat_eq in H0; [| transitivity (pow 4); [| apply pow_lt]; auto
+                                  | transitivity (pow 4); [| apply pow_lt]; auto].
+   simpl H0.
+   inversion H0.
+   rewrite <- H29 in H.
+   rewrite <- H14 in H.
+   inversion H.
+   rewrite_for b9.
+   rewrite_for b10.
+   rewrite_for ys.
+   assumption.
+Qed.
+
+Lemma soundness_array16_cons: forall x xs t1 t2 s1 s2 y ys,
+  (t1, t2) = ascii16_of_nat (length xs) ->
+  (s1, s2) = ascii16_of_nat (length (x :: xs)) ->
+  Serialized x y ->
+  (Serialized x y -> Soundness x y) ->
+  Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
+  (Serialized (Array16 xs) ("220" :: t1 :: t2 :: ys) ->
+    Soundness (Array16 xs) ("220" :: t1 :: t2 :: ys)) ->
+  Soundness (Array16 (x :: xs)) ("220" :: s1 :: s2 :: y ++ ys).
+Proof.
+unfold Soundness.
+intros.
+inversion H6.
+ rewrite_for s1.
+ rewrite_for s2.
+ apply ascii16_not_O in H0; [ contradiction |].
+ split; [ simpl; omega |].
+ inversion H7.
+ assumption.
+
+ rewrite_for obj2.
+ inversion H7.
+ inversion H8.
+ assert (y = y0).
+  generalize prefix.
+  unfold Prefix.
+  intro Hprefix.
+  apply (Hprefix x _ x0 _ ys ys0); auto.
+
+  rewrite_for y0.
+  apply H2 with (obj2:=x0) in H1; auto.
+  apply app_same in H11.
+  apply H4 with (obj2:=(Array16 xs0)) in H3; auto.
+   inversion H3.
+   rewrite H1.
+   reflexivity.
+
+   rewrite H14 in H0.
+   simpl in H0.
+   apply ascii16_of_nat_eq in H0; auto.
+   inversion H0.
+   rewrite <- H27 in H.
+   rewrite <- H12 in H.
+   inversion H.
+   rewrite_for t0.
+   rewrite_for t3.
+   rewrite_for ys.
+   assumption.
+Qed.
+
+Lemma soundness_array32_cons: forall x xs y ys s1 s2 s3 s4 t1 t2 t3 t4,
+  ((t1,t2),(t3,t4)) = ascii32_of_nat (length xs) ->
+  ((s1,s2),(s3,s4)) = ascii32_of_nat (length (x::xs)) ->
+  Serialized x y ->
+  (Serialized x y -> Soundness x y) ->
+  Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) ->
+  (Serialized (Array32 xs) ("221"::t1::t2::t3::t4::ys) -> Soundness (Array32 xs) ("221"::t1::t2::t3::t4::ys)) ->
+  Soundness (Array32 (x::xs)) ("221"::s1::s2::s3::s4::y ++ ys).
+Proof.
+unfold Soundness.
+intros.
+inversion H6.
+ rewrite_for s1.
+ rewrite_for s2.
+ rewrite_for s3.
+ rewrite_for s4.
+ apply ascii32_not_O in H0; [ contradiction |].
+ split; [ simpl; omega |].
+ inversion H7.
+ assumption.
+
+ rewrite_for obj2.
+ inversion H7.
+ inversion H8.
+ assert (y = y0).
+  generalize prefix.
+  unfold Prefix.
+  intro Hprefix.
+  apply (Hprefix x _ x0 _ ys ys0); auto.
+
+  rewrite_for y0.
+  apply H2 with (obj2:=x0) in H1; auto.
+  apply app_same in H15.
+  apply H4 with (obj2:=(Array32 xs0)) in H3; auto.
+   inversion H3.
+   rewrite H1.
+   reflexivity.
+
+   rewrite H16 in H0.
+   simpl in H0.
+   apply ascii32_of_nat_eq in H0; auto.
+   inversion H0.
+   rewrite <- H29 in H.
+   rewrite <- H14 in H.
+   inversion H.
+   rewrite_for t0.
+   rewrite_for t5.
+   rewrite_for t6.
+   rewrite_for t7.
+   rewrite_for ys.
+   assumption.
+Qed.
+
+Lemma soundness_fixmap_cons: forall x1 x2 xs y1 y2 ys b1 b2 b3 b4 b5 b6 b7 b8,
+  Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat (length xs) ->
+  Ascii b5 b6 b7 b8 false false false false = ascii8_of_nat (length ((x1,x2)::xs)) ->
+  Serialized x1 y1 -> Soundness x1 y1 ->
+  Serialized x2 y2 -> Soundness x2 y2 ->
+  Serialized (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
+  Soundness (FixMap xs) (Ascii b1 b2 b3 b4 false false false true :: ys) ->
+  Soundness (FixMap ((x1, x2) :: xs)) (Ascii b5 b6 b7 b8 false false false true :: y1 ++ y2 ++ ys).
+Proof.
+unfold Soundness.
+intros.
+inversion H8.
+ rewrite_for b5.
+ rewrite_for b6.
+ rewrite_for b7.
+ rewrite_for b8.
+ apply ascii8_not_O in H0; [ contradiction |].
+ split; [ simpl; omega |].
+ inversion H9.
+ transitivity (pow 4); [| apply pow_lt]; auto.
+
+ rewrite_for obj2.
+ inversion H9.
+ inversion H10.
+ generalize prefix.
+ unfold Prefix.
+ intro Hprefix.
+ assert (y1 = y0).
+  apply (Hprefix x1 _ x0 _ (y2 ++ ys) (y3 ++ ys0)); auto.
+
+  rewrite_for y0.
+  apply app_same in H15.
+  assert (y2 = y3).
+  apply (Hprefix x2 _ x3 _ ys ys0); auto.
+
+  rewrite_for y3.
+  apply H2 with (obj2:=x0) in H1; auto.
+  apply H4 with (obj2:=x3) in H3; auto.
+  apply H6 with (obj2:=(FixMap xs0)) in H5; auto.
+   inversion H5.
+   rewrite H1, H3.
+   reflexivity.
+
+   rewrite H18 in H0.
+   simpl in H0.
+   apply ascii8_of_nat_eq in H0; [| transitivity (pow 4); [| apply pow_lt]; auto
+                                  | transitivity (pow 4); [| apply pow_lt]; auto].
+   inversion H0.
+   rewrite <- H36 in H.
+   rewrite <- H17 in H.
+   inversion H.
+   rewrite_for b0.
+   rewrite_for b9.
+   rewrite_for b10.
+   rewrite_for b11.
+   apply app_same in H15.
+   rewrite_for ys.
+   assumption.
+Qed.
+
+Lemma soundness_map16_cons: forall x1 x2 xs y1 y2 ys s1 s2 t1 t2,
+  (t1, t2) = ascii16_of_nat (length xs) ->
+  (s1, s2) = ascii16_of_nat (length ((x1, x2) :: xs)) ->
+  Serialized x1 y1 ->
+  Soundness x1 y1 ->
+  Serialized x2 y2 ->
+  Soundness x2 y2 ->
+  Serialized (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
+  Soundness (Map16 xs) ("222" :: t1 :: t2 :: ys) ->
+  Soundness (Map16 ((x1, x2) :: xs)) ("222" :: s1 :: s2 :: y1 ++ y2 ++ ys).
+Proof.
+unfold Soundness.
+intros.
+inversion H8.
+ rewrite_for s1.
+ rewrite_for s2.
+ apply ascii16_not_O in H0; [ contradiction |].
+ split; [ simpl; omega |].
+ inversion H9.
+ assumption.
+
+ rewrite_for obj2.
+ inversion H9.
+ inversion H10.
+ generalize prefix.
+ unfold Prefix.
+ intro Hprefix.
+ assert (y1 = y0).
+  apply (Hprefix x1 _ x0 _ (y2 ++ ys) (y3 ++ ys0)); auto.
+
+  rewrite_for y0.
+  apply app_same in H13.
+  assert (y2 = y3).
+  apply (Hprefix x2 _ x3 _ ys ys0); auto.
+
+  rewrite_for y3.
+
+  apply H2 with (obj2:=x0) in H1; auto.
+  apply H4 with (obj2:=x3) in H3; auto.
+  apply H6 with (obj2:=(Map16 xs0)) in H5; auto.
+   inversion H5.
+   rewrite H1, H3.
+   reflexivity.
+
+   rewrite H15 in H0.
+   simpl in H0.
+   apply ascii16_of_nat_eq in H0; auto.
+   inversion H0.
+   rewrite <- H34 in H.
+   rewrite <- H14 in H.
+   inversion H.
+   rewrite_for t0.
+   rewrite_for t3.
+   apply app_same in H13.
+   rewrite_for ys.
+   assumption.
+Qed.
+
+Lemma soundness_map32_cons : forall x1 x2 xs y1 y2 ys s1 s2 s3 s4 t1 t2 t3 t4,
+  (t1, t2, (t3, t4)) = ascii32_of_nat (length xs) ->
+  (s1, s2, (s3, s4)) = ascii32_of_nat (length ((x1, x2) :: xs)) ->
+  Serialized x1 y1 ->
+  Soundness x1 y1 ->
+  Serialized x2 y2 ->
+  Soundness x2 y2 ->
+  Serialized (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Soundness (Map32 xs) ("223" :: t1 :: t2 :: t3 :: t4 :: ys) ->
+  Soundness (Map32 ((x1, x2) :: xs)) ("223" :: s1 :: s2 :: s3 :: s4 :: y1 ++ y2 ++ ys).
+Proof.
+unfold Soundness.
+intros.
+inversion H8.
+ rewrite_for s1.
+ rewrite_for s2.
+ rewrite_for s3.
+ rewrite_for s4.
+ apply ascii32_not_O in H0; [ contradiction |].
+ split; [ simpl; omega |].
+ inversion H9.
+ assumption.
+
+ rewrite_for obj2.
+ inversion H9.
+ inversion H10.
+ generalize prefix.
+ unfold Prefix.
+ intro Hprefix.
+ assert (y1 = y0).
+  apply (Hprefix x1 _ x0 _ (y2 ++ ys) (y3 ++ ys0)); auto.
+
+  rewrite_for y0.
+  apply app_same in H15.
+  assert (y2 = y3).
+  apply (Hprefix x2 _ x3 _ ys ys0); auto.
+
+  rewrite_for y3.
+  apply H2 with (obj2:=x0) in H1; auto.
+  apply H4 with (obj2:=x3) in H3; auto.
+  apply H6 with (obj2:=(Map32 xs0)) in H5; auto.
+   inversion H5.
+   rewrite H1, H3.
+   reflexivity.
+
+   rewrite H18 in H0.
+   simpl in H0.
+   apply ascii32_of_nat_eq in H0; auto.
+   inversion H0.
+   rewrite <- H36 in H.
+   rewrite <- H17 in H.
+   inversion H.
+   rewrite_for t0.
+   rewrite_for t5.
+   rewrite_for t6.
+   rewrite_for t7.
+   apply app_same in H15.
+   rewrite_for ys.
+   assumption.
+Qed.
+
+Hint Resolve
+  soundness_true soundness_false
+  soundness_nil soundness_pfixnum soundness_nfixnum
+  soundness_uint8 soundness_uint16 soundness_uint32 soundness_uint64
+  soundness_int8  soundness_int16  soundness_int32  soundness_int64
+  soundness_float soundness_double
+  soundness_raw16 soundness_raw32
+  soundness_fixarray_nil soundness_array16_nil soundness_array32_nil
+  soundness_fixmap_nil soundness_map16_nil soundness_map32_nil
+  : soundness.
+
+Lemma soundness_intro: forall obj x,
+  (Serialized obj x -> Soundness obj x)->
+  Soundness obj x.
+Proof.
+unfold Soundness.
+intros.
+apply H in H1; auto.
+Qed.
+
+Theorem soundness : forall obj1 x,
+  Soundness obj1 x.
+Proof.
+intros.
+apply soundness_intro.
+intro.
+pattern obj1,x.
+apply Serialized_ind; intros; auto with soundness.
+ apply soundness_fixraw; auto.
+ apply soundness_fixarray_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply soundness_array16_cons with (t1:=t1) (t2:=t2); auto.
+ apply soundness_array32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+ apply soundness_fixmap_cons with (b1:=b1) (b2:=b2) (b3:=b3) (b4:=b4); auto.
+ apply soundness_map16_cons with (t1:=t1) (t2:=t2); auto.
+ apply soundness_map32_cons with (t1:=t1) (t2:=t2) (t3:=t3) (t4:=t4); auto.
+Qed.
diff --git a/ocaml/proof/Util.v b/ocaml/proof/Util.v
new file mode 100644
index 00000000..1e104b36
--- /dev/null
+++ b/ocaml/proof/Util.v
@@ -0,0 +1,39 @@
+Require Ascii List.
+Require Import ExtractUtil.
+
+Definition mlchar_of_ascii a :=
+  mlchar_of_mlint (mlint_of_nat (Ascii.nat_of_ascii a)).
+Definition mlstring_of_string s :=
+  mlstring_of_list mlchar_of_ascii (list_of_string s).
+Definition ascii_of_mlchar c :=
+  Ascii.ascii_of_nat (nat_of_mlint (mlint_of_mlchar c)).
+Definition string_of_mlstring s :=
+  string_of_list (list_of_mlstring ascii_of_mlchar s).
+
+Definition print s := print_mlstring (mlstring_of_string s).
+Definition println s := println_mlstring (mlstring_of_string s).
+Definition prerr s := prerr_mlstring (mlstring_of_string s).
+Definition prerrln s := prerrln_mlstring (mlstring_of_string s).
+
+CoFixpoint lmap {A B:Type} (f: A -> B) (xs : llist A) : llist B :=
+  match xs with
+  | LNil => LNil
+  | LCons x xs => LCons (f x) (lmap f xs)
+  end.
+
+Fixpoint ltake {A:Type} n (xs: llist A) :=
+  match (n, xs) with
+  | (O, _) => List.nil
+  | (_, LNil) => List.nil
+  | (S n', LCons x xs) => List.cons x (ltake n' xs)
+  end.
+
+Definition get_contents := lmap ascii_of_mlchar get_contents_mlchars.
+
+Definition id {A:Type} (x:A) := x.
+
+Definition atat {A B:Type} (f:A -> B) (x: A) := f x.
+Infix "@@" := atat (right associativity, at level 75).
+
+Definition doll {A B C:Type} (g:B->C) (f:A->B) (x:A) := g (f x).
+Infix "$" := doll (at level 75).