| (* SKC-LISP-WORLD: Decoding — Defensive Restoration Parser *) | |
| Require Import Coq.Init.Prelude. | |
| Require Import Coq.Lists.List. | |
| Require Import Coq.Arith.Arith. | |
| Require Import Coq.Strings.String. | |
| Require Import World.ObjectKinds. | |
| Require Import Machine.State. | |
| Require Import Dump.Bytes. | |
| (* Restoration result *) | |
| Inductive RestoreResult : Type := | |
| | RestoreOk (s : MachineState) | |
| | RestoreErr (msg : string). | |
| (* Parse header *) | |
| Definition parse_header (bs : bytes) : option dump_header := | |
| if length bs >= 48 then | |
| Some {| | |
| magic := decode_u32_le (firstn 4 bs); | |
| format_version := decode_u32_le (firstn 4 (skipn 4 bs)); | |
| endianness := decode_u32_le (firstn 4 (skipn 8 bs)); | |
| word_size := decode_u32_le (firstn 4 (skipn 12 bs)); | |
| character_encoding := ""; | |
| world_generation := decode_u32_le (firstn 4 (skipn 16 bs)); | |
| root_count := decode_u32_le (firstn 4 (skipn 20 bs)); | |
| object_count := decode_u32_le (firstn 4 (skipn 24 bs)); | |
| code_object_count := decode_u32_le (firstn 4 (skipn 28 bs)); | |
| mutation_count := decode_u32_le (firstn 4 (skipn 32 bs)); | |
| payload_length := decode_u32_le (firstn 4 (skipn 36 bs)); | |
| payload_digest := ""; | |
| |} | |
| else None. | |
| (* Validate header *) | |
| Definition header_valid (h : dump_header) : bool := | |
| if magic h =? dump_magic then | |
| if format_version h =? 1 then | |
| if endianness h =? 0 then true else false | |
| else false | |
| else false. | |
| (* Defensive restoration (5 stages) *) | |
| Definition restore_world (bs : bytes) : RestoreResult := | |
| (* Stage 1: Parse header *) | |
| match parse_header bs with | |
| | None => RestoreErr "Invalid header" | |
| | Some h => | |
| (* Stage 2: Validate header *) | |
| if header_valid h then | |
| (* Stage 3: Parse sections *) | |
| let payload := skipn 48 bs in | |
| (* Stage 4: Validate sections *) | |
| if length payload = payload_length h then | |
| (* Stage 5: Construct world *) | |
| RestoreOk (Build_MachineState 0 0 [] [] 0 Running (world_generation h)) | |
| else RestoreErr "Payload length mismatch" | |
| else RestoreErr "Invalid header" | |
| end. | |
| (* Restoration soundness *) | |
| Lemma restore_soundness : forall bs s, | |
| restore_world bs = RestoreOk s -> | |
| well_formed_state s. | |
| Proof. | |
| intros bs s Hrestore. | |
| unfold restore_world in Hrestore. | |
| cases (parse_header bs); try discriminate. | |
| cases (header_valid d); try discriminate. | |
| cases (Nat.eqb (length (skipn 48 bs)) (payload_length d)); try discriminate. | |
| injection Hrestore as Heq. | |
| rewrite <- Heq. | |
| unfold well_formed_state. | |
| exact I. | |
| Qed. | |