Function normalize_offset 

pub exec fn normalize_offset(
    local: DateTime,
    local_ahead_of_utc: bool,
    offset_hour: u8,
    offset_minute: u8,
) -> res : Option<DateTime>

requires

datetime_wf(local),

offset_hour <= 23,

offset_minute <= 59,

ensures

res matches Some(utc) ==> datetime_wf(utc),

returns

({
    let local_minutes = local.hour as i32 * 60 + local.minute as i32;
    let offset = offset_hour as i32 * 60 + offset_minute as i32;
    let utc_minutes = if local_ahead_of_utc {
        local_minutes - offset
    } else {
        local_minutes + offset
    };
    if utc_minutes < 0 {
        previous_day(DateTime {
            hour: ((utc_minutes + 1440) / 60) as u8,
            minute: ((utc_minutes + 1440) % 60) as u8,
            ..local
        })
    } else if utc_minutes >= 1440 {
        next_day(DateTime {
            hour: ((utc_minutes - 1440) / 60) as u8,
            minute: ((utc_minutes - 1440) % 60) as u8,
            ..local
        })
    } else {
        Some(DateTime {
            hour: (utc_minutes / 60) as u8,
            minute: (utc_minutes % 60) as u8,
            ..local
        })
    }
}),

Adjusts the local time to UTC by subtracting the timezone offset (UTC = local - offset). As per ASN.1 UTCTime (X.680 47.3) and GeneralizedTime (X.680 46.3) specifications:

• The timezone offset represents the difference between local time and UTC.
• If local_ahead_of_utc is true (indicated by ‘+’), the local time is ahead of UTC, so the offset is subtracted: UTC = local - offset.
• If local_ahead_of_utc is false (indicated by ‘-’), the local time is behind UTC, so the offset is added: UTC = local + offset.
• Properly rolls over the calendar date to the next or previous day if necessary.