/-- Square two inputs in parallel, then add the squares. -/
def pipeline : ParProg := paralever {
[0] := 3;
[1] := 4;
parallel { %0 := [0]; [2] := R 0 * R 0 }
| { %0 := [1]; [3] := R 0 * R 0 };
%0 := [2];
%1 := [3];
[4] := R 0 + R 1
}
-- the independence obligation is a Bool, and the kernel evaluates it
example : wfB pipeline = true := ⊢ pipeline.wfB = true All goals completed! 🐙
/-- The parallel reading and the sequential reading agree, under *every* schedule. -/
theorem pipeline_ok (ρ : Regs) (σ : State) :
ParSeqEq (execPar pipeline ρ) (execSeq pipeline ρ) σ :=
par_seq_eq (ρ:Regsσ:State⊢ pipeline.wfB = true All goals completed! 🐙) ρ σ
-- and it computes 3*3 + 4*4
example : (runSeq (execPar pipeline (fun _ => 0)) (fun _ => .int 0)).2 4 = .int 25 := ⊢ (runSeq (pipeline.execPar fun x => 0) fun x => Val.int 0).snd 4 = Val.int 25 All goals completed! 🐙