Support for presampling tapes in the UB logic

[markusdemedeiros]

• add tapes to the ghost state (already done!)
• add wp rules for tapes at rand (already done!)
• add a presampling rule (wp_presample)
  • lifting lemma for state steps
• add an advanced composition rule for tapes
  • update exec modality
  • remaining admitted: exec_ub_bind
  • remaining admitted: adequacy
• implement analogue of wp_couple_rand_adv_comp (ie. wp_presample_adv_comp) on tapes
  • (FIXME) see if classic_proof_irrel.PIT.EqdepTheory.inj_pair2 is necessary
  • (FIXME) see if E = ∅ is necessary
  • finish wp_couple_rand_adv_comp?
  • cleanup
• port the planner rule to use tapes
  • apply Hei's proof as adequacy for almost-sure wp?
  • (FIXME) see if there's a more ergonomic way to remove the hypothesis which only get threaded through
• prove ec_spend_1 as WP (Hei is working on this)
  • update planner rule proof
  • cleanup
• reimplement some rejection sampler examples using the planner rule (different PR)
  • other examples from that paper?
• cleanup/remove notes
• implement wp_couple_rand_adv_comp as sequence of state steps w/ fresh tape?