From 1c6a24f7538f33fddc60816d3b29ae0044305caa Mon Sep 17 00:00:00 2001 From: Wolfgang Jeltsch Date: Sun, 26 Nov 2023 22:43:14 +0200 Subject: [PATCH] Correct and simplify server program MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This commit additionally includes the following changes: * Cause rollback after `IntersectFound` to happen also when the server chain hasn’t changed * Streamline the conformance proof * Turn the names of the universally quantified variables in the conformance proof into single-letter variants * Make the subproof of `program Server` conformance more robust by removing the dependency on subgoals left over by an automated prover --- src/Ouroboros-Mini_Protocols-Chain_Sync.thy | 112 +++++++++++--------- 1 file changed, 60 insertions(+), 52 deletions(-) diff --git a/src/Ouroboros-Mini_Protocols-Chain_Sync.thy b/src/Ouroboros-Mini_Protocols-Chain_Sync.thy index 7aa75d7..c6a86e3 100644 --- a/src/Ouroboros-Mini_Protocols-Chain_Sync.thy +++ b/src/Ouroboros-Mini_Protocols-Chain_Sync.thy @@ -134,16 +134,21 @@ definition index :: "('i \ 'q) \ 'q \ 'i lis definition first_intersection_point :: "('i \ 'q) \ 'q list \ 'i list \ 'q" where [simp]: "first_intersection_point \ qs C = find (\q. q \ \ ` set C) qs" -definition - chain_update_reaction :: "('i \ 'q) \ nat \ 'i list \ 'i list \ ('i, 'q) message \ nat" -where - [simp]: "chain_update_reaction \ k C C' = +datatype ('i, 'p) server_step = + is_wait: Wait | + is_progress: Progress \('i, 'p) message\ \'i list\ + +definition server_step :: "('i \ 'q) \ 'i list \ 'i list \ ('i, 'q) server_step" where + [simp]: "server_step \ C\<^sub>c C\<^sub>s = ( - if prefix C C' then - (RollForward (C' ! Suc k), Suc k) + if C\<^sub>c = C\<^sub>s then + Wait + else if prefix C\<^sub>c C\<^sub>s then + let C\<^sub>c' = C\<^sub>c @ [C\<^sub>s ! length C\<^sub>c] in + Progress (RollForward (last C\<^sub>c')) C\<^sub>c' else - let C\<^sub>p = longest_common_prefix C C' in - (RollBackward (\ (last C\<^sub>p)), length C\<^sub>p - 1) + let C\<^sub>c' = longest_common_prefix C\<^sub>c C\<^sub>s in + Progress (RollBackward (\ (last C\<^sub>c'))) C\<^sub>c' )" datatype server_phase = @@ -160,48 +165,46 @@ text \ \ corec server_program where - "server_program \ u k b C \ = (case \ of + "server_program \ u b C\<^sub>c \ = (case \ of ClientLagging \ \ M. (partial_case M of Done \ \ | Cont (FindIntersect qs) \ - (case first_intersection_point \ qs C of + u \ C\<^sub>s. + (case first_intersection_point \ qs C\<^sub>s of None \ \ Cont IntersectNotFound; - server_program \ u k b C \ | + server_program \ u b C\<^sub>c \ | Some q \ \ Cont (IntersectFound q); - server_program \ u (index \ q C) True C \ + server_program \ u True (take (Suc (index \ q C\<^sub>s)) C\<^sub>s) \ ) | Cont RequestNext \ - u \ C'. ( - if C' = C then - if b then - \ Cont (RollBackward (\ (C ! k))); - server_program \ u k False C \ - else if Suc k < length C then - \ Cont (RollForward (C ! Suc k)); - server_program \ u (Suc k) b C \ - else - \ Cont AwaitReply; - server_program \ u k b C ClientCatchUp + if b then + \ Cont (RollBackward (\ (last C\<^sub>c))); + server_program \ u False C\<^sub>c \ else - let (M', k') = chain_update_reaction \ k C C' in - \ Cont M'; - server_program \ u k' b C' \ + u \ C\<^sub>s. + (case server_step \ C\<^sub>c C\<^sub>s of + Wait \ + \ Cont AwaitReply; + server_program \ u b C\<^sub>c ClientCatchUp | + Progress m C\<^sub>c' \ + \ Cont m; + server_program \ u b C\<^sub>c' \ + ) ) ) | ClientCatchUp \ - u \ C'. - ( - if C' = C then - server_program \ u k b C \ - else - let (M', k') = chain_update_reaction \ k C C' in - \ Cont M'; - server_program \ u k' b C' ClientLagging + u \ C\<^sub>s. + (case server_step \ C\<^sub>c C\<^sub>s of + Wait \ + server_program \ u b C\<^sub>c \ | + Progress m C\<^sub>c' \ + \ Cont m; + server_program \ u b C\<^sub>c' ClientLagging ) )" @@ -217,13 +220,12 @@ primrec program where initial_client_chain IntersectionFinding" | "program Server = - server_chain_updates \ C. + server_chain_updates \ C\<^sub>s. server_program point server_chain_updates - 0 False - C + [hd C\<^sub>s] ClientLagging" end @@ -231,38 +233,44 @@ end sublocale chain_sync \ protocol_programs \possibilities\ \program\ proof have " - client_program point client_chain_updates candidate_intersection_points initial_client_chain phase + client_program point client_chain_updates candidate_intersection_points initial_client_chain \ \\<^bsub>Client\<^esub> - Cont possibilities" - for phase + Cont \state_machine\" + for \ by - (coinduction arbitrary: initial_client_chain phase rule: up_to_embedding_is_sound) + (coinduction arbitrary: initial_client_chain \ rule: up_to_embedding_is_sound) (state_machine_bisimulation program_expansion: client_program.code extra_splits: client_phase.splits or_done.splits message.splits ) + then have "program Client \\<^bsub>Client\<^esub> Cont possibilities" + by (simp add: protocol_state_machine.possibilities_def) moreover have " - server_program point server_chain_updates read_pointer must_roll_back initial_server_chain phase + server_program point server_chain_updates b C\<^sub>c \ \\<^bsub>Server\<^esub> - Cont \state_machine \initial_state := state_in_server_phase phase\\" - for read_pointer and must_roll_back and initial_server_chain and phase + Cont \state_machine \initial_state := state_in_server_phase \\\" + for b and C\<^sub>c and \ by - (coinduction - arbitrary: read_pointer must_roll_back initial_server_chain phase - rule: up_to_embedding_is_sound - ) + (coinduction arbitrary: b C\<^sub>c \ rule: up_to_embedding_is_sound) (state_machine_bisimulation program_expansion: server_program.code - extra_splits: server_phase.splits or_done.splits message.splits option.splits + extra_splits: server_phase.splits or_done.splits message.splits option.splits server_step.splits ) then have "program Server \\<^bsub>Server\<^esub> Cont possibilities" - unfolding possibilities_def + using import_conformance by - (simp, intro import_conformance) - (metis comp_apply state_in_server_phase.simps(1)) + (smt + program.simps(2) + possibilities_def + state_machine_def + state_machine.simps(6) + state_in_server_phase.simps(1) + comp_apply + ) ultimately show "program p \\<^bsub>p\<^esub> Cont possibilities" for p by (cases p) simp_all + qed subsection \The End\