Ticket #460: easycrypt_IB6_IB7_QueryTags143e2c4.v

(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
Require Import Rtrigo_def.
Require Import Rpower.
Require Import R_sqrt.
Require Import Rpower.
Require Import Rbasic_fun.
Parameter bitstring_hashDataLen : Type.

Parameter bitstring_hashTagLen : Type.

Parameter bitstring_symmKeyLen : Type.

Parameter bitstring_payloadLen : Type.

Inductive option (a:Type) :=
  | None : option a
  | Some : a -> option a.
Set Contextual Implicit.
Implicit Arguments None.
Unset Contextual Implicit.
Implicit Arguments Some.

Inductive list (a:Type) :=
  | Nil : list a
  | Cons : a -> (list a) -> list a.
Set Contextual Implicit.
Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.

Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
  a) :=
  match l1 with
  | Nil => l2
  | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2))
  end.
Unset Implicit Arguments.

Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
  (l3:(list a)), ((infix_plpl l1 (infix_plpl l2
  l3)) = (infix_plpl (infix_plpl l1 l2) l3)).

Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
  (Nil:(list a))) = l).

Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
  match l with
  | Nil => 0%Z
  | (Cons _ r) => (1%Z + (length r))%Z
  end.
Unset Implicit Arguments.

Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
  (0%Z <= (length l))%Z.

Axiom Length_nil : forall (a:Type), forall (l:(list a)),
  ((length l) = 0%Z) <-> (l = (Nil:(list a))).

Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
  ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).

Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
  match l with
  | Nil => False
  | (Cons y r) => (x = y) \/ (mem x r)
  end.
Unset Implicit Arguments.

Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
  (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)).

Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
  exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).

Definition log2(x:R): R := (Rdiv (ln x) (ln 2%R))%R.

Definition log10(x:R): R := (Rdiv (ln x) (ln 10%R))%R.

Parameter pow: R -> R -> R.


Axiom Pow_zero_y : forall (y:R), (~ (y = 0%R)) -> ((pow 0%R y) = 0%R).

Axiom Pow_x_zero : forall (x:R), (~ (x = 0%R)) -> ((pow x 0%R) = 1%R).

Axiom Pow_x_one : forall (x:R), ((pow x 1%R) = x).

Axiom Pow_one_y : forall (y:R), ((pow 1%R y) = 1%R).

Axiom Pow_x_two : forall (x:R), ((pow x 2%R) = (Rsqr x)).

Axiom Pow_half : forall (x:R), (0%R <= x)%R -> ((pow x
  (05 / 10)%R) = (sqrt x)).

Axiom Pow_exp_log : forall (x:R) (y:R), (0%R <  x)%R -> ((pow x
  y) = (exp (y * (ln x))%R)).

Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
  (x <= y)%Z).

Parameter power: Z -> Z -> Z.


Axiom Power_0 : forall (x:Z), ((power x 0%Z) = 1%Z).

Axiom Power_s : forall (x:Z) (n:Z), (0%Z <= n)%Z -> ((power x
  (n + 1%Z)%Z) = (x * (power x n))%Z).

Axiom Power_1 : forall (x:Z), ((power x 1%Z) = x).

Axiom Power_sum : forall (x:Z) (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
  ((power x (n + m)%Z) = ((power x n) * (power x m))%Z).

Axiom Power_mult : forall (x:Z) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
  ((power x (n * m)%Z) = (power (power x n) m))).

Parameter div: Z -> Z -> Z.


Parameter mod1: Z -> Z -> Z.


Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x
  y))%Z + (mod1 x y))%Z).

Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <  y)%Z) ->
  ((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z).

Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x
  y))%Z /\ ((mod1 x y) <  (Zabs y))%Z).

Axiom Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).

Axiom Div_1 : forall (x:Z), ((div x 1%Z) = x).

Parameter map : forall (qta:Type) (qtb:Type), Type.

Parameter real_of_bool: bool -> R.


Parameter upd_map: forall (qta:Type) (qtb:Type), (map qta qtb) -> qta
  -> qtb -> (map qta qtb).

Implicit Arguments upd_map.

Parameter get_map: forall (qta:Type) (qtb:Type), (map qta qtb) -> qta -> qtb.

Implicit Arguments get_map.

Parameter in_dom_map: forall (qta:Type) (qtb:Type), qta -> (map qta qtb) ->
  Prop.

Implicit Arguments in_dom_map.

Parameter in_rng_map: forall (qta:Type) (qtb:Type), qtb -> (map qta qtb) ->
  Prop.

Implicit Arguments in_rng_map.

Parameter sp_lk__: Z.


Definition fst (qta:Type) (qtb:Type)(p:(qta* qtb)%type): qta :=
  match p with
  | (a, b) => a
  end.
Implicit Arguments fst.

Definition snd (qta:Type) (qtb:Type)(p:(qta* qtb)%type): qtb :=
  match p with
  | (a, b) => b
  end.
Implicit Arguments snd.

Definition pi3_1 (qta:Type) (qtb:Type) (qtc:Type)(p:(qta* qtb*
  qtc)%type): qta := match p with
  | (a, b, c) => a
  end.
Implicit Arguments pi3_1.

Definition pi3_2 (qta:Type) (qtb:Type) (qtc:Type)(p:(qta* qtb*
  qtc)%type): qtb := match p with
  | (a, b, c) => b
  end.
Implicit Arguments pi3_2.

Definition pi3_3 (qta:Type) (qtb:Type) (qtc:Type)(p:(qta* qtb*
  qtc)%type): qtc := match p with
  | (a, b, c) => c
  end.
Implicit Arguments pi3_3.

Definition pi4_1 (qta:Type) (qtb:Type) (qtc:Type) (qtd:Type)(p:(qta* qtb*
  qtc* qtd)%type): qta := match p with
  | (a, b, c, d) => a
  end.
Implicit Arguments pi4_1.

Definition pi4_2 (qta:Type) (qtb:Type) (qtc:Type) (qtd:Type)(p:(qta* qtb*
  qtc* qtd)%type): qtb := match p with
  | (a, b, c, d) => b
  end.
Implicit Arguments pi4_2.

Definition pi4_3 (qta:Type) (qtb:Type) (qtc:Type) (qtd:Type)(p:(qta* qtb*
  qtc* qtd)%type): qtc := match p with
  | (a, b, c, d) => c
  end.
Implicit Arguments pi4_3.

Definition pi4_4 (qta:Type) (qtb:Type) (qtc:Type) (qtd:Type)(p:(qta* qtb*
  qtc* qtd)%type): qtd := match p with
  | (a, b, c, d) => d
  end.
Implicit Arguments pi4_4.

Parameter proj: forall (qta:Type), (option qta) -> qta.

Implicit Arguments proj.

Parameter hd: forall (qta:Type), (list qta) -> qta.

Implicit Arguments hd.

Parameter tl: forall (qta:Type), (list qta) -> (list qta).

Implicit Arguments tl.

Parameter empty_map: forall (qta:Type) (qtb:Type), (map qta qtb).

Set Contextual Implicit.
Implicit Arguments empty_map.
Unset Contextual Implicit.

Parameter nat : Type.

Parameter natProject: nat -> Z.


Parameter natInject: Z -> nat.


Parameter nth: forall (qta:Type), (list qta) -> Z -> (option qta).

Implicit Arguments nth.

Definition unique (qta:Type)(xs:(list qta)) (ys:(list qta)): Prop :=
  (forall (y:qta), (mem y ys) -> (mem y xs)) /\ ((forall (x:qta), (mem x
  xs) -> (mem x ys)) /\ forall (i:Z) (j:Z), (0%Z <= i)%Z ->
  ((i <  (length ys))%Z -> ((0%Z <= j)%Z -> ((j <  (length ys))%Z ->
  (((proj (nth ys i)) = (proj (nth ys j))) -> (i = j)))))).
Implicit Arguments unique.

Parameter unique1: forall (qta:Type), (list qta) -> (list qta).

Implicit Arguments unique1.

Definition noDups (qta:Type)(xs:(list qta)): Prop := (unique xs xs).
Implicit Arguments noDups.

Definition fromTo(i:Z) (j:Z) (xs:(list Z)): Prop := ((j <  i)%Z /\
  (xs = (Nil:(list Z)))) \/ ((i <= j)%Z /\ (((length xs) = (j - i)%Z) /\
  ((noDups xs) /\ forall (k:Z), (i <= k)%Z -> ((k <= j)%Z -> (mem k xs))))).

Parameter fromTo1: Z -> Z -> (list Z).


Definition remov (qta:Type)(i:Z) (xs:(list qta)) (ys:(list qta)): Prop :=
  (0%Z <= i)%Z /\ ((i <  (length xs))%Z /\
  (((length ys) = ((length xs) - 1%Z)%Z) /\ ((forall (j:Z), (0%Z <= j)%Z ->
  ((j <  i)%Z -> ((proj (nth ys j)) = (proj (nth xs j))))) /\ forall (j:Z),
  (i <  j)%Z -> ((j <  (length xs))%Z -> ((proj (nth ys
  (j - 1%Z)%Z)) = (proj (nth xs j))))))).
Implicit Arguments remov.

Parameter remov1: forall (qta:Type), Z -> (list qta) -> (list qta).

Implicit Arguments remov1.

Definition mapRepr (qta:Type) (qta1:Type)(map1:(map qta1 qta)) (domain:(list
  qta1)) (range:(list qta)): Prop := ((length domain) = (length range)) /\
  ((noDups domain) /\ ((forall (x:qta1), (in_dom_map x map1) <-> (mem x
  domain)) /\ forall (i:Z), (0%Z <= i)%Z -> ((i <  (length domain))%Z ->
  ((get_map map1 (proj (nth domain i))) = (proj (nth range i)))))).
Implicit Arguments mapRepr.

Definition injRepr (qtb:Type) (qta:Type)(map1:(map qta qtb)) (domain:(list
  qta)) (range:(list qtb)): Prop := (mapRepr map1 domain range) /\
  (noDups range).
Implicit Arguments injRepr.

Parameter attribute : Type.

Parameter attributeCard: Z.


Parameter exAttr: attribute.


Parameter payloadLen: Z.


Parameter xor_bs_payloadLen: bitstring_payloadLen -> bitstring_payloadLen ->
  bitstring_payloadLen.


Parameter bs0_payloadLen: bitstring_payloadLen.


Definition payload  := bitstring_payloadLen.

Parameter numAttrs: Z.


Definition indexConcreteValid(n:Z): Prop := (0%Z <= n)%Z /\
  (n <  numAttrs)%Z.

Parameter index : Type.

Parameter indexProject: index -> Z.


Parameter indexInject: Z -> index.


Parameter exAttrList: (list attribute).


Definition recordConcrete  := ((list attribute)* bitstring_payloadLen)%type.

Definition recordConcreteValid(rec:((list attribute)*
  bitstring_payloadLen)%type): Prop := ((length (fst rec)) = numAttrs).

Parameter record : Type.

Parameter recordProject: record -> ((list attribute)*
  bitstring_payloadLen)%type.


Parameter recordInject: ((list attribute)* bitstring_payloadLen)%type ->
  record.


Definition attrListOfRecord(rec:record): (list attribute) :=
  (fst (recordProject rec)).

Definition payloadOfRecord(rec:record): bitstring_payloadLen :=
  (snd (recordProject rec)).

Definition nthRecord(rec:record) (i:index): attribute :=
  (proj (nth (attrListOfRecord rec) (indexProject i))).

Definition db_concrete  := (list record).

Parameter db : Type.

Parameter dbProject: db -> (list record).


Parameter dbInject: (list record) -> db.


Definition query  := (index* attribute)%type.

Definition queryExecution(db1:db) (qry:(index* attribute)%type)
  (dbqt:db): Prop := let i := (fst qry) in let attr := (snd qry) in
  ((forall (rec:record), (mem rec (dbProject db1)) -> (((nthRecord rec
  i) = attr) -> (mem rec (dbProject dbqt)))) /\ forall (rec:record), (mem rec
  (dbProject dbqt)) -> ((mem rec (dbProject db1)) /\ ((nthRecord rec
  i) = attr))).

Parameter ord: Z.


Parameter mod_int: Z -> Z -> Z.


Parameter group : Type.

Parameter id: group.


Parameter gen: group.


Parameter groupMult: group -> group -> group.


Parameter groupPow: group -> Z -> group.


Parameter symmKeyLen: Z.


Parameter xor_bs_symmKeyLen: bitstring_symmKeyLen -> bitstring_symmKeyLen ->
  bitstring_symmKeyLen.


Parameter bs0_symmKeyLen: bitstring_symmKeyLen.


Definition symm_key  := bitstring_symmKeyLen.

Parameter symm_cipher : Type.

Definition symm_plain  := record.

Parameter bsshould_not_be_usedslsl_symmKeyGen: bitstring_symmKeyLen -> R.


Parameter bsshould_not_be_usedslsl_symmEncrypt: symm_cipher
  -> bitstring_symmKeyLen -> record -> R.


Parameter symmDecrypt: bitstring_symmKeyLen -> symm_cipher -> record.


Definition hash_group_oracle_state  := (map (index* attribute)%type Z).

Definition counterConcreteValid(n:Z): Prop := (0%Z <= n)%Z /\
  (n <= ((power attributeCard numAttrs) * (power 2%Z payloadLen))%Z)%Z.

Parameter counter : Type.

Parameter counterProject: counter -> Z.


Parameter counterInject: Z -> counter.


Definition annot_group  := (group* counter)%type.

Parameter hashTagLen: Z.


Parameter xor_bs_hashTagLen: bitstring_hashTagLen -> bitstring_hashTagLen ->
  bitstring_hashTagLen.


Parameter bs0_hashTagLen: bitstring_hashTagLen.


Definition hash_tag  := bitstring_hashTagLen.

Parameter hashDataLen: Z.


Parameter xor_bs_hashDataLen: bitstring_hashDataLen
  -> bitstring_hashDataLen -> bitstring_hashDataLen.


Parameter bs0_hashDataLen: bitstring_hashDataLen.


Definition hash_data  := bitstring_hashDataLen.

Parameter pad: bitstring_symmKeyLen -> bitstring_hashDataLen.


Parameter unpad: bitstring_hashDataLen -> bitstring_symmKeyLen.


Definition hash_tag_oracle_state  := (map (group* counter)%type
  bitstring_hashTagLen).

Definition hash_data_oracle_state  := (map (group* counter)%type
  bitstring_hashDataLen).

Parameter getDistinctHashTag: (list bitstring_hashTagLen) -> Z ->
  bitstring_hashTagLen.


Parameter getDistinctHashData: (list bitstring_hashDataLen) -> Z ->
  bitstring_hashDataLen.


Definition groupExps(ns:(list Z)): Prop := forall (i:Z), (0%Z <= i)%Z ->
  ((i <  (length ns))%Z -> let n := (proj (nth ns i)) in ((0%Z <= n)%Z /\
  (n <  ord)%Z)).

Parameter getDistinctHashGroup: (list Z) -> Z -> Z.


Definition table  := (list (bitstring_hashTagLen* bitstring_hashDataLen*
  nat)%type).

Definition files  := (map nat symm_cipher).

Definition edb_concrete  := ((list (bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type)* (map nat symm_cipher))%type.

Definition edbConcreteValid(edbc:((list (bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type)* (map nat symm_cipher))%type): Prop :=
  let table1 := (fst edbc) in let files1 := (snd edbc) in ((noDups table1) /\
  ((forall (ht:bitstring_hashTagLen) (hd1:bitstring_hashDataLen) (n:nat),
  (mem (ht, hd1, n) table1) -> (in_dom_map n files1)) /\ forall (n:nat),
  (in_dom_map n files1) -> exists ht:bitstring_hashTagLen,
  exists hd1:bitstring_hashDataLen, (mem (ht, hd1, n) table1))).

Parameter edb : Type.

Parameter edbProject: edb -> ((list (bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type)* (map nat symm_cipher))%type.


Parameter edbInject: ((list (bitstring_hashTagLen* bitstring_hashDataLen*
  nat)%type)* (map nat symm_cipher))%type -> edb.


Definition tableOfEDB(edb1:edb): (list (bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type) := (fst (edbProject edb1)).

Definition filesOfEDB(edb1:edb): (map nat symm_cipher) :=
  (snd (edbProject edb1)).

Definition makeEDB(table1:(list (bitstring_hashTagLen* bitstring_hashDataLen*
  nat)%type)) (files1:(map nat symm_cipher)): edb := (edbInject (table1,
  files1)).

Definition pub_vals  := group.

Definition server_tau  := Z.

Definition ib_tau  := edb.

Definition ib_query_resp  := (bitstring_hashDataLen* symm_cipher)%type.

Definition client_tau0  := (group* Z)%type.

Definition client_tau1  := (group* counter)%type.

Definition client_tau_2  := (group* counter)%type.

Definition view_inner_element  := (bitstring_hashTagLen* (list
  (bitstring_hashDataLen* symm_cipher)%type)* edb)%type.

Definition view_outer_element  := (list (bitstring_hashTagLen* (list
  (bitstring_hashDataLen* symm_cipher)%type)* edb)%type).

Definition view  := (group* edb* (list (list (bitstring_hashTagLen* (list
  (bitstring_hashDataLen* symm_cipher)%type)* edb)%type)))%type.

Definition consistTabEntHash(tabEnt:(bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type) (hashTagOracleState:(map (group*
  counter)%type bitstring_hashTagLen)) (hashDataOracleState:(map (group*
  counter)%type bitstring_hashDataLen)): Prop := exists ag:(group*
  counter)%type, (in_dom_map ag hashTagOracleState) /\
  (((get_map hashTagOracleState ag) = (pi3_1 tabEnt)) /\ (in_dom_map ag
  hashDataOracleState)).

Definition IB6_IB7_Queries_First(qrys:(list (index* attribute)%type))
  (hashGroupOtherOracleState1:(map (index* attribute)%type Z))
  (hashGroupOtherOracleState2:(map (index* attribute)%type Z)) (i:Z): Prop :=
  (0%Z <= i)%Z /\ ((i <= (length qrys))%Z /\ ((forall (q:(index*
  attribute)%type), (in_dom_map q hashGroupOtherOracleState1) ->
  (in_dom_map q hashGroupOtherOracleState2)) /\ ((forall (q:(index*
  attribute)%type), (in_dom_map q hashGroupOtherOracleState1) ->
  ((get_map hashGroupOtherOracleState1
  q) = (get_map hashGroupOtherOracleState2 q))) /\ forall (q:(index*
  attribute)%type), (in_dom_map q hashGroupOtherOracleState2) ->
  ((in_dom_map q hashGroupOtherOracleState1) \/ exists j:Z, (0%Z <= j)%Z /\
  ((j <  i)%Z /\ (q = (proj (nth qrys j)))))))).

Definition IB6_IB7_Queries_Second(qrys:(list (index* attribute)%type))
  (hashGroupOtherOracleState1:(map (index* attribute)%type Z))
  (hashGroupOtherOracleState2:(map (index* attribute)%type Z)) (i:Z): Prop :=
  (0%Z <= i)%Z /\ ((i <= (length qrys))%Z /\ ((forall (q:(index*
  attribute)%type), (in_dom_map q hashGroupOtherOracleState1) ->
  (in_dom_map q hashGroupOtherOracleState2)) /\ ((forall (q:(index*
  attribute)%type), (in_dom_map q hashGroupOtherOracleState1) ->
  ((get_map hashGroupOtherOracleState1
  q) = (get_map hashGroupOtherOracleState2 q))) /\ forall (q:(index*
  attribute)%type), (in_dom_map q hashGroupOtherOracleState2) ->
  ((in_dom_map q hashGroupOtherOracleState1) \/ exists j:Z, (i <= j)%Z /\
  ((j <  (length qrys))%Z /\ (q = (proj (nth qrys j)))))))).

Definition IB6_IB7_QueryTags_First(qrys:(list (index* attribute)%type))
  (qrysTags:(list (list bitstring_hashTagLen))) (qryTags:(list
  bitstring_hashTagLen)) (qryTagsDone:bool) (table1:(list
  (bitstring_hashTagLen* bitstring_hashDataLen* nat)%type))
  (hashGroupOtherOracleState1:(map (index* attribute)%type Z))
  (hashGroupOtherOracleState2:(map (index* attribute)%type Z))
  (hashTagOracleState1:(map (group* counter)%type bitstring_hashTagLen))
  (hashTagOracleState2:(map (group* counter)%type
  bitstring_hashTagLen)): Prop := ((qryTagsDone = true) ->
  ~ (qryTags = (Nil:(list bitstring_hashTagLen)))) /\ (((qryTags = (Nil:(list
  bitstring_hashTagLen))) -> ((length qrysTags) <= (length qrys))%Z) /\
  (((~ (qryTags = (Nil:(list bitstring_hashTagLen)))) ->
  (((length qrysTags) + 1%Z)%Z <= (length qrys))%Z) /\ ((forall (ag:(group*
  counter)%type), (in_dom_map ag hashTagOracleState1) -> (in_dom_map ag
  hashTagOracleState2)) /\ ((forall (ag:(group* counter)%type),
  (in_dom_map ag hashTagOracleState1) -> ((get_map hashTagOracleState1
  ag) = (get_map hashTagOracleState2 ag))) /\ ((forall (ag:(group*
  counter)%type), (in_dom_map ag hashTagOracleState2) -> ((in_dom_map ag
  hashTagOracleState1) \/ ((exists i:Z, (exists j:Z, (0%Z <= i)%Z /\
  ((i <  (length qrysTags))%Z /\ ((0%Z <= j)%Z /\
  ((j <  (length (proj (nth qrysTags i))))%Z /\ (ag = ((groupPow gen
  (get_map hashGroupOtherOracleState2 (proj (nth qrys i)))),
  (counterInject j)))))))) \/ exists j:Z, (0%Z <= j)%Z /\
  ((j <  (length qryTags))%Z /\ (ag = ((groupPow gen
  (get_map hashGroupOtherOracleState2 (proj (nth qrys (length qrysTags))))),
  (counterInject j))))))) /\ ((forall (i:Z), (0%Z <= i)%Z ->
  ((i <  (length qrysTags))%Z -> forall (j:Z), (0%Z <= j)%Z ->
  ((j <  (length (proj (nth qrysTags i))))%Z -> ((get_map hashTagOracleState2
  ((groupPow gen (get_map hashGroupOtherOracleState2 (proj (nth qrys i)))),
  (counterInject j))) = (proj (nth (proj (nth qrysTags i)) j)))))) /\
  ((forall (i:Z), (0%Z <= i)%Z -> ((i <  (length qrysTags))%Z ->
  ((1%Z <= (length (proj (nth qrysTags i))))%Z /\ ((forall (j:Z),
  (0%Z <= j)%Z -> ((j <  ((length (proj (nth qrysTags i))) - 1%Z)%Z)%Z ->
  exists k:Z, (0%Z <= k)%Z /\ ((k <  (length table1))%Z /\
  ((pi3_1 (proj (nth table1 k))) = (proj (nth (proj (nth qrysTags i))
  j)))))) /\ let j := ((length (proj (nth qrysTags i))) - 1%Z)%Z in
  ((j = ((power attributeCard numAttrs) * (power 2%Z payloadLen))%Z) \/
  ~ exists k:Z, (0%Z <= k)%Z /\ ((k <  (length table1))%Z /\
  ((pi3_1 (proj (nth table1 k))) = (proj (nth (proj (nth qrysTags i))
  j))))))))) /\ ((forall (j:Z), (0%Z <= j)%Z -> ((j <  (length qryTags))%Z ->
  ((get_map hashTagOracleState2 ((groupPow gen
  (get_map hashGroupOtherOracleState2 (proj (nth qrys (length qrysTags))))),
  (counterInject j))) = (proj (nth qryTags j))))) /\
  (((~ (qryTagsDone = true)) -> forall (j:Z), (0%Z <= j)%Z ->
  ((j <  (length qryTags))%Z -> exists k:Z, (0%Z <= k)%Z /\
  ((k <  (length table1))%Z /\ ((pi3_1 (proj (nth table1
  k))) = (proj (nth qryTags j)))))) /\ ((qryTagsDone = true) ->
  ((1%Z <= (length qryTags))%Z /\ ((forall (j:Z), (0%Z <= j)%Z ->
  ((j <  ((length qryTags) - 1%Z)%Z)%Z -> exists k:Z, (0%Z <= k)%Z /\
  ((k <  (length table1))%Z /\ ((pi3_1 (proj (nth table1
  k))) = (proj (nth qryTags j)))))) /\ let j := ((length qryTags) - 1%Z)%Z in
  ((j = ((power attributeCard numAttrs) * (power 2%Z payloadLen))%Z) \/
  ~ exists k:Z, (0%Z <= k)%Z /\ ((k <  (length table1))%Z /\
  ((pi3_1 (proj (nth table1 k))) = (proj (nth qryTags j))))))))))))))))).

Definition IB6_IB7_QueryTags_Second(qrys:(list (index* attribute)%type))
  (qrysTags:(list (list bitstring_hashTagLen))) (table1:(list
  (bitstring_hashTagLen* bitstring_hashDataLen* nat)%type))
  (hashGroupOtherOracleState1:(map (index* attribute)%type Z))
  (hashGroupOtherOracleState2:(map (index* attribute)%type Z))
  (hashTagOracleState1:(map (group* counter)%type bitstring_hashTagLen))
  (hashTagOracleState2:(map (group* counter)%type bitstring_hashTagLen))
  (i:Z) (j:Z): Prop := ((length qrys) = (length qrysTags)) /\
  ((0%Z <= i)%Z /\ ((i <= (length qrysTags))%Z /\
  (((i <  (length qrysTags))%Z -> ((0%Z <= j)%Z /\
  (j <  (length (proj (nth qrysTags i))))%Z)) /\ ((forall (ag:(group*
  counter)%type), (in_dom_map ag hashTagOracleState1) -> (in_dom_map ag
  hashTagOracleState2)) /\ ((forall (ag:(group* counter)%type),
  (in_dom_map ag hashTagOracleState1) -> ((get_map hashTagOracleState1
  ag) = (get_map hashTagOracleState2 ag))) /\ ((forall (ag:(group*
  counter)%type), (in_dom_map ag hashTagOracleState2) -> ((in_dom_map ag
  hashTagOracleState1) \/ (((i <  (length qrysTags))%Z /\ exists jqt:Z,
  (j <= jqt)%Z /\ ((jqt <  (length (proj (nth qrysTags i))))%Z /\ (ag = (
  (groupPow gen (get_map hashGroupOtherOracleState2 (proj (nth qrys i)))),
  (counterInject jqt))))) \/ exists iqt:Z, exists jqt:Z, (i <  iqt)%Z /\
  ((iqt <  (length qrysTags))%Z /\ ((0%Z <= jqt)%Z /\
  ((jqt <= (length (proj (nth qrysTags iqt))))%Z /\ (ag = ((groupPow gen
  (get_map hashGroupOtherOracleState2 (proj (nth qrys iqt)))),
  (counterInject jqt))))))))) /\ ((forall (i1:Z), (0%Z <= i1)%Z ->
  ((i1 <  (length qrysTags))%Z -> forall (j1:Z), (0%Z <= j1)%Z ->
  ((j1 <  (length (proj (nth qrysTags i1))))%Z ->
  ((get_map hashTagOracleState2 ((groupPow gen
  (get_map hashGroupOtherOracleState2 (proj (nth qrys i1)))),
  (counterInject j1))) = (proj (nth (proj (nth qrysTags i1)) j1)))))) /\
  forall (i1:Z), (0%Z <= i1)%Z -> ((i1 <  (length qrysTags))%Z ->
  ((1%Z <= (length (proj (nth qrysTags i1))))%Z /\ ((forall (j1:Z),
  (0%Z <= j1)%Z -> ((j1 <  ((length (proj (nth qrysTags i1))) - 1%Z)%Z)%Z ->
  exists k:Z, (0%Z <= k)%Z /\ ((k <  (length table1))%Z /\
  ((pi3_1 (proj (nth table1 k))) = (proj (nth (proj (nth qrysTags i1))
  j1)))))) /\ let j1 := ((length (proj (nth qrysTags i1))) - 1%Z)%Z in
  ((j1 = ((power attributeCard numAttrs) * (power 2%Z payloadLen))%Z) \/
  ~ exists k:Z, (0%Z <= k)%Z /\ ((k <  (length table1))%Z /\
  ((pi3_1 (proj (nth table1 k))) = (proj (nth (proj (nth qrysTags i1))
  j1))))))))))))))).

Axiom Some_inj : forall (qta:Type), forall (x:qta) (y:qta),
  ((Some x) = (Some y)) -> (x = y).

Axiom Proj_Some : forall (qta:Type), forall (x:qta), ((proj (Some x)) = x).

Axiom Proj_eq : forall (qta:Type), forall (o1:(option qta)) (o2:(option
  qta)), (~ (o1 = (None:(option qta)))) -> ((~ (o2 = (None:(option qta)))) ->
  (((proj o1) = (proj o2)) -> (o1 = o2))).

Axiom Some_or_None : forall (qta:Type), forall (o:(option qta)),
  (o = (None:(option qta))) \/ exists x:qta, (o = (Some x)).

Axiom head_def : forall (qta:Type), forall (a:qta) (l:(list qta)),
  ((hd (Cons a l)) = a).

Axiom tail_def : forall (qta:Type), forall (a:qta) (l:(list qta)),
  ((tl (Cons a l)) = l).

Axiom get_upd_map_same : forall (qtb:Type) (qta:Type), forall (m:(map qta
  qtb)) (a1:qta) (a2:qta) (b:qtb), (a1 = a2) -> ((get_map (upd_map m a1 b)
  a2) = b).

Axiom get_upd_map_diff : forall (qtb:Type) (qta:Type), forall (m:(map qta
  qtb)) (a1:qta) (a2:qta) (b:qtb), (~ (a1 = a2)) -> ((get_map (upd_map m a1
  b) a2) = (get_map m a2)).

Axiom upd_map_comm : forall (qtb:Type) (qta:Type), forall (m:(map qta qtb))
  (a:qta) (aqt:qta) (b:qtb) (bqt:qtb), (~ (a = aqt)) -> ((upd_map (upd_map m
  a b) aqt bqt) = (upd_map (upd_map m aqt bqt) a b)).

Axiom upd_in_dom_same : forall (qtb:Type) (qta:Type), forall (m:(map qta
  qtb)) (a:qta) (aqt:qta) (b:qtb), (a = aqt) -> (in_dom_map aqt (upd_map m a
  b)).

Axiom upd_in_dom_diff : forall (qtb:Type) (qta:Type), forall (m:(map qta
  qtb)) (a:qta) (aqt:qta) (b:qtb), (~ (a = aqt)) -> ((in_dom_map aqt
  (upd_map m a b)) <-> (in_dom_map aqt m)).

Axiom upd_in_rng_same : forall (qtb:Type) (qta:Type), forall (m:(map qta
  qtb)) (a:qta) (b:qtb) (bqt:qtb), (b = bqt) -> (in_rng_map bqt (upd_map m a
  b)).

Axiom upd_in_rng_diff : forall (qtb:Type) (qta:Type), forall (m:(map qta
  qtb)) (a:qta) (b:qtb) (bqt:qtb), (~ (b = bqt)) -> ((in_rng_map bqt
  (upd_map m a b)) <-> (in_rng_map bqt m)).

Axiom in_dom_in_rng : forall (qta:Type) (qtb:Type), forall (m:(map qta qtb))
  (a:qta), (in_dom_map a m) -> (in_rng_map (get_map m a) m).

Axiom in_rng_in_dom : forall (qtb:Type) (qta:Type), forall (m:(map qta qtb))
  (b:qtb), (in_rng_map b m) -> exists a:qta, (in_dom_map a m) /\ ((get_map m
  a) = b).

Axiom empty_in_dom : forall (qta:Type) (qtb:Type) (qtb1:Type),
  forall (a:qta), ~ (in_dom_map a (empty_map:(map qta qtb1))).

Axiom empty_in_rng : forall (qtb:Type) (qta:Type) (qta1:Type),
  forall (b:qtb), ~ (in_rng_map b (empty_map:(map qta1 qtb))).

Axiom real_of_bool_true : ((real_of_bool true) = (IZR 1%Z)).

Axiom real_of_bool_false : ((real_of_bool false) = (IZR 0%Z)).

Axiom real_of_int_le_compat : forall (x:Z) (y:Z), (x <= y)%Z ->
  ((IZR x) <= (IZR y))%R.

Axiom real_of_int_lt_compat : forall (x:Z) (y:Z), (x <  y)%Z ->
  ((IZR x) <  (IZR y))%R.

Axiom rmult_le_compat_l : forall (x:R) (y:R) (z:R), ((IZR 0%Z) <= x)%R ->
  ((y <= z)%R -> ((x * y)%R <= (x * z)%R)%R).

Axiom rmult_le_compat_r : forall (x:R) (y:R) (z:R), ((IZR 0%Z) <= z)%R ->
  ((x <= y)%R -> ((x * z)%R <= (y * z)%R)%R).

Axiom rmul_plus_distr_r : forall (x:R) (y:R) (z:R),
  (((x + y)%R * z)%R = ((x * z)%R + (y * z)%R)%R).

Axiom rdiv_le_compat : forall (x1:R) (x2:R) (y1:R) (y2:R),
  ((IZR 0%Z) <  y2)%R -> ((y2 <= y1)%R -> (((IZR 0%Z) <= x1)%R ->
  ((x1 <= x2)%R -> ((Rdiv x1 y1)%R <= (Rdiv x2 y2)%R)%R))).

Axiom rdiv_0_le : forall (x:R) (y:R), ((IZR 0%Z) <  y)%R ->
  (((IZR 0%Z) <= x)%R -> ((IZR 0%Z) <= (Rdiv x y)%R)%R).

Axiom pow2_pos : forall (n:Z), (0%Z <= n)%Z -> (0%Z <  (power 2%Z n))%Z.

Axiom ExNatConcreteValid : (0%Z <= 0%Z)%Z.

Axiom NatProjectInject : forall (n:nat), ((natInject (natProject n)) = n).

Axiom NatInjectProjectGood : forall (n:Z), (0%Z <= n)%Z ->
  ((natProject (natInject n)) = n).

Axiom NatInjectProjectBad : forall (n:Z), (~ (0%Z <= n)%Z) ->
  ((natProject (natInject n)) = 0%Z).

Axiom NatProjectValid : forall (n:nat), (0%Z <= (natProject n))%Z.

Axiom LengthEmpty : forall (qta:Type), ((length (Nil:(list qta))) = 0%Z).

Axiom LengthNonEmpty : forall (qta:Type), forall (x:qta) (xs:(list qta)),
  ((length (Cons x xs)) = ((length xs) + 1%Z)%Z).

Axiom NthZero : forall (qta:Type), forall (x:qta) (ls:(list qta)),
  ((nth (Cons x ls) 0%Z) = (Some x)).

Axiom NthNonZero : forall (qta:Type), forall (i:Z) (x:qta) (ls:(list qta)),
  (0%Z <  i)%Z -> ((i <  (length ls))%Z -> ((nth (Cons x ls) i) = (nth ls
  (i - 1%Z)%Z))).

Axiom NthGood : forall (qta:Type), forall (i:Z) (ls:(list qta)),
  (0%Z <= i)%Z -> ((i <  (length ls))%Z -> exists x:qta, ((nth ls
  i) = (Some x))).

Axiom NthGoodqt : forall (qta:Type), forall (i:Z) (ls:(list qta)),
  (0%Z <= i)%Z -> ((i <  (length ls))%Z -> ~ ((nth ls i) = (None:(option
  qta)))).

Axiom NthBad : forall (qta:Type), forall (i:Z) (ls:(list qta)),
  ((i <  0%Z)%Z \/ ((length ls) <= i)%Z) -> ((nth ls i) = (None:(option
  qta))).

Axiom NthMem : forall (qta:Type), forall (ls:(list qta)) (i:Z),
  (0%Z <= i)%Z -> ((i <  (length ls))%Z -> (mem (proj (nth ls i)) ls)).

Axiom Unique : forall (qta:Type), forall (xs:(list qta)), (unique xs
  (unique1 xs)).

Axiom NoDups1 : forall (qta:Type), forall (x:qta) (ys:(list qta)),
  (noDups ys) -> ((~ (mem x ys)) -> (noDups (Cons x ys))).

Axiom NoDups2 : forall (qta:Type), forall (x:qta) (ys:(list qta)), (mem x
  ys) -> ~ (noDups (Cons x ys)).

Axiom NoDups3 : forall (qta:Type), forall (x:qta) (ys:(list qta)),
  (noDups (Cons x ys)) -> (noDups ys).

Axiom FromTo : forall (i:Z) (j:Z), (fromTo i j (fromTo1 i j)).

Axiom Remov1 : forall (qta:Type), forall (i:Z) (xs:(list qta)),
  (((i <  0%Z)%Z \/ ((length xs) <  i)%Z) -> ((remov1 i xs) = (Nil:(list
  qta)))) /\ ((0%Z <= i)%Z -> ((i <  (length xs))%Z -> (remov i xs (remov1 i
  xs)))).

Axiom Remov2 : forall (qta:Type), forall (i:Z) (xs:(list qta)) (y:qta),
  (mem y (remov1 i xs)) -> (mem y xs).

Axiom MapRepr1 : forall (qtb:Type) (qta:Type), (mapRepr (empty_map:(map qta
  qtb)) (Nil:(list qta)) (Nil:(list qtb))).

Axiom MapRepr2 : forall (qtb:Type) (qta:Type), forall (map1:(map qta qtb))
  (domain:(list qta)) (range:(list qtb)) (x:qta) (y:qtb), (mapRepr map1
  domain range) -> ((~ (in_dom_map x map1)) -> (mapRepr (upd_map map1 x y)
  (Cons x domain) (Cons y range))).

Axiom MapRepr3 : forall (qtb:Type) (qta:Type), forall (map1:(map qta qtb))
  (domain:(list qta)) (range:(list qtb)), (mapRepr map1 domain range) ->
  forall (x:qtb), (in_rng_map x map1) <-> (mem x range).

Axiom InjRepr1 : forall (qtb:Type) (qta:Type), (injRepr (empty_map:(map qta
  qtb)) (Nil:(list qta)) (Nil:(list qtb))).

Axiom InjRepr2 : forall (qtb:Type) (qta:Type), forall (map1:(map qta qtb))
  (domain:(list qta)) (range:(list qtb)) (x:qta) (y:qtb), (injRepr map1
  domain range) -> ((~ (in_dom_map x map1)) -> ((~ (in_rng_map y map1)) ->
  (injRepr (upd_map map1 x y) (Cons x domain) (Cons y range)))).

Axiom InjRepr3 : forall (qtb:Type) (qta:Type), forall (map1:(map qta qtb))
  (domain:(list qta)) (range:(list qtb)), (injRepr map1 domain range) ->
  forall (x:qtb), (in_rng_map x map1) <-> (mem x range).

Axiom InjRepr4 : forall (qtb:Type) (qta:Type), forall (map1:(map qta qtb))
  (domain:(list qta)) (range:(list qtb)) (x1:qta) (x2:qta), (injRepr map1
  domain range) -> ((in_dom_map x1 map1) -> ((in_dom_map x2 map1) ->
  (((get_map map1 x2) = (get_map map1 x1)) -> (x1 = x2)))).

Axiom AttributeCard : (1%Z <= attributeCard)%Z.

Axiom xor_payloadLen_comm : forall (x:bitstring_payloadLen)
  (y:bitstring_payloadLen), ((xor_bs_payloadLen x y) = (xor_bs_payloadLen y
  x)).

Axiom xor_payloadLen_assoc : forall (x:bitstring_payloadLen)
  (y:bitstring_payloadLen) (z:bitstring_payloadLen),
  ((xor_bs_payloadLen (xor_bs_payloadLen x y) z) = (xor_bs_payloadLen x
  (xor_bs_payloadLen y z))).

Axiom xor_payloadLen_zero_r : forall (x:bitstring_payloadLen),
  ((xor_bs_payloadLen x bs0_payloadLen) = x).

Axiom xor_payloadLen_cancel : forall (x:bitstring_payloadLen),
  ((xor_bs_payloadLen x x) = bs0_payloadLen).

Axiom NumAttrs : (1%Z <= numAttrs)%Z.

Axiom ExIndexConcreteValid : (indexConcreteValid 0%Z).

Axiom IndexProjectInject : forall (n:index),
  ((indexInject (indexProject n)) = n).

Axiom IndexInjectProjectGood : forall (n:Z), (indexConcreteValid n) ->
  ((indexProject (indexInject n)) = n).

Axiom IndexInjectProjectBad : forall (n:Z), (~ (indexConcreteValid n)) ->
  ((indexProject (indexInject n)) = 0%Z).

Axiom IndexProjectValid : forall (n:index),
  (indexConcreteValid (indexProject n)).

Axiom ExAttrList : ((length exAttrList) = numAttrs) /\ forall (i:Z),
  (0%Z <= i)%Z -> ((i <  numAttrs)%Z -> ((proj (nth exAttrList
  i)) = exAttr)).

Axiom ExRecConcValid : (recordConcreteValid (exAttrList, bs0_payloadLen)).

Axiom RecordCard : (1%Z <= ((power attributeCard numAttrs) * (power 2%Z
  payloadLen))%Z)%Z.

Axiom RecordProjectInject : forall (rec:record),
  ((recordInject (recordProject rec)) = rec).

Axiom RecordInjectProjectGood : forall (conc:((list attribute)*
  bitstring_payloadLen)%type), (recordConcreteValid conc) ->
  ((recordProject (recordInject conc)) = conc).

Axiom RecordInjectProjectBad : forall (conc:((list attribute)*
  bitstring_payloadLen)%type), (~ (recordConcreteValid conc)) ->
  ((recordProject (recordInject conc)) = (exAttrList, bs0_payloadLen)).

Axiom RecordProjectValid : forall (rec:record),
  (recordConcreteValid (recordProject rec)).

Axiom ExDBConc : (noDups (Nil:(list record))).

Axiom DBProjectInject : forall (db1:db), ((dbInject (dbProject db1)) = db1).

Axiom DBInjectProjectGood : forall (conc:(list record)), (noDups conc) ->
  ((dbProject (dbInject conc)) = conc).

Axiom dbInjectProjectBad : forall (conc:(list record)), (~ (noDups conc)) ->
  ((dbProject (dbInject conc)) = (Nil:(list record))).

Axiom DBProjectValid : forall (db1:db), (noDups (dbProject db1)).

Axiom QueryCard : forall (qrys:(list (index* attribute)%type)),
  (noDups qrys) -> ((length qrys) <= (numAttrs * attributeCard)%Z)%Z.

Axiom OrderPos : (1%Z <= ord)%Z.

Axiom ModSmall : forall (x:Z), (0%Z <= x)%Z -> ((x <  ord)%Z -> ((mod_int x
  ord) = x)).

Axiom ModBound : forall (x:Z), (0%Z <= (mod_int x ord))%Z /\ ((mod_int x
  ord) <  ord)%Z.

Axiom ModAdd : forall (x:Z) (y:Z), ((mod_int ((mod_int x ord) + y)%Z
  ord) = (mod_int (x + y)%Z ord)).

Axiom ModSub : forall (x:Z) (y:Z), ((mod_int ((mod_int x ord) - y)%Z
  ord) = (mod_int (x - y)%Z ord)).

Axiom ModTimes : forall (x:Z) (y:Z), ((mod_int ((mod_int x ord) * y)%Z
  ord) = (mod_int (x * y)%Z ord)).

Axiom GroupAssoc : forall (x:group) (y:group) (z:group), ((groupMult x
  (groupMult y z)) = (groupMult (groupMult x y) z)).

Axiom GroupIdentityRight : forall (x:group), ((groupMult x id) = x).

Axiom GroupIdentityLeft : forall (x:group), ((groupMult id x) = x).

Axiom GroupPowMod : forall (x:group) (n:Z), ((groupPow x n) = (groupPow x
  (mod_int n ord))).

Axiom GroupPowId : forall (x:group), ((groupPow x 0%Z) = id).

Axiom GroupPlusInPower : forall (x:group) (n:Z) (m:Z), ((groupPow x
  (n + m)%Z) = (groupMult (groupPow x n) (groupPow x m))).

Axiom GroupLeftNestedPower : forall (x:group) (n:Z) (m:Z),
  ((groupPow (groupPow x n) m) = (groupPow x (n * m)%Z)).

Axiom GroupTimesInPower : forall (x:group) (y:group) (n:Z),
  ((groupPow (groupMult x y) n) = (groupMult (groupPow x n) (groupPow y n))).

Axiom SymmKeyLen : (0%Z <= symmKeyLen)%Z.

Axiom xor_symmKeyLen_comm : forall (x:bitstring_symmKeyLen)
  (y:bitstring_symmKeyLen), ((xor_bs_symmKeyLen x y) = (xor_bs_symmKeyLen y
  x)).

Axiom xor_symmKeyLen_assoc : forall (x:bitstring_symmKeyLen)
  (y:bitstring_symmKeyLen) (z:bitstring_symmKeyLen),
  ((xor_bs_symmKeyLen (xor_bs_symmKeyLen x y) z) = (xor_bs_symmKeyLen x
  (xor_bs_symmKeyLen y z))).

Axiom xor_symmKeyLen_zero_r : forall (x:bitstring_symmKeyLen),
  ((xor_bs_symmKeyLen x bs0_symmKeyLen) = x).

Axiom xor_symmKeyLen_cancel : forall (x:bitstring_symmKeyLen),
  ((xor_bs_symmKeyLen x x) = bs0_symmKeyLen).

Axiom QueryOrd : ((numAttrs * attributeCard)%Z <= ord)%Z.

Axiom ExCounterConcreteValid : (counterConcreteValid 0%Z).

Axiom CounterProjectInject : forall (n:counter),
  ((counterInject (counterProject n)) = n).

Axiom CounterInjectProjectGood : forall (n:Z), (counterConcreteValid n) ->
  ((counterProject (counterInject n)) = n).

Axiom CounterInjectProjectBad : forall (n:Z), (~ (counterConcreteValid n)) ->
  ((counterProject (counterInject n)) = 0%Z).

Axiom CounterProjectValid : forall (n:counter),
  (counterConcreteValid (counterProject n)).

Axiom AnnotGroupCardPos : (1%Z <= (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z.

Axiom AnnotGroupCard : forall (xs:(list (group* counter)%type)),
  (noDups xs) -> ((length xs) <= (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z.

Axiom xor_hashTagLen_comm : forall (x:bitstring_hashTagLen)
  (y:bitstring_hashTagLen), ((xor_bs_hashTagLen x y) = (xor_bs_hashTagLen y
  x)).

Axiom xor_hashTagLen_assoc : forall (x:bitstring_hashTagLen)
  (y:bitstring_hashTagLen) (z:bitstring_hashTagLen),
  ((xor_bs_hashTagLen (xor_bs_hashTagLen x y) z) = (xor_bs_hashTagLen x
  (xor_bs_hashTagLen y z))).

Axiom xor_hashTagLen_zero_r : forall (x:bitstring_hashTagLen),
  ((xor_bs_hashTagLen x bs0_hashTagLen) = x).

Axiom xor_hashTagLen_cancel : forall (x:bitstring_hashTagLen),
  ((xor_bs_hashTagLen x x) = bs0_hashTagLen).

Axiom HashTagLen1 : (0%Z <= hashTagLen)%Z.

Axiom HashTagLen2 : ((ord * (((power attributeCard numAttrs) * (power 2%Z
  payloadLen))%Z + 1%Z)%Z)%Z <= (power 2%Z hashTagLen))%Z.

Axiom xor_hashDataLen_comm : forall (x:bitstring_hashDataLen)
  (y:bitstring_hashDataLen), ((xor_bs_hashDataLen x
  y) = (xor_bs_hashDataLen y x)).

Axiom xor_hashDataLen_assoc : forall (x:bitstring_hashDataLen)
  (y:bitstring_hashDataLen) (z:bitstring_hashDataLen),
  ((xor_bs_hashDataLen (xor_bs_hashDataLen x y) z) = (xor_bs_hashDataLen x
  (xor_bs_hashDataLen y z))).

Axiom xor_hashDataLen_zero_r : forall (x:bitstring_hashDataLen),
  ((xor_bs_hashDataLen x bs0_hashDataLen) = x).

Axiom xor_hashDataLen_cancel : forall (x:bitstring_hashDataLen),
  ((xor_bs_hashDataLen x x) = bs0_hashDataLen).

Axiom HashDataLen1 : (symmKeyLen <= hashDataLen)%Z.

Axiom HashDataLen2 : ((ord * (((power attributeCard numAttrs) * (power 2%Z
  payloadLen))%Z + 1%Z)%Z)%Z <= (power 2%Z hashDataLen))%Z.

Axiom PadUnpad : forall (k:bitstring_symmKeyLen), ((unpad (pad k)) = k).

Axiom ListLengthBound : forall (qta:Type), forall (x:qta) (xs:(list qta))
  (n:Z), ((length (Cons x xs)) <= n)%Z -> ((length xs) <  n)%Z.

Axiom AnnotGroupListLengthBound : forall (xs:(list (group* counter)%type))
  (x:(group* counter)%type), ((length (Cons x
  xs)) <= (ord * (((power attributeCard numAttrs) * (power 2%Z
  payloadLen))%Z + 1%Z)%Z)%Z)%Z ->
  ((length xs) <  (ord * (((power attributeCard numAttrs) * (power 2%Z
  payloadLen))%Z + 1%Z)%Z)%Z)%Z.

Axiom QueryListLengthBound : forall (xs:(list (index* attribute)%type))
  (x:(index* attribute)%type), ((length (Cons x
  xs)) <= (numAttrs * attributeCard)%Z)%Z ->
  ((length xs) <  (numAttrs * attributeCard)%Z)%Z.

Axiom AnnotGroupNoDupsIncompleteListLengthBoundqt : forall (xs:(list (group*
  counter)%type)) (x:(group* counter)%type), (noDups xs) -> ((~ (mem x
  xs)) -> (((length (Cons x xs)) <= (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z /\
  ((length xs) <  (ord * (((power attributeCard numAttrs) * (power 2%Z
  payloadLen))%Z + 1%Z)%Z)%Z)%Z)).

Axiom QueryNoDupsIncompleteListLengthBoundqt : forall (xs:(list (index*
  attribute)%type)) (x:(index* attribute)%type), (noDups xs) -> ((~ (mem x
  xs)) -> (((length (Cons x xs)) <= (numAttrs * attributeCard)%Z)%Z /\
  ((length xs) <  (numAttrs * attributeCard)%Z)%Z)).

Axiom AnnotGroupNoDupsIncompleteListLengthBound : forall (xs:(list (group*
  counter)%type)) (x:(group* counter)%type), (noDups xs) -> ((~ (mem x
  xs)) -> ((length xs) <  (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z).

Axiom QueryNoDupsIncompleteListLengthBound : forall (xs:(list (index*
  attribute)%type)) (x:(index* attribute)%type), (noDups xs) -> ((~ (mem x
  xs)) -> ((length xs) <  (numAttrs * attributeCard)%Z)%Z).

Axiom HashTagMapReprBound : forall (hashTagOracleState:(map (group*
  counter)%type bitstring_hashTagLen)) (hashTagOracleDomain:(list (group*
  counter)%type)) (hashTagOracleRange:(list bitstring_hashTagLen)),
  (mapRepr hashTagOracleState hashTagOracleDomain hashTagOracleRange) ->
  ((length hashTagOracleRange) <= (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z.

Axiom HashTagMapReprIncompleteBoundqt : forall (hashTagOracleState:(map
  (group* counter)%type bitstring_hashTagLen)) (hashTagOracleDomain:(list
  (group* counter)%type)) (hashTagOracleRange:(list bitstring_hashTagLen))
  (ag:(group* counter)%type), (mapRepr hashTagOracleState hashTagOracleDomain
  hashTagOracleRange) -> ((~ (mem ag hashTagOracleDomain)) ->
  ((length hashTagOracleRange) <  (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z).

Axiom HashTagMapReprIncompleteBound : forall (hashTagOracleState:(map (group*
  counter)%type bitstring_hashTagLen)) (hashTagOracleDomain:(list (group*
  counter)%type)) (hashTagOracleRange:(list bitstring_hashTagLen))
  (ag:(group* counter)%type), (mapRepr hashTagOracleState hashTagOracleDomain
  hashTagOracleRange) -> ((~ (in_dom_map ag hashTagOracleState)) ->
  ((length hashTagOracleRange) <  (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z).

Axiom HashDataMapReprBound : forall (hashDataOracleState:(map (group*
  counter)%type bitstring_hashDataLen)) (hashDataOracleDomain:(list (group*
  counter)%type)) (hashDataOracleRange:(list bitstring_hashDataLen)),
  (mapRepr hashDataOracleState hashDataOracleDomain hashDataOracleRange) ->
  ((length hashDataOracleRange) <= (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z.

Axiom HashDataMapReprIncompleteBoundqt : forall (hashDataOracleState:(map
  (group* counter)%type bitstring_hashDataLen)) (hashDataOracleDomain:(list
  (group* counter)%type)) (hashDataOracleRange:(list bitstring_hashDataLen))
  (ag:(group* counter)%type), (mapRepr hashDataOracleState
  hashDataOracleDomain hashDataOracleRange) -> ((~ (mem ag
  hashDataOracleDomain)) ->
  ((length hashDataOracleRange) <  (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z).

Axiom HashDataMapReprIncompleteBound : forall (hashDataOracleState:(map
  (group* counter)%type bitstring_hashDataLen)) (hashDataOracleDomain:(list
  (group* counter)%type)) (hashDataOracleRange:(list bitstring_hashDataLen))
  (ag:(group* counter)%type), (mapRepr hashDataOracleState
  hashDataOracleDomain hashDataOracleRange) -> ((~ (in_dom_map ag
  hashDataOracleState)) ->
  ((length hashDataOracleRange) <  (ord * (((power attributeCard
  numAttrs) * (power 2%Z payloadLen))%Z + 1%Z)%Z)%Z)%Z).

Axiom HashGroupOtherMapReprBound : forall (hashGroupOtherOracleState:(map
  (index* attribute)%type Z)) (hashGroupOtherOracleDomain:(list (index*
  attribute)%type)) (hashGroupOtherOracleRange:(list Z)),
  (mapRepr hashGroupOtherOracleState hashGroupOtherOracleDomain
  hashGroupOtherOracleRange) ->
  ((length hashGroupOtherOracleRange) <= (numAttrs * attributeCard)%Z)%Z.

Axiom HashGroupOtherMapReprIncompleteBoundqt : forall (hashGroupOtherOracleState:(map
  (index* attribute)%type Z)) (hashGroupOtherOracleDomain:(list (index*
  attribute)%type)) (hashGroupOtherOracleRange:(list Z)) (q:(index*
  attribute)%type), (mapRepr hashGroupOtherOracleState
  hashGroupOtherOracleDomain hashGroupOtherOracleRange) -> ((~ (mem q
  hashGroupOtherOracleDomain)) ->
  ((length hashGroupOtherOracleRange) <  (numAttrs * attributeCard)%Z)%Z).

Axiom HashGroupOtherMapReprIncompleteBound : forall (hashGroupOtherOracleState:(map
  (index* attribute)%type Z)) (hashGroupOtherOracleDomain:(list (index*
  attribute)%type)) (hashGroupOtherOracleRange:(list Z)) (q:(index*
  attribute)%type), (mapRepr hashGroupOtherOracleState
  hashGroupOtherOracleDomain hashGroupOtherOracleRange) -> ((~ (in_dom_map q
  hashGroupOtherOracleState)) ->
  ((length hashGroupOtherOracleRange) <  (numAttrs * attributeCard)%Z)%Z).

Axiom getDistinctHashTag1 : forall (xs:(list bitstring_hashTagLen)) (i:Z),
  ((~ (noDups xs)) \/ ((i <  0%Z)%Z \/ (((power 2%Z
  hashTagLen) - (length xs))%Z <= i)%Z)) -> ((getDistinctHashTag xs
  i) = bs0_hashTagLen).

Axiom getDistinctHashTag2 : forall (xs:(list bitstring_hashTagLen)) (i:Z),
  (noDups xs) -> ((0%Z <= i)%Z -> ((i <  ((power 2%Z
  hashTagLen) - (length xs))%Z)%Z -> ~ (mem (getDistinctHashTag xs i) xs))).

Axiom getDistinctHashTag3 : forall (xs:(list bitstring_hashTagLen)) (i:Z)
  (j:Z), (noDups xs) -> ((0%Z <= i)%Z -> ((i <  ((power 2%Z
  hashTagLen) - (length xs))%Z)%Z -> ((0%Z <= j)%Z -> ((j <  ((power 2%Z
  hashTagLen) - (length xs))%Z)%Z -> (((getDistinctHashTag xs
  i) = (getDistinctHashTag xs j)) -> (i = j)))))).

Axiom getDistinctHashData1 : forall (xs:(list bitstring_hashDataLen)) (i:Z),
  ((~ (noDups xs)) \/ ((i <  0%Z)%Z \/ (((power 2%Z
  hashDataLen) - (length xs))%Z <= i)%Z)) -> ((getDistinctHashData xs
  i) = bs0_hashDataLen).

Axiom getDistinctHashData2 : forall (xs:(list bitstring_hashDataLen)) (i:Z),
  (noDups xs) -> ((0%Z <= i)%Z -> ((i <  ((power 2%Z
  hashDataLen) - (length xs))%Z)%Z -> ~ (mem (getDistinctHashData xs i)
  xs))).

Axiom getDistinctHashData3 : forall (xs:(list bitstring_hashDataLen)) (i:Z)
  (j:Z), (noDups xs) -> ((0%Z <= i)%Z -> ((i <  ((power 2%Z
  hashDataLen) - (length xs))%Z)%Z -> ((0%Z <= j)%Z -> ((j <  ((power 2%Z
  hashDataLen) - (length xs))%Z)%Z -> (((getDistinctHashData xs
  i) = (getDistinctHashData xs j)) -> (i = j)))))).

Axiom getDistinctHashGroup1 : forall (xs:(list Z)) (i:Z),
  ((~ (groupExps xs)) \/ ((noDups xs) \/ ((i <  0%Z)%Z \/
  ((ord - (length xs))%Z <= i)%Z))) -> ((getDistinctHashGroup xs i) = 0%Z).

Axiom getDistinctHashGroup2 : forall (xs:(list Z)) (i:Z), (groupExps xs) ->
  ((noDups xs) -> ((0%Z <= i)%Z -> ((i <  (ord - (length xs))%Z)%Z ->
  ~ (mem (getDistinctHashGroup xs i) xs)))).

Axiom getDistinctHashGroup3 : forall (xs:(list Z)) (i:Z) (j:Z),
  (groupExps xs) -> ((noDups xs) -> ((0%Z <= i)%Z ->
  ((i <  (ord - (length xs))%Z)%Z -> ((0%Z <= j)%Z ->
  ((j <  (ord - (length xs))%Z)%Z -> (((getDistinctHashGroup xs
  i) = (getDistinctHashGroup xs j)) -> (i = j))))))).

Axiom ExEDBConcValid : (edbConcreteValid ((Nil:(list (bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type)), (empty_map:(map nat symm_cipher)))).

Axiom EDBProjectInject : forall (edb1:edb),
  ((edbInject (edbProject edb1)) = edb1).

Axiom EDBInjectProjectGood : forall (conc:((list (bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type)* (map nat symm_cipher))%type),
  (edbConcreteValid conc) -> ((edbProject (edbInject conc)) = conc).

Axiom EDBInjectProjectBad : forall (conc:((list (bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type)* (map nat symm_cipher))%type),
  (~ (edbConcreteValid conc)) -> ((edbProject (edbInject conc)) = ((Nil:(list
  (bitstring_hashTagLen* bitstring_hashDataLen* nat)%type)), (empty_map:(map
  nat symm_cipher)))).

Axiom eDBProjectValid : forall (qry:edb),
  (edbConcreteValid (edbProject qry)).

Axiom ConsistTabEntHash1 : forall (tabEnt:(bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type) (hashTagOracleState:(map (group*
  counter)%type bitstring_hashTagLen)) (hashDataOracleState:(map (group*
  counter)%type bitstring_hashDataLen)) (ag:(group* counter)%type)
  (ht:bitstring_hashTagLen), (consistTabEntHash tabEnt hashTagOracleState
  hashDataOracleState) -> ((~ (in_dom_map ag hashTagOracleState)) ->
  (consistTabEntHash tabEnt (upd_map hashTagOracleState ag ht)
  hashDataOracleState)).

Axiom ConsistTabEntHash2 : forall (tabEnt:(bitstring_hashTagLen*
  bitstring_hashDataLen* nat)%type) (hashTagOracleState:(map (group*
  counter)%type bitstring_hashTagLen)) (hashDataOracleState:(map (group*
  counter)%type bitstring_hashDataLen)) (ag:(group* counter)%type)
  (hd1:bitstring_hashDataLen), (consistTabEntHash tabEnt hashTagOracleState
  hashDataOracleState) -> (consistTabEntHash tabEnt hashTagOracleState
  (upd_map hashDataOracleState ag hd1)).

Axiom IB6_IB7_Queries1 : forall (qrys:(list (index* attribute)%type))
  (hashGroupOtherOracleState1:(map (index* attribute)%type Z))
  (hashGroupOtherOracleState2:(map (index* attribute)%type Z)),
  (IB6_IB7_Queries_First qrys hashGroupOtherOracleState1
  hashGroupOtherOracleState2 (length qrys)) -> (IB6_IB7_Queries_Second qrys
  hashGroupOtherOracleState1 hashGroupOtherOracleState2 0%Z).

(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem IB6_IB7_QueryTags1 : forall (qrys:(list (index* attribute)%type))
  (qrysTags:(list (list bitstring_hashTagLen))) (table1:(list
  (bitstring_hashTagLen* bitstring_hashDataLen* nat)%type))
  (hashGroupOtherOracleState1:(map (index* attribute)%type Z))
  (hashGroupOtherOracleState2:(map (index* attribute)%type Z))
  (hashTagOracleState1:(map (group* counter)%type bitstring_hashTagLen))
  (hashTagOracleState2:(map (group* counter)%type bitstring_hashTagLen)),
  ((length qrys) = (length qrysTags)) -> ((IB6_IB7_QueryTags_First qrys
  qrysTags (Nil:(list bitstring_hashTagLen)) false table1
  hashGroupOtherOracleState1 hashGroupOtherOracleState2 hashTagOracleState1
  hashTagOracleState2) -> (IB6_IB7_QueryTags_Second qrys qrysTags table1
  hashGroupOtherOracleState1 hashGroupOtherOracleState2 hashTagOracleState1
  hashTagOracleState2 0%Z 0%Z)).
(* YOU MAY EDIT THE PROOF BELOW *)



(* DO NOT EDIT BELOW *)