LASAPP: Language-Agnostic Static Analysis of Probabilistic Programs

LASAPP Supplementary Material Contents 1 A small formal PPL: SimpleProb 1 1.1 Syntax............................................... 1 1.2 Semantics............................................. 1 1.3 Control-Flow-Graph ....................................... 2 1.3.1 CFGSemantics...................................... 3 1.4 Provenance and Evaluation Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2 LASAPP API for SimpleProb 8 3 Statistical Dependency Analysis 9 4 HMC Assumption Checker 11 5 Parameter Constraint Verification 15 6 Model-Guide Validation 18 1 A small formal PPL: SimpleProb 1.1 Syntax The complete syntax of SimpleProb is given below. Syntax of SimpleProb: E::= expression cconstant xvariable g(E1, . . . , En)function call S::= statement skip skip x=Eassignment S1;S2sequence if Ethen S1else S2if statement x=sample(E0, f(E1, . . . , En)) sample observe(E0, f(E1, . . . , En)) observe P::= program model Smodel definition model S1;guide S2model and guide We assume that the constants of this language range over a set of values including booleans, integers, real numbers, immutable real-valued vectors, finite-length strings, and a special null value. We define V to be the set of all values. A program contains a finite set of program variables denoted by x,xi,y, or z. We further assume a set of built-in functions g. We assume that functions gare total and return null for erroneous inputs. The only non-standard construct in the language are sample and observe statements. For these statements, the expression E0corresponds to the user-defined sample address, which is assumed to evaluate to a string. The symbol franges over a set of built-in distributions which are parameterised by arguments E1, . . . , En. 1.2 Semantics The meaning of a program is the density implicitly defined by its sample and observe statements. This density is evaluated for a program trace and returns a real number. A program trace is a mapping from finite-length addresses to numeric values, tr :Strings → V. We denote the set of all traces with T. In a probabilistic context, the program density corresponds to the (unnormalised) joint probability density of latent and observed variables. Thus, observe statements are semantically equivalent to sample statements but serve a purpose for static analyses. For a statement Sthe density will be defined in terms of operational semantics of the control-flowgraph of Sin the next section. The model density is the density defined by the statement Sin model S and the guide density is the density defined by the statement Sin guide S. 1 1.3 Control-Flow-Graph Before defining the operational semantics of a control-flow-graph (CFG) we first state the translation rules of a statement Sto a CFG. The following construction is fairly standard but necessary for formally verifying the correctness of the static analyses. A CFG has five types of nodes: start, end, assign, branch, and join nodes. Branch nodes have two successor nodes, end nodes have no successor, all other nodes have one. The CFG contains exactly one start node from which every other node is reachable. Further, it contains exactly one end node that is reachable from any other node. We describe the recursive translation rules for program Sboth mathematically and as diagrams. Sub-graphs are drawn by circular nodes, branch and join nodes are drawn as diamond nodes, and assign, start, and end nodes have rectangular shape. In text, branch nodes are written as Branch(E). Assignment and sample nodes are denoted with Assign(x=E) and Assign(x=sample(E0, . . . ) ), respectively. The observe statement observe(E0, f(E1, . . . , En)) is equivalent to _ =sample(E0, f(E1, . . . , En)) and is ommited in the following. •The CFG of a skip-statement, S=skip, consists of only start and end node. START END •The CFG of an assignment, x=E, or sample statement x=sample(E0, f(E1, . . . , En)), is a sequence of start, assign, and end node: START x=EEND START x=sample(E0, f(E1, . . . , En)) END •The CFG for a sequence of statements, S=S1;S2, is recursively defined by the CFGs G1and G2 of S1and S2respectively. START G1G2END The resulting CFG can be written as G= (G1∪G2)\ {N1 end, N2 start}, with Nstart =N1 start, Nend =N2 end,predecessor(N1 end)→successor(N2 start), where Ni start is the start node of Giand Ni end is the end node of Gi. •The CFG of an if statement, S= (if Ethen S1else S2), is also defined in terms of the CFGs of S1and S2 START E G1 G2 END consequent alternative The resulting CFG can be written as G=G1\ {N1 start, N1 end} ∪ G2\ {N2 start, N2 end}∪{Nstart, Nend, Nbranch, Njoin},where Nbranch =Branch(E), Nstart →Nbranch, Njoin →Nend, Nbranch →successorG1(N1 start) =:consequent(Nbranch), Nbranch →successorG2(N2 start) =:alternative(Nbranch), predcons(Njoin):=predecessorG1(N1 end)→Njoin, predalt(Njoin):=predecessorG2(N2 end)→Njoin. Above, we have also introduced some additional labels for the successors of branch nodes and predecessors of join nodes. Furthermore, we say the tuple (Nbranch, Njoin)is a brain-join pair and define BranchJoin(G)to be the set of all branch-join pairs of G. Definition 1. Let Sbe a statement and Gits CFG. We define a function CFGNode(.)that maps some sub-statements and sub-expressions of Sto a node in the CFG. Assignment sub-statements S′=x=E and sub-expressions of Eare be mapped to the assign node CFGNode(S′) = Assign(x=E′). Sample sub-statements S′=x=sample(E0, f(E1, . . . , En)) as well as the sub-expressions of Eiare mapped to the assign node Assign(x=sample(E0, ...) ). Sub-expressions of Ein if ( if Ethen ... ) or while (while Edo ... ) statements are mapped to the branch node Branch(E). 2 1.3.1 CFG Semantics For a control-flow-graph G, we define the small-step operational semantics for a trace tr as a relation that models the transition from node to node depending on the current program state: (σ, N)tr −→ (σ′, N′) The program state σ∈Σis a finite map from program variables to values σ::= x17→ V1, . . . , xn7→ Vn, xidistinct, Vi∈ V. The transition rules depending on node type and program state are given below: N=START N′=successor(N) (σ, N)tr −→ (σ, N′) N=Assign(x=E)N′=successor(N) (σ, N)tr −→ (σ[x7→ σ(E)], N′) N=Join N′=successor(N) (σ, N)tr −→ (σ, N′) N=Branch(E)σ(E) = true (σ, N)tr −→ (σ, consequent(N)) N=Branch(E)σ(E) = false (σ, N)tr −→ (σ, alternative(N)) Above, σ[x7→ V]denotes the updated program state σ′, where σ′(x) = Vand σ′(y) = σ(y)for all other variables y=x. At sample statements, we inject the value of the trace at address V0. We multiply the density, represented by the reserved variable p, with the value of function pdffevaluated at tr(V0). Note that the function pdffmay be an arbitrary function to real values. However, in the context of probabilistic programming we interpret it as the density function of distribution fwith values in R≥0. Lastly, the value tr(V0)is stored in the program state at variable x. The semantics of sample statements are summarised in the following rule: N=Assign(x=sample(E0, f(E1, . . . , En)) ) N′=successor(N) ∀i:σ(Ei) = Vi∧Vi=null V0∈Strings V=tr(V0)∧V=null (σ, N)tr −→ (σ[x7→ V, p7→ σ(p)×pdff(V;V1, . . . , Vn)], N′) Again, the semantics of observe(E0, f(E1, . . . , En)) are equivalent to _ =sample(E0, f(E1, . . . , En)) . Finally, the meaning of a CFG is a mapping from trace to density. It is defined for traces tr if there exists a path of node transitions from start to end node. Definition 2. Let σ0= (xi7→ 0,p7→ 1) be the initial program state. The semantics of a CFG Gis the function pG:T → R≥0given by pG(tr):=     σ(p)if ∃σ∈Σ, n ∈N:∀i= 1, .. . , n:∃σi, Ni: (σ0,START)tr −→ . . . tr −→ (σi, Ni)tr −→ . . . tr −→ (σ, END) undefined otherwise. Non-termination and errors are modelled implicitly: If there is an error or if the program does not terminate, then there is no finite sequence of node transition from start to end node. Next, we introduce some ubiquitously useful concepts. Definition 3. For a CFG G, let AssignNodes(G, x)be all nodes N′in Gthat assign variable x,N′= Assign(x=. . . ). The set of reaching definitions for variable xin node Nare defined as RD(N, x) = {N′∈AssignNodes(G, x) : ∃path (N′, . . . , Ni, . . . , N), Ni/∈AssignNodes(G, x)}. Intuitively, the set of reaching definitions are all nodes that could have written the value of xin the program state before executing node N. Definition 4. For CFG Gand node Nthe set of branch parents is defined as BP(N) = {B: (B, J)∈BranchJoin(G)∧ ∃ path (B, . . . , N, . . . , J)}. A branch node Band join node Jare a branch-join pair (B, J)∈BranchJoin(G)if they belong to the same if-statement (see the translation rule for if-statements to CFGs). The set of branch parents are all parent branch nodes of Nthat determine if the program branch of Nis executed. Lastly, we need the set of all strings that the address expression of a sample statement may evaluate to. 3 Definition 5. For a sample statement S=x=sample(E0, f(E1, . . . , En)) , we define the set of all possible addresses as addresses(S) = {σ(E0) : σ∈Σ} ⊆ Strings. For N=Assign(S)we define addresses(N) = addresses(S). Definition 6. The set of variables of an expressions is given recursively by vars(c) = ∅ vars(x) = {x} vars(g(E1, . . . , En)) = vars(E1)∪ · · · ∪ vars(En) Definition 7. The set of variables read in an expression, assignment statement, or sample statement is defined as vars_read(E) = vars(E) vars_read(x=E) = vars(E) vars_read(x=sample(E0, f(E1, . . . , En)) ) = vars(E0)∪ · · · ∪ vars(En) 1.4 Provenance and Evaluation Functions As described in the previous section, when encountering sample nodes in the CFG, the operational semantics inject values tr(α)of trace tr at a certain address α. Since the CFG is acyclic, we can determine the value of each program variable at each node in terms of values in tr. We will construct evaluation functions VN x:T → V that exactly compute the value of variable xbefore executing node N for all traces tr. For the subsequent static analyses, it is important to know which addresses this value depends on. We call this set of addresses provenance and denote it with prov(N, x). In Figure 1, you can see an example of evaluation functions and provencance sets. In Algorithm 1, we formally define provenance sets and in Lemma 4 we define the evaluation functions. b = sample("b",Bernoulli(0.5)) s = sample("s",InverseGamma(1.,1.)) if b == 1 then m = sample("mu",Normal(0.,1.)) else m = 1 x = sample("x",Normal(m, s)) N=Assign(x=. . . ) VN s(tr) = tr("s") VN m(tr) = δtr("b")·tr("mu") + (1 −δtr("b"))·1 START b = ... s = ... b == 1 m = 1 m = ... x = ... END RD(m)RD(m) RD(s) BP BP RD(b) prov(m) = {"b", "mu"} prov(s) = {"s"} Figure 1: Reaching definitions, branch parents, and the provenance set for a simple example. The evaluation functions are also given for node N. Lemma 1. Let Nbe a CFG Node and xa variable. prov(N, x)has following properties: •For all other nodes N′it holds that RD(N, x) = RD(N′, x) =⇒prov(N, x) = prov(N′, x).(1) •If N′∈RD(N, x)is an assignment node, N′=Assign(x=E), then prov(N′, E) = Sy∈vars(E)prov(N′, y)⊆prov(N, x).(2) •if N′∈RD(N, x)is a sample node, N′=Assign(x=sample(E0, . . . )), then prov(N′, E0)⊆prov(N, x)and addresses(N′)⊆prov(N, x).(3) •For all N′∈RD(N, x)it holds that for all branch parents Nbp =Branch(ENbp )∈BP(N′)we have prov(Nbp, ENbp )⊆prov(N, x)and SNbp∈BP(N′)prov(Nbp, ENbp ) = SNbp∈BP(N′)Sy∈vars(ENbp )prov(Nbp, y)⊆prov(N, x).(4) 4 Proof. If (N′, y)is pushed into the queue, then prov(N′, y)⊆prov(N, x)as the algorithm for computing prov(N′, y)starts with only (N′, y)in the queue. With this fact the properties follow directly from the definition of the algorithm. Algorithm 1 Computing the provenance set prov(N, x)statically from the CFG. 1: Input CFG node N, variable x 2: prov ← ∅ 3: queue ←[(N, x)] 4: while queue.is_not_empty() do 5: (N, x)←queue.pop() 6: for N′∈RD(N, x)do 7: if N′=Assign(x=sample(E0, f(E1, . . . , En)) ) then 8: prov ←prov ∪addresses(N′) 9: E′←E0▷ E0comes from pattern-matching N′ 10: else if N′=Assign(x=E)then 11: E′←E ▷ E comes from pattern-matching N′ 12: for y∈vars(E′)do 13: if is_unmarked((N′, y))then 14: mark((N′, y)) 15: queue.push((N′, y)) 16: for Nbp ∈BP(N′)do ▷ Nbp =Branch(ENbp ) 17: for y∈vars(ENbp )do 18: if is_unmarked((Nbp, y))then 19: mark((Nbp, y)) 20: queue.push((Nbp, y)) 21: return prov Recall that the purpose of finding the provenance of variable xat node Nis to determine which addresses contribute to the computation of its value. To prove that Algorithm 1 indeed finds the correct set of addresses, first, we have to precisely defined what we mean that a set of addresses contribute to the computation. Suppose that there is a function fthat maps a trace tr to a value v. The set of addresses Acontribute to the computation of value v, if any other trace tr′that has the same values as tr for all addresses α∈A, gets mapped to the same value f(tr′) = v. In other words, if we change the trace tr at an address β∈Strings \A, the value of f(tr)remains unchanged. Or equivalently, if f(tr)=f(tr′), then there must be an address α∈Asuch that tr(α)=tr′(α). Definition 8. For a function from traces to an arbitrary set B,f:T → B, we write f∈[T |A→B], for a subset of addresses A⊆Strings, if and only if ∀α∈A:tr(α) = tr′(α) =⇒f(tr) = f(tr′). That is, changing the values of tr at addresses β∈Strings \Adoes not change the value f(tr). The next lemma states that we can always over-approximate the set of addresses that contribute to the computation of the values f(tr). Lemma 2. If A⊆A′and f∈[T |A→B], then f∈[T |A′→B]. In other words, A⊆A′=⇒[T |A→B]⊆[T |A′→B].(5) Proof. Let f∈[T |A→B]. Assume ∀α∈A′:tr(α) = tr′(α). In particular, this holds for the smaller set A,∀α∈A:tr(α) = tr′(α), which implies f(tr) = f(tr′). Thus, f∈[T |A′→B]. If we combine two functions with provenance A1and A2respectively, then the resulting function has provenance A1∪A2. This is shown in the following lemma. Lemma 3. Let f1∈[T |A1→B1],f2∈[T |A2→B2],h:B1×B2→C. Then tr 7→ h(f1(tr), f2(tr)) ∈[T |A1∪A2→C]. Proof. Assume ∀α∈A1∪A2:tr(α) = tr′(α). Thus, fi(tr) = fi(tr′)and h(tr) = h(tr′). This brings us to the main soundness proof of Algorithm 1. Lemma 4 states that we can equip each CFG node Nwith evaluation functions that depend on the addresses determined by prov in the sense of Definition 8. The evaluation functions directly map the trace tr to the values of variables at node Nsuch that the values agree with the small-step CFG semantics relation tr −→. Importantly, while the operational semantics are defined for each individual trace, the evaluation functions work for all traces. In Fig. 1, you can see concrete examples of these evaluation functions for a simple program. 5 Lemma 4. For each node Nin a acyclic CFG Gand variable x, there exists an evaluation function VN x∈[T |prov(N,x)→ V], such that for all traces tr with σ0= (xi7→ 0,p7→ 1) and execution sequence (σ0,START)tr −→ · · · tr −→ (σi, Ni)tr −→ · · · tr −→ (σl,END) we have σi(x) = VNi x(tr). Intuitively, VN xcomputes the value of xbefore executing N. These evaluation functions VN xcan be lifted to evaluation functions for expressions VN E: VN c(tr) = c, V N g(E1,...,En)(tr) = g(VN E1(tr), . . . , V N En(tr)). By Lemma 3, if VN y∈[T |prov(N,y)→ V]for all y∈vars(E), then VN E∈[T |prov(N,E)→ V]. Proof. Step 1. Defining VN xand proving VN x∈[T |prov(N,x)→ V]. We begin by defining VN xinductively by noting that every node N=START has exactly one predecessor except for join nodes which have two predecessors. Further, the CFG Gis a directed acyclic graph with a single root node which makes mathematical induction possible. Base case. For ((xi7→ 0,p7→ 1),START), let VSTART p(tr)=1and VSTART x(tr)=0for all variables x. We have VSTART x∈[T |∅→ V]. Induction step. Case 1. Let Nbe a node with single predecessor N′(Nis not a join node). We define VN xbased on the node type of N′, for which we make the induction assumption that the evaluation functions VN′ x∈[T |prov(N′,x)→ V]exist for all variables. •Case 1.1. N′is an assignment node, N′=Assign(z=E). Define VN y(tr) = (VN′ E(tr)if y=z VN′ y(tr)otherwise. By assumption VN′ y∈[T |prov(N′,y)→ V]for all yand thus, VN′ E∈[T |prov(N′,E)→ V]. For x=z, RD(N, x) = RD(N′, x)and by Eq. (1) we have prov(N, x) = prov(N′, x), implying that VN x∈[T |prov(N,x)→ V]. For x=z, RD(N, x) = {N′}since N′is the single predecessor of Nand assigns x. By Eq. (2) prov(N′, E)⊆prov(N, x), and by Eq. (5) VN x=VN′ E∈[T |prov(N′,E)→ V]⊆[T |prov(N,x)→ V]. •Case 1.2. N′is a sample node, N′=Assign(z=sample(E0, f(E1, . . . , En)) ). Define VN y(tr) = (tr(VN′ E0(tr)) if y=z VN′ y(tr)otherwise. As before, for x=z,VN x∈[T |prov(N,x)→ V]. For x=z, by definition VN′ E0(tr)∈addresses(N′). Since N′∈RD(N, x)it follows from Eq. (3) that addresses(N′)⊆prov(N, x)and prov(N′, E0)⊆prov(N, x). Lastly, by Eq. (5) VN x∈[T |addresses(N′)∪prov(N′,E0)→ V]⊆[T |prov(N,x)→ V]. •Case 1.3. N′is a branch or join node. Define VN y=VN′ yfor all variables y. 6 Case 2. Let Jbe a join node with two predecessor nodes, N′ 1=predcons(J),N′ 2=predalt(J). Let B=Branch(E)be the corresponding branching node, (B, J)∈BranchJoin(G). For each variable x, there are two cases: 1. There exists a reaching definition N′∈RD(J, x)on a path (B, . . . , N′, . . . , J). Define V1 xand V2 x depending on the node type of N′ 1and N′ 2as in step 1. The functions Vi xcompute the value of x after executing N′ i. As before one can see that Vi x∈[T |prov(J,x)→ V]. Let VJ x(tr) := ife(VB E(tr), V 1 x(tr), V 2 x(tr)) = (V1 x(tr)if VB E(tr) = true, V2 x(tr)otherwise. Since B∈BP(N′), by Eq. (4) prov(B, E)⊆prov(J, x)and thus VJ x∈[T |prov(J,x)→ V]. 2. All reaching definitions of x(if there are any) are predecessors of B. Then, RD(J, x) = RD(B, x) and by Eq. (1) prov(J, x) = prov(B, x). Define VJ x:= VB x. Step 2: Proving that σi(x) = VNi x(tr). Having defined the evaluation functions, we now have to prove that they indeed compute the correct values. For trace tr let the corresponding execution sequence be (σ0,START)tr −→ · · · tr −→ (σi, Ni)tr −→ · · · tr −→ (σl,END). We will prove that σi(x) = VNi x(tr)by induction. Base case. The base case immediately follows from the definition σ0(x) = VSTART x(tr). Induction step. For transition (σi, Ni)tr −→ (σi+1, Ni+1)the assumption is that σj(x) = VNj x(tr) holds for all variables xand j≤i. If Ni+1 is not a join node, then σi+1(x) = VNi+1 x(tr)follows directly from the CFG semantics and definition of VNi+1 xin case 1 of step 1. Lastly, we consider the case when Ni+1 is a join node with branching node Nj=Branch(E), (Nj, Ni+1)∈BranchJoin(G), for some j≤i. Let N′ 1=predcons(Ni+1),N′ 2=predalt(Ni+1). By the semantics of if statements, VB E(tr) = true iff Ni=N′ 1and VB E(tr) = false iff Ni=N′ 2. If there is a node N′between Njand Ni+1 in the execution sequence that assigns x,N′∈RD(Ni+1, x), then by definitions of V1 x,V2 x, and VNi+1 xwe have σi+1(x) = ife(VB E(tr), V 1 x(tr), V 2 x(tr)) = VNi+1 x(tr). If there is no such N′, then σi+1(x) = σj(x) = VNj x(tr) = VNi+1 x(tr). 7 2 LASAPP API for SimpleProb In the following we formally define the LASAPP API endpoints for SimpleProb. We refrain from explicitly wrapping expressions or statements in the LASAPP SyntaxNode type to make the definitions less convoluted. API-Endpoint 1. For the SimpleProb programs P=model S1and P=model S1;guide S2, the get_model() API endpoint returns Model(S1). API-Endpoint 2. For the SimpleProb program P=model S1;guide S2, the get_guide() API endpoint returns Model(S2). API-Endpoint 3. For the SimpleProb programs P=model S1and P=model S1;guide S2, the get_random_variables() API endpoint collects statements in S1(and S2) of following form S=x=sample(E0, f(E1, . . . , En)) S=observe(E0, f(E1, . . . , En)) in the following structure RandomVariable(name: name,node: S, address_node: E0,is_observed: _, distribution=Distribution(name: namef,node: f(E1, . . . , En), params: [ DistributionParam(name: name1,node: E1), . . . DistributionParam(name: namen,node: En) ] ) ) where name is a unique name identifying Sand the names nameiare paramenter names depending on distribution f. For sample statements is_observed: false and for observe statements is_observed: true. API-Endpoint 4. Let SN be an expression, assignment statement, or sample statement with corresponding CFG node N=CFGNode(SN). The data dependencies of SN are given by {S:Assign(S)∈Sx∈vars_read(SN)RD(N, x)} The get_data_dependencies(SN) API endpoint returns this list without further structure as SyntaxNode objects. API-Endpoint 5. Let SN be an expression, assignment statement, or sample statement with corresponding CFG node N=CFGNode(SN). The control dependencies of SN are given by {E:Branch(E)∈BP(N)} The get_control_dependencies(SN) API endpoint returns this list in following structure ControlDependency(name: SE,control_node: E, kind: if,body: [SE 1, SE 2]) where SEis the encompassing if-statement of E:SE=if Ethen SE 1else SE 2. API-Endpoint 6. Let Ebe an expression with corresponding CFG node N=CFGNode(E). Let A={SNi7→ [ai, bi]}be a mask that maps sample statements and expressions to intervals. The estimate_value_range(E,A)endpoint returns the interval computed with estimate_interval(N, E, ˜ A) defined in Algorithm 4, where ˜ A={(CFGNode(SNi),SNi)7→ [ai, bi]}. API-Endpoint 7. Let P=model Sroot 1or P=model Sroot 1;guide Sroot 2and let Gibe the CFG of Sroot i. Let Ebe an expression with corresponding CFG node N=CFGNode(E)belonging to Gi with Ksample nodes Nk=Assign(Sk). Let A={SNi7→ sexpri}be a mask that maps sample statements and expressions to symbolic expressions. All sample statements Skin Gihave to be masked. The get_path_condition(E,Sroot i,A)API endpoint returns the symbolic expression computed with pc(N, ˜ A) defined in Algorithm 6, where ˜ A={(CFGNode(SNi),SNi)7→ sexpri}. 8 3 Statistical Dependency Analysis The implementation of the static dependency analysis in LASAPP is given below. With mark_processed we make sure that every dependency is only added to the queue once. 1dependencies = [] 2all_variables = program.get_random_variables() 3model = program.get_model() 4random_vars = filter(all_variables, model) 5for rv in random_vars: 6queue = [rv.address_node, rv.distribution.node] 7while len(queue) > 0: 8node = queue.popleft() 9data_deps = program.get_data_dependencies(node) 10 for dep in data_deps: 11 if not already_processed(dep): 12 if dep in random_vars: 13 dependencies.append((dep, rv)) 14 queue.append(dep.address_node) 15 else: 16 queue.append(dep) 17 mark_processed(dep) 18 control_deps = program.get_control_dependencies(node) 19 for dep in control_deps: 20 if not already_processed(dep.control_node): 21 queue.append(dep.control_node) 22 mark_processed(dep.control_node) Listing 1: Model graph extraction written in LASAPP. With API-Endpoint 4 and API-Endpoint 5 we can translate Listing 1 for SimpleProb in Algorithm 2. Algorithm 2 Model graph extraction translated for SimpleProb and single sample statement S 1: Input Sample statement S=x=sample(E0, f(E1, . . . , En)) 2: dependencies ←[ ] 3: queue ←[E0, f(E1, . . . , En)] 4: while queue.is_not_empty() do 5: SN ←queue.pop() 6: N←CFGNode(SN) 7: data_deps ← {S′:Assign(S′)∈Sy∈vars_read(SN)RD(N, y)} 8: for S′∈data_deps do 9: if is_unmarked(S′)then 10: if S′=x′=sample(E′ 0, f′(E′ 1, . . . , E′ n)) then 11: dependencies.push(S′) 12: queue.push(E′ 0) 13: else if S′=x′=E′)then 14: queue.push(S′) 15: mark(S′) 16: control_deps ← {E′:Branch(E′)∈BP(N)} 17: for E′∈control_deps do 18: if is_unmarked(E′)then 19: mark(E′) 20: queue.push(E′) 21: return dependencies Algorithm 2 is closely related to the provenance set defined in Algorithm 1. In fact, consider the sample statement S=x=sample(E0, f(E1, . . . , En)) with corresponding CFG node N=Assign(S). Let random_deps(S)be the dependencies computed with Algorithm 2. Then SS′∈random_deps(S)addresses(S′) = Sn i=0 prov(N, Ei)∪SN′∈BP(N)prov(N′, EN′)(6) This can be seen by noting that the only difference between the two algorithms is that Algorithm 1 collects directly the addresses while Algorithm 2 stores the nodes. Furthermore, in Algorithm 1 we push CFG nodes and individual variables yin the queue, whereas in Algorithm 2 we push entire statements or expressions in the queue. Lastly, the loop over branch parents is moved outside of the loop over reaching definitions in Algorithm 2. As a result, the branch parents of the input Nare also collected as dependencies. 9 Before stating the correctness result for the constraint verification static analysis, we prove the critical property of IN Ein following lemma. Lemma 9. For each node Nin the CFG Gand variable x, it holds that ∀tr ∈ T :pG(tr)>0 =⇒VN x(tr)∈IN x,or short VN x(T>0)⊆IN x(16) Proof. Base case. We have VSTART x(T>0) = {0} ⊆ [0,0] = ISTART xfor all variables x. Induction step. Case 1. Let Nbe a node with single predecessor N′(Nis not a join node). We make the induction assumption that VN′ x⊆IN′ xfor all variables x. •Case 1.1. N′is an assignment node, N′=Assign(z=E). Recall VN y(tr) = (VN′ E(tr)if y=z VN′ y(tr)otherwise. For x=z, RD(N, x) = RD(N′, x)and thus, VN x(T>0) = VN′ x(T>0)⊆IN′ x=IN x. For x=z, RD(N, x) = {N′}since N′is the single predecessor of Nand assigns x. As N′is an assignment node, VN x(T>0) = VN′ E(T>0)⊆IN′ E=IN x. •Case 1.2. N′is a sample node, N′=Assign(z=sample(E0, f(E1, . . . , En)) ). Recall VN y(tr) = (tr(VN′ E0(tr)) if y=z VN′ y(tr)otherwise. As before, for x=z,VN x=VN′ xand IN x=IN′ x. For x=z, by definition of the support of fwe have VN x(T>0) = support(f). Again, RD(N, x) = {N′}and VN x(T>0) = support(f)⊆IN x. •Case 1.3. N′is a branch or join node. We have VN y=VN′ yand IN y=IN′ yfor all variables y. Case 2. Let Jbe a join node with two predecessor nodes, N′ 1=predcons(J),N′ 2=predalt(J). Let B=Branch(E)be the corresponding branching node, (B, J)∈BranchJoin(G). First, consider the case when there exists a reaching definition N′∈RD(J, x)on a path (B, . . . , N′, . . . , J). If N′ i∈RD(J, x), then Vi x(T>0)⊆IJ xas before, where Vi xis defined as in step 1 with N′=N′ i. Otherwise, RD(N′ i, x)⊆RD(J, x) and Vi x=VN′ i x. By assumption VN′ i x(T>0)⊆IN′ i xand thus, we have again Vi x(T>0)⊆IN′ i x⊆IJ x. Recall that VJ x(tr) = ife(VB E(tr), V 1 x(tr), V 2 x(tr)) and so we also have VJ x(T>0)⊆IJ x. In the second case, there is no reaching definition on a path from B to Jand we have VJ x=VB x. Since also RD(J, x) = RD(B, x)we have again VJ x(T>0)⊆IJ x. Now we are ready to prove the soundness of the parameter constraint verifier. Proposition 3. Let P=model Sbe a SimpleProb program with numeric values restricted to scalars. In particular, only uni-variate random variables are allowed. For simplicity, we assume that these random variables have static support. If the analysis in Listing 4 produces no warnings, then Pis free of distribution parameter constraint violations in the following sense: Let Gbe the CFG of Sand let tr be a trace with following execution sequence in G: (σ0,START)tr −→ . . . tr −→ (σi, Ni)tr −→ . . . tr −→ (σ, END). If Ni=Assign(x=sample(E0, f(E1, . . . , En)) ) is a sample node with constraint Cf j= [aj, bj]for the j-th parameter of distribution f, then σi(Ej)∈Cf j. Proof. The mask collected in the beginning of Listing 4 is precisely A∗in Definition 9. Thus, for the parameter Ej(param.node) in sample node Ni=Assign(x=sample(E0, f(E1, . . . , En)) ), we have estimate_interval(Ni, Ej,A∗) = INi Ej. This interval is compared against Cf jin the static analysis. If there is no error then, INi Ej⊆Cf j. By the definition of evaluation functions and by Lemma 9, we have σi(Ej) = VNi Ej(tr)∈INi Ei j ⊆Cf j. 16 Note that the reverse implication in Proposition 3 does not hold, i.e. a program free of parameter constraint violations may still lead to warnings. Consider following program: b = sample("b",Gamma(1,1)) if b >= 0 then s = sample("s",Uniform(0.1,1)) else s = sample("s",Uniform(-1,0.1)) x = sample("x",Normal(0, s)) The value range of sis estimated with [−1,1] even though the alternative if-statement-branch is never taken, because bis always a positive number. Thus, sis always strictly greater than 0which is the constraint of the standard deviation parameter of a Normal distribution. However, a warning is produced. 17 6 Model-Guide Validation 1def get_dist_constraint(rv): 2props = lasapp.infer_distribution_properties(rv) 3a, b = Interval(props.support) 4X = SExpr(rv) 5return And(a < X, X < b) 6 7rvs = program.get_random_variables() 8P = program.get_model(); Q = program.get_guide(); 9# Q = program.get_model(); P = program.get_guide(); 10 P_rvs = ...; Q_rvs = ...; 11 12 A = {rv.node: SExpr(rv) for rv in rvs} # symbolic masks 13 pc = { 14 **{rv: program.get_path_condition(rv.node, P.node, A) 15 for rv in P_rvs}, 16 **{rv: program.get_path_condition(rv.node, Q.node, A) 17 for rv in Q_rvs} 18 } 19 20 dc = {rv: get_dist_constraint(rv) for rv in rvs} 21 22 impl = Implies( 23 And([Implies(pc[rv],dc[rv]) for rv in P_rvs]), 24 And([Implies(pc[rv],dc[rv]) for rv in Q_rvs]), 25 ) 26 if check(Not(impl)) == satisfiable: 27 raise Warning("Global absolute continuity violation ...") (W1) 28 29 # Extended checks (not included in main paper): 30 P_rvs_by_name = ...; Q_rvs_by_name = ...; 31 32 # following checks raise warnings if there are two sample statments 33 # with the same address in the same branch 34 check_disjointness(P_rvs_by_name, pc) (W2) 35 check_disjointness(Q_rvs_by_name, pc) (W2) 36 37 for name, P_stmts in P_rvs_by_name.items(): 38 Q_stmts = Q_rvs_by_name[name] 39 impl = Implies( 40 Or([And(pc[stmt],dc[stmt]) for stmt in P_stmts]), 41 Or([And(pc[stmt],dc[stmt]) for stmt in Q_stmts]) 42 ) 43 if check(Not(impl)) == satisfiable: 44 raise Warning("Absolute continuity violation for rv ...") (W3) Listing 5: Model-guide validation written in LASAPP. In Listing 5, you can find an extended version of the model-guide validator written in LASAPP. As this analysis heavily relies on symbolic evaluation of expressions, we start by introducing an algorithm for this purpose. In Algorithm 5, we have defined an algorithm to get a symbolic expression for the value of the syntactic expression Ein CFG node N, where certain expression in certain CFG nodes may be replaced with a pre-specified symbolic expression stored in the map A. In this definition, the symbolic counterpart of a function gis denoted with gand symbolic variables are denoted with SymVar(α)where α∈Strings. In the next definition, we introduce the notion of symbolic evaluation. Definition 10. The evaluation JsexprK(tr)of a symbolic expression sexpr at trace tr is computed by replacing all SymVar(α)with tr(α), i.e. JSymVar(α)K(tr) = tr(α),Jg(sexpr1,...,sexprn)K(tr) = g(Jsexpr1K(tr),...,JsexprnK(tr)). Algorithm 5 allows to mask certain syntactic expression and sample statements with an symbolic expression. Therefore, this algorithm can be used for many purposes. However, the get_path_condition endpoint is used in Listing 5, such that all sample statements are masked with a symbolic variable. To simplify the subsequent proofs, we introduce a special short-hand for this type of symbolic evaluation. Definition 11. Let A∗be the mask that maps sample nodes with static addresses to their symbolic variable, i.e., for N′=Assign(S′)and S′=x=sample(α, f(E1, . . . , En)) we define A∗[(N′, S′)] = SymVar(α). For each CFG node Nand expression E, let SN E=symbolic(N, E, A∗). 18 Algorithm 5 symbolic(N, E, A) 1: Input CFG node N, expression E, mask A 2: if (N, E)is masked in Athen 3: return A[(N, E)] 4: if E=cthen 5: sexpr ←c 6: else if E=g(E1, . . . , En)then 7: sexpr ←g(symbolic(N, E1,A),...,symbolic(N, En,A)) 8: else if E=xthen 9: if Nis the start node then 10: sexpr ←0 11: else if Nis a not join node then 12: N′←parent(N) 13: if N′=Assign(S′)and S′=x=sample(α, f(E1, . . . , En)) then 14: assert (N′, S′)is masked in A 15: sexpr ← A[(N′, S′)] ▷A[(N′, S′)] = SymVar(α) 16: else if N′=Assign(x=E′)then 17: sexpr ←symbolic(N′, E′,A) 18: else ▷ N′is a branch, join, or start node; or N′is assign node for variable different from x 19: sexpr ←symbolic(N′, x, A) 20: else ▷ N is a join node 21: N1←predcons(N) 22: N2←predalt(N) 23: B←branchnode(N)▷(B, N)∈BranchJoin(G) 24: Compute s1for N′=N1as in lines 13-19 25: Compute s2for N′=N2as in lines 13-19 26: sb←symbolic(B, EB)▷ B =Branch(EB) 27: sexpr ←ife(sb, s1, s2) 28: return sexpr With this special mask A∗, we can establish following crucial lemma. Lemma 10. For each CFG node Nand expression Eit holds that for all traces tr JSN EK(tr) = VN E(tr).(17) Proof. It is straightforward to see that the construction of SN Ein Algorithm 5 is equivalent to the construction of VN Ein Lemma 4. Algorithm 6 pc(N, A) 1: Input Node N, mask A 2: pc ←true 3: for N′∈BP(N)do ▷ N′=Branch(EN′) 4: if N′is in consequent branch of Nthen 5: pc ←pc ∧symbolic(N′, EN′,A) 6: else 7: pc ←pc ∧(¬symbolic(N′, EN′,A)) 8: return pc Finally, the algorithm for computing the symbolic path condition of a CFG node can be found in Algorithm 6. This completes the formal description of the get_path_condition endpoint and we are ready to prove the soundness of the model-guide validator. Proposition 4. Let P=model Sroot 1;guide Sroot 2be a SimpleProb program with numeric value restricted to scalars. In particular, only uni-variate random variables are allowed. For simplicity, we assume that these random variables have static support. Let GPbe the CFG of Sroot 1and GQbe the CFG of Sroot 2. Let pGPbe the model density and pGQthe guide density. If the analysis in Listing 5 produces no warnings at the line marked with (W1), then pGP≪pGQ, i.e. pGP(tr)>0 =⇒pGQ(tr)>0. If there are no warnings produced at (W2) and (W3), then executing a sample statement with address αin GPimplies executing a sample statement with the same address in GQ. 19 Proof. First, let Nk=Assign(xk=sample(αk, fk(Ek 1, . . . , Ek nk)) ) be all sample nodes in GP. From Proposition 1, we know that pGP(tr) = QK k=1 pk(tr)with pk(tr) = δbk(tr)pdffktr(αk); VNk Ek 1 (tr), . . . , V Nk Ek nk (tr)+ (1 −δbk(tr)). Thus, pGP(tr)>0⇐⇒ ∀k:bk(tr) = true =⇒tr(αk)∈support(fk). Recall bk(tr) = VN′∈BP(Nk)tk N′VN′ EN′(tr)where tk N′(v) = vif Nkis in the consequent branch of N′and tk N′(v) = ¬vif Nkis in the alternate branch. Further, bk(tr) = true if Nkis in the execution sequence for tr else false. By comparing Algorithm 6 to this definition and noting that the mask collected on line 13 corresponds precisely to the mask A∗in Definition 11, we see that Jpc(Nk,A∗)K(tr) = bk(tr). Denote the (static) interval support of fkwith support(fk)=[ck, dk]. The symbolic distribution constraint obtained with get_dist_constraint is precisely ck<SymVar(αk)< dk. In summary, pc(Nk,A∗) =⇒(ck<SymVar(αk)< dk)is the symbolic equivalent of the condition bk(tr) = true =⇒tr(αk)∈support(fk). The analogous condition for the guide density can be constructed in the same way and in fact, the implication build on lines 23-26 is equivalent to ∀tr :pGP(tr)>0 =⇒pGQ(tr)>0. Therefore, raising no warning at the line marked with (W1) proves that pGP≪pGQ. However, for practical purposes pGP≪pGQas above is often not enough, since a guide program with no sample statements, pGQ(tr) = 1, trivially fulfills the absolute continuity condition for every model density. Thus, we also require that executing a sample statement with address αin the model implies executing a sample statement with address αin the guide. Producing no warnings at (W2) and (W3) asserts this requirement as we will show in the following. Since the analysis produces no warnings at (W2), we have that the path conditions for sample nodes with the same address are disjoint: αk1=αk2=⇒bk1(tr)∧bk2(tr)=false.(18) Further, define ψα P(tr) := _ k:αk=α (bk(tr) = true)∧(tr(α)∈support(fk)), ϕα P(tr) := ^ k:αk=α (bk(tr) = false). where Wk∈∅ ... =false and Vk∈∅ ... =true. If ψα P(tr) = true, then there is a sample statement with address αin the execution sequence for tr and tr(α)lies in the support of the corresponding distribution. If ϕα P(tr) = true, then there is no sample statement with address αin the execution sequence for tr. As an aside, from (18) it follows that pGP(tr)>0⇐⇒ ^ α∈AP ψα P(tr)∨ϕα P(tr), where AP={αk:k= 1, . . . , K}is the set of all unique addresses of sample statements in the model. Assume the same construction for the guide, ψα Qand ϕα Q. No warnings at (W3) implies that ∀tr :ψα P(tr) =⇒ψα Q(tr), which completes the proof. 20