Remove V- from GossipS5 Call Transformer in SMCDEL

[Pathemeous]

The implementation of GossipS5 in SMCDEL contains a call transformer. This definition supposedly copies all atoms (secret propositions) at every call, which is a bottleneck.

Use of the $V^-$ operator is not needed in the gossip setting. This seems to be demonstrated by the optimize function too, which again removes the propositins.

The transformer should instead keep the original propositions

[Pathemeous]

The propositions seem to be changed in the SMCDEL library Update KnowScene Event shown below. File location: SMCDEL/Symbolic/S5.hs

instance Update KnowScene Event where
  unsafeUpdate (kns@(KnS props _ _),s) (ctrf, eventFactsUnshifted) = (KnS newprops newlaw newobs, news) where
    -- PART 1: SHIFTING addprops to ensure props and newprops are disjoint
    (KnTrf addprops _ changelaw _, shiftrel) = shiftPrepare kns ctrf
    -- the actual event:
    eventFacts = map (apply shiftrel) eventFactsUnshifted
    -- PART 2: COPYING the modified propositions
    changeprops = map fst changelaw
    copyrel = zip changeprops [(freshp $ props ++ addprops)..]
    -- do the pointless update and calculate new actual state
    KnS newprops newlaw newobs = unsafeUpdate kns ctrf
    news = sort $ concat
            [ s \\ changeprops
            , map (apply copyrel) $ s `intersect` changeprops
            , eventFacts
            , filter (\ p -> bddEval (s ++ eventFacts) (changelaw ! p)) changeprops ]

[Pathemeous]

It seems that $V^-$ is not entirely redundant: while the secret proposition $Sab$ indeed do not need copying (will remain true and observable), the call propositions $P{i.j}$ can only be true right after the transformation. The state law $\Theta$ (and change law $\Theta_-$) include bi-implications that describe what it means for a call to happen (what secrets were exchanged), meaning this information gets invalidated if we do not make fresh propositions for earlier variables.

Concretely: In the non-copying case (removing $V^-$) and after two transformations (call 12 and then 23)

1. Leaving $P_{1,2}$ TRUE will violate the event law (multiple calls happen) and conceptually: "agents do not anymore know in what order the calls happened"
2. Setting $P_{1,2}$ FALSE will remove all prior knowledge deduced from the proposition (e.g. what secrets were exchanged).

[Pathemeous]

I don't think that it is feasible to lose this dependency on the call proposition's old values: I believe that was the insight of using a single transformer rather than individual events for each call combination.

One insight is that the claimed performance gain of having a single transformer over 2^n call events, might not be so big: since the transformer by nature still necessarily copies the 2^n call propositions contained within it.

Possible routes o optimise this might be:

1. only copy the actually changed proposition (the single call proposition rather than all of them and including the secrets)
2. Avoid encoding the call effects in the change law, but instead somehow modify the 'observable' secret atoms correctly based on the actual call. The secret atoms -do- have the monotonicity property

For (1) the question is whether this will lead to a sound transformation. For (2) I'm not sure conditionally setting the observables is even possible

[Pathemeous]

Dropped because (2) is practically the SimpleTransformer approach.