ROSCOQ.trash

What does it mean for a physical quantity to be controlled by an output device.
uptoTime only makes sense if it is later than the timestamp of the last event

this is a correct proof; only temporarily wrong
Lemma velMessages:
   n : nat,
     match getVelFromMsg (motorEvents n) with
     | Some vv = speedv = (0-speed)
     | NoneTrue
     end.
Proof.
  intros n.
  unfold motorEvents.
  unfold getVelFromMsg.
  unfold getVelFromEv.
the message of this deque event must have come from a prior enque event as evEnq
  pose proof (corrFIFO eo) as Hfifo.
  pose proof (deqEnq Hfifo BASEMOTOR n) as Henq.
  unfold deqMesgOp in Henq.
  unfold opBind.
  unfold opBind in Henq.
  remember (localEvts BASEMOTOR n) as oev.
  destruct oev as [ ev| ]; [| auto; fail].
  remember (deqMesg ev) as om.
  destruct om as [ sm| ]; [| auto; fail].
  destruct Henq as [evEnq Henq].
  clear Hfifo.
someone must have sent this message which is contained in the receive (enque) event evEnq. let the sent message be sm and the corresponding event be es
  pose proof (recvSend eo evEnq) as Hrecv.
  repnd.
  destruct Hrecv as [es Hrecv];
    [unfold isRecvEvt; rewrite Henqrrl; auto |].
  TrimAndRHS Hrecv.
  unfold PossibleSendRecvPair in Hrecv.
  rewrite Henqrrl in Hrecv.
  rewrite Henqrrr in Hrecv.
  rewrite <- Henqrl in Hrecv.
  clear Henqrrl Henqrl Henqrrr.
  remember (eKind es) as eks.
  destruct eks; try contradiction;[].
  simpl in Hrecv.
  repnd. clear Hrecvrrr.
since BASEMOTOR only receives on MOTOR topic, the message sm must have that topic
  unfold validRecvMesg in Hrecvrl.
  simpl in Hrecvrl.
  unfold validSendMesg in Hrecvrrl.
  destruct Hrecvrl as [Hmt | ?];[| contradiction].
  rewrite Hrecvl in Hrecvrrl.
  rewrite <- Hmt in Hrecvrrl.
  remember (eLoc es) as sloc.
Only SWCONTROLLER sends on that topic
  destruct sloc; simpl in Hrecvrrl;
    try contradiction;
    inversion Hrecvrrl;
    try discriminate;
    try contradiction;[].
  clear H Hrecvrrl.
  apply swControllerMessages in Heqeks;
    [| trivial].
  rewrite <- Hrecvl. trivial.
Qed.

A node only receives messeages from subscribed topics

Some properties about events at a particular location. In the next Coq Section, we formalize the interlocation properties.
first event is innermost, last event is outermost
Fixpoint prevProcessedEvents (m : nat)
  (locEvents : natoption EV) : list EV :=
  match m with
  | 0 ⇒ nil
  | S m' ⇒ (match locEvents m' with
              | Some evmatch (eKind ev) with
                            | deqEvt ⇒ (ev)::nil
                            | _nil
                            end
              | Nonenil
             end
            )++ (prevProcessedEvents m' locEvents)
  end.

Fixpoint futureSends (start : nat) (len : nat)
  (locEvents : natoption EV) : list EV :=
  match len with
  | 0 ⇒ nil
  | S len'
      match locEvents (start + len') with
      | Some ev
          match (eKind ev) with
          | sendEvtev :: (futureSends (S start) len' locEvents)
          | deqEvtnil
          | enqEvt ⇒ (futureSends (S start) len' locEvents)
          end
      | Nonenil
       end
  end.

Definition sendsInRange (startIncl : nat) (endIncl : nat)
  (locEvents : natoption EV) : list Message :=
  map eMesg (futureSends startIncl (endIncl + 1 - startIncl) locEvents).

Open Scope Q_scope.

Definition CorrectSWNodeBehaviour
    (swNode : RosSwNode)
    (locEvts: natoption EV) : Prop :=

   n: nat,
  match (locEvts n) with
  | NoneTrue
  | Some ev
      let procEvts := prevProcessedEvents (S (eLocIndex ev))locEvts in
      let procMsgs := map eMesg procEvts in
      let lastOutMsgs := getLastOutputL (process swNode) procMsgs in
      let evIndex := eLocIndex ev in

      match (eKind ev) with
        | deqEvt
             len, let sEvts := (futureSends (eLocIndex ev) len locEvts) in
                    map eMesg sEvts = lastOutMsgs
                    ∧ match (rev sEvts) with
                        | hsm :: _
                                (eTime hsm <
                                         (eTime ev) +
                                              (pTiming swNode (eMesg ev)))
                        | nilTrue
                        end

        | sendEvt
          match procEvts with
          | nilFalse
          | last :: _
    
NOT REQD; DERIVABLE
In (eMesg ev) lastOutMsgs
              length (sendsInRange (eLocIndex last) evIndex locEvts)
                 ≤ length lastOutMsgs
          end

        | enqEvtTrue
      end
  end.

Definition DeviceBehaviourCorrect
    {Env : Type}
    (physQ : TimeEnv)
    (inpDev : Device Env)
    (locEvents : natoption EV) : Prop :=

 inpDev physQ locEvents.





There is no code to extract for devices These are here to model environment

Record RosInpDevNode (Env : Type) :=
{
  
    outTopic : RosTopic;
    idev :> InpDev Env (topicType outTopic)
}.

Definition substIDev {Env : Type} (rid : RosInpDevNode Env)
  (newd : InpDev Env ((topicType (outTopic rid))))
  : RosInpDevNode Env :=
Build_RosInpDevNode
                    (outTopic rid)
                    newd.

Record RosOutDevNode (Env : Type) :=
{
    
    inpTopic : RosTopic;
    odev :> OutDev Env ((topicType inpTopic))
}.


Implementing this will need simplification of topic definitions. We need decidable equality on topics, which is not currently true. Also, one could have 2 topics with same string name and different payload types


Definition getRosOutDevBhv {Env : Type}
    (p: RosOutDevNode Env )
    (allInputs : list Message) : OutDevBehaviour Env :=
    let filterMsgs := filterMegsByTopic allInputs (inpTopic p) in
    match filterMsgs with
    | nilfst (odev p)
    | last :: restgetLastOutput (snd (odev p)) rest last
    end.

Lemma RHSSafe : t: QTime, (centerPosAtTime tstate t) [<=] Z2R 95.
Proof.
  intros.
  pose proof (less_cotransitive_unfolded _ (Z2R 94) (Z2R 95)) as Hdi.
  lapply Hdi; [clear Hdi; intro Hdi
                |apply inj_Q_less; unfold inject_Z; simpl; lra; fail].
  match goal with
  [|- ?l [<=] ?r] ⇒ specialize (Hdi l)
  end.
  destruct Hdi;[|apply less_leEq].
  assert False;[| contradiction].
Abort.
While this method works, a better one is also constructive

Lemma velocityMessagesEv : m t,
  member m (velocityMessages t)
  → sig (fun ev⇒ (eMesg ev) = ((mkMesg MOTOR (fst m))::nil)
                ∧ eTime ev < t
                ∧ eTime ev = (snd m)
                ∧ eLoc ev = BASEMOTOR
                ∧ isDeqEvt ev).
Admitted.

not relevant for code generation, only relevant for reasoning

Section Dev.

Variable Env : Type.

Output devices receive messages and affect their environment. Examples are heating devices, motors in mobile robots like iCreate
In our model, an output device receives a message and outputs a property about how future environment evolves. Note that the device can use the previous history of inputs.
For example, when a roomba icreate receives a message with a request to go along X axis with speed 1m/s , the output property could be that the robots physical speed somewhere between 0.9m/s and 1.1 m/s until a new message arrives
Open Scope type_scope.

Record OutDevBehaviour := {
  allowedBhv :> (t:RTime), (RInInterval (clcr [0] t) → Env) → Prop

    
}.

Definition OutDev (Inp : Type) :=
  OutDevBehaviour × Process Inp OutDevBehaviour.

Definition MemoryLessOutDev (Inp : Type) :=
  OutDevBehaviour × (InpOutDevBehaviour).
Close Scope type_scope.

CoFixpoint makeOutDevAux {Inp: Type}
  (m: InpOutDevBehaviour)
    : Process Inp OutDevBehaviour :=
   buildP (fun inp : Inp ⇒ (makeOutDevAux m, m inp)).

Definition makeOutDev {Inp: Type}
  (m: MemoryLessOutDev Inp)
    : OutDev Inp :=
  (fst m, makeOutDevAux (snd m)).

Definition getOutDevBhv {In : Type}
    (p: OutDev In )
    (allInputs : list In) : OutDevBehaviour :=
    match allInputs with
    | nilfst p
    | last :: restgetLastOutput (snd p) rest last
    end.

Coercion makeOutDev : MemoryLessOutDev >-> OutDev.

An input device observes the environment over time and may emit messages. In the following model, it is a function which when given how environment evolved, either never outputs a message (unit case) our outputs a triple indicating the output message, time of output and a new device (possibly storing some state)
Time is relative to the previous emitted message. If no message was emitted yet, time is relative to the instant the device (driver) was turned on.
The reason why InpDev cannot be modeled by a software node is because unlike software nodes, input devices can emit messages even when they did not receive any input. Maybe we can generalize software nodes to do that.
CoInductive InpDev (Out : Type) :=
maybeSendMesg :
      ((TimeEnv)
        → (unit + (Out × Time × InpDev Out)))
        → InpDev Out.

Input devices may receive message as instructions. This model is not expressive enough to capture that.
Howver, that is not too bad. In ROS, sensors like kinect continuously emit and there is no control data.

Definition getIDev {Out : Type} (idv : InpDev Out ) :
((TimeEnv) → (unit + (Out × Time × InpDev Out)))
  :=
match idv with
maybeSendMesg mmmmmm
end.

End Dev.


Lemma restrictTill {A} (f : TimeA)
    (right : Time) : (RInInterval (clcr [0] right)) → A.
  intro rint.
  destruct rint.
  apply f. realV0.
  unfold iprop.
  unfold iprop in realVPos0.
  destruct realVPos0.
  trivial.
Defined.

Lemma fastFwd {A} (f : TimeA)
    (duration : Time) : TimeA.
  intro rint.
  destruct rint.
  apply f. (realV0 [+] duration).
  destruct duration. simpl.
  unfold iprop.
  unfold iprop in realVPos0.
  unfold iprop in realVPos1.
  eauto with ×.
Defined.

Lemma TimeDiffOprBnd : ∀ (opr : QTime),
  let t0 : QTime := MotorEventsNthTime 0 (decAuto (0<4)%nat I) in
  let t1 : QTime := MotorEventsNthTime 1 (decAuto (1<4)%nat I) in
 (Qabs.Qabs
        (opr × (t1 - t0) -
         opr ×
         (Qabs.Qabs (approximate (polarTheta targetPos) anglePrec) ×
          / rotspeed)) ≤ opr × ((1 + 1) × (sendTimeAcc + delivDelayVar)))%Q.
Proof.
  intros ? ? ?. pose proof MotorEv01Gap as Hg.
  simpl in Hg.
  fold t0 t1 in Hg.
  apply Q.Qmult_le_compat_l with (z:= Qabs.Qabs opr) in Hg;
      [|apply Qabs.Qabs_nonneg].
  rewrite <- Qabs.Qabs_Qmult in Hg. idtac.
  revert Hg.
  unfoldMC.
  intros Hg.
  rewrite foldQminus in Hg.
  rewrite QmultOverQminusL in Hg.
  rewrite foldQminus in Hg.
  unfold CanonicalNotations.norm, NormSpace_instance_Q in Hg.
  revert Hg.
  unfoldMC.
  intros Hg.
  rewrite QabsTime in Hg.
  trivial.
Qed.


Definition isVecDerivativeOf
    {n : nat} (f f' : Vector n TContR) : Type.
  revert f f'.
  induction n as [| np Hind]; intros f f';[exact unit|].
  destruct f as [fv ft].
  destruct f' as [fv' ft'].
  exact ((isDerivativeOf ft ft') × (Hind fv fv')).
Defined.