/* MuCAPSL Prelude */

TYPESPEC BOOLEAN;
TYPES
    Boolean: Object;
CONSTANTS
    true, false: Boolean;
FUNCTIONS
    and(Boolean, Boolean): Boolean,ASSOC,COMM;
    or(Boolean, Boolean): Boolean,ASSOC,COMM;
    not(Boolean): Boolean;
    if(Boolean, Boolean, Boolean): Boolean;
END;


TYPESPEC FIELD;
IMPORTS BOOLEAN;
TYPES 
    Field: Object;
    Tape, Atom: Field;
    Principal: Atom;
    Nonce, Nat: Atom, INFINITE;
CONSTANTS
    undef: Field;
FUNCTIONS 
    cat(Field, Field): Tape, ASSOC;
    first(Tape): Atom;
    rest(Tape): Field;
    eqn(Field,Field): Boolean;
VARIABLES 
    Al: Atom;
    Xl: Field;
AXIOMS
    first(cat(Al, Xl)) = Al; 
    rest(cat(Al, Xl)) = Xl;
    INVERT cat(Al, Xl): Al; 
    INVERT cat(Al, Xl): Xl;
    eqn(Xl,Xl);
END;

TYPESPEC GROUP;
TYPES
    Role: Object;
    GroupMember: Object;
FUNCTIONS
    owner(GroupMember): Principal;
    groupid(GroupMember): Nat;
END;

TYPESPEC SKEY;
IMPORTS FIELD;
TYPES Skey: Nat,INFINITE;
FUNCTIONS
    sha(Field): Skey;
    mac(Skey,Field): Skey;
END;


TYPESPEC DSKE;
IMPORTS SKEY;
FUNCTIONS
    se(Skey, Atom): Atom;
    sd(Skey, Atom): Atom;
    se(Skey, Field): Field;
    sd(Skey, Field): Field;
VARIABLES
    Kl, K1l: Skey;
AXIOMS 
    sd(Kl, se(Kl, Xl)) = Xl;
    se(Kl, sd(Kl, Xl)) = Xl;
    INVERT se(Kl, Xl): Xl | Kl;
    INVERT sd(Kl, Xl): Xl | Kl;
END;


TYPESPEC XOR;
IMPORTS SKEY;
FUNCTIONS
    xor(Skey, Skey): Skey, ASSOC, COMM;
AXIOMS
    xor(xor(Kl,Kl),K1l) = K1l;
    INVERT xor(Kl,K1l): Kl | K1l;
    INVERT xor(Kl,K1l): K1l | Kl;
END;


/* Symmetric Key Client, Server */

TYPESPEC SKCS;
TYPES Client, Server: Principal;
VARIABLES
	Sl : Server;
	Cl : Client;
FUNCTIONS
	 csk(Client): Skey, PRIVATE;
	 ssk(Server,Client): Skey, PRIVATE; 
AXIOMS
	 ssk(Sl, Cl) = csk(Cl);
END;


/* Mutual Symmetric Key Node */

TYPESPEC MSKN;
TYPES Node: Principal;
FUNCTIONS
	msk(Node, Node): Skey, COMM, PRIVATE;
END;

TYPESPEC NUMS;
IMPORTS SKEY;
CONSTANTS 0,1,2,3: Skey;
FUNCTIONS /* infix syntax + - * ^ > <   */
    pls(Nat, Nat): Nat, ASSOC, COMM;
    mns(Nat): Nat;
    tms(Nat, Nat): Nat, ASSOC, COMM;
    exp(Nat, Nat): Nat;
    isgrtr(Nat,Nat): Boolean;
    isless(Nat,Nat): Boolean;
END;

TYPESPEC ARITH;
IMPORTS SKEY;
FUNCTIONS
    pls(Skey, Skey): Skey, ASSOC, COMM;
    mns(Skey): Skey;
    tms(Skey, Skey): Skey, ASSOC, COMM;
    div(Skey, Skey): Skey;
    exp(Skey, Skey): Skey;
/*
AXIOMS
*/
END;

TYPESPEC PKEY;
IMPORTS FIELD;
TYPES Pkey;
VARIABLES PKl, PKIl: Pkey;
FUNCTIONS
    keypair(Pkey, Pkey): Boolean, COMM;
END;

TYPESPEC SPKE;
IMPORTS PKEY;
FUNCTIONS
    ped(Pkey, Atom): Atom;
    ped(Pkey, Field): Field;

AXIOMS 
   IF keypair(PKl,PKIl) THEN ped(PKIl, ped(PKl, Xl)) = Xl ENDIF; 
END;

TYPESPEC PPK;
IMPORTS PKEY;
TYPES 
  PKUser: Principal;
FUNCTIONS
  sk(PKUser): Pkey, PRIVATE;
  pk(PKUser): Pkey;
VARIABLES 
  PKUl: PKUser;
AXIOMS
  keypair(sk(PKUl),pk(PKUl));
  INVERT ped(sk(PKUl),Xl): Xl | pk(PKUl);
  INVERT ped(pk(PKUl),Xl): Xl | sk(PKUl);
END;


TYPESPEC KEYAGREEMENT;
IMPORTS SKEY;
TYPES Pval;
FUNCTIONS
    kap(Skey): Pval;
    kas(Pval, Skey): Skey;
AXIOMS
    kas(kap(Kl),K1l) = kas(kap(K1l),Kl);
END;


TYPESPEC PKSeal;
IMPORTS PKEY;
TYPES Pseal;
FUNCTIONS
    seal(Pkey, Field): Pseal;
    verify(Pkey, Pseal, Field): Boolean;
AXIOMS
    keypair(PKl,PKIl) =
    verify(PKIl,seal(PKl, Xl), Xl);
END;


TYPESPEC TIMESTAMP;
TYPES Timestamp: Atom,INFINITE;
END;


TYPESPEC LIST;
TYPES List;
FUNCTIONS
    con(Field, Field): List;
    head(List): Field;
    tail(List): Field;
VARIABLES
    Xl,Yl: Field;
AXIOMS
    head(con(Xl, Yl)) = Xl;
    tail(con(Xl, Yl)) = Yl;
    INVERT con(Xl, Yl): Xl;
    INVERT con(Xl, Yl): Yl;
END;

TYPESPEC ARRAY;
TYPES Array: Field;
FUNCTIONS
    arr(Field): Array;
    at(Array,Nat): Field;
    with(Array,Nat,Field): Array;
    proj(Array,Nat,Nat): Array;
    acat(Array,Array): Array;
    size(Array): Nat;
    adel(Array,Nat): Array;
    isnull(Array): Boolean;
    last(Array): Field;
CONSTANTS
    anull: Array;
VARIABLES
    ARl, ARl2: Array;
    Xl: Field;
    Nl, Nl2, Nl3: Nat;
AXIOMS
    size(anull) = 0;
    size(arr(Xl)) = 1;
    size(acat(ARl,ARl2)) = size(ARl)+size(ARl2);

    IF 0<Nl AND Nl-1<Nl2 AND Nl2-1<size(ARl)
    THEN size(proj(ARl,Nl,Nl2)) = (Nl2-Nl)+1 ENDIF;

    IF 0<Nl AND Nl-1<size(ARl)
    THEN size(with(ARl,Nl,Xl)) = size(ARl) ENDIF;

    at(arr(Xl),1) = Xl;        /* 1-based array addressing */

    IF 0<Nl AND Nl-1<size(ARl) 
    THEN at(with(ARl,Nl,Xl),Nl) = Xl ENDIF;

    IF 0<Nl AND Nl-1<size(ARl)
    THEN at(acat(ARl,ARl2),Nl) = at(ARl,Nl) ENDIF;

    IF size(ARl)<Nl AND Nl-1<size(ARl)+size(ARl2)
    THEN at(acat(ARl,ARl2),Nl) = at(ARl2,Nl-size(ARl)) ENDIF;

    IF 0<Nl AND Nl-1<Nl2 AND Nl2-1<size(ARl) 
       AND 0<Nl3 AND Nl3-1<size(proj(ARl,Nl,Nl2))
    THEN at(proj(ARl,Nl,Nl2),Nl3) = at(ARl,Nl3+(Nl-1)) ENDIF;

    IF 0<Nl AND Nl-1<size(ARl)
    THEN proj(ARl,Nl,Nl) = arr(at(ARl,Nl)) ENDIF;

    IF 0<Nl AND Nl-1<Nl2 AND Nl2-1<size(ARl) 
    THEN proj(acat(ARl,ARl2),Nl,Nl2) = proj(ARl,Nl,Nl2) ENDIF;

    IF size(ARl)<Nl AND Nl-1<Nl2 AND Nl2-1<size(ARl)+size(ARl2)  
    THEN proj(acat(ARl,ARl2),Nl,Nl2) =
         proj(ARl2,Nl-size(ARl),Nl2-size(ARl)) ENDIF;

    IF 0<Nl AND Nl-1<size(ARl) AND size(ARl)<Nl2 AND Nl2-1<size(ARl2) 
    THEN proj(acat(ARl,ARl2),Nl,Nl2)=
         acat(proj(ARl,Nl,size(ARl)),proj(ARl2,1,Nl2-size(ARl))) ENDIF;

    IF 0<Nl2 AND Nl2-1<Nl3 AND Nl3-1<size(ARl) AND Nl2-1<Nl AND Nl-1<Nl3 
    THEN proj(with(ARl,Nl,Xl),Nl2,Nl3) = with(proj(ARl,Nl2,Nl3),(Nl-Nl2)+1,Xl) ENDIF;

    IF 0<Nl2 AND Nl2-1<Nl3 AND Nl3-1<size(ARl) AND 0<Nl AND Nl<Nl2
    THEN proj(with(ARl,Nl,Xl),Nl2,Nl3) = proj(ARl,Nl2,Nl3) ENDIF;
 
    IF 0<Nl2 AND Nl2-1<Nl3 AND Nl3-1<size(ARl) AND Nl3<Nl AND Nl<size(ARl)
    THEN proj(with(ARl,Nl,Xl),Nl2,Nl3) = proj(ARl,Nl2,Nl3) ENDIF;

    IF 0<Nl AND Nl-1<size(ARl)
    THEN acat(with(ARl,Nl,Xl),ARl2) = with(acat(ARl,ARl2),Nl,Xl) ENDIF;

    IF 0<Nl AND Nl-1<size(ARl2)
    THEN acat(ARl,with(ARl2,Nl,Xl)) = with(acat(ARl,ARl2),Nl+size(ARl),Xl) ENDIF;

    IF 0<Nl AND Nl-1<size(ARl)
    THEN adel(ARl,Nl) = acat(proj(ARl,1,Nl-1),proj(ARl,Nl+1,size(ARl))) ENDIF;

    IF isnull(ARl) THEN size(ARl) = 0 ENDIF;
    IF size(ARl) = 0 THEN isnull(ARl) ENDIF;

    acat(anull,ARl) = ARl;
    acat(ARl,anull) = ARl;

    IF 0<Nl AND Nl < Nl2 THEN proj(ARl,Nl2,Nl) = anull ENDIF;

    last(ARl) = at(ARl,size(ARl));
END;

TYPESPEC NARRAY;
TYPES Narray: Array;
FUNCTIONS
    arr(Nat): Narray;
    at(Narray,Nat): Nat;
    with(Narray,Nat,Nat): Narray;
    proj(Narray,Nat,Nat): Narray;
    acat(Narray,Narray): Narray;
    adel(Narray,Nat): Narray;
    aexp(Narray,Nat): Narray;
VARIABLES
    NARl: Narray;
AXIOMS
    at(aexp(NARl,Nl),Nl2) = exp(at(NARl,Nl2),Nl);
    size(aexp(NARl,Nl)) = size(NARl);
END;

TYPESPEC SARRAY;
TYPES Sarray: Narray;
FUNCTIONS
    arr(Skey): Sarray;
    at(Sarray,Nat): Skey;
    with(Sarray,Nat,Skey): Sarray;
    proj(Sarray,Nat,Nat): Sarray;
    acat(Sarray,Sarray): Sarray;
    adel(Sarray,Nat): Sarray;
    aexp(Sarray,Nat): Sarray;
END;

TYPESPEC ENDPRELUDE;
CONSTANTS endprelude: Boolean;
AXIOMS
    endprelude = true;
END;