「SF-PLF」1 Equiv

Posted on 2024-02-02

issues on `coqc` module linking

Some module (e.g.Map) not found
either maunally make map.vo or proof general can solve that.

Behavioral Equivalence 行为等价

How to define the correctness of program transformation, e.g. optimize_0plus ?

in the setting w/o var (imp w/o var and state) : yield a program the evals to same number as original.
in the setting w/ var (full imp w/ assignment) : we need to consider the role of var and state.

Definitions

Two aexps or bexps are behaviorally equivalent if they evaluate to the same result in every state.

Definition aequiv (a1 a2 : aexp) : Prop :=
  ∀(st : state), aeval st a1 = aeval st a2.
Definition bequiv (b1 b2 : bexp) : Prop :=
  ∀(st : state), beval st b1 = beval st b2.

For commands, We can’t simply say … if they evaluate to the same ending state
some commands don’t terminate in any final state at all!

So to define, they either or…

both diverge 都发散
both terminate in the same final state 都在同一个状态停机

A compact way is

“if the first one terminates in a particular state then so does the second, and vice versa.”

1
2
3

Definition cequiv (c1 c2 : com) : Prop :=
  ∀(st st' : state),
    (st =[ c1 ]⇒ st') ↔ (st =[ c2 ]⇒ st').

Example 1 - Simple (but demonstrated)

Theorem skip_left : forall c,
  cequiv (SKIP;; c) c.
Proof.
  intros c st st'. split; intros H.
  - (* -> *)         
    inversion H; subst.  (* inverse E_Seq   *)
    inversion H2. subst. (* inverse E_Skip  *)
    assumption.
  - (* <- *)             (* reversely *)
    apply E_Seq with st. (* apply E_Seq *)
    apply E_Skip.        (* apply E_Skip *)
    assumption.
Qed.

Noticed that the inversion is like use the inverse function of constructors.

Example 2 - WHILE true non-terminating

one interesting theorem is that we can prove WHILE <things ⇓ true> is not terminating.
and is equivalent to any other non-terminating program, e.g. WHILE BTrue DO SKIP END: (因为我们的「等价」只要求同「发散」即可)

Theorem WHILE_true : ∀b c,
  bequiv b true →
  cequiv
    (WHILE b DO c END)
    (WHILE true DO SKIP END).

Example 3 - Loop Unrolling

any number of copies of the body can be “unrolled” without changing meaning

Theorem loop_unrolling : ∀b c,
  cequiv
    (WHILE b DO c END)         
    (TEST b THEN (c ;; WHILE b DO c END) ELSE SKIP FI).    (** 展开一层 **)

Example 4 - Use of extenionality 外延性

x !-> m x ; x is same map with m by extenionality!

1 2	Theorem identity_assignment : ∀x, cequiv (x ::= x) SKIP.

Properties of Behavioral Equivalence 行为等价的性质

等价关系 (Equivalence)

自反性（reflexive）、对称性（symmetric）和传递性（transitive）

同余关系（Congruence）

That is, the equivalence of two subprograms implies the equivalence of the larger programs in which they are embedded
如果两个子程序等价，那么当二者所在的更大的程序中_只有二者不同_时，这两个更大的程序也等价

          aequiv a1 a1'
  -----------------------------
  cequiv (x ::= a1) (x ::= a1')

          cequiv c1 c1'
          cequiv c2 c2'
     --------------------------
     cequiv (c1;;c2) (c1';;c2')

这个术语应该是来自抽象代数 : 能在运算下保持的等价关系
…in the sense that algebraic operations done with equivalent elements will yield equivalent elements.
Congruence relation

Theorem CAss_congruence : ∀x a1 a1',     (** cequiv 是集合 commands 上的等价关系 **)
  aequiv a1 a1' →
  cequiv (CAss x a1) (CAss x a1').       (** 在 `CAss` 这个 operation 下保持等价 => 同余 **)
  cequiv (x ::= a1) (x ::= a1').         (** 或，在 `::=` 这个 command 下保持等价 => 同余 **)

在 commands 上等价但不同余的关系?

I guess…”both terminating” relation?
which is equivalence relation on commands, but the equivalence would not be maintained after, say C_WHILE operation.

Example - Using Congruence

Example congruence_example:
  cequiv
    (* 程序 1： *)
    (X ::= 0;;
     TEST X = 0
     THEN
       Y ::= 0
     ELSE
       Y ::= 42
     FI)
    (* 程序 2： *)
    (X ::= 0;;
     TEST X = 0
     THEN
       Y ::= X - X (* <--- 这里不同 *)
     ELSE
       Y ::= 42
     FI).
Proof.
  apply CSeq_congruence.
  - apply refl_cequiv.
  - apply CIf_congruence.
    + apply refl_bequiv.
    + apply CAss_congruence.     (** <--- 化简到只需要证明 aequiv 0 (X - X) **) 
      unfold aequiv. simpl.
      * symmetry. apply minus_diag.
    + apply refl_cequiv.
Qed.

Program Transformations 程序变换

A program transformation is sound if it preserves the behavior of the original program.
如果一个程序变换保留了其原始行为，那么它就是_可靠_的

我们可以定义在不同集合 aexp, bexp, com 上的 sound 关系：
(有趣的是，Inductive 定义的非 Prop 的 Type, 确实就是 Set, 这是一种 PL 和数学的 Correspondence)

当我们的 datatype 是 constructor 时 => 不交并
当我们的 datatype 有 recursive 时 => 集合的递归定义

Definition atrans_sound (atrans : aexp → aexp) : Prop :=
  ∀(a : aexp), aequiv a (atrans a).
Definition btrans_sound (btrans : bexp → bexp) : Prop :=
  ∀(b : bexp), bequiv b (btrans b).
Definition ctrans_sound (ctrans : com → com) : Prop :=
  ∀(c : com), cequiv c (ctrans c).

Constant Folding 常量折叠

An expression is constant when it contains no variable references.
不引用变量的表达式为_常量_

Constant folding is an optimization that finds constant expressions and replaces them by their values.
常量折叠是一种找到常量表达式并把它们替换为其值的优化方法。

Soundness of Constant Folding

`aexp`

Theorem fold_constants_aexp_sound :
  atrans_sound fold_constants_aexp.
Proof.
  unfold atrans_sound. intros a. unfold aequiv. intros st.
  
(** 这个时候的状态：**)

  a : aexp
  st : state
  ============================
  aeval st a = aeval st (fold_constants_aexp a)

`bexp`

证明 btrans_sound fold_constants_bexp. 要难一些，因为其中还用到了 fold_constants_aexp, 所以我们需要一些技巧

(** 如果不记住而是直接 destruct 的话，这部分信息就丢失了 **)
    remember (fold_constants_aexp a1) as a1' eqn:Heqa1'.
    remember (fold_constants_aexp a2) as a2' eqn:Heqa2'.

(** 保留了这部分信息的目的是，使用 aexp 的可靠性定理来建立 aexp 与 值 的关系 **)
    replace (aeval st a1) with (aeval st a1') by
       (subst a1'; rewrite <- fold_constants_aexp_sound; reflexivity).
    replace (aeval st a2) with (aeval st a2') by
       (subst a2'; rewrite <- fold_constants_aexp_sound; reflexivity).

(** 最后才分类讨论 **)
    destruct a1'; destruct a2'; try reflexivity.

`cmd`

主要技巧在于配合使用 Congruence 与 IH 解决大部分 case，然后分类讨论 fold_constants_bexp 用 sound 做替换解决剩余 case.

Soundness of (0 + n)

类似，但是接下来我们就可以证明先 fold_constants 再 optimize_0plus 也是 sound 的.
这里我更 general 得证明了 ctrans 关系的传递性：

Theorem trans_ctrans_sound : forall tr1 tr2,
  ctrans_sound tr1 -> 
  ctrans_sound tr2 -> 
  ctrans_sound (fun c => tr2 (tr1 c)).

Proving Inequivalence 证明程序不等价

在这个例子中，subst_aexp 是 sound 得，被称为 Constant Propagation (常量传播)

(**    [X := 42 + 53](Y + X)  =>  Y + (42 + 53)    **)
Example subst_aexp_ex :
  subst_aexp X (42 + 53) (Y + X)%imp = (Y + (42 + 53))%imp.
Proof. reflexivity. Qed.

所以我们断言这么做是 always sound 得：

1
2
3

Definition subst_equiv_property := ∀x1 x2 a1 a2,
  cequiv (x1 ::= a1;; x2 ::= a2)
         (x1 ::= a1;; x2 ::= subst_aexp x1 a1 a2).

然而如果 a1 不是常量，副作用很容易让这个转换 unsound
那么怎么证明 ¬subst_equiv_property (即该性质不成立)? 举一个反例就好

Informal proof

provide a witness

Formal

give counterexamples via remember, then show ⊥.

(** 给出一组反例，使用性质证明他们 cequiv **)

  remember (X ::= X + 1;;
            Y ::= X)%imp     as c1.
  remember (X ::= X + 1;;
            Y ::= X + 1)%imp as c2.
  assert (cequiv c1 c2) by (subst; apply Contra).
  
(* => *)  Heqc1 : c1 = (X ::= X + 1;; Y ::= X)%imp
          Heqc2 : c2 = (X ::= X + 1;; Y ::= X + 1)%imp
          H : cequiv c1 c2
          ============================
          False
    
    
(** 给出他们将 eval 出不同的 heap **)

  remember (Y !-> 1 ; X !-> 1) as st1.
  remember (Y !-> 2 ; X !-> 1) as st2.
  assert (H1 : empty_st =[ c1 ]=> st1);
  assert (H2 : empty_st =[ c2 ]=> st2);

  apply H in H1. (** 使用 H : cequiv c1 c2 , 我们得到 **)
  
(* => *)  H1 : empty_st =[ c2 ]=> st1
          H2 : empty_st =[ c2 ]=> st2
          ============================
          False


(** 利用 ceval 的 deterministic **)

  assert (Hcontra : st1 = st2)
    by (apply (ceval_deterministic c2 empty_st); assumption).
    
(* => *)  Hcontra : st1 = st2
          ============================
          False

    
(** st1, st2 are map, which are actually function! 
    这时我们可以反用 functional extenionality，直接 apply Y 然后 discrinminate **)

  assert (Hcontra' : st1 Y = st2 Y)
    by (rewrite Hcontra; reflexivity).
  subst. inversion Hcontra'.  Qed.

Extended Exercise: Nondeterministic Imp

HAVOC roughly corresponds to an uninitialized variable in a low-level language like C.
After the HAVOC, the variable holds a fixed but arbitrary number.

我们增加一个 HAVOC X 语句（大灾难），会为 X 随机赋一个值…类似于「未初始化变量」

Inductive com : Type :=
  ...
  | CHavoc : string → com. (* <--- 新增 *)

Notation "'HAVOC' l" :=
  (CHavoc l) (at level 60) : imp_scope.
  

Inductive ceval : com -> state -> state -> Prop :=
  ...
  | E_Havoc : forall st (n : nat) x,
      st =[ HAVOC x ]=> (x !-> n)        (** can eval to arbitraty heap **)

Small-Step

deterministic

also the def of partial function?

solve_by_inverts

in LTac. (used to generate proof)
LTac doesn’t have termination check. (might not be able to find…)

match is back-tracking point.

number passing in = depth of the iteration/recursion

ST_Plus2 need value v1. not redundant with ST_Plus1
we might have things not value but cannot take step as well.

Strong Progress

Normal form

= no relation related to (so cannot step to)

vs Value…

destruct (apply t).
can we do that?

Slide Q&A.

value_not_sae_as normal_form

e.g (1+2) + 7
e.g. 3 + 7

One-step

plus
left + 0
right + 0

Inf-step -> Inf terms

go from 3 to 3+0

Stuck

No StepR

0 term can step into

Multi-Step Reduction ->*

Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : ∀(x : X), multi R x x
  | multi_step : ∀(x y z : X),
                    R x y →
                    multi R y z →
                    multi R x z.

can be either defined as a “head + tail” style (or “tail + head” style), or “refl + trans” style (as in Rel.v).

the trans relation are underteministic in terms of the transtive relation using. (you can throw infinitely many trans constructors in)

having multiple form so we can jump back and forth to pick one easier for proof.

PLT PM lang

multiple smallstep relation can be markded deepner state.qjw
er state.

IMP

astep no need for `value``

for If, in PLT we have 2 rules for T/F.
here we can compute…

Par w/o Concurrency is deterministic
(not vice versa)

suddenly / ->* / tuple

issues on coqc module linking