From 8b78d270d6e250366e844473948d9b70e8c081d8 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 16:59:59 +0100 Subject: [PATCH 1/2] fix(coq/cno): drop cno_decidable axiom (Rice's theorem territory) Owner-ruled drop. Universal decidability of is_CNO over arbitrary programs asks for a constructive decision procedure over an unbounded state space (Memory, Registers, IOState all unbounded; is_CNO's universally-quantified clauses range over all states). This is essentially the Rice's theorem situation: deciding a non-trivial semantic property of an arbitrary program is undecidable. Net axiom count in proofs/coq/common/CNO.v: 3 -> 2 with this commit. Refs hyperpolymath/standards#124, scoping doc standards#157 (Stage 3). Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/coq/common/CNO.v | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/proofs/coq/common/CNO.v b/proofs/coq/common/CNO.v index eb31e5a..ccdd630 100644 --- a/proofs/coq/common/CNO.v +++ b/proofs/coq/common/CNO.v @@ -572,9 +572,21 @@ Qed. (** ** Decidability *) (** Question: Is CNO verification decidable? *) -(** This is a major research question *) -Axiom cno_decidable : forall p, {is_CNO p} + {~ is_CNO p}. +(** Universal decidability of [is_CNO] over arbitrary programs was + previously asserted as an [Axiom] [cno_decidable]. That axiom has + been dropped (owner ruling, Stage 3 of standards#157): the + universal form asks for a constructive decision procedure over an + unbounded state space ([Memory : nat -> nat], unbounded + registers, unbounded I/O traces), and [is_CNO]'s + universally-quantified clauses range over all of them. This is + essentially the Rice's-theorem situation: deciding a non-trivial + semantic property of an arbitrary program is undecidable, so the + universal-decidability claim is not constructively achievable in + Coq and any client that wants decidability must work in a + restricted syntactic fragment of [Program] (which the current + development does not formalise). No theorem in this file depended + on it. *) (** ** Complexity *) From 89deef78e02887c91d2a7c50bc8688120ac4c54f Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 17:06:29 +0100 Subject: [PATCH 2/2] fix(coq/cno): discharge eval_respects_state_eq_{left,right} via existential reformulation PR #25's Stage 3 left these two as Axiom after the agent discovered that the original universal form is unsound under the Stage-2 relaxed state_eq: the eval_empty base case requires s1 = s2 syntactically, but the hypothesis only provides s1 =st= s2 (pc-blind after Stage 2). The sound replacement uses an existential conclusion: forall p s1 s2 s', s1 =st= s2 -> eval p s1 s' -> exists s'', eval p s2 s'' /\ s' =st= s''. This is provable by induction on the eval derivation. The eval_empty case witnesses s'' = s2 directly. The eval_step case uses a new step_respects_state_eq helper that shows step preserves =st=-equivalence on inputs. Two callers updated to destructure the existential conclusion: - cno_eval_on_equal_states (in this file) - cno_logically_reversible (proofs/coq/physics/StatMech.v) The StatMech caller also required relaxing the logically_reversible definition: the inverse-run conclusion is now phrased modulo =st= rather than strict equality on the start state, since rerunning a CNO from its output can only recover the start state pc-modulo (state_pc is ignored by Stage-2 state_eq). The single downstream consumer bennett_logical_implies_thermodynamic does not use the hypothesis structurally, so it is unaffected. Net axiom count in proofs/coq/common/CNO.v: 2 -> 0. Stage 3 complete; the file is now Admitted-free AND Axiom-free. Note: physics/StatMech.v requires Coq.Reals which the local sandbox cannot exercise; the edit is CI-verifiable only (same pattern as prior PR's downstream files). common/CNO.v builds locally green. Refs hyperpolymath/standards#124, scoping doc standards#157 (Stage 3). Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/coq/common/CNO.v | 229 ++++++++++++++++++++++++++++------ proofs/coq/physics/StatMech.v | 50 ++++---- 2 files changed, 222 insertions(+), 57 deletions(-) diff --git a/proofs/coq/common/CNO.v b/proofs/coq/common/CNO.v index ccdd630..73e00fa 100644 --- a/proofs/coq/common/CNO.v +++ b/proofs/coq/common/CNO.v @@ -643,32 +643,188 @@ Conjecture cno_verification_overhead : (** ** State Equality and Evaluation *) -(** CRITICAL LEMMA: Evaluation respects state equality on the right - - This lemma is essential for proving CNO reversibility. - It states that if we can evaluate p from s to s', and s' is - state-equal to s'', then we can also evaluate p from s to s''. - - This is needed because the eval relation is defined inductively - on specific states, but CNO theory works with state equality (=st=). -*) -Axiom eval_respects_state_eq_right : - forall p s s' s'', - eval p s s' -> - s' =st= s'' -> - eval p s s''. +(** Inversion helpers for [step], extracted so the [step_respects_state_eq] + case-analysis below doesn't rely on Coq 8.18's positional [Hn] + auto-naming. Each returns the explicit equations that the [step_*] + constructor's premises imply about the post-state. *) + +Lemma step_load_inv : + forall s addr reg s', + step s (Load addr reg) s' -> + s' = mkState s.(state_memory) + (set_reg s.(state_registers) reg (s.(state_memory) addr)) + s.(state_io) + (S s.(state_pc)). +Proof. + intros s addr reg s' H. + inversion H; subst. + reflexivity. +Qed. -(** TODO: Prove this axiom by induction on eval structure. - This requires showing that each step constructor respects state equality. - For now, we axiomatize it to unblock cno_logically_reversible proof. -*) +Lemma step_store_inv : + forall s addr reg s', + step s (Store addr reg) s' -> + exists val, get_reg s.(state_registers) reg = Some val /\ + s' = mkState (mem_update s.(state_memory) addr val) + s.(state_registers) + s.(state_io) + (S s.(state_pc)). +Proof. + intros s addr reg s' H. + inversion H; subst. + eexists. split; [ eassumption | reflexivity ]. +Qed. -(** Similarly for the left side *) -Axiom eval_respects_state_eq_left : - forall p s s' s'', - eval p s s'' -> - s =st= s' -> - eval p s' s''. +Lemma step_add_inv : + forall s r1 r2 r3 s', + step s (Add r1 r2 r3) s' -> + exists v1 v2, get_reg s.(state_registers) r1 = Some v1 /\ + get_reg s.(state_registers) r2 = Some v2 /\ + s' = mkState s.(state_memory) + (set_reg s.(state_registers) r3 (v1 + v2)) + s.(state_io) + (S s.(state_pc)). +Proof. + intros s r1 r2 r3 s' H. + inversion H; subst. + do 2 eexists. split; [ eassumption | split; [ eassumption | reflexivity ] ]. +Qed. + +(** [step] respects [state_eq] on inputs: if [s1 =st= s2] and + [step s1 i sm], then there exists a post-state [sm'] with + [step s2 i sm'] and [sm =st= sm']. + + The witness for [sm'] is determined by case-analysis on [i] (since + [step] is deterministic given [=st=]-equal inputs — registers and + memory agree pointwise, and any read-out value from memory or + registers matches). The conclusion uses [=st=] rather than + syntactic equality because [Load]/[Store]/[Add] re-build records + from [s2]'s components, which differ from [s1]'s on [state_pc] and + are only [=mem=]-equal (not syntactically equal) on + [state_memory]. *) +Lemma step_respects_state_eq : + forall s1 s2 i sm, + s1 =st= s2 -> + step s1 i sm -> + exists sm', step s2 i sm' /\ sm =st= sm'. +Proof. + intros s1 s2 i sm Heq Hstep. + destruct Heq as [Hmem [Hreg Hio]]. + destruct i. + - (* Nop *) + inversion Hstep; subst. + exists (mkState s2.(state_memory) s2.(state_registers) s2.(state_io) + (S s2.(state_pc))). + split. + + constructor. + + unfold state_eq. simpl. split; [assumption | split; assumption]. + - (* Load addr reg *) + apply step_load_inv in Hstep. subst sm. + exists (mkState s2.(state_memory) + (set_reg s2.(state_registers) n0 + (s2.(state_memory) n)) + s2.(state_io) + (S s2.(state_pc))). + split. + + econstructor. reflexivity. + + unfold state_eq. simpl. split; [assumption | split; [| assumption]]. + (* set_reg s1.regs n0 (s1.mem n) = set_reg s2.regs n0 (s2.mem n) *) + rewrite Hreg. + f_equal. + apply Hmem. + - (* Store addr reg *) + apply step_store_inv in Hstep. + destruct Hstep as [val [Hget Hsm]]. subst sm. + exists (mkState (mem_update s2.(state_memory) n val) + s2.(state_registers) + s2.(state_io) + (S s2.(state_pc))). + split. + + econstructor. rewrite <- Hreg. exact Hget. + + unfold state_eq, mem_eq. simpl. + split; [| split; assumption]. + (* mem_update s1.mem n val =mem= mem_update s2.mem n val *) + intros addr. + unfold mem_update. + destruct (Nat.eqb addr n); [reflexivity | apply Hmem]. + - (* Add r1 r2 r3 *) + apply step_add_inv in Hstep. + destruct Hstep as [v1 [v2 [Hg1 [Hg2 Hsm]]]]. subst sm. + exists (mkState s2.(state_memory) + (set_reg s2.(state_registers) n1 (v1 + v2)) + s2.(state_io) + (S s2.(state_pc))). + split. + + econstructor; rewrite <- Hreg; eassumption. + + unfold state_eq. simpl. split; [assumption | split; [| assumption]]. + rewrite Hreg. reflexivity. + - (* Jump target *) + inversion Hstep; subst. + exists (mkState s2.(state_memory) s2.(state_registers) s2.(state_io) n). + split. + + constructor. + + unfold state_eq. simpl. split; [assumption | split; assumption]. + - (* Halt *) + inversion Hstep; subst. + exists s2. + split. + + constructor. + + unfold state_eq. split; [assumption | split; assumption]. +Qed. + +(** CRITICAL LEMMA: Evaluation respects state equality on the input side. + + The original universal form + [s =st= s' -> eval p s s'' -> eval p s' s''] + is unsound under the relaxed 3-clause [state_eq] from Stage 2: the + [eval_empty] base case would need [s = s'] syntactically, but + [s =st= s'] only constrains memory + registers + I/O (not + [state_pc]). Stage 3 (standards#157) accordingly reformulates the + conclusion existentially: from [s1 =st= s2] and [eval p s1 s'] we + obtain *some* [s''] reached by [p] starting from [s2], with + [s' =st= s''] (i.e. final states agree modulo [state_pc]). + + The proof is by induction on the [eval] derivation, using + [step_respects_state_eq] to advance the witness one instruction at + a time. *) +Theorem eval_respects_state_eq_left : + forall p s1 s2 s', + s1 =st= s2 -> + eval p s1 s' -> + exists s'', eval p s2 s'' /\ s' =st= s''. +Proof. + intros p s1 s2 s' Heq Heval. + generalize dependent s2. + induction Heval as [s | i is sa sb sc Hstep_a Heval_rest IH]; + intros s2 Heq. + - (* eval_empty: p = [], s' = s, witness s'' = s2 *) + exists s2. split. + + constructor. + + assumption. + - (* eval_step: step sa i sb, eval is sb sc *) + destruct (step_respects_state_eq _ _ _ _ Heq Hstep_a) + as [sb' [Hstep_b Heq_b]]. + destruct (IH sb' Heq_b) as [sc' [Heval_rest' Heq_c]]. + exists sc'. split. + + eapply eval_step; eassumption. + + assumption. +Qed. + +(** Symmetric form on the output side. + + The output-side version is trivial under the existential + reformulation: simply witness [s'' := s1]. We retain the + statement (now a [Theorem] rather than an [Axiom]) so that + downstream files have the symmetric API available. *) +Theorem eval_respects_state_eq_right : + forall p s s1 s2, + eval p s s1 -> + s1 =st= s2 -> + exists s'', eval p s s'' /\ s'' =st= s2. +Proof. + intros p s s1 s2 Heval Heq. + exists s1. split; assumption. +Qed. (** For CNOs specifically, if s =st= s', then eval p s s evaluates the same as eval p s' s' *) Lemma cno_eval_on_equal_states : @@ -678,16 +834,19 @@ Lemma cno_eval_on_equal_states : (exists s1, eval p s s1) <-> (exists s2, eval p s' s2). Proof. intros p s s' H_cno H_eq. - split; intros [sx H_eval]. - - (* Forward: eval p s sx and s =st= s' ==> eval p s' sx *) - exists sx. - eapply eval_respects_state_eq_left. - + eassumption. - + assumption. - - (* Backward: eval p s' sx and s =st= s' ==> eval p s sx *) - exists sx. - eapply eval_respects_state_eq_left. - + eassumption. - + apply state_eq_sym. assumption. + split. + { (* Forward direction *) + intros [sx H_eval]. + destruct (eval_respects_state_eq_left _ _ _ _ H_eq H_eval) + as [sx' [H_eval' _]]. + exists sx'. assumption. + } + { (* Backward direction *) + intros [sx H_eval]. + destruct (eval_respects_state_eq_left _ _ _ _ + (state_eq_sym _ _ H_eq) H_eval) + as [sx' [H_eval' _]]. + exists sx'. assumption. + } Qed. diff --git a/proofs/coq/physics/StatMech.v b/proofs/coq/physics/StatMech.v index 5fb5ec6..4e3c53f 100644 --- a/proofs/coq/physics/StatMech.v +++ b/proofs/coq/physics/StatMech.v @@ -251,12 +251,20 @@ Qed. (** Bennett (1973): Computation can be made thermodynamically reversible by never erasing information, only permuting it. *) -(** A program is logically reversible if it's bijective *) +(** A program is logically reversible if it's bijective. + + Stage 3 (standards#157) note: the conclusion is phrased modulo + [=st=] (the relaxed Stage-2 state equality that ignores + [state_pc]) rather than strict equality on [s]. This is necessary + because [eval] from a re-entered state may differ from [s] only on + the program counter, and Stage 2 explicitly chose to ignore that + field in the semantic notion of state-equivalence. The + [cno_logically_reversible] proof below witnesses this directly. *) Definition logically_reversible (p : Program) : Prop := exists p_inv : Program, forall s s', eval p s s' -> - eval p_inv s' s. + exists s_inv, eval p_inv s' s_inv /\ s_inv =st= s. (** Logical reversibility implies thermodynamic reversibility *) @@ -292,7 +300,13 @@ Proof. reflexivity. Qed. -(** CNOs are trivially logically reversible (identity is its own inverse) *) +(** CNOs are trivially logically reversible (identity is its own inverse). + + Stage 3 (standards#157) note: with [logically_reversible] now + phrased existentially modulo [=st=], the proof no longer needs an + [eval_respects_state_eq_*] coercion: we witness the inverse run + directly from CNO termination, then use the CNO state-preservation + property to discharge the [=st=] obligation by transitivity. *) Theorem cno_logically_reversible : forall p : Program, is_CNO p -> @@ -303,36 +317,28 @@ Proof. exists p. (* CNO is its own inverse *) intros s s' H_eval. - (* Key insight: For a CNO, eval p s s' implies s =st= s' - So "reversing" just means running p again on s', which maps back to s. - Since s =st= s', running p on s' gives a result =st= to s'. *) - (* Step 1: CNO property gives us s =st= s' *) assert (s =st= s') as H_state_eq. { apply cno_preserves_state with (p := p) (s := s) (s' := s'). - assumption. - assumption. } - (* Step 2: By termination, eval p s' s'' for some s'' *) - destruct (cno_terminates p H_cno s') as [s'' H_eval']. + (* Step 2: By termination, eval p s' s_inv for some s_inv *) + destruct (cno_terminates p H_cno s') as [s_inv H_eval']. - (* Step 3: By CNO identity property, s' =st= s'' *) - assert (s' =st= s'') as H_s'_eq_s''. - { apply cno_preserves_state with (p := p) (s := s') (s' := s''). + (* Step 3: By CNO identity property, s' =st= s_inv *) + assert (s' =st= s_inv) as H_s'_eq_s_inv. + { apply cno_preserves_state with (p := p) (s := s') (s' := s_inv). - assumption. - assumption. } - (* Step 4: By transitivity, s'' =st= s *) - assert (s'' =st= s) as H_s''_eq_s. - { apply state_eq_trans with (s2 := s'). - - apply state_eq_sym. exact H_s'_eq_s''. - - apply state_eq_sym. exact H_state_eq. } - - (* Step 5: We have eval p s' s'' and s'' =st= s - Apply eval_respects_state_eq_right to get eval p s' s *) - apply eval_respects_state_eq_right with (s' := s''). + (* Step 4: Witness s_inv satisfies eval p s' s_inv and s_inv =st= s *) + exists s_inv. split. - exact H_eval'. - - exact H_s''_eq_s. + - (* s_inv =st= s by transitivity: s_inv =st= s' =st= s *) + apply state_eq_trans with (s2 := s'). + + apply state_eq_sym. assumption. + + apply state_eq_sym. assumption. Qed. (** ** Physical Implications *)