Add simulation settings and assumptions to docs

[yudetamago]

e.g.

• discrete time simulation (byslot)

[nrryuya]

• No invalid message
  • assuming every validator can verify the messages
• Bounded double vote (multiple blocks at the same height) (in CBC, bounded equivocation)
  • assuming we can bound the Byzantine faults by economic incentives