)]}'
{"/COMMIT_MSG":[{"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":"87c76e439543d1d45318a7a22502a495e13ed585","unresolved":false,"context_lines":[{"line_number":10,"context_line":"ceiling is 0x100000. Every DisplayPort rate is above that ceiling, so"},{"line_number":11,"context_line":"link N was 0x100000 for all link rates (RBR, HBR, and HBR2)."},{"line_number":12,"context_line":""},{"line_number":13,"context_line":"i915 rounds the link clock in kHz. 270000 becomes 0x80000 and"},{"line_number":14,"context_line":"540000 becomes 0x100000. The edk2 Haswell GOP driver likewise programs"},{"line_number":15,"context_line":"0x80000 for a 2.7 GHz eDP link. Divide the link clock and dotclock by"},{"line_number":16,"context_line":"1000 before the existing round so HBR matches them, and HBR2 still"},{"line_number":17,"context_line":"reaches 0x100000."}],"source_content_type":"text/x-gerrit-commit-message","patch_set":1,"id":"114d5796_916a7475","line":14,"range":{"start_line":13,"start_character":0,"end_line":14,"end_character":24},"updated":"2026-10-28 23:10:22.000000000","message":"Looks like that\u0027s what they did 9 years ago ;)","commit_id":"cb712be6e583f230d8807d024b226c97d1a6bc58"}],"/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":"87c76e439543d1d45318a7a22502a495e13ed585","unresolved":true,"context_lines":[],"source_content_type":"","patch_set":1,"id":"1d4366de_1f07cbb2","updated":"2026-10-28 23:10:22.000000000","message":"Looks like `i915` had some back and forth because some N values didn\u0027t work. Let\u0027s have a look at the numbers first. `i915` uses constant N values that supposedly match Windows/GOP for 4 years now (c46af5621a drm/i915: Use a fixed N value always). I guess we should consider to follow. Though this seems to have high regression potential.\n\nDo you have the logs at hand? I want to make sure that we don\u0027t cover up another bug.","commit_id":"cb712be6e583f230d8807d024b226c97d1a6bc58"},{"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":"913ae2ed7b0d8f34e6ae4652e0b0bea526984170","unresolved":true,"context_lines":[],"source_content_type":"","patch_set":1,"id":"2aa88f65_6aa24f4b","in_reply_to":"10dde3b2_ce70f796","updated":"2026-10-29 11:51:04.000000000","message":"Also noticed the `0x8000000` (2^27) in i915 (`intel_link_compute_m_n()`) looks like a typo. They have to reduce that later to 24 bits anyway.","commit_id":"cb712be6e583f230d8807d024b226c97d1a6bc58"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"864615c6d022f8be20f6b486be20d881a595074b","unresolved":true,"context_lines":[],"source_content_type":"","patch_set":1,"id":"32a4e931_e274ba90","in_reply_to":"1d4366de_1f07cbb2","updated":"2026-10-29 02:49:30.000000000","message":"two users that had the issue on Falco posted some on my github issue tracker here: the user attached some logs to the issue here: https://github.com/MrChromebox/firmware/issues/1044\n\nI don\u0027t have any from testing on Wolf (HSW) but I didn\u0027t have the issue there. Can grab some though if useful.","commit_id":"cb712be6e583f230d8807d024b226c97d1a6bc58"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"1285fa54e532fe2144160f27cbabece84bbed7a2","unresolved":false,"context_lines":[],"source_content_type":"","patch_set":1,"id":"3b6baf6a_47a97d31","in_reply_to":"2aa88f65_6aa24f4b","updated":"2026-10-30 14:16:17.000000000","message":"Done","commit_id":"cb712be6e583f230d8807d024b226c97d1a6bc58"},{"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":"d11b709f8bdf6fa66ada1dc748604b7b84c0adf8","unresolved":true,"context_lines":[],"source_content_type":"","patch_set":1,"id":"10dde3b2_ce70f796","in_reply_to":"32a4e931_e274ba90","updated":"2026-10-29 11:45:07.000000000","message":"Thx. I see https://github.com/user-attachments/files/33914717/cbmem.log has correct calculations / register values. If I followed the thread correctly, it\u0027s for a slightly different panel than the failing one, but I doubt the 0.014% difference matter. I assume it\u0027s a quirky panel like those i915 devs encountered.\n\nIf we change this code, we should do what Linux does now, i.e. always use the same final N values. But this will need further testing.\n\nInline is a sketch of a rewritten `Cancel_M_N ()`. Types look a bit different to prove there\u0027s no overflow. Not sure when I\u0027ll get a chance to test.","commit_id":"cb712be6e583f230d8807d024b226c97d1a6bc58"}],"common/hw-gfx-dp_info.adb":[{"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":"d11b709f8bdf6fa66ada1dc748604b7b84c0adf8","unresolved":true,"context_lines":[{"line_number":252,"context_line":"      Link_M   :    out M_Type;"},{"line_number":253,"context_line":"      Link_N   :    out N_Type)"},{"line_number":254,"context_line":"   is"},{"line_number":255,"context_line":"      DATA_N_MAX : constant :\u003d 16#800000#;"},{"line_number":256,"context_line":"      LINK_N_MAX : constant :\u003d 16#100000#;"},{"line_number":257,"context_line":""},{"line_number":258,"context_line":"      subtype Calc_M_Type is Int64 range 0 .. 2 ** 38;"},{"line_number":259,"context_line":"      subtype Calc_N_Type is Int64 range 0 .. 2 ** 38;"},{"line_number":260,"context_line":"      subtype N_Rounded_Type is Int64 range"},{"line_number":261,"context_line":"         0 .. Int64\u0027Max (DATA_N_MAX, LINK_N_MAX);"},{"line_number":262,"context_line":""},{"line_number":263,"context_line":"      M : Calc_M_Type;"},{"line_number":264,"context_line":"      N : Calc_N_Type;"},{"line_number":265,"context_line":""},{"line_number":266,"context_line":"      procedure Cancel_M_N"},{"line_number":267,"context_line":"        (M     : in out Calc_M_Type;"},{"line_number":268,"context_line":"         N     : in out Calc_N_Type;"},{"line_number":269,"context_line":"         N_Max : in     N_Rounded_Type)"},{"line_number":270,"context_line":"      with"},{"line_number":271,"context_line":"         Depends \u003d\u003e ((M, N) \u003d\u003e (M, N, N_Max)),"},{"line_number":272,"context_line":"         Pre \u003d\u003e (N \u003e 0 and M in 0 .. Calc_M_Type\u0027Last / 2),"},{"line_number":273,"context_line":"         Post \u003d\u003e (M \u003c\u003d M_N_Max and N \u003c\u003d M_N_Max)"},{"line_number":274,"context_line":"      is"},{"line_number":275,"context_line":"         Orig_N : constant Calc_N_Type :\u003d N;"},{"line_number":276,"context_line":""},{"line_number":277,"context_line":"         function Round_N (N : Calc_N_Type) return N_Rounded_Type"},{"line_number":278,"context_line":"         with"},{"line_number":279,"context_line":"            Post \u003d\u003e (Round_N\u0027Result \u003c\u003d N * 2)"},{"line_number":280,"context_line":"         is"},{"line_number":281,"context_line":"            RN : Calc_N_Type;"},{"line_number":282,"context_line":"            RN2 : Calc_N_Type :\u003d N_Max;"},{"line_number":283,"context_line":"         begin"},{"line_number":284,"context_line":"            loop"},{"line_number":285,"context_line":"               RN :\u003d RN2;"},{"line_number":286,"context_line":"               RN2 :\u003d RN2 / 2;"},{"line_number":287,"context_line":"               exit when RN2 \u003c N;"},{"line_number":288,"context_line":"               pragma Loop_Invariant (RN2 \u003d RN / 2 and RN2 in N .. N_Max);"},{"line_number":289,"context_line":"            end loop;"},{"line_number":290,"context_line":"            return RN;"},{"line_number":291,"context_line":"         end Round_N;"},{"line_number":292,"context_line":"      begin"},{"line_number":293,"context_line":"         N :\u003d Round_N (N);"},{"line_number":294,"context_line":""},{"line_number":295,"context_line":"         -- The automatic provers need a little nudge here."},{"line_number":296,"context_line":"         pragma Assert"},{"line_number":297,"context_line":"            (if M \u003c\u003d Calc_M_Type\u0027Last / 2 and"},{"line_number":298,"context_line":"                N \u003c\u003d Orig_N * 2 and"},{"line_number":299,"context_line":"                Orig_N \u003e 0 and"},{"line_number":300,"context_line":"                M \u003e 0"},{"line_number":301,"context_line":"             then"},{"line_number":302,"context_line":"                M * N / Orig_N \u003c\u003d Calc_M_Type\u0027Last);"},{"line_number":303,"context_line":""},{"line_number":304,"context_line":"         pragma Annotate (GNATprove, False_Positive,"},{"line_number":305,"context_line":"            \"assertion might fail\","},{"line_number":306,"context_line":"            \"The property cannot be proven automatically. An Isabelle proof is included as an axiom\");"},{"line_number":307,"context_line":""},{"line_number":308,"context_line":"         M :\u003d M * N / Orig_N;"},{"line_number":309,"context_line":""},{"line_number":310,"context_line":"         -- This loop is never hit for sane values (i.e. M \u003c\u003d N) but"},{"line_number":311,"context_line":"         -- we have to make sure returned values are always in range."},{"line_number":312,"context_line":"         while M \u003e M_N_Max loop"},{"line_number":313,"context_line":"            pragma Loop_Invariant (N \u003c\u003d M_N_Max);"},{"line_number":314,"context_line":"            M :\u003d M / 2;"},{"line_number":315,"context_line":"            N :\u003d N / 2;"},{"line_number":316,"context_line":"         end loop;"},{"line_number":317,"context_line":"      end Cancel_M_N;"},{"line_number":318,"context_line":"   begin"},{"line_number":319,"context_line":"      pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));"},{"line_number":320,"context_line":""}],"source_content_type":"text/x-ada","patch_set":1,"id":"c73bab47_014b45aa","side":"PARENT","line":317,"range":{"start_line":255,"start_character":0,"end_line":317,"end_character":21},"updated":"2026-10-29 11:45:07.000000000","message":"```suggestion\n      FIXED_DATA_N : constant :\u003d 16#80_0000#;\n      FIXED_LINK_N : constant :\u003d 16#08_0000#;\n\n      subtype Calc_M_Type is Int64 range 0 .. 2 ** 38;\n      subtype Calc_N_Type is Int64 range 0 .. 2 ** 38;\n      subtype Target_N_Type is Pos64 range FIXED_LINK_N .. FIXED_DATA_N;\n\n      M : Calc_M_Type;\n      N : Calc_N_Type;\n\n      procedure Cancel_M_N\n        (M        : in out Calc_M_Type;\n         N        : in out Calc_N_Type;\n         Target_N : in     Target_N_Type)\n      with\n         Depends \u003d\u003e ((M, N) \u003d\u003e (M, N, Target_N)),\n         Pre \u003d\u003e N \u003e\u003d Target_N_Type\u0027Last,\n         Post \u003d\u003e M in M_Type and N in N_Type\n      is\n      begin\n         M :\u003d M * Target_N / N;\n         N :\u003d Target_N;\n\n         -- This loop is never hit for sane values (i.e. M \u003c\u003d N) but\n         -- we have to make sure returned values are always in range.\n         while M \u003e M_N_Max loop\n            pragma Loop_Invariant (N \u003c\u003d M_N_Max);\n            M :\u003d M / 2;\n            N :\u003d N / 2;\n         end loop;\n      end Cancel_M_N;\n\n```","commit_id":"ae3fcea12c2464eacdab823e8a4192146ff93024"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"1285fa54e532fe2144160f27cbabece84bbed7a2","unresolved":false,"context_lines":[{"line_number":252,"context_line":"      Link_M   :    out M_Type;"},{"line_number":253,"context_line":"      Link_N   :    out N_Type)"},{"line_number":254,"context_line":"   is"},{"line_number":255,"context_line":"      DATA_N_MAX : constant :\u003d 16#800000#;"},{"line_number":256,"context_line":"      LINK_N_MAX : constant :\u003d 16#100000#;"},{"line_number":257,"context_line":""},{"line_number":258,"context_line":"      subtype Calc_M_Type is Int64 range 0 .. 2 ** 38;"},{"line_number":259,"context_line":"      subtype Calc_N_Type is Int64 range 0 .. 2 ** 38;"},{"line_number":260,"context_line":"      subtype N_Rounded_Type is Int64 range"},{"line_number":261,"context_line":"         0 .. Int64\u0027Max (DATA_N_MAX, LINK_N_MAX);"},{"line_number":262,"context_line":""},{"line_number":263,"context_line":"      M : Calc_M_Type;"},{"line_number":264,"context_line":"      N : Calc_N_Type;"},{"line_number":265,"context_line":""},{"line_number":266,"context_line":"      procedure Cancel_M_N"},{"line_number":267,"context_line":"        (M     : in out Calc_M_Type;"},{"line_number":268,"context_line":"         N     : in out Calc_N_Type;"},{"line_number":269,"context_line":"         N_Max : in     N_Rounded_Type)"},{"line_number":270,"context_line":"      with"},{"line_number":271,"context_line":"         Depends \u003d\u003e ((M, N) \u003d\u003e (M, N, N_Max)),"},{"line_number":272,"context_line":"         Pre \u003d\u003e (N \u003e 0 and M in 0 .. Calc_M_Type\u0027Last / 2),"},{"line_number":273,"context_line":"         Post \u003d\u003e (M \u003c\u003d M_N_Max and N \u003c\u003d M_N_Max)"},{"line_number":274,"context_line":"      is"},{"line_number":275,"context_line":"         Orig_N : constant Calc_N_Type :\u003d N;"},{"line_number":276,"context_line":""},{"line_number":277,"context_line":"         function Round_N (N : Calc_N_Type) return N_Rounded_Type"},{"line_number":278,"context_line":"         with"},{"line_number":279,"context_line":"            Post \u003d\u003e (Round_N\u0027Result \u003c\u003d N * 2)"},{"line_number":280,"context_line":"         is"},{"line_number":281,"context_line":"            RN : Calc_N_Type;"},{"line_number":282,"context_line":"            RN2 : Calc_N_Type :\u003d N_Max;"},{"line_number":283,"context_line":"         begin"},{"line_number":284,"context_line":"            loop"},{"line_number":285,"context_line":"               RN :\u003d RN2;"},{"line_number":286,"context_line":"               RN2 :\u003d RN2 / 2;"},{"line_number":287,"context_line":"               exit when RN2 \u003c N;"},{"line_number":288,"context_line":"               pragma Loop_Invariant (RN2 \u003d RN / 2 and RN2 in N .. N_Max);"},{"line_number":289,"context_line":"            end loop;"},{"line_number":290,"context_line":"            return RN;"},{"line_number":291,"context_line":"         end Round_N;"},{"line_number":292,"context_line":"      begin"},{"line_number":293,"context_line":"         N :\u003d Round_N (N);"},{"line_number":294,"context_line":""},{"line_number":295,"context_line":"         -- The automatic provers need a little nudge here."},{"line_number":296,"context_line":"         pragma Assert"},{"line_number":297,"context_line":"            (if M \u003c\u003d Calc_M_Type\u0027Last / 2 and"},{"line_number":298,"context_line":"                N \u003c\u003d Orig_N * 2 and"},{"line_number":299,"context_line":"                Orig_N \u003e 0 and"},{"line_number":300,"context_line":"                M \u003e 0"},{"line_number":301,"context_line":"             then"},{"line_number":302,"context_line":"                M * N / Orig_N \u003c\u003d Calc_M_Type\u0027Last);"},{"line_number":303,"context_line":""},{"line_number":304,"context_line":"         pragma Annotate (GNATprove, False_Positive,"},{"line_number":305,"context_line":"            \"assertion might fail\","},{"line_number":306,"context_line":"            \"The property cannot be proven automatically. An Isabelle proof is included as an axiom\");"},{"line_number":307,"context_line":""},{"line_number":308,"context_line":"         M :\u003d M * N / Orig_N;"},{"line_number":309,"context_line":""},{"line_number":310,"context_line":"         -- This loop is never hit for sane values (i.e. M \u003c\u003d N) but"},{"line_number":311,"context_line":"         -- we have to make sure returned values are always in range."},{"line_number":312,"context_line":"         while M \u003e M_N_Max loop"},{"line_number":313,"context_line":"            pragma Loop_Invariant (N \u003c\u003d M_N_Max);"},{"line_number":314,"context_line":"            M :\u003d M / 2;"},{"line_number":315,"context_line":"            N :\u003d N / 2;"},{"line_number":316,"context_line":"         end loop;"},{"line_number":317,"context_line":"      end Cancel_M_N;"},{"line_number":318,"context_line":"   begin"},{"line_number":319,"context_line":"      pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));"},{"line_number":320,"context_line":""}],"source_content_type":"text/x-ada","patch_set":1,"id":"1c00583c_2e486d36","side":"PARENT","line":317,"range":{"start_line":255,"start_character":0,"end_line":317,"end_character":21},"in_reply_to":"9475be95_5fc5f3ba","updated":"2026-10-30 14:16:17.000000000","message":"done: tested on IVB, HSW, BYT, BSW, SKL, CML","commit_id":"ae3fcea12c2464eacdab823e8a4192146ff93024"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"23860c3d106b58c58ef339632715afaff8733697","unresolved":true,"context_lines":[{"line_number":252,"context_line":"      Link_M   :    out M_Type;"},{"line_number":253,"context_line":"      Link_N   :    out N_Type)"},{"line_number":254,"context_line":"   is"},{"line_number":255,"context_line":"      DATA_N_MAX : constant :\u003d 16#800000#;"},{"line_number":256,"context_line":"      LINK_N_MAX : constant :\u003d 16#100000#;"},{"line_number":257,"context_line":""},{"line_number":258,"context_line":"      subtype Calc_M_Type is Int64 range 0 .. 2 ** 38;"},{"line_number":259,"context_line":"      subtype Calc_N_Type is Int64 range 0 .. 2 ** 38;"},{"line_number":260,"context_line":"      subtype N_Rounded_Type is Int64 range"},{"line_number":261,"context_line":"         0 .. Int64\u0027Max (DATA_N_MAX, LINK_N_MAX);"},{"line_number":262,"context_line":""},{"line_number":263,"context_line":"      M : Calc_M_Type;"},{"line_number":264,"context_line":"      N : Calc_N_Type;"},{"line_number":265,"context_line":""},{"line_number":266,"context_line":"      procedure Cancel_M_N"},{"line_number":267,"context_line":"        (M     : in out Calc_M_Type;"},{"line_number":268,"context_line":"         N     : in out Calc_N_Type;"},{"line_number":269,"context_line":"         N_Max : in     N_Rounded_Type)"},{"line_number":270,"context_line":"      with"},{"line_number":271,"context_line":"         Depends \u003d\u003e ((M, N) \u003d\u003e (M, N, N_Max)),"},{"line_number":272,"context_line":"         Pre \u003d\u003e (N \u003e 0 and M in 0 .. Calc_M_Type\u0027Last / 2),"},{"line_number":273,"context_line":"         Post \u003d\u003e (M \u003c\u003d M_N_Max and N \u003c\u003d M_N_Max)"},{"line_number":274,"context_line":"      is"},{"line_number":275,"context_line":"         Orig_N : constant Calc_N_Type :\u003d N;"},{"line_number":276,"context_line":""},{"line_number":277,"context_line":"         function Round_N (N : Calc_N_Type) return N_Rounded_Type"},{"line_number":278,"context_line":"         with"},{"line_number":279,"context_line":"            Post \u003d\u003e (Round_N\u0027Result \u003c\u003d N * 2)"},{"line_number":280,"context_line":"         is"},{"line_number":281,"context_line":"            RN : Calc_N_Type;"},{"line_number":282,"context_line":"            RN2 : Calc_N_Type :\u003d N_Max;"},{"line_number":283,"context_line":"         begin"},{"line_number":284,"context_line":"            loop"},{"line_number":285,"context_line":"               RN :\u003d RN2;"},{"line_number":286,"context_line":"               RN2 :\u003d RN2 / 2;"},{"line_number":287,"context_line":"               exit when RN2 \u003c N;"},{"line_number":288,"context_line":"               pragma Loop_Invariant (RN2 \u003d RN / 2 and RN2 in N .. N_Max);"},{"line_number":289,"context_line":"            end loop;"},{"line_number":290,"context_line":"            return RN;"},{"line_number":291,"context_line":"         end Round_N;"},{"line_number":292,"context_line":"      begin"},{"line_number":293,"context_line":"         N :\u003d Round_N (N);"},{"line_number":294,"context_line":""},{"line_number":295,"context_line":"         -- The automatic provers need a little nudge here."},{"line_number":296,"context_line":"         pragma Assert"},{"line_number":297,"context_line":"            (if M \u003c\u003d Calc_M_Type\u0027Last / 2 and"},{"line_number":298,"context_line":"                N \u003c\u003d Orig_N * 2 and"},{"line_number":299,"context_line":"                Orig_N \u003e 0 and"},{"line_number":300,"context_line":"                M \u003e 0"},{"line_number":301,"context_line":"             then"},{"line_number":302,"context_line":"                M * N / Orig_N \u003c\u003d Calc_M_Type\u0027Last);"},{"line_number":303,"context_line":""},{"line_number":304,"context_line":"         pragma Annotate (GNATprove, False_Positive,"},{"line_number":305,"context_line":"            \"assertion might fail\","},{"line_number":306,"context_line":"            \"The property cannot be proven automatically. An Isabelle proof is included as an axiom\");"},{"line_number":307,"context_line":""},{"line_number":308,"context_line":"         M :\u003d M * N / Orig_N;"},{"line_number":309,"context_line":""},{"line_number":310,"context_line":"         -- This loop is never hit for sane values (i.e. M \u003c\u003d N) but"},{"line_number":311,"context_line":"         -- we have to make sure returned values are always in range."},{"line_number":312,"context_line":"         while M \u003e M_N_Max loop"},{"line_number":313,"context_line":"            pragma Loop_Invariant (N \u003c\u003d M_N_Max);"},{"line_number":314,"context_line":"            M :\u003d M / 2;"},{"line_number":315,"context_line":"            N :\u003d N / 2;"},{"line_number":316,"context_line":"         end loop;"},{"line_number":317,"context_line":"      end Cancel_M_N;"},{"line_number":318,"context_line":"   begin"},{"line_number":319,"context_line":"      pragma Debug (Debug.Put_Line (GNAT.Source_Info.Enclosing_Entity));"},{"line_number":320,"context_line":""}],"source_content_type":"text/x-ada","patch_set":1,"id":"9475be95_5fc5f3ba","side":"PARENT","line":317,"range":{"start_line":255,"start_character":0,"end_line":317,"end_character":21},"in_reply_to":"c73bab47_014b45aa","updated":"2026-10-30 03:35:11.000000000","message":"I\u0027ll give it a try across all the platforms I have here over the weekend and push an updated patch with it if everything looks good","commit_id":"ae3fcea12c2464eacdab823e8a4192146ff93024"},{"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":"2c8049cff79f1839e3f73891df75a1ade917aa95","unresolved":true,"context_lines":[{"line_number":256,"context_line":"      FIXED_DATA_N : constant :\u003d 16#80_0000#;"},{"line_number":257,"context_line":"      FIXED_LINK_N : constant :\u003d 16#08_0000#;"},{"line_number":258,"context_line":""},{"line_number":259,"context_line":"      -- Wide enough for M * FIXED_DATA_N before dividing by N."},{"line_number":260,"context_line":"      subtype Calc_M_Type is Int64 range 0 .. 2 ** 62;"},{"line_number":261,"context_line":"      subtype Calc_N_Type is Int64 range 0 .. 2 ** 62;"},{"line_number":262,"context_line":"      subtype Target_N_Type is Pos64 range FIXED_LINK_N .. FIXED_DATA_N;"}],"source_content_type":"text/x-ada","patch_set":2,"id":"8043c8a6_a0bee7ef","line":259,"updated":"2026-10-30 22:29:16.000000000","message":"This is not necessary, intermediate values only need to be within the base type (`Int64`). Increasing the range also changes the contract of `Cancel_M_N ()` so the proof actually gets harder (we don\u0027t know anymore that the arguments will be small enough). It\u0027s likely to fail now.","commit_id":"17c54d85ad5b610d8e8d48c56f11bf57c8ee3bb0"},{"author":{"_account_id":1000031,"name":"Matt DeVillier","email":"mrchromebox@gmail.com","username":"mrchromebox","avatars":[{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/fe3370e8ca14823a6e5ffb797b1974ef.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"40ee9ad7532926ccf77887e0a55d4d2132685a1b","unresolved":false,"context_lines":[{"line_number":256,"context_line":"      FIXED_DATA_N : constant :\u003d 16#80_0000#;"},{"line_number":257,"context_line":"      FIXED_LINK_N : constant :\u003d 16#08_0000#;"},{"line_number":258,"context_line":""},{"line_number":259,"context_line":"      -- Wide enough for M * FIXED_DATA_N before dividing by N."},{"line_number":260,"context_line":"      subtype Calc_M_Type is Int64 range 0 .. 2 ** 62;"},{"line_number":261,"context_line":"      subtype Calc_N_Type is Int64 range 0 .. 2 ** 62;"},{"line_number":262,"context_line":"      subtype Target_N_Type is Pos64 range FIXED_LINK_N .. FIXED_DATA_N;"}],"source_content_type":"text/x-ada","patch_set":2,"id":"a7769edf_641f9d02","line":259,"in_reply_to":"8043c8a6_a0bee7ef","updated":"2026-10-31 04:51:49.000000000","message":"Done","commit_id":"17c54d85ad5b610d8e8d48c56f11bf57c8ee3bb0"},{"author":{"_account_id":1000029,"name":"Ada SPARK","email":"gnatbot@sourcearcade.org","username":"gnatbot","avatars":[{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d32","height":32},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d56","height":56},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d100","height":100},{"url":"https://www.gravatar.com/avatar/c244ab97f43ca382a72e76784b616a4b.jpg?d\u003didenticon\u0026r\u003dpg\u0026s\u003d120","height":120}]},"change_message_id":"3969655f9a1773254540967d541a2edf436d50e8","unresolved":false,"context_lines":[{"line_number":274,"context_line":"         Post \u003d\u003e M in M_Type and N in N_Type"},{"line_number":275,"context_line":"      is"},{"line_number":276,"context_line":"      begin"},{"line_number":277,"context_line":"         M :\u003d M * Target_N / N;"},{"line_number":278,"context_line":"         N :\u003d Target_N;"},{"line_number":279,"context_line":""},{"line_number":280,"context_line":"         -- This loop is never hit for sane values (i.e. M \u003c\u003d N) but"}],"source_content_type":"text/x-ada","patch_set":2,"id":"d3fbf514_18d82858","line":277,"updated":"2026-10-30 23:28:33.000000000","message":"Config(s): alderlake broxton ironlake i945 g45 ironlake_edp haswell tigerlake skylake\n```\nhw-gfx-dp_info.adb:277: medium: overflow check might fail, in instantiation at hw-gfx-gma-dp_info.ads:19\n  277 |         M :\u003d M * Target_N / N;\n      |                ^ here\n  e.g. when M \u003d 1099511496705\n        and Target_N \u003d Target_N_Type\u0027First\n  reason for check: result of multiplication must fit in a 64-bits machine integer\n  possible fix: precondition of subprogram at line 267, instance at hw-gfx-gma-dp_info.ads:19 should mention M and Target_N\n  267 |      procedure Cancel_M_N\n      |      ^ here\n```","commit_id":"17c54d85ad5b610d8e8d48c56f11bf57c8ee3bb0"}]}
