)]}'
{"/PATCHSET_LEVEL":[{"author":{"_account_id":1000000,"name":"Nico Huber","email":"nico.h@gmx.de","username":"icon","avatars":[{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"5ad750f06f473435475957327119d1b35fb1dd09","unresolved":false,"context_lines":[],"source_content_type":"","patch_set":1,"id":"b1d8f7da_261d45ab","updated":"2026-04-18 13:08:11.000000000","message":"Thanks a lot for all the reviews, Angel!","commit_id":"9b83390776337881fdbe7cf059b6d90f07e9e297"}],"common/hw-gfx-gma-pipe_setup.adb":[{"author":{"_account_id":1000012,"name":"Angel Pons","email":"th3fanbus@gmail.com","username":"th3fanbus","avatars":[{"url":"https://www.gravatar.com/avatar/61cdfc186d8caca5a8908b0a382de6d8.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/61cdfc186d8caca5a8908b0a382de6d8.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/61cdfc186d8caca5a8908b0a382de6d8.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/61cdfc186d8caca5a8908b0a382de6d8.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"fbbb2d06b8e946eeeb1a46340772645ac180ee67","unresolved":true,"context_lines":[{"line_number":408,"context_line":"            Width  :\u003d Max_Width;"},{"line_number":409,"context_line":"         when Pillarbox \u003d\u003e"},{"line_number":410,"context_line":"            Width  :\u003d (Src_Width * Max_Height) / Src_Height;"},{"line_number":411,"context_line":"            pragma Assert (Max_Height * Src_Width \u003c Max_Width * Src_Height);"},{"line_number":412,"context_line":"            pragma Assert ((Max_Height * Src_Width) / Src_Height \u003c Max_Width);"},{"line_number":413,"context_line":"            pragma Assert (Width \u003c\u003d Max_Width);"},{"line_number":414,"context_line":"            Height :\u003d Max_Height;"},{"line_number":415,"context_line":"         when Uniform \u003d\u003e"}],"source_content_type":"application/octet-stream","patch_set":1,"id":"93451b43_8a13e139","line":412,"range":{"start_line":411,"start_character":12,"end_line":412,"end_character":78},"updated":"2026-04-18 10:41:40.000000000","message":"Aren\u0027t these two assertions mostly equivalent? Or am I missing something?","commit_id":"9b83390776337881fdbe7cf059b6d90f07e9e297"},{"author":{"_account_id":1000000,"name":"Nico Huber","email":"nico.h@gmx.de","username":"icon","avatars":[{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/60d420b5d650d48b86d6921a9f683b64.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"5ad750f06f473435475957327119d1b35fb1dd09","unresolved":true,"context_lines":[{"line_number":408,"context_line":"            Width  :\u003d Max_Width;"},{"line_number":409,"context_line":"         when Pillarbox \u003d\u003e"},{"line_number":410,"context_line":"            Width  :\u003d (Src_Width * Max_Height) / Src_Height;"},{"line_number":411,"context_line":"            pragma Assert (Max_Height * Src_Width \u003c Max_Width * Src_Height);"},{"line_number":412,"context_line":"            pragma Assert ((Max_Height * Src_Width) / Src_Height \u003c Max_Width);"},{"line_number":413,"context_line":"            pragma Assert (Width \u003c\u003d Max_Width);"},{"line_number":414,"context_line":"            Height :\u003d Max_Height;"},{"line_number":415,"context_line":"         when Uniform \u003d\u003e"}],"source_content_type":"application/octet-stream","patch_set":1,"id":"ec587a0e_38e7f720","line":412,"range":{"start_line":411,"start_character":12,"end_line":412,"end_character":78},"in_reply_to":"93451b43_8a13e139","updated":"2026-04-18 13:08:11.000000000","message":"They are. But technically all assertion that are used to assist automatic proofs\nare just rephrasing what is already know.\n\nThis particular step is not as easy as it seems if you think about integers\ninstead of abstract numbers. For instance, one has to consider that rounding\nworks in our favor here.","commit_id":"9b83390776337881fdbe7cf059b6d90f07e9e297"},{"author":{"_account_id":1000012,"name":"Angel Pons","email":"th3fanbus@gmail.com","username":"th3fanbus","avatars":[{"url":"https://www.gravatar.com/avatar/61cdfc186d8caca5a8908b0a382de6d8.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/61cdfc186d8caca5a8908b0a382de6d8.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/61cdfc186d8caca5a8908b0a382de6d8.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/61cdfc186d8caca5a8908b0a382de6d8.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"b0e15411de0864d8722362f245358f3f4148b3a1","unresolved":false,"context_lines":[{"line_number":408,"context_line":"            Width  :\u003d Max_Width;"},{"line_number":409,"context_line":"         when Pillarbox \u003d\u003e"},{"line_number":410,"context_line":"            Width  :\u003d (Src_Width * Max_Height) / Src_Height;"},{"line_number":411,"context_line":"            pragma Assert (Max_Height * Src_Width \u003c Max_Width * Src_Height);"},{"line_number":412,"context_line":"            pragma Assert ((Max_Height * Src_Width) / Src_Height \u003c Max_Width);"},{"line_number":413,"context_line":"            pragma Assert (Width \u003c\u003d Max_Width);"},{"line_number":414,"context_line":"            Height :\u003d Max_Height;"},{"line_number":415,"context_line":"         when Uniform \u003d\u003e"}],"source_content_type":"application/octet-stream","patch_set":1,"id":"9bcaf55c_50a5d4b6","line":412,"range":{"start_line":411,"start_character":12,"end_line":412,"end_character":78},"in_reply_to":"ec587a0e_38e7f720","updated":"2026-04-18 14:34:18.000000000","message":"Ah, I see it now. Thank you!","commit_id":"9b83390776337881fdbe7cf059b6d90f07e9e297"}]}