Towards Safe Programming of Wireless Sensor Networks

Alastair R. Beresford and Simon Gay (Eds.): Programming Language Approaches to Concurrency and Communication-cEntric Software EPTCS 17, 2010, pp. 49–62, doi:10.4204/EPTCS.17.5 c Martins, Lopes, and Barros This work is licensed under the Creative Commons Attribution License. Towards the Safe Programming of Wireless Sensor Networks Francisco Martins LASIGE & DI-FCUL, Lisbon, Portugal fmartin[email protected]c.ul.pt Lu´ıs Lopes CRACS/INESC-Porto & DCC-FCUP, Porto, Portugal [email protected] Jo˜ao Barros IT & FEUP, Porto, Portugal [email protected] Sensor networks are rather challenging to deploy, program, and debug. Current programming languages for these platforms suffer from a significant semantic gap between their specifications and underlying implementations. This fact precludes the development of (type-)safe applications, which would potentially simplify the task of programming and debugging deployed networks. In this paper we define a core calculus for programming sensor networks and propose to use it as an assembly language for developing type-safe, high-level programming languages. keywords: Sensor Networks, Programming Languages, Process-Calculi. 1 Introduction and Motivation Wireless sensor networks are composed of huge numbers of small physical devices capable of sensing the environment and connected using ad-hoc networking protocols over radio links [1]. These platforms have several unique characteristics when compared with other ad-hoc networks. First, sensor networks are often designed for specific applications or application domains making software re-usability and portability an issue. Sensor devices have very limited processing power (CPU), available memory, and battery lifetime, and are often deployed at remote locations making physical access to the devices (e.g. for maintenance) difficult or even impossible. For these reasons, programming such large scale distributed systems can be daunting. Programs must be lightweight, produce a small memory footprint, be power conservative, be self-reconfigurable (i.e. may be reprogrammed dynamically without physical intervention on the devices) and, we argue, be (type-)safe. To date several programming languages and run-time systems have been proposed for wireless sensor networks (see [10] and references therein) that address some of the above issues, but few tackle the safety issue. Regiment [16], a strongly typed functional macroprogramming language, is the closest to achieve this goal by providing a type-safe compiler. However, Regiment is then compiled into a lowlevel token machine language that is not type-safe. This intermediate language is itself compiled into a nesC implementation of the run-time based on the distributed token machine model, for which no safety properties are available. In fact, in general, an underlying model with well-studied operational semantics for sensor networks seems to be lacking. The absence of such a model reveals itself as a considerable semantic gap between the semantics of the (sometimes high-level) programming languages and their respective implementations. In this paper we propose Callas, a calculus for programming sensor networks, based on the formalism of process calculi [6, 15], that aims to establish a basic computational model for sensor networks. The goal is to diminish the above mentioned semantic gap by proceeding bottom-up, using Callas as a basic assembly language upon which high-level programming abstractions may be encoded as semantics preserving, derived constructs. Callas is an evolution from a previous proposal [11] by the authors, which 50 Towards Safe Programming of WSN S::=Sensors 0empty network |S|Scomposition |[P,R⊲M,T]I,O p,tsensor v::=Values bbuilt-in value |xvariable |Mmodule |sensor installed functions m::=hl(~v)imessages R::=P1:: ···:: Pnrun-queue I,O::=m1:: ···:: mnmessage queues M::=Modules {li= (~xi)Pi}i∈Imodule P::=Processes vvalue |v.l(~v)function call |extern l(~v)external call |timer l(~v)every vexpire vtimed call |send l(~v)communication |receive communication |v.install vinstall code |let x=Pin Psequence T::={(li(~vi),vi,vi,vi)}i∈Itimed calls Figure 1: The syntax of Callas. unlike its original sibling provides: (a) decoupled semantics for in-sensor computation (associated with the application layer) and networking (associated with the data-link and network layers); b) support for a form of timed events; and c) event-driven semantics. 2 Overview of Callas The syntax of Callas is provided by the grammar in Figure 1. Let ~ α denote a possibly empty sequence α 1... α nof elements of some syntactic category α . We let lrange over a countable set of labels representing function names, and let xrange over a countable set of variables. These sets are pairwise disjoint. A network Sis an abstraction for a network of real-world sensors connected via radio links. We write it as a flat, unstructured collection of sensors combined using the parallel composition operator. The empty network is represented by symbol 0. A sensor [P,R⊲M,T]I,O t,pis an abstraction for a sensor device. It features a running process (P) and a double-ended queue of processes scheduled for execution (R). Its memory stores both the installed code for the application (M) and a table of timers for function calls (T). These components represent the application layer of the protocol stack for the sensor. The interface with the lower level networking and data-link layers is modeled using incoming (I) and outgoing (O) queues of messages. The sensors have a measurable position (p) and their own clocks (t), and are able to measure some physical property (e.g. temperature, humidity) by calling appropriate external functions. The code in Mconsists of a set of named functions. The syntax l= (~x)Prepresents a function, where lis the name, (~x)the parameters, and Pthe body. The I(O) queue buffers messages received from (sent to) the network. Messages are just packaged function calls hl(~v)i. Finally, Tis a set that keeps information on timers for function calls. For each timer, a tuple is maintained with the following information: the Martins, Lopes, and Barros 51 call to be triggered, the timer period, the time after which the timer expires and, the time of the next call. A process Pcan be one of the following: (a) a value vthat represents the data exchanged between sensors. It can be a basic value (b) that can intuitively be seen as the primitive data types supported by the sensor’s hardware or a module (M). The special value sensor represents the module that holds the functions installed at the sensor; (b) a synchronous call v.l(~v)to a function lin a module v; (c) a synchronous external call – extern l(~v); (d) a timer – timer l(~v)every vexpire v, that calls an installed function l(~v)periodically, controlled by a timer; (e) an asynchronous remote call – send l(~v), that adds a message hl(~v)ito the outgoing queue (O); (f) a receptor – receive, that gets a message from the incoming queue (I); (g) a module installation – v.install v′, that adds the set of functions in v′to v; and, finally (h) a let construct that allows the processing of intermediate values in computations. The latter is also useful to derive a basic sequential composition construct (in fact, let x=Pin P′≡P;P′with x6∈ fv(P′)). We make frequent use of this construct to impose a more imperative style of programming. Each function in a module has as the first parameter the variable self that is, as usual, a reference to the current module, i.e., the one the function belongs to. Each call to a function v.l(~v)passes vas the first argument in l(~v). In the sequel we present two small examples of programs written in Callas. Both examples have two components: the code to be run at a base-station (sink) and the code to be run at each of the other nodes (sensor). Streaming data. The program that runs on the sink starts by installing, in the local memory (M), a module with a receiver function and a gather function. The former just listens for messages from the network on the incoming queue. The latter simply logs the arguments using a built-in external call. Then, it starts a timer for the receiver function with a period of 5 milliseconds for 10 seconds. Finally, the sink broadcasts a setup message with a period of 100 milliseconds and a duration of 10 seconds. The call is placed in the outgoing queue of the sink (O). In these examples we write install as a compact form for sensor.install . // sink i n s t a l l { r e c e i v e r = ( s e l f ) rece ive gather = ( s e l f , x , y ) e x t e r n a l l og ( x , y ) }; timer r e c e i v e r ( ) every 5exp i r e 10000; send setup (100 ,10000) // sensor i n s t a l l { r e c e i v e r = ( s e l f ) rece ive setup = ( s e l f , x , y ) timer sample () every xexpir e y sample = ( s e l f ) l e t x = e x t e r n a l time ( ) i n l e t y = e x t e r n a l data ( ) i n send g ather ( x , y ) }; timer r e c e i v e r ( ) every 5exp i r e 10000; 52 Towards Safe Programming of WSN Each sensor starts by installing a module with a receiver function, similar to that on the sink, and setup and sample functions. Then it starts a timer on receiver and waits for incoming messages. When a sensor receives a setup message from the network, it sets up another timer to periodically call sample in the same module. When this function is executed the local time and the desired data are read with external calls and a gather message is sent to the network carrying those values. Note that the routing of messages is transparent at this level. It is controlled at the network and data-link layers and we model this by having an extra semantic layer for the network (c.f. Figure 4). In this example, the messages from the sink are delivered to every sensor that carries a setup function. The information originating in the sensors, in the form of gather messages, on the other hand, is successively relayed up to the sink (since sensors have no gather functions implemented). The maximum value of a data attribute and the MAC address of the sensor that reads it. This example follows much the same principles of the above, except that it is a single shot request. Instead of computing the maximum value of the data attribute only at the sink, we optimize the program so that each sensor has two attributes max data and max mac that keep, respectively, the maximum value for the data that passed through the sensor, and the associated MAC address. // sink i n s t a l l { r e c e i v e r = ( s e l f ) rece ive gather = ( s e l f , x , y ) e x t e r n a l l og ( x , y ) }; timer r e c e i v e r ( ) every 5exp i r e 10000; send setup () // sensors i n s t a l l { r e c e i v e r = ( s e l f ) rece ive setup = ( s e l f ) l e t x = e x t e r n a l data ( ) i n l e t y = e x t e r n a l mac () in s e l f . i n s t a l l {max data = ( s e l f ) x max mac = ( s e l f ) y }; send g ather ( x , y ) gather = ( s e l f , x , y ) l e t v a l = s e l f . max data () in i f x>v a l then s e l f . i n s t a l l {max data = ( s e l f ) x max mac = ( s e l f ) y }; send gather ( x , y ) ; }; timer r e c e i v e r ( ) every 5exp i r e 10000; The program that runs on the sink is very similar to that of the previous example. After installing the receiver and the gather functions, it starts the receiver and broadcasts a setup message to the network. The sensors get the call from the network using their receivers and execute setup. The data and MAC Martins, Lopes, and Barros 53 S1|S2≡S2|S1,S|0≡S,S1|(S2|S3)≡(S1|S2)|S3(S-MONOID-SENSOR) [P,R⊲M,T]I,O p,t≡[P,R⊲M,T]I,O p,t{0}(S-INIT-SEND) Figure 2: Structural congruence for sensors. address are obtained by calling external functions and sent to the network in gather messages. Each time such a message is relayed by a sensor on its way to the sink, the relaying sensor checks whether it is worth to send the data forward by comparing it with the local maximum. This strategy manages to substantially reduce the required bandwidth at the sensors closest to the sink. The sink implementation of gather stops the relaying and logs the data. Note that in this example, to simplify, more than one maximum value may be recorded at the sink. Also, we use an if −then construct that is not provided in the base calculus but that can easily be added for convenience. Unlike the previous example, here every sensor will relay gather messages only after some internal processing, by its own version of the homonym function. Semantics. The calculus has two variable binders: the let and the function constructs, inducing the usual definition for free and bound variables. The displayed occurrence of variable xis a binding with scope P both in let x=P′in Pand in l= (...,x,...)P. An occurrence of a variable is free if it is not in the scope of a binding. Otherwise, the occurrence of the variable is bound. The set of free variables of a sensor Sis referred to as fv(S). We present the reduction relation with the help of a structural congruence, as it is usual [14], given in Figure 2. Here, S-INIT-SEND is the only non-standard rule and provides a sensor with a conceptual membrane that engulfs neighboring sensors as they become engaged in communication. This prevents the reception of duplicate copies of the same message from the source sensor during a transmission. The reduction relation is inductively defined by the rules in Figures 3 and 4. Since processes evaluate to values, we allow for reduction within the let construct and therefore present the reduction relation using the following reduction contexts: C[[·]] ::= [ ] |let x=C[[·]] in P. The reduction in a sensor is driven by running process P. Within sensors reduction proceeds without obstacle while the internal clock tis not such that a timed call must be triggered. This is controlled by the predicate noEvent that checks the time of the next activation for every timed call against the current time. There is no special reason why the increments in the clock are unitary. One could easily assume that each instruction consumes a different number of processor cycles and reflect that scenario in the rules. Some rules (e.g. R-LET) simply re-structure a process and thus we assume that no cycles are consumed. Rule R-EXTERN calls a synchronous external function and receives a value as the result. The rules R-INSTALL-SENSOR and R-INSTALL-MODULE handle module updates. The former takes the module with the code installed at the sensor and updates it with the code of another module M′. The resulting new module is installed in the sensor. The latter applies only to volatile anonymous modules and therefore the resulting module is not installed in the sensor. The rule R-SEND (R-RECEIVE) handles the interaction with the network by putting (getting) messages in (from) the outgoing (incoming) queue. Notice that receiving a message is non-blocking (R-NO-MESSAGE). The rules R-CALL-SENSOR,R-CALL-MODULE and RNO-FUNCTION handle calls to functions in modules. R-CALL-SENSOR selects the function in the sensor’s 54 Towards Safe Programming of WSN noEvent(T,t) [C[[extern l(~v)]],R⊲M,T]I,O p,t→[C[[v]],R⊲M,T]I,O p,t+1 (R-EXTERN) noEvent(T,t) [C[[sensor .install M′]],R⊲M,T]I,O p,t→[C[[{}]],R⊲M+M′,T]I,O p,t+1 (R-INSTALL-SENSOR) noEvent(T,t) [C[[M′.install M′′]],R⊲M,T]I,O p,t→[C[[M′+M′′]],R⊲M,T]I,O p,t+1 (R-INSTALL-MODULE) noEvent(T,t) [C[[send l(~v)]],R⊲M,T]I,O p,t→[C[[{}]],R⊲M,T]I,O::hl(~v)i p,t+1 (R-SEND) noEvent(T,t) [C[[receive]],R⊲M,T]hl(~v)i::I,O p,t→[C[[{}]],R:: sensor.l(~v)⊲M,T]I,O p,t+1 (R-RECEIVE) noEvent(T,t) [C[[receive]],R⊲M,T] ε ,O p,t→[C[[{}]],R⊲M,T]I,O p,t+1 noEvent(T,t) [v, ε ⊲M,T]I,O p,t→[v, ε ⊲M,T]I,O p,t+1 (R-NO-MESSAGE,R-IDLE) noEvent(T,t) [v,P:: R⊲M,T]I,O p,t→[P,R⊲M,T]I,O p,t+1 noEvent(T,t) [P,R⊲M,T]I,O p,t→[P,R⊲M,T]I,O p′,t (R-NEXT,R-MOVE) noEvent(T,t) [C[[let x=vin P]],R⊲M,T]I,O p,t→[C[[P[v/x]]],R⊲M,T]I,O p,t (R-LET) M(l) = (self~x)PnoEvent(T,t) [C[[sensor .l(~v)]],R⊲M,T]I,O p,t→[C[[P[M~v/self~x]]],R⊲M,T]I,O p,t+1 (R-CALL-SENSOR) M′(l) = (self~x)PnoEvent(T,t) [C[[M′.l(~v)]],R⊲M,T]I,O p,t→[C[[P[M′~v/self~x]]],R⊲M,T]I,O p,t+1 (R-CALL-MODULE) l6∈ dom(M)noEvent(T,t) [C[[sensor .l(~v)]],R⊲M,T]I,O p,t→[{},R:: C[[sensor .l(~v)]]⊲M,T]I,O p,t+1 (R-NO-FUNCTION) T′=T⊎(l(~v),v,t+v′,t+v)noEvent(T,t) [C[[timer l(~v)every vexpire v′]],R⊲M,T]I,O p,t→[C[[{}]],sensor .l(~v):: R⊲M,T′]I,O p,t+1 (R-TIMER) t≤v′T′=T⊎(l(~v),v,v′,t+v) [P,R⊲M,T⊎(l(~v),v,v′,t)]I,O p,t→[P,sensor .l(~v):: R⊲M,T′]I,O p,t (R-TRIGGER) t>v′ [P,R⊲M,T⊎(l(~v),v,v′,t)]I,O p,t→[P,R⊲M,T]I,O p,t (R-EXPIRE) See Definition 1 for the formal meaning of operator +. Figure 3: Reduction semantics for sensors. Martins, Lopes, and Barros 55 S→S′ S|S′′ →S′|S′′ S1≡S2S2→S3S3≡S4 S1→S4(R-NETWORK,R-CONGR) inRange(p,p′) (I′′,O′′) = networkRoute(m,I′,O′) [P,R⊲M,T]I,m::O p,t{S}|[P′,R′⊲M′,T′]I′,O′ p′,t′→[P,R⊲M,T]I,m::O p,t{S|[P′,R′⊲M′,T′]I′′,O′′ p′,t′}(R-BROADCAST) [P,R⊲M,T]I,m::O p,t{S} → [P,R⊲M,T]I,O p,t|S(R-RELEASE) Figure 4: Reduction semantics for sensor networks. module, gets its code and replaces the parameters with the arguments passing the sensor’s module M as the first argument in variable self. R-CALL-MODULE is similar to R-CALL-SENSOR but uses module M′ instead of the sensor’s module M. Rule R-NO-FUNCTION handles the case of a call to a function that is not yet installed. The call is deferred to the end of the run-queue. The idea is that the module containing the function may not have arrived at the sensor to be installed and so we postpone the execution of the function. When a value of tis reached such that it implies the triggering of a call, the rules R-TRIGGER and R-EXPIRE come into action. Rule R-TRIGGER places a timed function call l(~v)at the front of the runqueue. The execution of the call is delegated to rule R-CALL-SENSOR. Note that only calls to functions installed in the sensor (in M) are allowed. Other calls are deferred to the end of the run-queue by the rule R-NO-FUNCTION. If the timer has expired, rule R-EXPIRE removes the corresponding tuple from T. Network level reduction proceeds concurrently with in-sensor processing. It handles the distribution of messages placed by the sensors in their outgoing queues. A message broadcast starts with the creation of an empty membrane for the broadcasting sensor (rule S-INIT-SEND from the structural congruence). Then, each time a new sensor is added to the membrane of a broadcasting sensor (rule R-BROADCAST), a function networkRoute decides where the message in the Oqueue of the broadcasting sensor should be copied into the new sensor. The function can be thought off as implementing the routing protocol for the sensor network. The message broadcast ends with the destruction of the membrane, the captive sensors becoming again free to engage in communication (rule R-RELEASE). 3 The Type System In this section we present a simple type system for Callas, discuss run-time errors, and prove a type safety result guaranteeing that a well-typed sensor network does not get “stuck” while computing. Type checking. The syntax for types is depicted in Figure 5. Types τ are built from the built-in type β , the types for functions~ τ → τ , where~ τ is the type for parameters of the function and τ is its return type, the types for the sensor code module hli:~ τ i→ τ iii∈Ithat is a record type gathering type information for 56 Towards Safe Programming of WSN τ ::=Types β built-in type |~ τ → τ recursive function type | hli:~ τ i→ τ iii∈Isensor code type | {li:~ τ i→ τ i}i∈Ianonymous code type | µα . τ recursive type | α type variable Figure 5: The syntax of types. each function of the code module, the types for anonymous code modules {li:~ τ i→ τ i}i∈I, recursive types, and type variables. The need for distinct code module types comes from the fact that we need to distinguish from installing code in the sensor module or in an anonymous module. The µ operator is a binder, giving rise, in the standard way, to notions of bound and free variables and alpha-equivalence. We do not distinguish between alpha-convertible types. Furthermore, we take an equi-recursive view of types [19], not distinguishing between a type µα . τ and its unfolding τ [ µα . τ /X]. Definition 1. The +operator is defined (overloaded) for modules, code types, and type environment as follows: • {li= (~xi)Pi}i∈I+{l′ j= (~xj)P′ j}j∈J={li= (~xi)Pi,l′ j= (~xj)P′ j}i∈(I\J),j∈J • {li: τ i}i∈I+{l′ j: τ ′ j}j∈J={li: τ i,l′ j: τ ′ j}i∈(I\J),j∈J •Γ1+Γ2= (Γ1\Γ2)∪Γ2. The typing rules for values, processes, sensors and queues are presented in Figures 6 to 9. Type judgments for values are of the form τ S; τ M;Γ⊢v: τ , where τ Sand τ Mare code module types representing the types for the built-in functions of the sensor ( τ S) and for functions installed in the sensor memory τ M, and Γis a typing environment mapping variables to types. The rules are straightforward, but notice that rule T-SENSOR assigns the sensor code type τ Mto sensor value. The judgments for processes are the same as for values. Rule T-EXTERN ensures that no user-defined function is executed as a system call and that a system call always belongs to a predefined type τ s ( τ S⊢l:~ τ → τ ). Broadcasting a call (Rule T-SEND) is only possible if the call can be made locally ( τ S; τ M;Γ⊢sensor .l(~v):{}) and for functions that return the empty module, since it is an asynchronous remote call and no value is going to be returned (cf. the return value of a system or a local call, which is synchronous). Notice that the type system does not distinguish between local and remote functions, however such refinement may be interesting and can easily be added. Installing code in the sensor’s code module (Rule T-SINSTALL)implies that the module is entirely replaced and that its type is preserved. On the other hand, installation over an anonymous module (Rule T-MINSTALL) is more flexible and only requires that functions common to both code modules should agree on their type (vide the definition of + operation). When calling a local function the type of the first parameter ( τ 1) corresponds to the type of module containing the function being called (vide operation semantic Rules R-CALL-SENSOR and RCALL-MODULE in Figure 3). The rules for let and receive are straightforward. Finally, firing an event (Rule T-TIMER) amounts to calling a user-defined function locally. Martins, Lopes, and Barros 57 τ S; τ M;Γ⊢b: β τ S; τ M;Γ,x: τ ⊢x: τ τ S; τ M;Γ⊢sensor : τ M(T-BUILT-IN,T-VAR,T-SENSOR) j∈I [li:~ τ i→ τ i]i∈I⊢lj:~ τ j→ τ j ∀i. τ S; τ M;Γ⊢vi: τ i τ S; τ M;Γ⊢~v:~ τ (T-LABEL,T-SEQ) ∀i∈I. τ S; τ M;Γ,si: τ M′,~xi:~ τ i⊢Pi: τ i τ M′= µα .{li: α ~ τ i→ τ i}i∈I τ S; τ M;Γ⊢ {li= (si,~xi)Pi}i∈I: τ M′(T-CODE) where [li:~ τ i→ τ i]i∈Imeans either a sensor or an anonymous code type. Figure 6: Typing rules for values. τ S⊢l:~ τ → τ τ S; τ M;Γ⊢~v:~ τ τ S; τ M;Γ⊢extern l(~v): τ τ S; τ M;Γ⊢sensor .l(~v):{} τ S; τ M;Γ⊢send l(~v):{} (T-EXTERN,T-SEND) τ S; τ M;Γ⊢v1: µα .hli: α ~ τ i→ τ iii∈I τ S; τ M;Γ⊢v2: µα .{li: α ~ τ i→ τ i}i∈I τ S; τ M;Γ⊢v1.install v2:{} τ S; τ M;Γ⊢v1: τ 1 τ 1={li:~ τ i→ τ i}i∈I τ S; τ M;Γ⊢v2: τ 2 τ 2={lj:~ τ j→ τ j}j∈J τ S; τ M;Γ⊢v1.install v2: τ 1+ τ 2 (T-SINSTALL,T-MINSTALL) τ S; τ M;Γ⊢v1: τ 1 τ 1⊢l: τ 1~ τ → τ 2 τ S; τ M;Γ⊢~v2:~ τ τ S; τ M;Γ⊢v1.l(~v2): τ 2 τ S; τ M;Γ⊢P1: τ 1 τ S; τ M;Γ,x: τ 1⊢P2: τ 2 τ S; τ M;Γ⊢let x=P1in P2: τ 2 (T-CALL,T-LET) τ S; τ M;Γ⊢receive :{} τ S; τ M;Γ⊢sensor .l(~v):{} τ S; τ M;Γ⊢v1v2: ββ τ S; τ M;Γ⊢timer l(~v)every v1expire v2:{} (T-RECEIVE,T-TIMER) Figure 7: Typing rules for processes. Typing judgments for sensor networks are of the form τ S; τ M⊢S. We only comment the rule for typing a sensor (Rule T-SENSOR), in particular, that the type of each function in the sensor’s code module (M) must agree with predefined sensor’s type interface ( τ M), apart from the self parameter. Typing the run-queue (Rule T-RUN-QUEUE,Figure 9), the incoming and outgoing queues, and the event table is equivalent to typing each element of the structure individually (Rules T-COMM-QUEUE and T-EVENTQUEUE). Notice that each element of the incoming (outgoing) queue is typable if it can be called as a local sensor function. The same holds for timed calls (l(~v)). The proofs for our main results (Theorem 6, Theorem 7, and Corollary 8) are based on the following auxiliary results. We call context process, denoted C[[P]], the processes resulting from filling its context hole. Informally, Lemma 1 states that if a context process is well typed, then the same also holds for the process that fills its hole, although not necessarily with an identical type. Lemma 2 states that the typability of a context process holds and its type is preserved if we fill the context’s hole with processes of the same type. Lemma 3 handles module’s substitution. Lemmas 4 and 5 are discussed below. Lemma 1. If τ S; τ M;Γ⊢C[[P]]: τ , then τ S; τ M;Γ′⊢P: τ ′. Proof. The proof proceeds by induction on the contexts’ structure and both cases are straightforward.