• Andrei Paskevich's avatar
    track dangerous applications of equality · bb6734a1
    Andrei Paskevich authored
    In programs, but also in pure theories, it is not safe to compare
    arbitrary types. For example, if we have a record with ghost fields,
    a comparison may produce different results before and after ghost
    code elimination. Even for pure types like 'map' or 'set', it is
    unlikely that the result of logical equality will be the same as
    the result of OCaml structural equality on the implemented type.
    
    This commit makes the first step towards fixing this issue.
    We proceed in the following way:
    
    1. Every lsymbol (pure function or predicate symbol) carries
       a subset of type variables of its signature, called "opaque
       type variables". By marking a type variable 'a opaque in an
       lsymbol's signature, the user guarantees that this lsymbol
       can be implemented without ever comparing values of type 'a.
       In other words, this is a promise not to break into a type
       variable.
    
       The corresponding syntax is: "predicate safe (x y : ~'a)".
    
       All type variables in undefined symbols are non-opaque,
       unless annotated otherwise. Non-opaque is the default
       to keep the change conservative.
    
       Opacity of type variables in defined symbols is inferred
       from the definition. If the definition violates a given
       opacity annotation, an exception is raised. Notice that
       we only check definitions in _theory_ declarations. One
       can define an lsymbol in a _task_ in a way that violates
       opacity. We cannot forbid it, because various elimination
       transformations would replace safe operations (such as
       matching) with equalities. This is not a problem, since in
       the pure logical realm of provers opacity is not required
       One exception would be Coq, whose transformation chain must
       never perform such operations.
    
       All type variables in inductive predicates are non-opaque.
       Indeed, we can redefine equality via an inductive predicate.
       [TODO: find safe forms of inductive definitions and implement
       more reasonable restrictions.]
    
       All type variables in constructors and field symbols are opaque.
    
       It is forbidden to instantiate an opacity-preserving symbol
       with an opacity-breaking one in a clone substitution.
    
    2. Similar type variable tracking is implemented for program symbols.
       Type variables in the signature of a "val" are non-opaque unless
       annotated otherwise. Opacity of type variables in defined symbols
       is inferred from the definition, and an exception is raised, if
       a given annotation is violated.
    
       The internal mechanism of tracking is different: the "eff_compar"
       field in effects contains the type variables that occur under
       equality or any other opacity-breaking operation. In this respect,
       our API is inconsistent between lsymbols and psymbols: the former
       asks for the opaque tvsymbols, the latter requires us to fill the
       spec with "comparison effects" for the non-opaque ones. [TODO:
       add the "~opaque" argument to create_psymbol and make the WhyML
       core fill the effect under the hood.]
    
       Every time an lsymbol or a psymbol is applied in a program,
       we check the substitution into its signature's type variables.
       If a non-opaque type variable is instantiated with a program type,
       an exception is raised. [TODO: be more precise and reject only
       types with ghost and model components - being mutable, private,
       or carrying an invariant doesn't conflict with equality.]
    
       Notice that we do not allow to compare program types even in
       the ghost code. This is not needed if we only consider the
       problems of the code extraction, but _might_ be necessary,
       if we also want to protect Coq realisations (see below).
    
    This commit fixes the immediate problem of breaking the ghost
    guarantees when equality or some other opacity-breaking lsymbol
    is applied in a program to a type with ghost or "model" parts.
    
    This leaves the problem of code extraction for programs that
    compare complex types such as maps or sets (Coq driver is
    affected by this, too, I guess). The next step is to provide
    annotations for problematic type constructors. A declaration
    "type ~map 'a 'b" would mean "logical equality on this type
    is likely to be different from the structural equality on any
    implementation of this type - therefore do not apply equality
    to it: neither in programs (because this can't be implemented),
    nor in pure functions (because they are extracted, too, and
    because this can't be realized with Leibniz equality in Coq)."
    [TODO: discuss and implement.]
    
    [TODO: mb choose better term for "opaque" and notation for ~'a.]
    bb6734a1
theory.ml 26.8 KB