IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Certificate Structure and Internal Significance
Continuing from the discussion in Certificate Significance we elaborate upon what counts as a certificate, and how certification procedures are determined by certificate content.
Before getting specific, let us sketch the design. The principal, dominant form of certificate indicates two Native Language programs, the first being the procedure invoked to create the certificate (and others like it), and the second being a procedure to be applied when "reconsidering" the certificate later. These native language programs are pointed to by the certificate, and to understand them along with understanding the general method for reconsidering Stale Certificates is to understand the "internal" or direct significance of the certificate. In order to facilitate Borrowing Certificates, we admit a special kind of certificate that has the same content as a normal "native" certificate, but which cannot be updated and can be created only by copying from a foreign FDL. A third kind of certificate-like object is a "certificate identifier" which may exist in the FDL
abinitio, but is a distinguished object created as part of the FDL in order to identify other certificates by their content.
The unifying characteristic of these certificates is that their content is strictly regulated by the FDL, unlike ordinary objects whose content is whatever the Clients make it.
We defer discussion of Certificate Identifiers, stipulating here that the FDL classifies each certificate identifier as either "native" or "borrowed".
Both native and borrowed certificates of the ordinary kind, ie not certificate ids, have as content a Text whose operator consists of two object references, the first being a certificate identifier and the second being a reference to an appropriate code specifying object. The intention is that this second object contain the Native Language programs for creating and updating certificates referring to it in this way. This pair <C,K> of references constituting the certificate contents' operator may the considered the certificate "kind", and it can never be altered in an object once created. The content of K cannot be altered as long as K is part of the certificate kind for any existing certificate; this policy is part of what makes the FDL trustworthy. If you want better code and the old code still matters to someone, you must make a new object K' and employ a new certificate kind <C,K'>.
A certificate with kind <C,K>, where C is a native-certificate identifier, can only be created by interpreting the first subtext of object K, applied to some specified arguments. If this execution returns a TextT, then a new object is created whose operator is <C,K> and whose first subtext is T. There may be other subtexts as well indicating generally useful information as determined by the FDL implementors, such as dates or other transaction related data. How the native language program is interpreted is determined by the C in a way inherent to the FDL process. Thus, within an FDL, there may be multiple native language interpreters indexed by the certificate id. If one needs to add a native language to an FDL or improve a native language of an FDL, then a new certificate identifier should be introduced for the new interpreter. Once an interpreter is employed it must be unaltered if clients are to be able to trust the FDL. Similarly, different FDLs may have different implementations of a native language, perhaps with different execution results either intentionally or accidentally, or may support different native languages. Thus, native certificates must never be transferred as such between FDLs if client trust is to be maintained.
A certificate with kind <C,K>, again where C indicates native, can be updated only under circumstances explained in Stale Certificates. Then the second subtext of the content of object K is executed as a native language program according to C, applied to arguments as stipulated in Stale Certificates. If the procedure returns a text, then that becomes the new first subtext of the extant certificate. Again, any other subtexts are updated as the FDL implementors choose. We shall consider Borrowed Certificates in more detail.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html