feat (report): progress

doc/rep.typ

@@ -4,19 +4,20 @@
 
 #set text(size: 11pt)
 #set page(paper: "a4", numbering: "1")
-#set par(
-  justify: true,
-  // first-line-indent: 10pt
-)
-#set raw(
-  syntaxes: "zelus.sublime-syntax",
-  // theme: none,
-)
-// #show raw: set text(font: "CaskaydiaCove NF")
-#set cite(style: "alphanumeric.csl")
-#set heading(numbering: "1.1")
 
-#set figure(gap: 20pt, placement: top)
+#set cite(style: "alphanumeric.csl")
+
+#set par(justify: true)
+#set par.line(numbering: "1")
+
+#set raw(syntaxes: "zelus.sublime-syntax")
+#show raw: set par.line(numbering: none)
+
+#set heading(numbering: "1.1")
+#show heading: set par.line(numbering: none)
+
+#set figure(placement: top)
+#show figure: set par.line(numbering: none)
 
 #let zelus    = smallcaps[Zélus]
 #let lustre   = smallcaps[Lustre]
@@ -33,7 +34,8 @@
 #let DNodeC   = math.italic[DNodeC]
 #let CNode    = math.italic[CNode]
 #let HNode    = math.italic[HNode]
-#let HNodeA   = math.italic[HNodeA]
+#let ANode    = math.italic[ANode]
+#let ASNode   = math.italic[ASNode]
 #let Dense    = math.italic[Dense]
 #let IVP      = math.italic[IVP]
 #let ZCP      = math.italic[ZCP]
@@ -61,6 +63,7 @@
 } else []
 #let todo(body) = note(color: rgb(255, 0, 0, 50), prefix: "TODO: ")[#body]
 
+#set par.line(numbering: none)
 #align(center)[
   #text(16pt)[
     *Internship Report --- MPRI M2 \
@@ -69,6 +72,7 @@
 
   Henri Saudubray, supervised by Marc Pouzet, Inria PARKAS
 ]\
+#set par.line(numbering: "1")
 
 // #heading(outlined: false, numbering: none)[General Context]
 // What is the report about? Where does the problem come from? What is the state
@@ -152,7 +156,10 @@ _à la_ #haskell, but the addition of typeclasses into the type system of #zelus
 is a problem of its own.
 
 #pagebreak()
+#pagebreak()
+#set par.line(numbering: none)
 #outline()
+#set par.line(numbering: "1")
 
 = Introduction <sec:introduction>
 
@@ -199,8 +206,6 @@ program written in the synchronous kernel to be considered independently of its
 physical implementation. Nothing in this representation tells us anything about
 how much physical time passes between successive instants.
 
-#note[Should we give a precise definition of the kernel?]
-
 The programs expressed in this kernel, called _discrete nodes_, are functions on
 streams. At each time instant, given inputs $I$, they produce outputs $O$.
 Producing these outputs may also depend on previously computed values through
@@ -223,18 +228,17 @@ instant.
 ]
 
 Since programs may wish to reset the state of a node (for instance, when writing
-automata), nodes also define a reset function $f_"reset" : S -> R -> S$. Since
+automata; further motivation will be given in the following sections), nodes
-nodes may be parameterized by a value, this reset function takes in an
+also define a reset function $f_"reset" : S -> R -> S$. Since nodes may be
-additional reset parameter $R$ and the previous state, and returns an updated
+parameterized by a value, this reset function takes in an additional reset
-state. A discrete model with input $I$ and output $O$ is then a triple of an
+parameter $R$ and the previous state, and returns an updated state. A discrete
-initial state, and a step and reset function:
+model with input $I$ and output $O$ is then a triple of an initial state, and a
-
+step and reset function:
-#todo[Justify resets. Why not $R$ in $f_"step"$?]
 
 $ DNode(I, O, R, S) eq.def {
     s_0 : S;
     f_"step" : S -> I -> O times S;
-    f_"reset" : S -> R -> S;
+    f_"reset" : S -> R -> S
   } $
 
 The simulation of such a model then defines two streams: the inner state $s$ and
@@ -244,16 +248,15 @@ $ DSim(M)(i_n) = o_n "where"
     (o_n, s_(n+1)) = M.f_"step" (i_n, s_n), s_0 = M.s_0 $
 
 A possible implementation of this simulation in #ocaml, where streams are
-represented by lists of values, is given in @lst:discrete_sim.
+represented by lists of values, is given in @lst:discrete_sim #footnote[
-
+  Due to space concerns, #ocaml type definitions are ommitted from the main body
-#todo[Make figures stand out more.]
+  of the report, and are instead given in @sec:appendix, @lst:ocaml_typedefs.
+  These type definitions are direct translations of the mathematical definitions
+  into #ocaml.
+].
 
 #figure(
   ```ocaml
-  (** Discrete model representation. *)
-  type ('a, 'b, 'r, 's) dnode =
-    DNode of { s0 : 's; step : 's -> 'a -> 'b * 's; reset : 's -> 'r -> 's }
-
   (** Run a model on a list of inputs. *)
   let dsim (DNode model) input =
     let rec run s = function
@@ -369,7 +372,7 @@ two functions:
 ]
 
 $ CNode(I, O, S, S') eq.def
-    { s_0: S; f_"der": I -> S -> S'; f_"out": I -> S -> O; } $
+    { s_0: S; f_"der": I -> S -> S'; f_"out": I -> S -> O } $
 
 For instance, the model of @lst:sincos_discrete can be expressed in continuous
 time as seen in @lst:sincos_continuous. Here, `sin` and `cos` are expressed
@@ -562,16 +565,6 @@ implementation in #ocaml is given in @lst:continuous_sim.
 
 #figure(
   ```ocaml
-  (** Continuous model. *)
-  type ('i, 'o, 's, 'sder) cnode =
-    CNode of { s0: 's; fder: 'i -> 's -> 'sder; fout: 'i -> 's -> 'o }
-  (** Dense values. *)
-  type 'a dense = { h : time; u : time -> 'a }
-  (** Initial value problem. *)
-  type ('y, 'yder) ivp = { y0 : 'y; f : time -> 'y -> 'yder; h : time }
-  (** ODE solver. *)
-  type ('y, 'yder, 's) csolver = (time, 'y dense, ('y, 'yder) ivp, 's) dnode
-
   (** Simulation of a continuous model, as a discrete node. *)
   let csim (CNode model) (DNode solver) =
     let s0 = (None, model.s0, solver.s0) in
@@ -724,7 +717,6 @@ $ HNode(I, O, R, S, Y, Y', Zi, Zo) eq.def {
     f_"horizon" : S -> Time;
     f_"jump" : S -> BB
 } $
-#todo[This definition is ugly.]
 
 #zelus provides several ways to specify zero-crossing events, of which the
 ```zelus up(e)``` construct is the most common. It monitors its subexpression
@@ -903,38 +895,19 @@ A possible implementation of the discrete step in #ocaml is given in
 
 #figure(
   ```ocaml
-  (** Simulation mode.  *)
-  type mode = Discrete | Continuous | Idle
-  (** Simulation state. *)
-  type ('i, 'sm, 'ss) sim_state =
-    { sm: 'sm; ss: 'ss; mode: mode; r : bool; i: 'i dense option; now: time }
-  (** Zero-crossing problem. *)
-  type ('y, 'zo) zcp = { f : time -> 'y -> 'zo; y0 : 'y }
-  (** Hybrid model. *)
-  type ('i, 'o, 'r, 's, 'y, 'yd, 'zi, 'zo) hnode = HNode of {
-    s0 : 's; cget : 's -> 'y; cset : 's -> 'y -> 's; zset : 's -> 'zi -> 's;
-    horizon : 's -> time; jump : 's -> bool; step : 's -> 'i -> 'o * 's;
-    fder : 's -> 'i -> 'y -> 'yd; fzer : 's -> 'i -> 'y -> 'zo;
-    fout : 's -> 'i -> 'y -> 'o; reset : 's -> 'r -> 's;
-  }
-
   let dstep (HNode model) (DNode solver) state =
     let i = Option.get state.i in
     let (o, sm) = model.step state.sm (i.u state.now) in
-    let out = { u=(fun _ -> out); h=0.0 } in
     let state =
-      let h = model.horizon sm in
+      if model.horizon sm <= 0 then { state with sm }
-      if h <= 0 then { state with sm }
       else if state.now >= i.h then { state with mode=Idle; i=None; sm }
       else if model.jump sm || state.r then (* Reset solver. *)
-        let fder t y = model.fder sm (i.u t) y in
+        let ivp = { h=i.h; y0=model.cget sm; f=fun t y -> model.fder sm (i.u t) y } in
-        let fzer t y = model.fzer sm (i.u t) y in
+        let zcp = { y0=model.cget sm; f=fun t y -> model.fzer sm (i.u t) y } in
-        let ivp = { f=fder; h=i.h; y0=model.cget sm } in
-        let zcp = { f=fzer; y0=model.cget sm } in
         let ss = solver.reset (ivp, zcp) state.ss in
         { state with mode=Continuous; sm; ss; r=false }
       else { state with mode=Continuous; sm } in
-    (Some out, state)
+    (Some { h=0.0; u=fun _ -> o }, state)
   ```,
   caption: [Discrete simulation step in #ocaml]
 ) <lst:sim_step_discrete>
@@ -1014,16 +987,16 @@ Its implementation in #ocaml is given in @lst:sim_algorithm.
 #figure(
   ```ocaml
   let hsim (HNode model) (DNode solver) =
-    let s0 = { mode=Idle; i=None; now=0.0; ss=model.s0; ss=solver.s0; r=true } in
+    let s0 = { mode=Idle; i=None; now=0.0; sm=model.s0; ss=solver.s0; r=true } in
     let step state i = match (i, state.mode) with
       | Some _, Idle ->
           let state =  { state with mode=Discrete; i; now=0.0; r=true } in
           dstep (HNode model) (DNode solver) state
       | None, Discrete -> dstep (HNode model) (DNode solver) state
       | None, Continuous -> cstep (HNode model) (DNode solver) state
-      | None, Idle -> (None, state) in
+      | None, Idle -> (None, state)
-      | Some _, _ -> assert false
+      | Some _, _ -> assert false in
-    let reset r state =
+    let reset state r =
       { state with mode=Idle; sm=model.reset r state.sm; r=true } in
     DNode { s0; step; reset }
   ```,
@@ -1162,16 +1135,6 @@ instanciate and call a solver, this seems entirely feasible.
 
 = Hybrid Observers and Assertions <sec:hybrid_observers>
 
-#todo[
-  Describe assertions as a run-time defensive construct (as in #ocaml), and
-  their equivalent in #lustre: synchronous observers. Emphasize that the
-  synchronous subset does not cause any problem, since the observer has no
-  impact on its underlying model. Describe their naïve extension to continuous
-  time, and their unexpected impact on the behaviour of the continuous model:
-  recall the examples of Section 1.1. Conclusion: we need to simulate continuous
-  observers with their own solver.
-]
-
 During the design and implementation of software, programmers often use
 assertions in order to check certain properties, both before and during
 execution. In #ocaml, for instance, the ```ocaml assert``` instruction checks
@@ -1252,9 +1215,7 @@ simulation, as described in @sec:sim_algorithm.
 
   let hybrid f (*...*) =
     let v = (*...*) in
-    (present(assertion_f(v)) ->
+    (present(assertion_f(v)) -> print_endline "ERROR" else ());
-       print_endline "ERROR"
-     else ());
     (*...*)
   ```,
   caption: [A naïve implementation of a continuous observer.]
@@ -1274,26 +1235,18 @@ with its own ODE solver.
 
 == Models With Assertions <sec:models_with_assertions>
 
-#todo[
-  Since we are able to transform a hybrid model into a discrete one (albeit with
-  a complicated type), we can isolate parts of a model in order to simulate them
-  with a dedicated solver, and provide the obtained stream as input to another
-  hybrid model simulation, which performs the assertion on this precomputed
-  solution. This gives rise to a new datatype for a model together with its
-  assertions.
-]
-
 Since an assertion can be considered as a separate model operating on the inner
 state of its parent model, we can represent a model with assertions as a pair
 of the parent model $m$, operating on its inner state $S_M$, and a list of
 assertion models. All assertions operate on the same input datatype $S_M$ (the
 state of the parent model) and return Boolean output signals $BB$.
 
-$ HNodeA(I, O, R, S_M, Y, Y', Zi, Zo) eq.def {
+$ ANode(I, O, R, S_M, Y, Y', Zi, Zo) eq.def {
-  & m : HNode(I, O, R, S_M, Y, Y', Zi, Zo); \
+    & m : HNode(I, O, R, S_M, Y, Y', Zi, Zo); \
-  & a : List(HNodeA(S_M, BB, R_A, S_A, Y_A, Y'_A, Zi_A, Zo_A)) } $
+    & a : List(ANode(S_M, BB, R_A, S_A, Y_A, Y'_A, Zi_A, Zo_A))
+  } $
 
-Note that the output signal is Boolean even in continuous time. There are
+Note <t> that the output signal is Boolean even in continuous time. There are
 two possible interpretations of this: either assertions benefit from relaxed
 typing rules for their output, and are allowed a limited subset of discrete
 behaviours in continuous time; or assertions in continuous time are defined in
@@ -1301,23 +1254,92 @@ terms of zero-crossing events, and as such the output of the assertion will be
 constant during continuous phases (in fact, the output will be constantly true,
 as the simulation would not have entered a continuous step otherwise). Both
 interpretations lead to the same updated simulation algorithm, as we will see in
-@sec:updated_sim.
+@sec:updated_sim. The $ANode$ datatype is recursive: indeed, nothing prevents
+assertions from containing their own assertions, and so on and so forth.
 
-The $HNodeA$ datatype is recursive: indeed, nothing prevents assertions from
+#todo[Clarify why Boolean values as output is surprising.]
-containing their own assertions, and so on and so forth.
+
+While this representation allows for a lot of expressivity, in most cases, a
+model with a single assertion suffices. Multiple assertions may be combined as
+a single one by simply taking the conjunction of their outputs, and nested
+assertions (assertions within assertions) can be checked as part of the
+simulation of their parents. We can then define a simpler datatype
+
+$ ASNode(I, O, R, S_M, Y, Y', Zi, Zo) eq.def {
+    & m : HNode(I, O, R, S_M, Y, Y', Zi, Zo); \
+    & a : DNode(Signal(S_M), BB, R, S_A)
+  } $
+
+where the assertion is a single, discrete node operating on dense functions of
+the model state and returning Boolean values. During compilation, assertions are
+compiled down to hybrid models, and turned into discrete simulations using a
+variant of the `solve` function of @sec:lifting_runtime. This is the current
+target model of the #zelus compiler; however, simulations of both $ANode$ and
+$ASNode$ are implemented in the runtime.
 
 == Updated Simulation <sec:updated_sim>
 
-#todo[
+The simulation of a system with assertions requires little adjustments from the
-  Present a version of the simulation with assertions (probably the simple
+original simulation algorithm. The main difficulty resides in the fact that we
-  version with a single assertion, rather than the complex one with polymorphic
+need to construct a dense function of the entire parent model's state. For
-  recursion and such).
+discrete steps, this is simple: we build a constant function on the model's
-]
+state defined on the interval $[0, 0]$. For continuous steps, the ODE solver
+provides us with a dense function of the continuous part of the state. Since the
+discrete part of the state is constant during integration, we can  use the
+approximation returned by the solver, combined with the model's $c_"set"$
+function, to build a dense function of the entire state. We need to be careful,
+however: if the $c_"set"$ function rewrites the model's state in-place (this is
+the case in the code produced by the #zelus compiler), we must update the state
+back to its value at the horizon reached by the ODE solver before starting the
+next simulation step.
 
-#todo[
+The simulation state then stores a copy of the model's continuous state at the
-  Maybe present a high-level overview of the compilation passes? This seems a
+reached horizon after every continuous step. Before every step, we update the
-  little out of scope.
+model's state to ensure its correctness. Continuous steps now produce an
-]
+additional dense function of the state, which is used as input to the assertion.
+A step of the simulation then performs a step of the parent model, as seen in
+@sec:sim_algorithm, and uses the additional output to step the simulation of
+the assertion as often as needed for it to reach the model's reached time,
+checking the assertion's output at each step.
+
+The updated #ocaml implementation is given in @lst:sim_assert.
+
+#figure(
+  ```ocaml
+  let acstep (HNode model) (DNode solver) state =
+    let i = (*...*) in let stop = (*...*) in
+    let (({ h=now; u=dky }, z), ss) = solver.step state.ss stop in
+    let out = { h=now; u=fun t -> model.fout state.sm (i.u t) (dky t) } in
+    let dst = { h=now; u=fun t -> model.cset state.sm (dky t) } in
+    let state = (*...*) in
+    (Some out, state, Some dst)
+
+  let asim (ASNode { m=HNode model; a=DNode assertion }) (DNode solver) =
+    let s0 = { (*...*); y=None; sa=a.state } in
+    let dstep state =
+      let state = { state with sm=model.cset state.sm state.y } in
+      let o, state = dstep (HNode model) (DNode solver) state in
+      let y = model.cget state.sm in
+      let b, sa = assertion.step state.sa (Some { h=0.0; u=fun _ -> state.sm }) in
+      assert b; (o, { state with sa; y }) in
+    let cstep state =
+      let state = { state with sm=model.cset state.sm state.y } in
+      let o, state, st = acstep (HNode model) (DNode solver) state in
+      let y = model.cget state.sm in
+      let b, sa = assertion.step state.sa st in
+      assert b; (o, { state with sa; y }) in
+    let step state i = match (i, state.mode) with
+      | (*...*)
+      | None, Discrete -> dstep state
+      | None, Continuous -> cstep state
+      | (*...*) in
+    let reset state r =
+      let sm = model.reset r state.sm and sa = assertion.reset r state.sa in
+      { state with mode=Idle; sm; sa; r=true } in
+    DNode { s0; step; reset }
+  ```,
+  caption: [Simulation of a model with assertions in #ocaml]
+) <lst:sim_assert>
 
 = Future Work <sec:future_work>
 
@@ -1336,20 +1358,64 @@ containing their own assertions, and so on and so forth.
 
 #pagebreak()
 
+= Bibliography <sec:bibliography>
+
 #bibliography(
   "sources.bib",
   // full: true,
   style: "alphanumeric.csl",
-  title: [Bibliography]
+  title: none
 )
+#todo[Find a proper bibliographic style.]
 
 = Appendix <sec:appendix>
 
-#todo[Find a proper bibliographic style.]
-
 == Additional Code <sec:additional_code>
 
 #set figure(placement: none)
+
+#figure(
+  ```ocaml
+  (** Discrete-time model. *)
+  type ('i, 'o, 'r, 's) dnode =
+    DNode of { s0 : 's; step : 's -> 'i -> 'o * 's; reset : 's -> 'r -> 's }
+  (** Continuous-time model. *)
+  type ('i, 'o, 's, 'sd) cnode =
+    CNode of { s0 : 's; fder : 'i -> 's -> 'sd; fout : 'i -> 's -> 'o }
+  (** Dense values. *)
+  type 'a dense = { h : time; u : time -> 'a }
+  (** Initial value problem. *)
+  type ('y, 'yd) ivp = { y0 : 'y; stop : time; f : time -> 'y -> 'yd }
+  (** ODE solver. *)
+  type ('y, 'yd, 's) csolver = (time, 'y dense, ('y, 'yd) ivp, 's) dnode
+  (** Hybrid simulation mode. *)
+  type mode = Discrete | Continuous | Idle
+  (** Hybrid simulation state. *)
+  type ('i, 'sm, 'ss) state =
+    { sm : 'sm; ss : 'ss; mode : mode; r : bool; i : 'i dense option; now : time }
+  (** Zero-crossing problem. *)
+  type ('y, 'zo) zcp = { y0 : 'y; f : time -> 'y -> 'zo }
+  (** Zero-crossing solver. *)
+  type ('y, 'zi, 'zo, 's) zsolver =
+    ('y dense, time * 'zi option, ('y, 'zo) zcp, 's) dnode
+  (** Hybrid model. *)
+  type ('i, 'o, 'r, 's, 'y, 'yd, 'zi, 'zo) hnode =
+    HNode of { s0 : 's;
+               cget : 's -> 'y; cset : 's -> 'y -> 's; zset : 's -> 'zi -> 's;
+               horizon : 's -> time; jump : 's -> bool; reset : 's -> 'r -> 's;
+               step : 's -> 'i -> 'o * 's; fder : 's -> 'i -> 'y -> 'yd;
+               fzero : 's -> 'i -> 'y -> 'zo; fout : 's -> 'i -> 'y -> 'o }
+  (** Full solver. *)
+  type ('y, 'yd, 'zi, 'zo, 's) solver =
+    (time, 'y dense * 'zi option, ('y, 'yd) ivp * ('y, 'zo) zcp, 's) dnode
+  (** Hybrid model with a single assertion. *)
+  type ('i, 'o, 'r, 'sm, 'sa, 'y, 'yd, 'zi, 'zo) asnode =
+    ASNode of { m : ('i, 'o, 'r, 'sm, 'y, 'yd, 'zi, 'zo) hnode;
+                a : ('sm signal, bool, 'sa) dnode }
+  ```,
+  caption: [#ocaml type definitions]
+) <lst:ocaml_typedefs>
+
 #figure(
   ```ocaml
   let compose (DNode f) (DNode g) =
@@ -1361,14 +1427,31 @@ containing their own assertions, and so on and so forth.
           (o, (sf, sg))
       | None ->
           let (o, sf) = f.step sf None in
-          match o with Some _ -> (o, (sf, sg)) | None ->
+          match o with
-          let (o, sg) = g.step sg None in
+          | Some _ -> (o, (sf, sg))
-          match o with None -> (None, (sf, sg)) | Some _ ->
+          | None ->
-          let (o, sf) = f.step sf o in
+              let (v, sg) = g.step sg None in
-          (o, (sf, sg)) in
+              match v with
+              | None -> (None, (sf, sg))
+              | Some _ ->
+                  let (o, sf) = f.step sf o in
+                  (o, (sf, sg)) in
     let reset (sf, sg) (rf, rg) = (f.reset sf rf, g.reset sg rg) in
     DNode { s0; step; reset }
   ```,
   caption: [Composition of simulations in #ocaml]
-)
+) <lst:compose>
 
+#figure(
+  ```ocaml
+  let synchr (DNode f) (DNode g) =
+  ```,
+  caption: [Synchronization of simulations in #ocaml]
+) <lst:synchr>
+
+#todo[Complete @lst:synchr.]
+
+#note[
+  Ideas:
+  - Detailed synchronous kernel of #zelus
+]