extend source and target calculi with observable tick effects + add invariant checks for relation preservation and target arity/shape

README.md

@@ -8,6 +8,10 @@ the target language makes representation explicit and forces each transition to
 
 the target calculus is intentionally lower level than the source and trades abstraction for control over layout and calling. it has decent tuple and sum representations and uses explicit box and unbox operations to mediate between them. equality on integers and booleans is primitive rather than encoded as well as recursive binding being built in rather than derived
 
+the audit path now records pass-boundary observations for source, specialisation, inlining, effect rewriting, and representation lowering. each corpus case is checked against relation preservation, target arity/shape validation, termination class preservation, and effect trace preservation. unsafe profiles intentionally refute these invariants so optimiser bugs show up as small source/target deltas rather than vague failures.
+
+the source calculus also has an explicit `tick` effect. this is enough to expose unsound dce-style rewrites: eliminating a dead binding is only valid when the eliminated term is effect free.
+
 ## example(s)
 
 a representation exposure witness starts from a polymorphic constant false term
@@ -33,4 +37,3 @@ TArrow (TPair (TInt, TBool), TPair (TInt, TBool))
 ```
 
 the target worker receives `RInt` and `RBool` while the wrapper preserves the boxed source interface
-

bin/main.ml

@@ -7,7 +7,7 @@ type profile = {
 }
 
 let safe_flags =
-  { Pipeline.default_flags with unsafe_repr_eq = false; unsafe_strict_unroll = false }
+  { Pipeline.default_flags with unsafe_repr_eq = false; unsafe_strict_unroll = false; unsafe_effect_drop = false }
 
 let profiles =
   [
@@ -17,17 +17,28 @@ let profiles =
     { name = "unsafe-inline"; flags = { safe_flags with unsafe_repr_eq = true }; relation = Relation.Boxed_unboxed };
     { name = "unsafe-unbox"; flags = Pipeline.default_flags; relation = Relation.Boxed_unboxed };
     { name = "unsafe-strictness"; flags = { safe_flags with inline = false; unsafe_strict_unroll = true }; relation = Relation.Boxed_unboxed };
+    { name = "unsafe-effects"; flags = { safe_flags with unsafe_effect_drop = true }; relation = Relation.Boxed_unboxed };
   ]
 
 let run_case (case : Corpus.case) =
   let audit = Audit.audit_case case in
+  let failed_invariants =
+    audit.Audit.invariants
+    |> List.filter (fun result -> not result.Audit.passed)
+    |> List.map (fun result -> Audit.invariant_kind_to_string result.Audit.kind)
+  in
   Printf.printf
-    "case %s\nclassification %s\nverdict %s\nsource %s\ntarget %s\n\n"
+    "case %s\nclassification %s\nverdict %s\nsource %s\ntarget %s\nfailed invariants %s\n\n"
     case.Corpus.name
     (Audit.failure_mode_to_string audit.Audit.failure_mode)
     (Reporting.verdict_to_string audit.Audit.comparison.Relation.verdict)
-    (Reporting.string_of_source_outcome audit.Audit.source_trace.Source.outcome)
+    (Reporting.string_of_source_trace audit.Audit.source_trace)
-    (Reporting.string_of_target_outcome audit.Audit.target_trace.Target.outcome)
+    (Reporting.string_of_target_trace audit.Audit.target_trace)
+    (if failed_invariants = [] then "none" else String.concat ", " failed_invariants);
+  if audit.Audit.failure_mode <> Audit.Preserved then begin
+    Printf.printf "%s\n\n" (Reporting.emit_pipeline_visualisation audit.Audit.compiled);
+    Printf.printf "%s\n\n" (Audit.emit_pass_boundaries audit)
+  end
 
 let run_profile profile =
   let result = Gen.run_campaign profile.flags profile.relation ~count:160 ~max_depth:4 () in

src/audit.ml

@@ -2,9 +2,30 @@ type failure_mode =
   | Preserved
   | Representation_exposure
   | Strictness_shift
+  | Effect_shift
   | Type_error of string
   | Other_failure of string
 
+type invariant_kind =
+  | Relation_preservation
+  | Target_arity
+  | Termination_class
+  | Effect_trace
+
+type invariant_result = {
+  kind : invariant_kind;
+  passed : bool;
+  detail : string;
+}
+
+type pass_boundary = {
+  pass : string;
+  source_outcome : Source.outcome option;
+  target_outcome : Target.outcome option;
+  effects : int;
+  verdict : string;
+}
+
 type obligation_status =
   | Discharged
   | Assumed
@@ -27,15 +48,24 @@ type case_audit = {
   typecheck : (unit, string) result;
   failure_mode : failure_mode;
   obligations : obligation_result list;
+  invariants : invariant_result list;
+  pass_boundaries : pass_boundary list;
 }
 
 let failure_mode_to_string = function
   | Preserved -> "preserved"
   | Representation_exposure -> "representation_exposure"
   | Strictness_shift -> "strictness_shift"
+  | Effect_shift -> "effect_shift"
   | Type_error msg -> "type_error " ^ msg
   | Other_failure msg -> "other_failure " ^ msg
 
+let invariant_kind_to_string = function
+  | Relation_preservation -> "relation_preservation"
+  | Target_arity -> "target_arity"
+  | Termination_class -> "termination_class"
+  | Effect_trace -> "effect_trace"
+
 let obligation_status_to_string = function
   | Discharged -> "discharged"
   | Assumed -> "assumed"
@@ -50,6 +80,8 @@ let classify validation compiled comparison =
   | Ok () ->
       begin match comparison.Relation.verdict with
       | Relation.Related -> Preserved
+      | Relation.Unrelated msg when String.equal msg "effect trace changed" -> Effect_shift
+      | Relation.Unrelated msg when String.equal msg "effect trace changed before divergence" -> Effect_shift
       | Relation.Unrelated msg when has_obligation Pipeline.Exposed_representation compiled.Pipeline.obligations ->
           Representation_exposure
       | Relation.Unrelated msg when String.equal msg "target diverged where source terminated" ->
@@ -69,6 +101,8 @@ let status_for_obligation failure_mode (obligation : Pipeline.obligation) =
       { obligation; status = Refuted; note = "counterexample exposes a representation specific equality primitive" }
   | Strictness_shift, Pipeline.Strictness_risk ->
       { obligation; status = Refuted; note = "counterexample changes termination by forcing a recursive payload" }
+  | Effect_shift, Pipeline.Effect_observation ->
+      { obligation; status = Refuted; note = "counterexample changes the observable effect trace" }
   | Type_error msg, _ ->
       { obligation; status = Refuted; note = "program failed validation: " ^ msg }
   | Other_failure msg, _ ->
@@ -81,6 +115,65 @@ let status_for_obligation failure_mode (obligation : Pipeline.obligation) =
       { obligation; status = Assumed; note = "unsafe inlining may expose representation observers" }
   | _, Pipeline.Strictness_risk ->
       { obligation; status = Assumed; note = "unsafe lowering may shift strictness" }
+  | _, Pipeline.Effect_observation ->
+      { obligation; status = Assumed; note = "effectful source terms require effect preservation" }
+
+let same_termination_class source target =
+  match source, target with
+  | Source.Value _, Target.Value _ -> true
+  | Source.Diverged _, Target.Diverged _ -> true
+  | Source.Stuck _, Target.Stuck _ -> true
+  | _ -> false
+
+let invariant_result kind passed detail = { kind; passed; detail }
+
+let check_invariants comparison source_trace target_trace target_program =
+  let target_validation = Target.validate target_program in
+  [
+    invariant_result
+      Relation_preservation
+      (comparison.Relation.verdict = Relation.Related)
+      (Reporting.verdict_to_string comparison.Relation.verdict);
+    invariant_result
+      Target_arity
+      (match target_validation with Ok () -> true | Error _ -> false)
+      (match target_validation with Ok () -> "target IR validates" | Error errors -> String.concat "; " errors);
+    invariant_result
+      Termination_class
+      (same_termination_class source_trace.Source.outcome target_trace.Target.outcome)
+      (Reporting.string_of_source_outcome source_trace.Source.outcome ^ " / " ^
+       Reporting.string_of_target_outcome target_trace.Target.outcome);
+    invariant_result
+      Effect_trace
+      (source_trace.Source.effects = target_trace.Target.effects)
+      ("source effects " ^ string_of_int source_trace.Source.effects ^
+       ", target effects " ^ string_of_int target_trace.Target.effects);
+  ]
+
+let pass_boundaries compiled target_trace =
+  let source_boundary pass term =
+    let trace = Source.evaluate term in
+    {
+      pass;
+      source_outcome = Some trace.Source.outcome;
+      target_outcome = None;
+      effects = trace.Source.effects;
+      verdict = Reporting.string_of_source_trace trace;
+    }
+  in
+  [
+    source_boundary "source" compiled.Pipeline.source_program;
+    source_boundary "specialise" compiled.Pipeline.specialised;
+    source_boundary "inline" compiled.Pipeline.inlined;
+    source_boundary "effect" compiled.Pipeline.effect_rewritten;
+    {
+      pass = "repr_lower";
+      source_outcome = None;
+      target_outcome = Some target_trace.Target.outcome;
+      effects = target_trace.Target.effects;
+      verdict = Reporting.string_of_target_trace target_trace;
+    };
+  ]
 
 let audit_case (case : Corpus.case) =
   let compiled = Pipeline.compile case.Corpus.flags case.Corpus.ty case.Corpus.source in
@@ -95,6 +188,8 @@ let audit_case (case : Corpus.case) =
         {
           Relation.source_outcome = source_trace.Source.outcome;
           target_outcome = Target.Stuck ("invalid target IR: " ^ String.concat "; " errors);
+          source_effects = source_trace.Source.effects;
+          target_effects = 0;
           verdict = Relation.Unrelated "invalid target IR";
         }
   in
@@ -105,6 +200,7 @@ let audit_case (case : Corpus.case) =
         {
           Target.steps = [compiled.Pipeline.target_program];
           outcome = Target.Stuck ("invalid target IR: " ^ String.concat "; " errors);
+          effects = 0;
         }
   in
   let typecheck = Typecheck.check case.Corpus.ty case.Corpus.source in
@@ -116,7 +212,9 @@ let audit_case (case : Corpus.case) =
   in
   let failure_mode = classify validation compiled comparison in
   let obligations = List.map (status_for_obligation failure_mode) compiled.Pipeline.obligations in
-  { case; compiled; comparison; source_trace; specialised_trace; inlined_trace; target_trace; typecheck; failure_mode; obligations }
+  let invariants = check_invariants comparison source_trace target_trace compiled.Pipeline.target_program in
+  let pass_boundaries = pass_boundaries compiled target_trace in
+  { case; compiled; comparison; source_trace; specialised_trace; inlined_trace; target_trace; typecheck; failure_mode; obligations; invariants; pass_boundaries }
 
 let source_outcome trace = Reporting.string_of_source_outcome trace.Source.outcome
 let target_outcome trace = Reporting.string_of_target_outcome trace.Target.outcome
@@ -126,6 +224,33 @@ let emit_obligation_result result =
   "| `" ^ o.Pipeline.pass ^ "` | `" ^ Reporting.obligation_kind_to_string o.Pipeline.kind ^
   "` | `" ^ obligation_status_to_string result.status ^ "` | " ^ result.note ^ " |"
 
+let emit_invariant_result result =
+  "| `" ^ invariant_kind_to_string result.kind ^ "` | `" ^
+  (if result.passed then "ok" else "failed") ^ "` | " ^ result.detail ^ " |"
+
+let emit_boundary boundary =
+  "| `" ^ boundary.pass ^ "` | `" ^ boundary.verdict ^ "` |"
+
+let emit_invariants audit =
+  String.concat "\n"
+    ([
+       "### invariants";
+       "";
+       "| invariant | status | detail |";
+       "| --- | --- | --- |";
+     ]
+     @ List.map emit_invariant_result audit.invariants)
+
+let emit_pass_boundaries audit =
+  String.concat "\n"
+    ([
+       "### pass boundaries";
+       "";
+       "| pass | observation |";
+       "| --- | --- |";
+     ]
+     @ List.map emit_boundary audit.pass_boundaries)
+
 let emit_case_audit audit =
   let typecheck =
     match audit.typecheck with
@@ -144,6 +269,14 @@ let emit_case_audit audit =
        "| specialised | `" ^ source_outcome audit.specialised_trace ^ "` |";
        "| inlined | `" ^ source_outcome audit.inlined_trace ^ "` |";
        "| target | `" ^ target_outcome audit.target_trace ^ "` |";
+       "| source effects | `" ^ string_of_int audit.source_trace.Source.effects ^ "` |";
+       "| target effects | `" ^ string_of_int audit.target_trace.Target.effects ^ "` |";
+       "";
+       Reporting.emit_pipeline_visualisation audit.compiled;
+       "";
+       emit_pass_boundaries audit;
+       "";
+       emit_invariants audit;
        "";
        "### obligation ledger";
        "";

src/audit.mli

@@ -2,9 +2,30 @@ type failure_mode =
   | Preserved
   | Representation_exposure
   | Strictness_shift
+  | Effect_shift
   | Type_error of string
   | Other_failure of string
 
+type invariant_kind =
+  | Relation_preservation
+  | Target_arity
+  | Termination_class
+  | Effect_trace
+
+type invariant_result = {
+  kind : invariant_kind;
+  passed : bool;
+  detail : string;
+}
+
+type pass_boundary = {
+  pass : string;
+  source_outcome : Source.outcome option;
+  target_outcome : Target.outcome option;
+  effects : int;
+  verdict : string;
+}
+
 type obligation_status =
   | Discharged
   | Assumed
@@ -27,11 +48,15 @@ type case_audit = {
   typecheck : (unit, string) result;
   failure_mode : failure_mode;
   obligations : obligation_result list;
+  invariants : invariant_result list;
+  pass_boundaries : pass_boundary list;
 }
 
 val audit_case : Corpus.case -> case_audit
 val failure_mode_to_string : failure_mode -> string
 val obligation_status_to_string : obligation_status -> string
+val invariant_kind_to_string : invariant_kind -> string
+val emit_pass_boundaries : case_audit -> string
+val emit_invariants : case_audit -> string
 val emit_case_audit : case_audit -> string
 val emit_matrix : case_audit list -> string
-

src/corpus.ml

@@ -13,10 +13,13 @@ type case = {
 let default = Pipeline.default_flags
 
 let safer =
-  { default with unsafe_repr_eq = false; unsafe_strict_unroll = false }
+  { default with unsafe_repr_eq = false; unsafe_strict_unroll = false; unsafe_effect_drop = false }
 
 let strictness_flags =
-  { default with inline = false; unsafe_repr_eq = false; unsafe_strict_unroll = true }
+  { default with inline = false; unsafe_repr_eq = false; unsafe_strict_unroll = true; unsafe_effect_drop = false }
+
+let effect_flags =
+  { safer with unsafe_effect_drop = true }
 
 let poly_const_false =
   Source.TyLam ("a", Source.Lam ("x", TVar "a", TArrow (TVar "a", TBool), Source.Lam ("y", TVar "a", TBool, Source.Bool false)))
@@ -42,6 +45,9 @@ let pair_sum_roundtrip =
       ("p", Source.LetPair ("n", "b", Source.Var "p", Source.If (Source.Var "b", Source.Var "n", Source.Int 0))),
       ("k", Source.Var "k") )
 
+let effectful_dead_let =
+  Source.Let ("_", Source.Tick ("alloc", Source.Int 0), Source.Int 1)
+
 let boxed_pair_projection =
   Source.App
     ( Source.Lam
@@ -121,4 +127,13 @@ let all =
       flags = strictness_flags;
       relation = Relation.Boxed_unboxed;
     };
+    {
+      name = "effect-elision-breaks-observation";
+      summary = "drop an effectful dead binding during source simplification";
+      claim = "DCE is only valid when the eliminated term is effect free";
+      ty = TInt;
+      source = effectful_dead_let;
+      flags = effect_flags;
+      relation = Relation.Boxed_unboxed;
+    };
   ]

src/gen.ml

@@ -85,6 +85,10 @@ let sample_terms ~count ~max_depth () =
                   Source.Fix ("loop", TInt, Source.Var "loop") ),
               Source.Int 0 );
       };
+      {
+        ty = TInt;
+        term = Source.Let ("_", Source.Tick ("alloc", Source.Int 0), Source.Int 1);
+      };
     ]
   in
   let rec fill acc i attempts =

src/pipeline.ml

@@ -6,12 +6,14 @@ type optimisation_flags = {
   repr_lower : bool;
   unsafe_repr_eq : bool;
   unsafe_strict_unroll : bool;
+  unsafe_effect_drop : bool;
 }
 
 type obligation_kind =
   | Preserve_relation
   | Exposed_representation
   | Strictness_risk
+  | Effect_observation
   | Worker_wrapper_proof
 
 type obligation = {
@@ -26,6 +28,7 @@ type compiled = {
   source_program : Source.term;
   specialised : Source.term;
   inlined : Source.term;
+  effect_rewritten : Source.term;
   target_program : Target.term;
   obligations : obligation list;
 }
@@ -37,6 +40,7 @@ let default_flags =
     repr_lower = true;
     unsafe_repr_eq = true;
     unsafe_strict_unroll = true;
+    unsafe_effect_drop = true;
   }
 
 let obligation ?(kind = Preserve_relation) pass subject detail =
@@ -52,10 +56,22 @@ let rec inline_cost = function
   | Source.Fix (_, _, body) -> 2 + inline_cost body
   | Source.Eq (_, a, b) -> 1 + inline_cost a + inline_cost b
   | Source.If (c, t, e) -> 1 + inline_cost c + inline_cost t + inline_cost e
+  | Source.Tick (_, t) -> 1 + inline_cost t
   | Source.Let (_, a, b) -> inline_cost a + inline_cost b
   | Source.LetPair (_, _, a, b) -> 1 + inline_cost a + inline_cost b
   | Source.Case (s, (_, l), (_, r)) -> 1 + inline_cost s + inline_cost l + inline_cost r
 
+let rec contains_tick = function
+  | Source.Tick _ -> true
+  | Source.Pair (a, b) | Source.App (a, b) | Source.Eq (_, a, b) -> contains_tick a || contains_tick b
+  | Source.Inl (_, t) | Source.Inr (_, t) | Source.Roll (_, t) | Source.Unroll t -> contains_tick t
+  | Source.Lam (_, _, _, body) | Source.TyLam (_, body) | Source.Fix (_, _, body) -> contains_tick body
+  | Source.TyApp (t, _) -> contains_tick t
+  | Source.If (c, t, e) -> contains_tick c || contains_tick t || contains_tick e
+  | Source.Let (_, a, b) | Source.LetPair (_, _, a, b) -> contains_tick a || contains_tick b
+  | Source.Case (s, (_, l), (_, r)) -> contains_tick s || contains_tick l || contains_tick r
+  | Source.Var _ | Source.Int _ | Source.Bool _ -> false
+
 let rec inline_term note unsafe_repr_eq term =
   match term with
   | Source.App (Source.Lam (x, _, _, body), arg) when inline_cost body <= 8 ->
@@ -95,10 +111,11 @@ let rec inline_term note unsafe_repr_eq term =
   | Source.Eq (g, a, b) -> Source.Eq (g, inline_term note unsafe_repr_eq a, inline_term note unsafe_repr_eq b)
   | Source.If (c, t, e) ->
       Source.If (inline_term note unsafe_repr_eq c, inline_term note unsafe_repr_eq t, inline_term note unsafe_repr_eq e)
+  | Source.Tick (label, t) -> Source.Tick (label, inline_term note unsafe_repr_eq t)
   | Source.Let (x, a, b) ->
       let a' = inline_term note unsafe_repr_eq a in
       let b' = inline_term note unsafe_repr_eq b in
-      if inline_cost a' <= 4 then begin
+      if inline_cost a' <= 4 && not (contains_tick a') then begin
         note Preserve_relation "let inlining" ("inlined binding " ^ x);
         Source.substitute x a' b'
       end else Source.Let (x, a', b')
@@ -107,6 +124,28 @@ let rec inline_term note unsafe_repr_eq term =
       Source.Case (inline_term note unsafe_repr_eq s, (x, inline_term note unsafe_repr_eq l), (y, inline_term note unsafe_repr_eq r))
   | other -> other
 
+let rec drop_effects note = function
+  | Source.Tick (label, t) ->
+      note Effect_observation "source effect" ("dropped observable tick " ^ label);
+      drop_effects note t
+  | Source.Pair (a, b) -> Source.Pair (drop_effects note a, drop_effects note b)
+  | Source.Inl (ty, t) -> Source.Inl (ty, drop_effects note t)
+  | Source.Inr (ty, t) -> Source.Inr (ty, drop_effects note t)
+  | Source.Lam (x, a, b, body) -> Source.Lam (x, a, b, drop_effects note body)
+  | Source.App (f, a) -> Source.App (drop_effects note f, drop_effects note a)
+  | Source.TyLam (x, body) -> Source.TyLam (x, drop_effects note body)
+  | Source.TyApp (t, ty) -> Source.TyApp (drop_effects note t, ty)
+  | Source.Roll (ty, t) -> Source.Roll (ty, drop_effects note t)
+  | Source.Unroll t -> Source.Unroll (drop_effects note t)
+  | Source.Fix (f, ty, body) -> Source.Fix (f, ty, drop_effects note body)
+  | Source.Eq (g, a, b) -> Source.Eq (g, drop_effects note a, drop_effects note b)
+  | Source.If (c, t, e) -> Source.If (drop_effects note c, drop_effects note t, drop_effects note e)
+  | Source.Let (x, a, b) -> Source.Let (x, drop_effects note a, drop_effects note b)
+  | Source.LetPair (x, y, a, b) -> Source.LetPair (x, y, drop_effects note a, drop_effects note b)
+  | Source.Case (s, (x, l), (y, r)) ->
+      Source.Case (drop_effects note s, (x, drop_effects note l), (y, drop_effects note r))
+  | other -> other
+
 let rec repr_of_typ = function
   | TInt -> Target.RInt
   | TBool -> Target.RBool
@@ -142,6 +181,7 @@ let rec lower strict_unroll = function
   | Source.Eq (GBool, a, b) -> Target.EqBool (lower strict_unroll a, lower strict_unroll b)
   | Source.If (c, t, e) ->
       Target.If (lower strict_unroll c, lower strict_unroll t, lower strict_unroll e)
+  | Source.Tick (label, t) -> Target.Tick (label, lower strict_unroll t)
   | Source.Let (x, a, b) -> Target.Let (x, lower strict_unroll a, lower strict_unroll b)
   | Source.LetPair (x, y, a, b) ->
       Target.Let
@@ -188,14 +228,18 @@ let compile flags source_type source_program =
     if flags.inline then inline_term (note "inline") flags.unsafe_repr_eq specialised
     else specialised
   in
+  let effect_rewritten =
+    if flags.unsafe_effect_drop then drop_effects (note "effect") inlined
+    else inlined
+  in
   let target_program =
     if flags.repr_lower then begin
       note "repr_lower" Worker_wrapper_proof "worker-wrapper" "wrapper must refine the boxed to unboxed relation on arguments and results";
       if flags.unsafe_strict_unroll then
         note "repr_lower" Strictness_risk "roll/unroll" "strict unroll lowering may force recursive payloads earlier than the source";
       match source_type with
-      | TArrow (TPair (TInt, TBool), TPair (TInt, TBool)) -> synthesize_worker_wrapper source_type inlined
+      | TArrow (TPair (TInt, TBool), TPair (TInt, TBool)) -> synthesize_worker_wrapper source_type effect_rewritten
-      | _ -> lower flags.unsafe_strict_unroll inlined
+      | _ -> lower flags.unsafe_strict_unroll effect_rewritten
-    end else lower false inlined
+    end else lower false effect_rewritten
   in
-  { source_type; source_program; specialised; inlined; target_program; obligations = List.rev !obligations }
+  { source_type; source_program; specialised; inlined; effect_rewritten; target_program; obligations = List.rev !obligations }

src/pipeline.mli

@@ -6,12 +6,14 @@ type optimisation_flags = {
   repr_lower : bool;
   unsafe_repr_eq : bool;
   unsafe_strict_unroll : bool;
+  unsafe_effect_drop : bool;
 }
 
 type obligation_kind =
   | Preserve_relation
   | Exposed_representation
   | Strictness_risk
+  | Effect_observation
   | Worker_wrapper_proof
 
 type obligation = {
@@ -26,10 +28,10 @@ type compiled = {
   source_program : Source.term;
   specialised : Source.term;
   inlined : Source.term;
+  effect_rewritten : Source.term;
   target_program : Target.term;
   obligations : obligation list;
 }
 
 val default_flags : optimisation_flags
 val compile : optimisation_flags -> typ -> Source.term -> compiled
-

src/relation.ml

@@ -12,6 +12,8 @@ type verdict =
 type comparison = {
   source_outcome : Source.outcome;
   target_outcome : Target.outcome;
+  source_effects : int;
+  target_effects : int;
   verdict : verdict;
 }
 
@@ -53,18 +55,29 @@ let rec cross_value_relation rel ty sv tv =
   | _ -> false
 
 let compare_programs ?(fuel = 256) rel ty src tgt =
-  let source_outcome = Source.observe ~fuel src in
+  let source_trace = Source.evaluate ~fuel src in
-  let target_outcome = Target.observe ~fuel tgt in
+  let target_trace = Target.evaluate ~fuel tgt in
+  let source_outcome = source_trace.Source.outcome in
+  let target_outcome = target_trace.Target.outcome in
   let verdict =
     match source_outcome, target_outcome with
     | Source.Value sv, Target.Value tv ->
-        if cross_value_relation rel ty sv tv then Related
+        if source_trace.Source.effects <> target_trace.Target.effects then
+          Unrelated "effect trace changed"
+        else if cross_value_relation rel ty sv tv then Related
         else Unrelated "value relation failed"
-    | Source.Diverged _, Target.Diverged _ -> Related
+    | Source.Diverged _, Target.Diverged _ ->
+        if source_trace.Source.effects = target_trace.Target.effects then Related
+        else Unrelated "effect trace changed before divergence"
     | Source.Diverged _, Target.Value _ -> Unrelated "target terminated where source diverged"
     | Source.Value _, Target.Diverged _ -> Unrelated "target diverged where source terminated"
     | Source.Stuck msg, _ -> Unrelated ("source stuck: " ^ msg)
     | _, Target.Stuck msg -> Unrelated ("target stuck: " ^ msg)
   in
-  { source_outcome; target_outcome; verdict }
+  {
-
+    source_outcome;
+    target_outcome;
+    source_effects = source_trace.Source.effects;
+    target_effects = target_trace.Target.effects;
+    verdict;
+  }

src/relation.mli

@@ -12,10 +12,11 @@ type verdict =
 type comparison = {
   source_outcome : Source.outcome;
   target_outcome : Target.outcome;
+  source_effects : int;
+  target_effects : int;
   verdict : verdict;
 }
 
 val source_value_relation : relation -> typ -> Source.value -> Source.value -> bool
 val cross_value_relation : relation -> typ -> Source.value -> Target.value -> bool
 val compare_programs : ?fuel:int -> relation -> typ -> Source.term -> Target.term -> comparison
-

src/reporting.ml

@@ -2,6 +2,7 @@ let obligation_kind_to_string = function
   | Pipeline.Preserve_relation -> "preserve_relation"
   | Pipeline.Exposed_representation -> "exposed_representation"
   | Pipeline.Strictness_risk -> "strictness_risk"
+  | Pipeline.Effect_observation -> "effect_observation"
   | Pipeline.Worker_wrapper_proof -> "worker_wrapper_proof"
 
 let string_of_source_outcome = function
@@ -14,6 +15,12 @@ let string_of_target_outcome = function
   | Target.Stuck msg -> "stuck " ^ msg
   | Target.Diverged n -> "diverged after " ^ string_of_int n ^ " steps"
 
+let string_of_source_trace trace =
+  string_of_source_outcome trace.Source.outcome ^ ", effects " ^ string_of_int trace.Source.effects
+
+let string_of_target_trace trace =
+  string_of_target_outcome trace.Target.outcome ^ ", effects " ^ string_of_int trace.Target.effects
+
 let string_of_relation = function
   | Relation.Baseline -> "baseline"
   | Relation.Boxed_unboxed -> "boxed_unboxed"
@@ -41,6 +48,17 @@ let emit_obligations (obligations : Pipeline.obligation list) =
            " / " ^ o.Pipeline.subject ^ ": " ^ o.Pipeline.detail)
     |> String.concat "\n"
 
+let emit_pipeline_visualisation (compiled : Pipeline.compiled) =
+  String.concat "\n"
+    [
+      "pipeline";
+      "source: " ^ Source.string_of_term compiled.Pipeline.source_program;
+      "specialise: " ^ Source.string_of_term compiled.Pipeline.specialised;
+      "inline: " ^ Source.string_of_term compiled.Pipeline.inlined;
+      "effect: " ^ Source.string_of_term compiled.Pipeline.effect_rewritten;
+      "repr_lower: " ^ Target.string_of_term compiled.Pipeline.target_program;
+    ]
+
 let emit_case_header (case : Corpus.case) (comparison : Relation.comparison) (compiled : Pipeline.compiled) =
   String.concat "\n"
     [
@@ -75,7 +93,7 @@ let emit_counterexample title (src_trace : Source.trace) (tgt_trace : Target.tra
     else "\n... " ^ string_of_int tgt_hidden ^ " more target steps omitted"
   in
   "source trace:\n" ^ emit_steps Source.string_of_term src_steps ^
-  src_suffix ^ "\n\nsource outcome: " ^ string_of_source_outcome src_trace.Source.outcome ^
+  src_suffix ^ "\n\nsource outcome: " ^ string_of_source_trace src_trace ^
   "\n\ntarget trace:\n" ^ emit_steps Target.string_of_term tgt_steps ^
-  tgt_suffix ^ "\n\ntarget outcome: " ^ string_of_target_outcome tgt_trace.Target.outcome ^
+  tgt_suffix ^ "\n\ntarget outcome: " ^ string_of_target_trace tgt_trace ^
   "\n\nobligations:\n" ^ emit_obligations obligations ^ "\n"

src/reporting.mli

@@ -1,9 +1,12 @@
 val obligation_kind_to_string : Pipeline.obligation_kind -> string
 val string_of_source_outcome : Source.outcome -> string
 val string_of_target_outcome : Target.outcome -> string
+val string_of_source_trace : Source.trace -> string
+val string_of_target_trace : Target.trace -> string
 val string_of_relation : Relation.relation -> string
 val verdict_to_string : Relation.verdict -> string
 val take_steps : int -> 'a list -> 'a list * int
 val emit_obligations : Pipeline.obligation list -> string
+val emit_pipeline_visualisation : Pipeline.compiled -> string
 val emit_case_header : Corpus.case -> Relation.comparison -> Pipeline.compiled -> string
 val emit_counterexample : string -> Source.trace -> Target.trace -> Pipeline.obligation list -> string

src/source.ml

@@ -18,6 +18,7 @@ type term =
   | Fix of var * typ * term
   | Eq of ground * term * term
   | If of term * term * term
+  | Tick of string * term
   | Let of var * term * term
   | LetPair of var * var * term * term
   | Case of term * (var * term) * (var * term)
@@ -59,6 +60,7 @@ type outcome =
 type trace = {
   steps : term list;
   outcome : outcome;
+  effects : int;
 }
 
 let typ_of (Expr (ty, _)) = ty
@@ -83,6 +85,7 @@ let rec string_of_term = function
       "(eq_" ^ string_of_ground g ^ " " ^ string_of_term a ^ " " ^ string_of_term b ^ ")"
   | If (c, t, e) ->
       "(if " ^ string_of_term c ^ " then " ^ string_of_term t ^ " else " ^ string_of_term e ^ ")"
+  | Tick (label, t) -> "(tick[" ^ label ^ "] " ^ string_of_term t ^ ")"
   | Let (x, a, b) ->
       "(let " ^ x ^ " = " ^ string_of_term a ^ " in " ^ string_of_term b ^ ")"
   | LetPair (x, y, a, b) ->
@@ -127,6 +130,7 @@ let rec substitute x repl term =
       if String.equal x f then term else Fix (f, ty, go body)
   | Eq (g, a, b) -> Eq (g, go a, go b)
   | If (c, t, e) -> If (go c, go t, go e)
+  | Tick (label, t) -> Tick (label, go t)
   | Let (y, a, b) ->
       Let (y, go a, if String.equal x y then b else go b)
   | LetPair (y, z, a, b) ->
@@ -151,6 +155,7 @@ let rec substitute_type x repl term =
   | Fix (f, ty, body) -> Fix (f, sub_ty ty, go body)
   | Eq (g, a, b) -> Eq (g, go a, go b)
   | If (c, t, e) -> If (go c, go t, go e)
+  | Tick (label, t) -> Tick (label, go t)
   | Let (y, a, b) -> Let (y, go a, go b)
   | LetPair (y, z, a, b) -> LetPair (y, z, go a, go b)
   | Case (scrut, (y, l), (z, r)) -> Case (go scrut, (y, go l), (z, go r))
@@ -211,6 +216,8 @@ let rec step term =
   | If (Bool false, _, e) -> Ok e
   | If (c, t, e) when not (is_value c) -> Result.map (fun c' -> If (c', t, e)) (stepv c)
   | If _ -> stuck "if scrutinee is not a bool"
+  | Tick (_, t) when is_value t -> Ok t
+  | Tick (label, t) -> Result.map (fun t' -> Tick (label, t')) (stepv t)
   | Let (x, a, b) when is_value a -> Ok (substitute x a b)
   | Let (x, a, b) -> Result.map (fun a' -> Let (x, a', b)) (stepv a)
   | LetPair (x, y, Pair (a, b), body) when is_value a && is_value b ->
@@ -234,24 +241,43 @@ let rec step term =
   | Int _ | Bool _ | Lam _ | TyLam _ | Roll _ -> stuck "value"
   | Inl _ | Inr _ -> stuck "sum injection expects value subterm"
 
+let rec active_tick = function
+  | Tick (_, payload) when is_value payload -> 1
+  | Tick (_, payload) -> active_tick payload
+  | App (f, a) when not (is_value f) -> active_tick f
+  | App (f, a) when not (is_value a) -> active_tick a
+  | Pair (a, _) when not (is_value a) -> active_tick a
+  | Pair (_, b) when not (is_value b) -> active_tick b
+  | Inl (_, t) | Inr (_, t) when not (is_value t) -> active_tick t
+  | Eq (_, a, _) when not (is_value a) -> active_tick a
+  | Eq (_, _, b) when not (is_value b) -> active_tick b
+  | If (c, _, _) when not (is_value c) -> active_tick c
+  | Let (_, a, _) when not (is_value a) -> active_tick a
+  | LetPair (_, _, scrut, _) when not (is_value scrut) -> active_tick scrut
+  | Case (scrut, _, _) when not (is_value scrut) -> active_tick scrut
+  | TyApp (t, _) when not (is_value t) -> active_tick t
+  | Unroll t when not (is_value t) -> active_tick t
+  | _ -> 0
+
 let evaluate ?(fuel = 256) term =
-  let rec go n acc t =
+  let rec go effects n acc t =
-    if n = 0 then { steps = List.rev (t :: acc); outcome = Diverged fuel }
+    if n = 0 then { steps = List.rev (t :: acc); outcome = Diverged fuel; effects }
     else if is_value t then
       match value_of_term t with
-      | Some v -> { steps = List.rev (t :: acc); outcome = Value v }
+      | Some v -> { steps = List.rev (t :: acc); outcome = Value v; effects }
-      | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal value decoding failure" }
+      | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal value decoding failure"; effects }
     else
+      let ticked = active_tick t in
       match step t with
-      | Ok t' -> go (n - 1) (t :: acc) t'
+      | Ok t' -> go (effects + ticked) (n - 1) (t :: acc) t'
       | Error "value" ->
           begin
             match value_of_term t with
-            | Some v -> { steps = List.rev (t :: acc); outcome = Value v }
+            | Some v -> { steps = List.rev (t :: acc); outcome = Value v; effects }
-            | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal value decoding failure" }
+            | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal value decoding failure"; effects }
           end
-      | Error msg -> { steps = List.rev (t :: acc); outcome = Stuck msg }
+      | Error msg -> { steps = List.rev (t :: acc); outcome = Stuck msg; effects }
   in
-  go fuel [] term
+  go 0 fuel [] term
 
 let observe ?fuel term = (evaluate ?fuel term).outcome

src/source.mli

@@ -18,6 +18,7 @@ type term =
   | Fix of var * typ * term
   | Eq of ground * term * term
   | If of term * term * term
+  | Tick of string * term
   | Let of var * term * term
   | LetPair of var * var * term * term
   | Case of term * (var * term) * (var * term)
@@ -59,6 +60,7 @@ type outcome =
 type trace = {
   steps : term list;
   outcome : outcome;
+  effects : int;
 }
 
 val typ_of : 'a expr -> typ

src/target.ml

@@ -30,6 +30,7 @@ type term =
   | EqInt of term * term
   | EqBool of term * term
   | If of term * term * term
+  | Tick of string * term
   | Box of typ * term
   | Unbox of term
   | Roll of typ * term
@@ -66,6 +67,7 @@ type outcome =
 type trace = {
   steps : term list;
   outcome : outcome;
+  effects : int;
 }
 
 let rec string_of_repr = function
@@ -99,6 +101,7 @@ let rec string_of_term = function
   | EqBool (a, b) -> "(eq_bool# " ^ string_of_term a ^ " " ^ string_of_term b ^ ")"
   | If (c, t, e) ->
       "(if# " ^ string_of_term c ^ " then " ^ string_of_term t ^ " else " ^ string_of_term e ^ ")"
+  | Tick (label, t) -> "(tick#[" ^ label ^ "] " ^ string_of_term t ^ ")"
   | Box (_, t) -> "(box " ^ string_of_term t ^ ")"
   | Unbox t -> "(unbox " ^ string_of_term t ^ ")"
   | Roll (_, t) -> "(roll# " ^ string_of_term t ^ ")"
@@ -270,6 +273,7 @@ let validate term =
         let tr, errors = infer ctx env t errors in
         let er, errors = infer ctx env e errors in
         (tr, expect_repr ctx tr er (expect_repr ctx RBool cr errors))
+    | Tick (_, t) -> infer ctx env t errors
     | Box (ty, t) ->
         let _r, errors = infer ctx env t errors in
         (RBox ty, errors)
@@ -356,6 +360,7 @@ let rec substitute x repl term =
   | EqInt (a, b) -> EqInt (go a, go b)
   | EqBool (a, b) -> EqBool (go a, go b)
   | If (c, t, e) -> If (go c, go t, go e)
+  | Tick (label, t) -> Tick (label, go t)
   | Box (ty, t) -> Box (ty, go t)
   | Unbox t -> Unbox (go t)
   | Roll (ty, t) -> Roll (ty, go t)
@@ -421,6 +426,8 @@ let rec step term =
   | If (Bool false, _, e) -> Ok e
   | If (c, t, e) when not (is_value c) -> Result.map (fun c' -> If (c', t, e)) (step c)
   | If _ -> Error "if# on non-bool value"
+  | Tick (_, t) when is_value t -> Ok t
+  | Tick (label, t) -> Result.map (fun t' -> Tick (label, t')) (step t)
   | Box (ty, t) when not (is_value t) -> Result.map (fun t' -> Box (ty, t')) (step t)
   | Unbox (Box (_, v)) when is_value v -> Ok v
   | Unbox t when not (is_value t) -> Result.map (fun t' -> Unbox t') (step t)
@@ -443,24 +450,54 @@ let rec step term =
   | Int _ | Bool _ | Lam _ | Box _ | Roll _ -> Error "value"
   | Inl _ | Inr _ -> Error "sum injection expects value subterm"
 
+let rec first_active_tick = function
+  | Tick (_, payload) when is_value payload -> 1
+  | Tick (_, payload) -> first_active_tick payload
+  | App (f, _) when not (is_value f) -> first_active_tick f
+  | App (_, args) ->
+      args
+      |> List.find_opt (fun arg -> not (is_value arg))
+      |> Option.map first_active_tick
+      |> Option.value ~default:0
+  | Tuple xs ->
+      xs
+      |> List.find_opt (fun arg -> not (is_value arg))
+      |> Option.map first_active_tick
+      |> Option.value ~default:0
+  | Proj (_, t) when not (is_value t) -> first_active_tick t
+  | Inl (_, _, t) | Inr (_, _, t) when not (is_value t) -> first_active_tick t
+  | Case (s, _, _) when not (is_value s) -> first_active_tick s
+  | Let (_, a, _) when not (is_value a) -> first_active_tick a
+  | EqInt (a, _) when not (is_value a) -> first_active_tick a
+  | EqInt (_, b) when not (is_value b) -> first_active_tick b
+  | EqBool (a, _) when not (is_value a) -> first_active_tick a
+  | EqBool (_, b) when not (is_value b) -> first_active_tick b
+  | If (c, _, _) when not (is_value c) -> first_active_tick c
+  | Box (_, t) when not (is_value t) -> first_active_tick t
+  | Unbox t when not (is_value t) -> first_active_tick t
+  | Unroll t when not (is_value t) -> first_active_tick t
+  | Halt t when not (is_value t) -> first_active_tick t
+  | _ -> 0
+
 let evaluate ?(fuel = 256) term =
-  let rec go n acc t =
+  let rec go effects n acc t =
-    if n = 0 then { steps = List.rev (t :: acc); outcome = Diverged fuel }
+    if n = 0 then { steps = List.rev (t :: acc); outcome = Diverged fuel; effects }
     else if is_value t then
       match value_of_term t with
-      | Some v -> { steps = List.rev (t :: acc); outcome = Value v }
+      | Some v -> { steps = List.rev (t :: acc); outcome = Value v; effects }
-      | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal target value decoding failure" }
+      | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal target value decoding failure"; effects }
     else
+      let ticked = first_active_tick t in
       match step t with
-      | Ok t' -> go (n - 1) (t :: acc) t'
+      | Ok t' -> go (effects + ticked) (n - 1) (t :: acc) t'
       | Error "value" ->
           begin match value_of_term t with
-          | Some v -> { steps = List.rev (t :: acc); outcome = Value v }
+          | Some v -> { steps = List.rev (t :: acc); outcome = Value v; effects }
-          | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal target value decoding failure" }
+          | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal target value decoding failure"; effects }
           end
-      | Error msg -> { steps = List.rev (t :: acc); outcome = Stuck msg }
+      | Error msg -> { steps = List.rev (t :: acc); outcome = Stuck msg; effects }
   in
-  go fuel [] term
+  go 0 fuel [] term
 
 let observe ?fuel term = (evaluate ?fuel term).outcome
 

src/target.mli

@@ -30,6 +30,7 @@ type term =
   | EqInt of term * term
   | EqBool of term * term
   | If of term * term * term
+  | Tick of string * term
   | Box of typ * term
   | Unbox of term
   | Roll of typ * term
@@ -66,6 +67,7 @@ type outcome =
 type trace = {
   steps : term list;
   outcome : outcome;
+  effects : int;
 }
 
 val string_of_repr : repr -> string

src/typecheck.ml

@@ -95,6 +95,7 @@ let rec type_of_env env term =
       let* te = type_of_env env e in
       let* () = expect tt te in
       Ok tt
+  | Source.Tick (_, t) -> type_of_env env t
   | Source.Let (x, a, b) ->
       let* ta = type_of_env env a in
       type_of_env ((x, ta) :: env) b
@@ -125,4 +126,3 @@ let is_well_typed expected term =
   match check expected term with
   | Ok () -> true
   | Error _ -> false
-

test/invariants.ml

@@ -57,6 +57,18 @@ let () =
   assert_true
     "expected strictness shift witness"
     (strict.failure_mode = Audit.Strictness_shift);
+  let effect_audit = Audit.audit_case (find_case "effect-elision-breaks-observation") in
+  assert_true
+    "expected effect shift witness"
+    (effect_audit.failure_mode = Audit.Effect_shift);
+  assert_true
+    "expected unsafe effect rewrite to emit effect observation obligation"
+    (has_obligation Pipeline.Effect_observation effect_audit.compiled.obligations);
+  assert_true
+    "expected effect trace invariant failure"
+    (List.exists
+       (fun result -> result.Audit.kind = Audit.Effect_trace && not result.Audit.passed)
+       effect_audit.Audit.invariants);
   let generated = Gen.sample_terms ~count:80 ~max_depth:4 () in
   List.iter
     (fun specimen ->
@@ -84,7 +96,7 @@ let () =
     "expected unsupported worker-wrapper source shape to be rejected"
     (fun () ->
        Pipeline.compile
-         { Pipeline.default_flags with unsafe_repr_eq = false; unsafe_strict_unroll = false }
+         { Pipeline.default_flags with unsafe_repr_eq = false; unsafe_strict_unroll = false; unsafe_effect_drop = false }
          (Types.TArrow (Types.TPair (Types.TInt, Types.TBool), Types.TPair (Types.TInt, Types.TBool)))
          (Source.Lam
             ( "p",