doc-src/Logics/logics.rao

Client, Server certificates now sent using the separate Certificate rule,
simplifying ServerHello and ClientKeyExch. Resumption no longer needs its
own version of ServerHello. Proofs run nearly three minutes faster.

% This file was generated by 'rail' from 'logics.rai'
\rail@i {1}{ typedef : 'typedef' ( () | '(' name ')') type '=' set witness; type : typevarlist name ( () | '(' infix ')' ); set : string; witness : () | '(' id ')'; }
\rail@o {1}{
\rail@begin{2}{typedef}
\rail@term{typedef}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{name}[]
\rail@term{)}[]
\rail@endbar
\rail@nont{type}[]
\rail@term{=}[]
\rail@nont{set}[]
\rail@nont{witness}[]
\rail@end
\rail@begin{2}{type}
\rail@nont{typevarlist}[]
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{infix}[]
\rail@term{)}[]
\rail@endbar
\rail@end
\rail@begin{1}{set}
\rail@nont{string}[]
\rail@end
\rail@begin{2}{witness}
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{id}[]
\rail@term{)}[]
\rail@endbar
\rail@end
}
\rail@i {2}{ typedecl : typevarlist id '=' (cons + '|') ; cons : name (typ *) ( () | mixfix ) ; typ : id | tid | ('(' typevarlist id ')') ; }
\rail@o {2}{
\rail@begin{2}{typedecl}
\rail@nont{typevarlist}[]
\rail@nont{id}[]
\rail@term{=}[]
\rail@plus
\rail@nont{cons}[]
\rail@nextplus{1}
\rail@cterm{|}[]
\rail@endplus
\rail@end
\rail@begin{3}{cons}
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@plus
\rail@nont{typ}[]
\rail@nextplus{2}
\rail@endplus
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@nont{mixfix}[]
\rail@endbar
\rail@end
\rail@begin{3}{typ}
\rail@bar
\rail@nont{id}[]
\rail@nextbar{1}
\rail@nont{tid}[]
\rail@nextbar{2}
\rail@term{(}[]
\rail@nont{typevarlist}[]
\rail@nont{id}[]
\rail@term{)}[]
\rail@endbar
\rail@end
}