work unchanged, rounds reducedmade with verso-snippets
View
-- Work is unchanged: the same memory operations run either way, so parallelism buys nothing in
-- total operations. Conflating this with time is the usual mistake.
#check @work_par_eq_seq

@work_par_eq_seq : ∀ {α β : Type} (p : ParM α) (q : ParM β) (σ : State), work (p ∥ q) σ = work (p ;; q) σ-- Par ≤ Seq in rounds, for every program the check accepts — the cost counterpart of
-- `par_seq_eq`, out of the same `Bool`.
#check @ParProg.time_le

@time_le : ∀ {s : ParProg}, s.wfB = true → ∀ (ρ : Regs) (σ : State), time (s.execPar ρ) σ ≤ time (s.execSeq ρ) σ-- Strictly fewer rounds when both branches actually do something. `max` at a fork is stipulated
-- nowhere in the cost semantics; it is derived, and independence is what earns it.
#check @time_par_lt_seq

@time_par_lt_seq : ∀ {α β : Type} (p : ParM α) (q : ParM β) (σ : State),
  WellFormed (p ∥ q) σ → 0 < time p σ → 0 < time q σ → time (p ∥ q) σ < time (p ;; q) σ-- the pipeline: the same work either way, fewer rounds in parallel
#eval (work (execPar pipeline (fun _ => 0)) (fun _ => .int 0),
       (9, 9)work (execSeq pipeline (fun _ => 0)) (fun _ => .int 0))
#eval (time (execPar pipeline (fun _ => 0)) (fun _ => .int 0),
       (7, 9)time (execSeq pipeline (fun _ => 0)) (fun _ => .int 0))