wiki:Language/Core/Witnesses

Version 3 (modified by benl, 8 years ago) (diff)

--

Witnesses

WIT
   ::= VAR
    |  WCON
    |  WIT WARG+
    |  WIT & WIT
    |  ( WIT )

WARG      ::= ARGWIT | { TYPE } | {: ARGTTYPE+ :}

ARGWIT    ::= VAR | CON | ( WITNESS )
ARGTYPE   ::= VAR | CON | !0 | $0 | ( TYPE )

A witness can be a variable, witness constructor, witness application or witness join. All the witness constructors are baked in, and are listed below.

Witness constructors:

NameType
UpurePure !0
UemptyEmpty !0
Rglobal[r:%].Global r
Rconst[r:%].Const r
Rmutable[r:%].Mutable r
Rlazy[r:%].Lazy r
Rdirect[r:%].Direct r
RdistinctN[r1 .. rN:%].DistinctN r1 .. rN
Uuse[r:%].Global r => Const r => Empty (Use r)
Uread[r:%].Const r => Pure (Read r)
Ualloc[r:%].Const r => Pure (Alloc r)
  • Runtime witness constructors are marked with (R). These are introduced into the program at runtime and cannot appear in the source code. They are introduced by the system only when the associated property is true, and the type system ensures that they are eliminated from the program when this is no longer the case.
  • User witness constructors are marked with (U). These can be used in the source code. The user witness constructors are either always true, as with the axioms pure and empty, or combine existing witnesses in a sound way, as with use, read and alloc.
  • Only witnesses of types Pure t or Empty t can be joined, for some type t.

The following witness expressions are equivalent:

WIT1 WIT2 WIT3 = (WIT1 WIT2) WIT3
distinct3 {r1} {r2} {r3} = distinct3 {:r1 r2 r3:}
WIT1 & WIT2 = WIT2 & WIT1
(WIT1 & WIT2) & WIT3 = WIT1 & (WIT2 & WIT3)

Example witnesses:

 1) pure  :: Pure !0

 2) const {r1} :: Const r1

 3) read {r1} <w1> :: Pure (Read r1) 
    ... where w1 :: Const r1

 4) read {r1} <w1> & alloc {r2} <w2> :: Pure (Read r1 + Alloc r1)
    ... where w1 :: Const r1  and  w2 :: Const r2


History

  • 2009: Introduced a polymorphic witness join operator (&) instead of using join constructors MkJoinEffect and MkJoinClosure. These really cluttered the core programs too much.
  • 2011/12: Split the Witness universe from the Spec universe.
  • 2011/12: Added multiple application sugar {: ... :} and <: ... :> to beautify the core programs. This really helps with recursive functions when many type variables need to be passed back in the recursive call.