-- In this file, we create a concrete instances of the chip model and prove that all algorithms are good

--#include "ChipModelProps5.alfa"

--#include "FunFM.alfa"

--#include "MemoryProps.alfa"

{- Error: Error in the definition of goodRunAlg because:
Type error: 
Expression
s1  has type
Memory  but should have type that is equal to
NatFM Word
At: "/disk/hopper/users/pacsoft/hallgren/src/programatica/examples/ChannelSeparation/Alfa/Memories.alfa", line 19, column 11
Expression 
Memory
is not equal to
Nat -> Word-}

package ChipModelApp where
  open Propositions  use  IsTrue
  open Propositional
   use  Prop,  Absurdity,  AbsurdityElim,  Triviality,  TrivialityIntro,
        Pred,  Rel,  And,  AndIntro,  AndElim1,  AndElim2,  AndElimCont
  open Types  use  Maybe,  Bool
  open BoolProp  use  ifPropD,  ifTrueProp,  ifFalseProp
  open MaybeDefs  use  Maybe,  maybe,  MaybeProp,  MaybePropD
  open Identity
   use  (==),  refl,  subst,  substSym,  sym,  trans,  cong,  cong1
  open Natural  use  Nat,  natEq,  (+),  natLt
  open NatIdentities  use  natEqRefl,  eq2id
  open Tuples  use  Pair,  Unit,  unit,  pair,  fst,  snd
  open Lists  use  List,  cons,  null,  length
  open FiniteMaps  use  FiniteMap
  open FunFM  use  FM,  KeyEq,  funFM
  Reg = Nat
  Word = Nat
  NatFM = FM Nat
  RegFile = NatFM Word
  natKey :: KeyEq Nat
    = struct {
        eqK = natEq;
        eqRefl = natEqRefl;
        eqId = eq2id;}
  natFM :: FiniteMap NatFM Nat
    = funFM Nat natKey
  open ChipModelProps NatFM natFM Word RegFile
   use  separation,  separation1
  open ChipModel NatFM natFM Word RegFile
   use  Code,  Alg,  runAlg,  Channel,  Packet,  ChipState,  mm,  mmp,
        Algs,  doPacket3,  doPacket2,  doPacket1,  doPacket,  onePacket,
        chip
  open Monads
   use  Monad,  return,  (>>=),  (>>),  liftM,  ap,  liftM2,  sequence_,
        sequence,  mapM
  open State
   use  StateM,  uncurry,  inst,  load,  store,  update,  inFst,  inSnd
  open Memories NatFM natFM Word
   use  Addr,  nullPtr,  Memory,  Data,  empty,  lookupM,  updateM,
        updatePropM,updateSameM,  updateOtherM,  storeList,  loadList
  open MemoryProps NatFM natFM Word
   use  loadStoreLemma,  EqRange,  storeEqRange,  loadEqRange,
        lookupEqRange
  open PropertyDefs NatFM natFM Word RegFile
   use  StateIndependent,  MostlyStateIndependent,  GoodAlg,  regfile,
        sameChannel,  pick,  Separation,  Separation1,  bindIndependent,
        RelatedResult,  bindIndependentP
  open Protected
   use  EnvEx,  inst,  Protect,  protect,  mmprot,  runProtected
  -- The identity algorithm:
  idAlg :: Alg
    = \(a::Addr) -> \(regf::RegFile) -> Done@_ regf
  idAlgs :: Algs
    = \(h::Channel) -> idAlg
  idAlgGood :: GoodAlg idAlg
    = \(ws::Data) ->
      \(regf::RegFile) ->
      \(mem1::Memory) ->
      \(mem2::Memory) ->
      cong1
        Data
        RegFile
        (Pair Data RegFile)
        (loadList nullPtr (length Word ws) (storeList nullPtr ws mem1))
        (loadList nullPtr (length Word ws) (storeList nullPtr ws mem2))
        regf
        (pair Data RegFile)
        (trans
           Data
           (loadList nullPtr (length Word ws) (storeList nullPtr ws mem1))
           ws
           (loadList nullPtr (length Word ws) (storeList nullPtr ws mem2))
           (loadStoreLemma ws nullPtr mem1)
           (sym
              Data
              (loadList nullPtr (length Word ws) (storeList nullPtr ws mem2))
              ws
              (loadStoreLemma ws nullPtr mem2)))
  -- Separation holds in the special case when all channels use the identity algorithm:
  separationForId (ch::Channel)(state::ChipState)(ps::List Packet)
    :: (==)
         (List Packet)
         (pick ch (chip idAlgs state ps))
         (chip idAlgs state (pick ch ps))
    = separation1 idAlgs ch idAlgGood state ps
  goodAlgLemma3 (n::Nat)(regf'::RegFile)
    :: MostlyStateIndependent
         (Pair Data RegFile)
         Memory
         (EqRange n nullPtr)
         (doPacket3 n regf')
    = bindIndependent
        Memory
        Data
        (Pair Data RegFile)
        (EqRange n nullPtr)
        (liftM
           Memory
           (List Word)
           (StateM Memory)
           (State.inst Memory)
           (loadList nullPtr n)
           (load Memory))
        (\(ws'::List Word) ->
         return
           (Pair Data RegFile)
           (StateM Memory)
           (State.inst Memory)
           (Pair@_ ws' regf'))
        (\(s1::Memory) ->
         \(s2::Memory) ->
         \(r::EqRange n nullPtr s1 s2) ->
         AndIntro
           ((==)
              Data
              (fst
                 Data
                 Memory
                 (liftM
                    Memory
                    (List Word)
                    (StateM Memory)
                    (State.inst Memory)
                    (loadList nullPtr n)
                    (load Memory)
                    s1))
              (fst
                 Data
                 Memory
                 (liftM
                    Memory
                    (List Word)
                    (StateM Memory)
                    (State.inst Memory)
                    (loadList nullPtr n)
                    (load Memory)
                    s2)))
           (EqRange
              n
              nullPtr
              (snd
                 Data
                 Memory
                 (liftM
                    Memory
                    (List Word)
                    (StateM Memory)
                    (State.inst Memory)
                    (loadList nullPtr n)
                    (load Memory)
                    s1))
              (snd
                 Data
                 Memory
                 (liftM
                    Memory
                    (List Word)
                    (StateM Memory)
                    (State.inst Memory)
                    (loadList nullPtr n)
                    (load Memory)
                    s2)))
           (loadEqRange
              nullPtr
              n
              (fst Memory Memory (load Memory s1))
              (fst Memory Memory (load Memory s2))
              r)
           r)
        (\(a::Data) ->
         \(s1::Memory) ->
         \(s2::Memory) ->
         \(r::EqRange n nullPtr s1 s2) ->
         AndIntro
           ((==)
              (Pair Data RegFile)
              (fst
                 (Pair Data RegFile)
                 Memory
                 (return
                    (Pair Data RegFile)
                    (StateM Memory)
                    (State.inst Memory)
                    (Pair@_ a regf')
                    s1))
              (fst
                 (Pair Data RegFile)
                 Memory
                 (return
                    (Pair Data RegFile)
                    (StateM Memory)
                    (State.inst Memory)
                    (Pair@_ a regf')
                    s2)))
           (EqRange
              n
              nullPtr
              (snd
                 (Pair Data RegFile)
                 Memory
                 (return
                    (Pair Data RegFile)
                    (StateM Memory)
                    (State.inst Memory)
                    (Pair@_ a regf')
                    s1))
              (snd
                 (Pair Data RegFile)
                 Memory
                 (return
                    (Pair Data RegFile)
                    (StateM Memory)
                    (State.inst Memory)
                    (Pair@_ a regf')
                    s2)))
           (refl
              (Pair Data RegFile)
              (fst
                 (Pair Data RegFile)
                 Memory
                 (return
                    (Pair Data RegFile)
                    (StateM Memory)
                    (State.inst Memory)
                    (Pair@_ a regf')
                    s1)))
           r)
  goodProtect (A::Set)
              (addr::Addr)
              (n::Nat)
              (m::StateM Memory A)
              (p::IsTrue (natLt addr n) ->
                  MostlyStateIndependent A Memory (EqRange n nullPtr) m)
    :: MostlyStateIndependent
         (Maybe A)
         Memory
         (EqRange n nullPtr)
         (protect
            (StateM Memory)
            Addr
            A
            Word
            mm
            addr
            m
            (\(a::Addr) -> natLt a n))
    = \(s1::Memory) ->
      \(s2::Memory) ->
      \(r::EqRange n nullPtr s1 s2) ->
      ifPropD
        ((h::Memory) -> Pair (Maybe A) Memory)
        (\(h::Memory -> Pair (Maybe A) Memory) ->
         RelatedResult
           (Maybe A)
           Memory
           (EqRange n nullPtr)
           (protect
              (StateM Memory)
              Addr
              A
              Word
              mm
              addr
              m
              (\(a::Addr) -> natLt a n)
              s1)
           (h s2))
        (natLt addr n)
        (liftM A (Maybe A) (StateM Memory) mm.monad (\(b::A) -> Just@_ b) m)
        (mm.monad.unit (Maybe A) Nothing@_)
        (\(h::IsTrue (natLt addr n)) ->
         ifTrueProp
           ((h'::Memory) -> Pair (Maybe A) Memory)
           (natLt addr n)
           (liftM A (Maybe A) (StateM Memory) mm.monad (\(b::A) -> Just@_ b) m)
           (mm.monad.unit (Maybe A) Nothing@_)
           (\(h'::Memory -> Pair (Maybe A) Memory) ->
            RelatedResult
              (Maybe A)
              Memory
              (EqRange n nullPtr)
              (h' s1)
              (liftM
                 A
                 (Maybe A)
                 (StateM Memory)
                 mm.monad
                 (\(b::A) -> Just@_ b)
                 m
                 s2))
           h
           (AndElimCont
              ((==) A (fst A Memory (m s1)) (fst A Memory (m s2)))
              (EqRange n nullPtr (snd A Memory (m s1)) (snd A Memory (m s2)))
              (RelatedResult
                 (Maybe A)
                 Memory
                 (EqRange n nullPtr)
                 (liftM
                    A
                    (Maybe A)
                    (StateM Memory)
                    mm.monad
                    (\(b::A) -> Just@_ b)
                    m
                    s1)
                 (liftM
                    A
                    (Maybe A)
                    (StateM Memory)
                    mm.monad
                    (\(b::A) -> Just@_ b)
                    m
                    s2))
              (p h s1 s2 r)
              (\(a::(==) A (fst A Memory (m s1)) (fst A Memory (m s2))) ->
               \(b::EqRange
                      n
                      nullPtr
                      (snd A Memory (m s1))
                      (snd A Memory (m s2))) ->
               AndIntro
                 ((==)
                    (Maybe A)
                    (fst
                       (Maybe A)
                       Memory
                       (liftM
                          A
                          (Maybe A)
                          (StateM Memory)
                          mm.monad
                          (\(b'::A) -> Just@_ b')
                          m
                          s1))
                    (fst
                       (Maybe A)
                       Memory
                       (liftM
                          A
                          (Maybe A)
                          (StateM Memory)
                          mm.monad
                          (\(b'::A) -> Just@_ b')
                          m
                          s2)))
                 (EqRange
                    n
                    nullPtr
                    (snd
                       (Maybe A)
                       Memory
                       (liftM
                          A
                          (Maybe A)
                          (StateM Memory)
                          mm.monad
                          (\(b'::A) -> Just@_ b')
                          m
                          s1))
                    (snd
                       (Maybe A)
                       Memory
                       (liftM
                          A
                          (Maybe A)
                          (StateM Memory)
                          mm.monad
                          (\(b'::A) -> Just@_ b')
                          m
                          s2)))
                 (cong
                    A
                    (Maybe A)
                    (fst A Memory (m s1))
                    (fst A Memory (m s2))
                    (\(h'::A) -> Just@_ h')
                    a)
                 b)))
        (\(h::(h::IsTrue (natLt addr n)) -> Absurdity) ->
         ifFalseProp
           ((h'::Memory) -> Pair (Maybe A) Memory)
           (natLt addr n)
           (liftM A (Maybe A) (StateM Memory) mm.monad (\(b::A) -> Just@_ b) m)
           (mm.monad.unit (Maybe A) Nothing@_)
           (\(h'::Memory -> Pair (Maybe A) Memory) ->
            RelatedResult
              (Maybe A)
              Memory
              (EqRange n nullPtr)
              (h' s1)
              (mm.monad.unit (Maybe A) Nothing@_ s2))
           h
           (AndIntro
              ((==)
                 (Maybe A)
                 (fst (Maybe A) Memory (mm.monad.unit (Maybe A) Nothing@_ s1))
                 (fst (Maybe A) Memory (mm.monad.unit (Maybe A) Nothing@_ s2)))
              (EqRange
                 n
                 nullPtr
                 (snd (Maybe A) Memory (mm.monad.unit (Maybe A) Nothing@_ s1))
                 (snd (Maybe A) Memory (mm.monad.unit (Maybe A) Nothing@_ s2)))
              (refl
                 (Maybe A)
                 (fst (Maybe A) Memory (mm.monad.unit (Maybe A) Nothing@_ s1)))
              r))
  goodRunAlg (code::Code)(n::Nat)
    :: MostlyStateIndependent
         (Maybe RegFile)
         Memory
         (EqRange n nullPtr)
         (runAlg
            (Protect (StateM Memory) Addr)
            mmp
            code
            (\(a::Addr) -> natLt a n))
    = case code of {
        (Done regf) ->
          \(s1::Memory) ->
          \(s2::Memory) ->
          \(r::EqRange n nullPtr s1 s2) ->
          AndIntro
            ((==)
               (Maybe RegFile)
               (fst
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     (Done@_ regf)
                     (\(a::Addr) -> natLt a n)
                     s1))
               (fst
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     (Done@_ regf)
                     (\(a::Addr) -> natLt a n)
                     s2)))
            (EqRange
               n
               nullPtr
               (snd
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     (Done@_ regf)
                     (\(a::Addr) -> natLt a n)
                     s1))
               (snd
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     (Done@_ regf)
                     (\(a::Addr) -> natLt a n)
                     s2)))
            (refl
               (Maybe RegFile)
               (fst
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     (Done@_ regf)
                     (\(a::Addr) -> natLt a n)
                     s1)))
            r;
        (Read addr cont) ->
          bindIndependentP
            Memory
            Word
            RegFile
            (EqRange n nullPtr)
            (\(a::Addr) -> natLt a n)
            (protect (StateM Memory) Addr Word Word mm addr (mm.rd addr))
            (\(w::Word) -> runAlg (Protect (StateM Memory) Addr) mmp (cont w))
            (goodProtect
               Word
               addr
               n
               (mm.rd addr)
               (\(h::IsTrue (natLt addr n)) ->
                \(s1::Memory) ->
                \(s2::Memory) ->
                \(r::EqRange n nullPtr s1 s2) ->
                AndIntro
                  ((==)
                     Word
                     (fst Word Memory (mm.rd addr s1))
                     (fst Word Memory (mm.rd addr s2)))
                  (EqRange
                     n
                     nullPtr
                     (snd Word Memory (mm.rd addr s1))
                     (snd Word Memory (mm.rd addr s2)))
                  (lookupEqRange addr n s1 s2 h r)
                  r))
            (\(w::Word) -> goodRunAlg (cont w) n);
        (Write addr word cont) ->
          bindIndependentP
            Memory
            Unit
            RegFile
            (EqRange n nullPtr)
            (\(a::Addr) -> natLt a n)
            (protect (StateM Memory) Addr Unit Word mm addr (mm.wr addr word))
            (\(h::Unit) -> runAlg (Protect (StateM Memory) Addr) mmp cont)
            (goodProtect
               Unit
               addr
               n
               (mm.wr addr word)
               (\(h::IsTrue (natLt addr n)) ->
                \(s1::Memory) ->
                \(s2::Memory) ->
                \(r::EqRange n nullPtr s1 s2) ->
                AndIntro
                  ((==)
                     Unit
                     (fst Unit Memory (mm.wr addr word s1))
                     (fst Unit Memory (mm.wr addr word s2)))
                  (EqRange
                     n
                     nullPtr
                     (snd Unit Memory (mm.wr addr word s1))
                     (snd Unit Memory (mm.wr addr word s2)))
                  (refl Unit (fst Unit Memory (mm.wr addr word s1)))
                  (\(i::Nat) ->
                   \(p::IsTrue (natLt i n)) ->
                   updatePropM (nullPtr + i) addr word s1 s2 (r i p))))
            (\(a::Unit) -> goodRunAlg cont n);}
  goodRunProtected (code::Code)(n::Nat)(regf::RegFile)
    :: MostlyStateIndependent
         RegFile
         Memory
         (EqRange n nullPtr)
         (runProtected
            (StateM Memory)
            Addr
            Word
            RegFile
            mm
            regf
            (\(a::Addr) -> natLt a n)
            (runAlg (Protect (StateM Memory) Addr) mmp code))
    = \(s1::Memory) ->
      \(s2::Memory) ->
      \(r::EqRange n nullPtr s1 s2) ->
      let lemma = goodRunAlg code n s1 s2 r
      in  AndElimCont
            ((==)
               (Maybe RegFile)
               (fst
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     code
                     (\(a::Addr) -> natLt a n)
                     s1))
               (fst
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     code
                     (\(a::Addr) -> natLt a n)
                     s2)))
            (EqRange
               n
               nullPtr
               (snd
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     code
                     (\(a::Addr) -> natLt a n)
                     s1))
               (snd
                  (Maybe RegFile)
                  Memory
                  (runAlg
                     (Protect (StateM Memory) Addr)
                     mmp
                     code
                     (\(a::Addr) -> natLt a n)
                     s2)))
            (And
               ((==)
                  RegFile
                  (fst
                     RegFile
                     Memory
                     (runProtected
                        (StateM Memory)
                        Addr
                        Word
                        RegFile
                        mm
                        regf
                        (\(a::Addr) -> natLt a n)
                        (runAlg (Protect (StateM Memory) Addr) mmp code)
                        s1))
                  (fst
                     RegFile
                     Memory
                     (runProtected
                        (StateM Memory)
                        Addr
                        Word
                        RegFile
                        mm
                        regf
                        (\(a::Addr) -> natLt a n)
                        (runAlg (Protect (StateM Memory) Addr) mmp code)
                        s2)))
               (EqRange
                  n
                  nullPtr
                  (snd
                     RegFile
                     Memory
                     (runProtected
                        (StateM Memory)
                        Addr
                        Word
                        RegFile
                        mm
                        regf
                        (\(a::Addr) -> natLt a n)
                        (runAlg (Protect (StateM Memory) Addr) mmp code)
                        s1))
                  (snd
                     RegFile
                     Memory
                     (runProtected
                        (StateM Memory)
                        Addr
                        Word
                        RegFile
                        mm
                        regf
                        (\(a::Addr) -> natLt a n)
                        (runAlg (Protect (StateM Memory) Addr) mmp code)
                        s2))))
            lemma
            (\(a::(==)
                    (Maybe RegFile)
                    (fst
                       (Maybe RegFile)
                       Memory
                       (runAlg
                          (Protect (StateM Memory) Addr)
                          mmp
                          code
                          (\(a::Addr) -> natLt a n)
                          s1))
                    (fst
                       (Maybe RegFile)
                       Memory
                       (runAlg
                          (Protect (StateM Memory) Addr)
                          mmp
                          code
                          (\(a::Addr) -> natLt a n)
                          s2))) ->
             \(b::EqRange
                    n
                    nullPtr
                    (snd
                       (Maybe RegFile)
                       Memory
                       (runAlg
                          (Protect (StateM Memory) Addr)
                          mmp
                          code
                          (\(a'::Addr) -> natLt a' n)
                          s1))
                    (snd
                       (Maybe RegFile)
                       Memory
                       (runAlg
                          (Protect (StateM Memory) Addr)
                          mmp
                          code
                          (\(a'::Addr) -> natLt a' n)
                          s2))) ->
             AndIntro
               ((==)
                  RegFile
                  (fst
                     RegFile
                     Memory
                     (runProtected
                        (StateM Memory)
                        Addr
                        Word
                        RegFile
                        mm
                        regf
                        (\(a'::Addr) -> natLt a' n)
                        (runAlg (Protect (StateM Memory) Addr) mmp code)
                        s1))
                  (fst
                     RegFile
                     Memory
                     (runProtected
                        (StateM Memory)
                        Addr
                        Word
                        RegFile
                        mm
                        regf
                        (\(a'::Addr) -> natLt a' n)
                        (runAlg (Protect (StateM Memory) Addr) mmp code)
                        s2)))
               (EqRange
                  n
                  nullPtr
                  (snd
                     RegFile
                     Memory
                     (runProtected
                        (StateM Memory)
                        Addr
                        Word
                        RegFile
                        mm
                        regf
                        (\(a'::Addr) -> natLt a' n)
                        (runAlg (Protect (StateM Memory) Addr) mmp code)
                        s1))
                  (snd
                     RegFile
                     Memory
                     (runProtected
                        (StateM Memory)
                        Addr
                        Word
                        RegFile
                        mm
                        regf
                        (\(a'::Addr) -> natLt a' n)
                        (runAlg (Protect (StateM Memory) Addr) mmp code)
                        s2)))
               (cong
                  (Maybe RegFile)
                  RegFile
                  (fst
                     (Maybe RegFile)
                     Memory
                     (runAlg
                        (Protect (StateM Memory) Addr)
                        mmp
                        code
                        (\(a'::Addr) -> natLt a' n)
                        s1))
                  (fst
                     (Maybe RegFile)
                     Memory
                     (runAlg
                        (Protect (StateM Memory) Addr)
                        mmp
                        code
                        (\(a'::Addr) -> natLt a' n)
                        s2))
                  (\(h::Maybe RegFile) ->
                   maybe RegFile RegFile regf (\(b'::RegFile) -> b') h)
                  a)
               b)
  goodAlgLemma (code::Code)(n::Nat)(regf::RegFile)
    :: MostlyStateIndependent
         (Pair Data RegFile)
         Memory
         (EqRange n nullPtr)
         (doPacket2 code n regf)
    = bindIndependent
        Memory
        RegFile
        (Pair Data RegFile)
        (EqRange n nullPtr)
        (runProtected
           (StateM Memory)
           Addr
           Word
           RegFile
           mm
           regf
           (\(a::Addr) -> natLt a n)
           (runAlg (Protect (StateM Memory) Addr) mmp code))
        (doPacket3 n)
        (goodRunProtected code n regf)
        (goodAlgLemma3 n)
  goodAlg (alg::Alg) :: GoodAlg alg
    = \(ws::Data) ->
      \(regf::RegFile) ->
      \(mem1::Memory) ->
      \(mem2::Memory) ->
      let code = alg Zero@_ regf
          n = length Word ws
          m = doPacket1 code ws regf
          lemma
            :: RelatedResult
                 (Pair Data RegFile)
                 Memory
                 (EqRange n nullPtr)
                 (m mem1)
                 (m mem2)
            = goodAlgLemma
                code
                n
                regf
                (storeList nullPtr ws mem1)
                (storeList nullPtr ws mem2)
                (storeEqRange ws nullPtr mem1 mem2)
      in  AndElim1
            ((==)
               (Pair Data RegFile)
               (fst (Pair Data RegFile) Memory (doPacket alg ws regf mem1))
               (fst (Pair Data RegFile) Memory (doPacket alg ws regf mem2)))
            (EqRange
               n
               nullPtr
               (snd (Pair Data RegFile) Memory (m mem1))
               (snd (Pair Data RegFile) Memory (m mem2)))
            lemma
  separationForAll (algs::Algs)
                   (ch::Channel)
                   (state::ChipState)
                   (ps::List Packet)
    :: (==)
         (List Packet)
         (pick ch (chip algs state ps))
         (chip algs state (pick ch ps))
    = separation1 algs ch (goodAlg (algs ch)) state ps
{-# Alfa unfoldgoals off
brief on
hidetypeannots on
wide

nd
hiding on
var "index" hide 1
var "maybeD" hide 1
var "MaybeProp" hide 4
var "MaybePropD" hide 4
var "goodProtect" hide 1
 #-}