generic-library/msgpack
1
0
Fork 0
mirror of https://github.com/msgpack/msgpack-c.git synced 2025-03-19 04:52:59 +01:00
Code Issues Projects Releases Wiki Activity

MessagePack for OCaml moved to https://github.com/msgpack/msgpack-ocaml

Browse Source
This commit is contained in:
FURUHASHI Sadayuki 2012-07-04 17:40:11 -07:00
parent b2839ac78b
commit 320510506b
42 changed files with 1 additions and 7908 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
ocaml/.gitignore vendored
View File

@ -1,11 +0,0 @@
*~
*.omc
.omakedb
.omakedb.lock
*.vo
*.glob
*.cm[iox]
*.o
*.annot
*.opt
*.run

8
ocaml/OMakefile
View File

@ -1,8 +0,0 @@
NATIVE_ENABLED = true
BYTE_ENABLED = true
.PHONY: clean
.SUBDIRS: ocaml proof
clean:
rm -rf *.vo *.glob *~ *.omc .omakedb .omakedb.lock

45
ocaml/OMakeroot
View File

@ -1,45 +0,0 @@
########################################################################
# 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: .

1
ocaml/README Normal file
View File

@ -0,0 +1 @@
MessagePack for OCaml moved to https://github.com/msgpack/msgpack-ocaml.

22
ocaml/README.markdown
View File

@ -1,22 +0,0 @@
MsgPack for OCaml
==============================
See http://wiki.msgpack.org/display/MSGPACK/QuickStart+for+OCaml

14
ocaml/bleis-hooks/commit-msg
View File

@ -1,14 +0,0 @@
#! /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

60
ocaml/bleis-hooks/common.sh
View File

@ -1,60 +0,0 @@
#! /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 }"
}

22
ocaml/bleis-hooks/pre-commit
View File

@ -1,22 +0,0 @@
#! /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

2
ocaml/ocaml/.gitignore vendored
View File

@ -1,2 +0,0 @@
runner
doc

6
ocaml/ocaml/META
View File

@ -1,6 +0,0 @@
name="msgpack"
version="0.1.0"
description="a library for MessagePack."
requires="extlib, num"
archive(byte)="msgpack.cmo"
archive(native)="msgpack.cmx"

80
ocaml/ocaml/OMakefile
View File

@ -1,80 +0,0 @@
.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: all
ocamlfind install msgpack META *.cmo *.cmx *.cmi
clean:
rm -rf *.cm[iox] *.o *~ *.omc .omakedb .omakedb.lock *.cmxa *.a *.opt *.run *.annot runner msgpackCore.*

142
ocaml/ocaml/base.ml
View File

@ -1,142 +0,0 @@
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

1
ocaml/ocaml/config.ml
View File

@ -1 +0,0 @@
let version = (1,0,0)

191
ocaml/ocaml/hList.ml
View File

@ -1,191 +0,0 @@
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

2
ocaml/ocaml/main.ml
View File

@ -1,2 +0,0 @@
let _ =
print_endline "hello"

46
ocaml/ocaml/msgpack.mli
View File

@ -1,46 +0,0 @@
(** 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

2581
ocaml/ocaml/msgpackCore.ml
View File

File diff suppressed because it is too large Load Diff

141
ocaml/ocaml/msgpackCore.mli
View File

@ -1,141 +0,0 @@
val fst : ('a1 * 'a2) -> 'a1
val snd : ('a1 * 'a2) -> 'a2
val length : 'a1 list -> int
val app : 'a1 list -> 'a1 list -> 'a1 list
val plus : int -> int -> int
val mult : int -> int -> int
type positive =
| XI of positive
| XO of positive
| XH
val psucc : positive -> positive
val pplus : positive -> positive -> positive
val pplus_carry : positive -> positive -> positive
val pmult_nat : positive -> int -> int
val nat_of_P : positive -> int
val p_of_succ_nat : int -> positive
val pmult : positive -> positive -> positive
type n =
| N0
| Npos of positive
val nplus : n -> n -> n
val nmult : n -> n -> n
val nat_of_N : n -> int
val n_of_nat : int -> n
val flat_map : ('a1 -> 'a2 list) -> 'a1 list -> 'a2 list
val eucl_dev : int -> int -> (int * int)
type ascii =
| Ascii of bool * bool * bool * bool * bool * bool * bool * bool
val zero : ascii
val one : ascii
val shift : bool -> ascii -> ascii
val ascii_of_pos : positive -> ascii
val ascii_of_N : n -> ascii
val ascii_of_nat : int -> ascii
val n_of_digits : bool list -> n
val n_of_ascii : ascii -> n
val nat_of_ascii : ascii -> int
val take : int -> 'a1 list -> 'a1 list
val drop : int -> 'a1 list -> 'a1 list
val split_at : int -> 'a1 list -> 'a1 list * 'a1 list
val pair : 'a1 list -> ('a1 * 'a1) list
val pow : int -> int
val divmod : int -> int -> (int * int)
type ascii8 = ascii
type ascii16 = ascii8 * ascii8
type ascii32 = ascii16 * ascii16
type ascii64 = ascii32 * ascii32
val nat_of_ascii8 : ascii -> int
val ascii8_of_nat : int -> ascii
val ascii16_of_nat : int -> ascii * ascii
val nat_of_ascii16 : ascii16 -> int
val ascii32_of_nat : int -> (ascii * ascii) * (ascii * ascii)
val nat_of_ascii32 : ascii32 -> int
val list_of_ascii8 : ascii8 -> ascii8 list
val list_of_ascii16 : ascii16 -> ascii8 list
val list_of_ascii32 : ascii32 -> ascii8 list
val list_of_ascii64 : ascii64 -> ascii8 list
type object0 =
| Bool of bool
| Nil
| PFixnum of ascii8
| NFixnum of ascii8
| Uint8 of ascii8
| Uint16 of ascii16
| Uint32 of ascii32
| Uint64 of ascii64
| Int8 of ascii8
| Int16 of ascii16
| Int32 of ascii32
| Int64 of ascii64
| Float of ascii32
| Double of ascii64
| FixRaw of ascii8 list
| Raw16 of ascii8 list
| Raw32 of ascii8 list
| FixArray of object0 list
| Array16 of object0 list
| Array32 of object0 list
| FixMap of (object0 * object0) list
| Map16 of (object0 * object0) list
| Map32 of (object0 * object0) list
val atat : ('a1 -> 'a2) -> 'a1 -> 'a2
val serialize : object0 -> ascii8 list
val compact : object0 list -> ascii8 list
val deserialize : int -> ascii8 list -> object0 list

206
ocaml/ocaml/pack.ml
View File

@ -1,206 +0,0 @@
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)

32
ocaml/ocaml/pack.mli
View File

@ -1,32 +0,0 @@
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

175
ocaml/ocaml/packTest.ml
View File

@ -1,175 +0,0 @@
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

20
ocaml/ocaml/serialize.ml
View File

@ -1,20 +0,0 @@
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

4
ocaml/ocaml/serialize.mli
View File

@ -1,4 +0,0 @@
type t = Pack.t
val deserialize_string : string -> t
val serialize_string : t -> string

16
ocaml/ocaml/serializeTest.ml
View File

@ -1,16 +0,0 @@
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

2
ocaml/proof/.gitignore vendored
View File

@ -1,2 +0,0 @@
msgpackCore.ml
msgpackCore.mli

14
ocaml/proof/CoqBuildRule
View File

@ -1,14 +0,0 @@
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) $<

630
ocaml/proof/DeserializeImplement.v
View File

@ -1,630 +0,0 @@
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.

95
ocaml/proof/ExtractUtil.v
View File

@ -1,95 +0,0 @@
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 ()".

259
ocaml/proof/ListUtil.v
View File

@ -1,259 +0,0 @@
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.

3
ocaml/proof/Main.v
View File

@ -1,3 +0,0 @@
Require Import ExtrOcamlBasic ExtrOcamlIntConv ExtrOcamlNatInt.
Require Import SerializeImplement DeserializeImplement.
Extraction "msgpackCore.ml" serialize deserialize.

334
ocaml/proof/MultiByte.v
View File

@ -1,334 +0,0 @@
(*
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.

8
ocaml/proof/OCamlBase.v
View File

@ -1,8 +0,0 @@
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).

26
ocaml/proof/OMakefile
View File

@ -1,26 +0,0 @@
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

122
ocaml/proof/Object.v
View File

@ -1,122 +0,0 @@
(* -*- 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.

162
ocaml/proof/Pow.v
View File

@ -1,162 +0,0 @@
(**
算術演算関連の補題
*)
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.

674
ocaml/proof/Prefix.v
View File

@ -1,674 +0,0 @@
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.

5
ocaml/proof/ProofUtil.v
View File

@ -1,5 +0,0 @@
Ltac rewrite_for x :=
match goal with
| [ H : x = _ |- _ ] => rewrite H in *; clear H
| [ H : _ = x |- _ ] => rewrite <- H in *; clear H
end.

465
ocaml/proof/SerializeImplement.v
View File

@ -1,465 +0,0 @@
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.

99
ocaml/proof/SerializeSpec.v
View File

@ -1,99 +0,0 @@
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).

521
ocaml/proof/SerializedList.v
View File

@ -1,521 +0,0 @@
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.

623
ocaml/proof/Soundness.v
View File

@ -1,623 +0,0 @@
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.

39
ocaml/proof/Util.v
View File

@ -1,39 +0,0 @@
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).