diff --git a/src/proto_alpha/lib_protocol/dal_slot_repr.ml b/src/proto_alpha/lib_protocol/dal_slot_repr.ml index 4db27295f63eae8d98d682900a1b8d6aa6a62212..f6a6db2cd244588afa511b7ef960465ad10cc1be 100644 --- a/src/proto_alpha/lib_protocol/dal_slot_repr.ml +++ b/src/proto_alpha/lib_protocol/dal_slot_repr.ml @@ -1486,9 +1486,6 @@ module History_v2 = struct pp_inclusion_proof inc_proof) - (* TODO: will be uncommented incrementally on the next MRs *) - - (* type error += | Dal_proof_error_v2 of string | Unexpected_page_size_v2 of {expected_size : int; page_size : int} @@ -1558,85 +1555,83 @@ module History_v2 = struct page_size = Bytes.length data; } + (** The [produce_proof_repr] function assumes that some invariants hold, such as: + - The DAL has been activated, + - The level of [page_id] is after the DAL activation level. + + Under these assumptions, we recall that we maintain an invariant + ensuring that we a have a cell per slot index in the skip list at every level + after DAL activation. *) let produce_proof_repr dal_params page_id ~page_info ~get_history slots_hist = let open Lwt_result_syntax in - let Page.{slot_id; page_index = _} = page_id in - (* We search for a slot whose ID is equal to target_id. *) + let Page.{slot_id = target_slot_id; page_index = _} = page_id in + (* We first search for the slots attested at level [published_level]. *) let*! search_result = - Skip_list.search ~deref:get_history ~target_id:slot_id ~cell:slots_hist + Skip_list.search ~deref:get_history ~target_slot_id ~cell:slots_hist in - match (page_info, search_result.Skip_list.last_cell) with - | _, Deref_returned_none -> + (* The search should necessarily find a cell in the skip list (assuming + enough cache is given) under the assumptions made when calling + {!produce_proof_repr}. *) + match search_result.Skip_list.last_cell with + | Deref_returned_none -> tzfail @@ dal_proof_error "Skip_list.search returned 'Deref_returned_none': Slots history \ cache is ill-formed or has too few entries." - | _, No_exact_or_lower_ptr -> + | No_exact_or_lower_ptr -> tzfail @@ dal_proof_error "Skip_list.search returned 'No_exact_or_lower_ptr', while it is \ initialized with a min elt (slot zero)." - | Some (page_data, page_proof), Found target_cell -> - (* The slot to which the page is supposed to belong is found. *) - let Header.{id; commitment} = Skip_list.content target_cell in - (* We check that the slot is not the dummy slot. *) - let*? () = - error_when - Compare.Int.(Header.compare_slot_id id Header.zero.id = 0) - (dal_proof_error - "Skip_list.search returned 'Found ': No existence \ - proof should be constructed with the slot zero.") - in - let*? () = - check_page_proof dal_params page_proof page_data page_id commitment - in - let inc_proof = List.rev search_result.Skip_list.rev_path in - let*? () = - error_when - (List.is_empty inc_proof) - (dal_proof_error "The inclusion proof cannot be empty") - in - (* All checks succeeded. We return a `Page_confirmed` proof. *) - return - ( Page_confirmed {inc_proof; target_cell; page_data; page_proof}, - Some page_data ) - | None, Nearest {lower = prev_cell; upper = next_cell_opt} -> - (* There is no previously confirmed slot in the skip list whose ID - corresponds to the {published_level; slot_index} information - given in [page_id]. But, `search` returned a skip list [prev_cell] - (and possibly [next_cell_opt]) such that: - - the ID of [prev_cell]'s slot is the biggest immediately smaller than - the page's information {published_level; slot_index} - - if not equal to [None], the ID of [next_cell_opt]'s slot is the smallest - immediately bigger than the page's slot id `slot_id`. - - if [next_cell_opt] is [None] then, [prev_cell] should be equal to - the given history_proof cell. *) - let* next_inc_proof = - match search_result.Skip_list.rev_path with - | [] -> assert false (* Not reachable *) - | prev :: rev_next_inc_proof -> - let*? () = - error_unless - (equal_history prev prev_cell) - (dal_proof_error - "Internal error: search's Nearest result is \ - inconsistent.") - in - return @@ List.rev rev_next_inc_proof - in - return - (Page_unconfirmed {prev_cell; next_cell_opt; next_inc_proof}, None) - | None, Found _ -> - tzfail - @@ dal_proof_error - "The page ID's slot is confirmed, but no page content and proof \ - are provided." - | Some _, Nearest _ -> + | Nearest _ -> + (* This should not happen: there is one cell at each level + after DAL activation. The case where the page's level is before DAL + activation level should be handled by the caller + ({!Sc_refutation_proof.produce} in our case). *) tzfail @@ dal_proof_error - "The page ID's slot is not confirmed, but page content and \ - proof are provided." + "Skip_list.search returned Nearest', while all given levels to \ + produce proofs are supposed to be in the skip list." + | Found target_cell -> ( + let inc_proof = List.rev search_result.Skip_list.rev_path in + match (page_info, Skip_list.content target_cell) with + | Some (page_data, page_proof), Attested {commitment; id = _} -> + (* The case where the slot to which the page is supposed to belong + is found and the page's information are given. *) + let*? () = + (* We check the page's proof against the commitment. *) + check_page_proof + dal_params + page_proof + page_data + page_id + commitment + in + (* All checks succeeded. We return a `Page_confirmed` proof. *) + return + ( Page_confirmed {target_cell; inc_proof; page_data; page_proof}, + Some page_data ) + | None, Unattested _ -> + (* The slot corresponding to the given page's index is not found in + the attested slots of the page's level, and no information is + given for that page. So, we produce a proof that the page is not + attested. *) + return (Page_unconfirmed {target_cell; inc_proof}, None) + | None, Attested _ -> + (* Mismatch: case where no page information are given, but the + slot is attested. *) + tzfail + @@ dal_proof_error + "The page ID's slot is confirmed, but no page content and \ + proof are provided." + | Some _, Unattested _ -> + (* Mismatch: case where page information are given, but the slot + is not attested. *) + tzfail + @@ dal_proof_error + "The page ID's slot is not confirmed, but page content and \ + proof are provided.") let produce_proof dal_params page_id ~page_info ~get_history slots_hist = let open Lwt_result_syntax in @@ -1670,97 +1665,77 @@ module History_v2 = struct let verify_proof_repr dal_params page_id snapshot proof = let open Result_syntax in - let Page.{slot_id; page_index = _} = page_id in - match proof with - | Page_confirmed {target_cell; page_data; page_proof; inc_proof} -> - (* If the page is supposed to be confirmed, the last cell in - [inc_proof] should store the slot of the page. *) - let Header.{id; commitment} = Skip_list.content target_cell in - let* () = - error_when - Compare.Int.(Header.compare_slot_id id Header.zero.id = 0) - (dal_proof_error - "verify_proof_repr: cannot construct a confirmation page \ - proof with 'zero' as target slot.") - in - let* () = - verify_inclusion_proof inc_proof ~src:snapshot ~dest:target_cell - in - (* We check that the page indeed belongs to the target slot at the - given page index. *) - let* () = - check_page_proof dal_params page_proof page_data page_id commitment - in - (* If all checks succeed, we return the data/content of the page. *) + let Page.{slot_id = Header.{published_level; index}; page_index = _} = + page_id + in + let* target_cell, inc_proof, page_proof_check = + match proof with + | Page_confirmed {target_cell; inc_proof; page_data; page_proof} -> + let page_proof_check = + Some + (fun commitment -> + (* We check that the page indeed belongs to the target slot at the + given page index. *) + let* () = + check_page_proof + dal_params + page_proof + page_data + page_id + commitment + in + (* If the check succeeds, we return the data/content of the + page. *) + return page_data) + in + return (target_cell, inc_proof, page_proof_check) + | Page_unconfirmed {target_cell; inc_proof} -> + return (target_cell, inc_proof, None) + in + let cell_content = Skip_list.content target_cell in + (* We check that the target cell has the same level and index than the + page we're about to prove. *) + let cell_id = Content.content_id cell_content in + let* () = + error_when + Raw_level_repr.(cell_id.published_level <> published_level) + (dal_proof_error "verify_proof_repr: published_level mismatch.") + in + let* () = + error_when + (not (Dal_slot_index_repr.equal cell_id.index index)) + (dal_proof_error "verify_proof_repr: slot index mismatch.") + in + (* We check that the given inclusion proof indeed links our L1 snapshot to + the target cell. *) + let* () = + verify_inclusion_proof inc_proof ~src:snapshot ~dest:target_cell + in + match (page_proof_check, cell_content) with + | None, Unattested _ -> return_none + | Some page_proof_check, Attested {commitment; _} -> + let* page_data = page_proof_check commitment in return_some page_data - | Page_unconfirmed {prev_cell; next_cell_opt; next_inc_proof} -> - (* The page's slot is supposed to be unconfirmed. *) - let ( < ) a b = Compare.Int.(Header.compare_slot_id a b < 0) in - (* We retrieve the last cell of the inclusion proof to be able to - call {!verify_inclusion_proof}. We also do some well-formedness on - the shape of the inclusion proof (see the case [Page_unconfirmed] - of type {!proof}). *) - let* () = - match next_cell_opt with - | None -> - let* () = - error_unless - (List.is_empty next_inc_proof) - (dal_proof_error - "verify_proof_repr: invalid next_inc_proof") - in - (* In case the inclusion proof has no elements, we check that: - - the prev_cell slot's id is smaller than the unconfirmed slot's ID - - the snapshot is equal to the [prev_cell] skip list. - - This way, and since the skip list is sorted wrt. - {!compare_slot_id}, we are sure that the skip list whose head - is [snapshot] = [prev_cell] cannot contain a slot whose ID is - [slot_id]. *) - error_unless - ((Skip_list.content prev_cell).id < slot_id - && equal_history snapshot prev_cell) - (dal_proof_error "verify_proof_repr: invalid next_inc_proof") - | Some next_cell -> - (* In case the inclusion proof has at least one element, - we check that: - - the [prev_cell] slot's id is smaller than [slot_id] - - the [next_cell] slot's id is greater than [slot_id] - - the [next_cell] cell is a direct successor of the - [prev_cell] cell. - - the [next_cell] cell is a predecessor of [snapshot] - - Since the skip list is sorted wrt. {!compare_slot_id}, and - if the call to {!verify_inclusion_proof} succeeds, we are - sure that the skip list whose head is [snapshot] cannot - contain a slot whose ID is [slot_id]. *) - let* () = - error_unless - ((Skip_list.content prev_cell).id < slot_id - && slot_id < (Skip_list.content next_cell).id - && - let prev_cell_pointer = - Skip_list.back_pointer next_cell 0 - in - match prev_cell_pointer with - | None -> false - | Some prev_ptr -> - Pointer_hash.equal prev_ptr (hash prev_cell)) - (dal_proof_error - "verify_proof_repr: invalid next_inc_proof") - in - verify_inclusion_proof - next_inc_proof - ~src:snapshot - ~dest:next_cell - in - return_none + | Some _, Unattested _ -> + error + @@ dal_proof_error + "verify_proof_repr: the unconfirmation proof contains the \ + target slot." + | None, Attested _ -> + error + @@ dal_proof_error + "verify_proof_repr: the confirmation proof doesn't contain the \ + attested slot." let verify_proof dal_params page_id snapshot serialized_proof = let open Result_syntax in let* proof_repr = deserialize_proof serialized_proof in verify_proof_repr dal_params page_id snapshot proof_repr + (* TODO: will be uncommented incrementally on the next MRs *) + + (* + module Internal_for_tests = struct let content = Skip_list.content diff --git a/src/proto_alpha/lib_protocol/dal_slot_repr.mli b/src/proto_alpha/lib_protocol/dal_slot_repr.mli index 4c7cfef28aa607c0486976cf3eaae501bc2f3be6..14c6089761d99d5a536baf86cef35d171de63c6b 100644 --- a/src/proto_alpha/lib_protocol/dal_slot_repr.mli +++ b/src/proto_alpha/lib_protocol/dal_slot_repr.mli @@ -291,6 +291,10 @@ module History : sig should be provided, as they are not needed to construct a non-confirmation proof. + The function returns an error in case the slot is not confirmed but the + page's content and proof are given. It also fails if the slot is confirmed + but no or bad information about the page are provided. + [dal_parameters] is used when verifying that/if the page is part of the candidate slot (if any). *)