fmod ASSOCKEY is

protecting SMESSAGE .


--- AssocKey
sort AssocKey .
op assockey : PartialKey KeyId -> AssocKey .

var assockey assockey' : AssocKey .
var partialkey partialkey' : PartialKey .
var keyid keyid' : KeyId .

op partialkey : AssocKey -> PartialKey .
eq partialkey(assockey(partialkey,keyid)) = partialkey .

op keyid : AssocKey -> KeyId .
eq keyid(assockey(partialkey,keyid)) = keyid .


--- AssocKeyList
sort AssocKeyList .
op eAssocKeyList : -> AssocKeyList .
op sAssocKeyList : AssocKey -> AssocKeyList .
op __ : AssocKeyList AssocKeyList -> AssocKeyList [assoc id: eAssocKeyList] . 

var assockeylist assockeylist' : AssocKeyList .

op contains : AssocKeyList AssocKey -> Bool .
eq contains(eAssocKeyList, assockey') = false .
eq contains((sAssocKeyList(assockey) assockeylist), assockey') = 
     (assockey' == assockey) or contains(assockeylist, assockey') .
          
op contains : AssocKeyList AssocKeyList -> Bool .
eq contains(assockeylist, eAssocKeyList) = false .
eq contains(assockeylist, (sAssocKeyList(assockey') assockeylist')) = 
     contains(assockeylist, assockey') or 
     contains(assockeylist, assockeylist') .

op add : AssocKeyList AssocKey -> AssocKeyList .
eq add(assockeylist,assockey) = (assockeylist sAssocKeyList(assockey)) .

op add : AssocKeyList AssocKeyList -> AssocKeyList .
eq add(assockeylist,assockeylist') = (assockeylist assockeylist') .

op  add' : AssocKeyList AssocKey -> AssocKeyList .
ceq add'(assockeylist,assockey) = assockeylist 
    if contains(assockeylist, assockey) .
ceq add'(assockeylist,assockey) = (assockeylist sAssocKeyList(assockey)) 
    if not(contains(assockeylist, assockey)) .  
     
op  rm : AssocKeyList AssocKey -> AssocKeyList .
eq  rm(eAssocKeyList, assockey) = eAssocKeyList .
ceq rm((sAssocKeyList(assockey) assockeylist), assockey') = 
      rm(assockeylist, assockey')
    if (assockey' == assockey) .
ceq rm((sAssocKeyList(assockey) assockeylist), assockey') = 
      (sAssocKeyList(assockey) rm(assockeylist, assockey'))
    if (assockey' =/= assockey) .
    
op  rm : AssocKeyList AssocKeyList -> AssocKeyList .
eq  rm(assockeylist, eAssocKeyList) = assockeylist .
eq  rm(assockeylist, (sAssocKeyList(assockey') assockeylist')) = 
      rm(rm(assockeylist, assockey'), assockeylist') .
       
op  subset : AssocKeyList AssocKeyList -> Bool .
eq  subset(eAssocKeyList, assockeylist') = true .
eq  subset((sAssocKeyList(assockey) assockeylist), assockeylist') = 
      contains(assockeylist',assockey) and subset(assockeylist,assockeylist') .

op  len : AssocKeyList -> Nat .
eq  len(eAssocKeyList) = 0 .
eq  len(sAssocKeyList(assockey) assockeylist) = 1 + len(assockeylist) .

var i : Nat .
op  ith : AssocKeyList Nat ~> AssocKey .
eq  ith((sAssocKeyList(assockey) assockeylist), 1) = assockey .
eq  ith((sAssocKeyList(assockey) assockeylist), (s i)) = ith(assockeylist,i) .

op  index : AssocKeyList AssocKey ~> Nat .
ceq index((sAssocKeyList(assockey) assockeylist), assockey') = 1 
    if assockey == assockey' .
ceq index((sAssocKeyList(assockey) assockeylist), assockey') = 
      1 + index(assockeylist,assockey') 
    if assockey =/= assockey' .

op  last : AssocKeyList ~> AssocKey .
eq  last(assockeylist sAssocKeyList(assockey)) = assockey .

op  last : AssocKeyList Nat ~> AssocKey .
eq  last(assockeylist sAssocKeyList(assockey), 1) = assockey .
eq  last(assockeylist sAssocKeyList(assockey), (s i)) = last(assockeylist, i) .

op  first : AssocKeyList ~> AssocKey .
eq  first(sAssocKeyList(assockey) assockeylist) = assockey .

op  next : AssocKeyList AssocKey ~> AssocKey .
ceq next(sAssocKeyList(assockey) assockeylist, assockey') = first(assockeylist)
    if assockey == assockey' .
ceq next(sAssocKeyList(assockey) assockeylist, assockey') = 
      next(assockeylist, assockey')
    if assockey =/= assockey' .

op contains : AssocKeyList KeyId -> Bool .
eq contains(eAssocKeyList, keyid') = false .
eq contains((sAssocKeyList(assockey) assockeylist), keyid') = 
     (keyid' == keyid(assockey)) or contains(assockeylist, keyid') .      
     
op  lookup : AssocKeyList KeyId ~> AssocKey .
ceq lookup(sAssocKeyList(assockey) assockeylist, keyid') = assockey
    if keyid' == keyid(assockey) .
ceq lookup(sAssocKeyList(assockey) assockeylist, keyid') = 
      lookup(assockeylist, keyid')
    if keyid' =/= keyid(assockey) .

op  lookup : AssocKeyList PartialKey ~> AssocKey .
ceq lookup(sAssocKeyList(assockey) assockeylist, partialkey') = assockey
    if partialkey' == partialkey(assockey) .
ceq lookup(sAssocKeyList(assockey) assockeylist, partialkey') = 
      lookup(assockeylist, partialkey')
    if partialkey' =/= partialkey(assockey) .


--- GroupAssocKeyList
var group, group' : Group .

sort GroupAssocKeyList .
op groupassockeylist : Group AssocKeyList -> GroupAssocKeyList .

op group : GroupAssocKeyList -> Group .
eq group(groupassockeylist(group, assockeylist)) = group .

op assockeylist : GroupAssocKeyList -> AssocKeyList .
eq assockeylist(groupassockeylist(group, assockeylist)) = assockeylist .

var groupassockeylist groupassockeylist' : GroupAssocKeyList .


--- GroupAssocKeyListSet
sort GroupAssocKeyListSet .
op eGroupAssocKeyListSet : -> GroupAssocKeyListSet .
op sGroupAssocKeyListSet : GroupAssocKeyList -> GroupAssocKeyListSet .
op __ : GroupAssocKeyListSet GroupAssocKeyListSet -> 
        GroupAssocKeyListSet [assoc comm id: eGroupAssocKeyListSet] .
    
var groupassockeylistset groupassockeylistset' : GroupAssocKeyListSet .

op  get : GroupAssocKeyListSet Group ~> AssocKeyList .
ceq get(sGroupAssocKeyListSet(groupassockeylist) groupassockeylistset, group') 
    = assockeylist(groupassockeylist)
    if group(groupassockeylist) == group' .
ceq get(sGroupAssocKeyListSet(groupassockeylist) groupassockeylistset, group')
    = get(groupassockeylistset,group')
    if group(groupassockeylist) =/= group' .

op  update : GroupAssocKeyListSet Group AssocKeyList -> GroupAssocKeyListSet .
eq  update(eGroupAssocKeyListSet, group', assockeylist') =
    sGroupAssocKeyListSet(groupassockeylist(group', assockeylist')) .
ceq update(sGroupAssocKeyListSet(groupassockeylist(group,assockeylist)) 
    groupassockeylistset, group', assockeylist') = 
    update(groupassockeylistset,group',assockeylist')
    if group == group' .
ceq update(sGroupAssocKeyListSet(groupassockeylist(group,assockeylist)) 
    groupassockeylistset, group', assockeylist') = 
    sGroupAssocKeyListSet(groupassockeylist(group,assockeylist)) 
    update(groupassockeylistset,group',assockeylist')
    if group =/= group' .

op  rm : GroupAssocKeyListSet Group AssocKeyList -> GroupAssocKeyListSet .
eq  rm(eGroupAssocKeyListSet, group', assockeylist') =
    eGroupAssocKeyListSet .
ceq rm(sGroupAssocKeyListSet(groupassockeylist(group,assockeylist)) 
    groupassockeylistset, group', assockeylist') = 
    rm(groupassockeylistset,group',assockeylist')
    if group == group' .
ceq rm(sGroupAssocKeyListSet(groupassockeylist(group,assockeylist)) 
    groupassockeylistset, group', assockeylist') = 
    sGroupAssocKeyListSet(groupassockeylist(group,assockeylist)) 
    rm(groupassockeylistset,group',assockeylist')
    if group =/= group' .

op contains : GroupAssocKeyListSet Group -> Bool .
eq contains(eGroupAssocKeyListSet, group') = false .
eq contains((sGroupAssocKeyListSet(groupassockeylist(group,assockeylist)) 
     groupassockeylistset), group') = (group' == group) or 
     contains(groupassockeylistset, group') .
   
op add : GroupAssocKeyListSet Group AssocKeyList -> GroupAssocKeyListSet .
eq add(groupassockeylistset, group', assockeylist') = 
   groupassockeylistset  
   sGroupAssocKeyListSet(groupassockeylist(group', assockeylist')) .

op  add' : GroupAssocKeyListSet Group AssocKeyList -> GroupAssocKeyListSet .
ceq add'(groupassockeylistset, group', assockeylist') = groupassockeylistset
    if contains(groupassockeylistset, group') .

ceq add'(groupassockeylistset, group', assockeylist') = 
    add(groupassockeylistset, group', assockeylist')
    if not(contains(groupassockeylistset, group')) .


endfm