mirror of
https://github.com/msgpack/msgpack-c.git
synced 2025-11-04 04:09:59 +01:00
123 lines
3.2 KiB
Coq
123 lines
3.2 KiB
Coq
(* -*- 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.
|
|
|