{"id":"pbft-view-change-safety-holds-with-stable-digests","text":"PBFT view changes maintain safety (2f+1 agreement) and liveness (carrying prepared requests forward with contiguous sequence numbers into the new view), ensuring no committed request is lost across leader transitions.","truth_value":"IN","source":"","source_url":"","source_hash":"","justifications":[{"type":"SL","antecedents":["pbft-view-change-preserves-safety-and-liveness","pbft-executed-log-sequence-numbers-contiguous"],"outlist":["pbft-default-str-fragile"],"label":"The fragile default=str digest function could cause honest nodes to compute different digests for identical requests, breaking prepared certificate matching and undermining the 2f+1 threshold"}],"dependents":[],"metadata":{},"created_at":"","updated_at":"","reviewed_at":"","verified_at":"","retracted_at":"","explanation":{"steps":[{"node":"pbft-view-change-safety-holds-with-stable-digests","truth_value":"IN","reason":"SL justification valid","antecedents":["pbft-view-change-preserves-safety-and-liveness","pbft-executed-log-sequence-numbers-contiguous"],"label":"The fragile default=str digest function could cause honest nodes to compute different digests for identical requests, breaking prepared certificate matching and undermining the 2f+1 threshold","outlist":["pbft-default-str-fragile"]},{"node":"pbft-view-change-preserves-safety-and-liveness","truth_value":"IN","reason":"SL justification valid","antecedents":["pbft-view-change-preserves-prepared-requests","view-change-requires-2f-plus-1"],"label":"Two independent observations confirm that the implementation correctly handles both halves of the view-change correctness argument"},{"node":"pbft-view-change-preserves-prepared-requests","truth_value":"IN","reason":"premise"},{"node":"view-change-requires-2f-plus-1","truth_value":"IN","reason":"premise"},{"node":"pbft-executed-log-sequence-numbers-contiguous","truth_value":"IN","reason":"premise"}]}}