fix: correct off-by-one in toSeconds and wrong day count in Year.days

src/Std/Time/Date/Unit/Month.lean

@@ -212,11 +212,13 @@ def ofFin (data : Fin 13) : Ordinal :=
   Bounded.LE.ofFin' data (by decide)
 
 /--
-Transforms `Month.Ordinal` into `Second.Offset`.
+Transforms `Month.Ordinal` into `Second.Offset`, representing the number of seconds elapsed since
+the beginning of the year up to the start of the given month. For example, January returns 0
+seconds since it is the first month of the year.
 -/
 def toSeconds (leap : Bool) (month : Ordinal) : Second.Offset :=
   let daysAcc := #[0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334]
-  let days : Day.Offset := daysAcc[month.toNat]!
+  let days : Day.Offset := daysAcc[month.toNat - 1]!
   let time := days.toSeconds
   if leap && month.toNat ≥ 2
     then time + 86400

src/Std/Time/Date/Unit/Year.lean

@@ -107,8 +107,8 @@ Calculates the number of days in the specified `year`.
 -/
 def days (year : Offset) : Bounded.LE 365 366 :=
   if year.isLeap
-    then .ofNatWrapping 366 (by decide)
-    else .ofNatWrapping 355 (by decide)
+    then Bounded.LE.mk 366 (by decide)
+    else Bounded.LE.mk 365 (by decide)
 
 /--
 Calculates the number of weeks in the specified `year`.

src/Std/Time/Duration.lean

@@ -142,8 +142,8 @@ Converts a `Duration` to a `Millisecond.Offset`
 @[inline]
 def toMilliseconds (duration : Duration) : Millisecond.Offset :=
   let secMillis := duration.second.mul 1000
-  let nanosMillis := duration.nano.ediv 1000000 (by decide)
-  let millis := secMillis + (.ofInt nanosMillis.val)
+  let nanosMillis := duration.nano.val.tdiv 1000000
+  let millis := secMillis + (.ofInt nanosMillis)
   millis
 
 /--

src/Std/Time/Format/Basic.lean

@@ -1361,8 +1361,8 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
     isDST := false,
   }
 
-  let month := builder.MorL |>.getD 0
-  let day := builder.d |>.getD 0
+  let month := builder.MorL |>.getD 1
+  let day := builder.d |>.getD 1
   let era := (builder.G.getD .ce)
 
   let year
@@ -1381,7 +1381,8 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
     hour <|> (
       let one : Option (Bounded.LE 0 23) := builder.H
       let other : Option (Bounded.LE 0 23) := (Bounded.LE.sub · 1) <$> builder.k
-      (one <|> other))
+      let hNoMarker : Option (Bounded.LE 0 23) := HourMarker.am.toAbsolute <$> builder.h
+      (one <|> other <|> hNoMarker))
       |>.getD ⟨0, by decide⟩
 
   let minute := builder.m |>.getD 0

src/Std/Time/Time/PlainTime.lean

@@ -233,8 +233,7 @@ def subNanoseconds (time : PlainTime) (nanosToSub : Nanosecond.Offset) : PlainTi
 Adds milliseconds to a `PlainTime`.
 -/
 def addMilliseconds (time : PlainTime) (millisToAdd : Millisecond.Offset) : PlainTime :=
-  let total := time.toMilliseconds + millisToAdd
-  ofMilliseconds total
+  ofNanoseconds (time.toNanoseconds + millisToAdd.toNanoseconds)
 
 /--
 Subtracts milliseconds from a `PlainTime`.
@@ -261,7 +260,7 @@ Creates a new `PlainTime` by adjusting the milliseconds component inside the `na
 -/
 @[inline]
 def withMilliseconds (pt : PlainTime) (millis : Millisecond.Ordinal) : PlainTime :=
-  let minorPart := pt.nanosecond.emod 1000 (by decide)
+  let minorPart := pt.nanosecond.emod 1000000 (by decide)
   let majorPart := millis.mul_pos 1000000 (by decide) |>.addBounds minorPart
   { pt with nanosecond := majorPart |>.expandTop (by decide) }
 

src/Std/Time/Zoned/DateTime.lean

@@ -391,7 +391,7 @@ Getter for the `Milliseconds` inside of a `DateTime`
 -/
 @[inline]
 def millisecond (dt : DateTime tz) : Millisecond.Ordinal :=
-  dt.date.get.time.nanosecond.emod 1000 (by decide)
+  dt.date.get.time.millisecond
 
 /--
 Getter for the `Nanosecond` inside of a `DateTime`

src/Std/Time/Zoned/ZoneRules.lean

@@ -142,7 +142,7 @@ def createTimeZoneFromTransition (transition : Transition) : TimeZone :=
 Applies the transition to a Timestamp.
 -/
 def apply (timestamp : Timestamp) (transition : Transition) : Timestamp :=
-  let offsetInSeconds := transition.localTimeType.gmtOffset.second |>.add transition.localTimeType.gmtOffset.second
+  let offsetInSeconds := transition.localTimeType.gmtOffset.second
   timestamp.addSeconds offsetInSeconds
 
 /--
@@ -159,7 +159,7 @@ If the timestamp falls between two transitions, it returns the most recent trans
 -/
 def findTransitionForTimestamp (transitions : Array Transition) (timestamp : Timestamp) : Option Transition :=
   if let some idx := findTransitionIndexForTimestamp transitions timestamp
-    then transitions[idx - 1]?
+    then if idx == 0 then none else transitions[idx - 1]?
     else transitions.back?
 
 /--
@@ -207,6 +207,21 @@ def findLocalTimeTypeForTimestamp (zr : ZoneRules) (timestamp : Timestamp) : Loc
   |>.map (·.localTimeType)
   |>.getD zr.initialLocalTimeType
 
+/--
+Finds the `LocalTimeType` for a given wall-clock time (seconds since Unix epoch in local time).
+Unlike `findLocalTimeTypeForTimestamp`, this compares each transition's UTC time adjusted by the
+previous offset — necessary when converting local time to UTC.
+-/
+def findLocalTimeTypeForWallTime (zr : ZoneRules) (wallSecs : Int) : LocalTimeType :=
+  let (ltt, _) := zr.transitions.foldl (init := (zr.initialLocalTimeType, false))
+    fun (ltt, done) t =>
+      if done then (ltt, true)
+      else
+        let localTransitionTime := t.time.add ltt.gmtOffset.second
+        if wallSecs < localTransitionTime.val then (ltt, true)
+        else (t.localTimeType, false)
+  ltt
+
 /--
 Find the current `TimeZone` out of a `Transition` in a `ZoneRules`
 -/

src/Std/Time/Zoned/ZonedDateTime.lean

@@ -64,28 +64,8 @@ Creates a new `ZonedDateTime` out of a `PlainDateTime` and a `ZoneRules`.
 @[inline]
 def ofPlainDateTime (pdt : PlainDateTime) (zr : TimeZone.ZoneRules) : ZonedDateTime :=
   let tm := pdt.toTimestampAssumingUTC
-
-  let transition :=
-    let value := tm.toSecondsSinceUnixEpoch
-    if let some idx := zr.transitions.findFinIdx? (fun t => t.time.val ≥ value.val)
-      then
-        let last := zr.transitions[idx.1 - 1]
-        let next := zr.transitions[idx]
-
-        let utcNext := next.time.sub last.localTimeType.gmtOffset.second.abs
-
-        if utcNext.val > tm.toSecondsSinceUnixEpoch.val
-          then some last
-          else some next
-
-      else zr.transitions.back?
-
-  let tz :=
-    transition
-    |>.map (·.localTimeType)
-    |>.getD zr.initialLocalTimeType
-    |>.getTimeZone
-
+  let ltt := zr.findLocalTimeTypeForWallTime tm.toSecondsSinceUnixEpoch.val
+  let tz := ltt.getTimeZone
   let tm := tm.subSeconds tz.toSeconds
   ZonedDateTime.mk (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC.addSeconds tz.toSeconds) tm zr tz
 

tests/elab/timeIO.lean

@@ -81,3 +81,52 @@ info: 2003-10-26T01:59:59.000000000-05:00
   println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T01:59:59") zr |>.toLeanDateTimeWithZoneString}"
   println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:00:00") zr |>.toLeanDateTimeWithZoneString}"
   println! "{ZonedDateTime.ofPlainDateTime datetime("2003-10-26T02:59:59") zr |>.toLeanDateTimeWithZoneString}"
+
+-- ZoneRules.findTransitionForTimestamp: a timestamp one second before the first transition
+-- uses initialLocalTimeType (LMT), not the first post-transition type.
+/--
+info: true
+-/
+#guard_msgs in
+#eval show IO Bool from do
+  let rules ← Database.defaultGetZoneRules "America/New_York"
+  if h : 0 < rules.transitions.size then
+    let first := rules.transitions[0]
+    let beforeFirst := Timestamp.ofSecondsSinceUnixEpoch ⟨first.time.val - 1⟩
+    let zdt := ZonedDateTime.ofTimestamp beforeFirst rules
+    return zdt.timezone.name == rules.initialLocalTimeType.identifier
+  else
+    return true
+
+-- ZonedDateTime.ofPlainDateTime resolves local wall-clock time using the correct offset sign.
+-- UTC+2 → UTC+3 spring-forward at UTC t=3600: gap is local 03:00–04:00.
+def bugZonePlus : TimeZone.ZoneRules :=
+  let before : TimeZone.LocalTimeType := {
+    gmtOffset := .ofSeconds 7200,
+    isDst := false, abbreviation := "TST2",
+    wall := .standard, utLocal := .ut, identifier := "Test/Plus2"
+  }
+  let after : TimeZone.LocalTimeType := {
+    gmtOffset := .ofSeconds 10800,
+    isDst := true, abbreviation := "TST3",
+    wall := .standard, utLocal := .ut, identifier := "Test/Plus3"
+  }
+  { initialLocalTimeType := before, transitions := #[⟨3600, after⟩] }
+
+/--
+info: "Test/Plus2"
+-/
+#guard_msgs in
+#eval
+  let pdt : PlainDateTime :=
+    ⟨PlainDate.ofYearMonthDayClip 1970 1 1, PlainTime.ofHourMinuteSecondsNano 2 30 0 0⟩
+  (ZonedDateTime.ofPlainDateTime pdt bugZonePlus).timezone.name
+
+/--
+info: "Test/Plus3"
+-/
+#guard_msgs in
+#eval
+  let pdt : PlainDateTime :=
+    ⟨PlainDate.ofYearMonthDayClip 1970 1 1, PlainTime.ofHourMinuteSecondsNano 4 30 0 0⟩
+  (ZonedDateTime.ofPlainDateTime pdt bugZonePlus).timezone.name

tests/elab/timeOperations.lean

@@ -317,3 +317,22 @@ info: 4
 -/
 #guard_msgs in
 #eval date("2024-01-22").alignedWeekOfMonth
+
+-- DateTime.millisecond delegates to PlainTime.millisecond (ediv 1000000), not emod 1000.
+/--
+info: 123
+-/
+#guard_msgs in
+#eval
+  let t := PlainTime.ofHourMinuteSecondsNano 10 30 ⟨0, by decide⟩ ⟨123456789, by decide⟩
+  let dt : DateTime .UTC := DateTime.ofPlainDateTime ⟨PlainDate.ofYearMonthDayClip 2024 .august 15, t⟩ .UTC
+  dt.millisecond.val
+
+-- PlainTime.addMilliseconds preserves sub-millisecond nanoseconds (uses nanosecond arithmetic).
+/--
+info: 501500000
+-/
+#guard_msgs in
+#eval
+  let t := PlainTime.ofHourMinuteSecondsNano 0 0 ⟨0, by decide⟩ ⟨500500000, by decide⟩
+  (t.addMilliseconds 1).nanosecond.val

tests/elab/timeParse.lean

@@ -84,15 +84,15 @@ info: "2024-08-16T01:28:00.000000000Z"
     ISO8601UTC.format t.toDateTime
 
 /--
-info: "0000-12-31T22:28:12.000000000+09:00"
+info: "0000-01-01T22:28:12.000000000+09:00"
 -/
 #guard_msgs in
 #eval
     let t : ZonedDateTime := Time24Hour.parse! "13:28:12"
     ISO8601UTC.format (t.toDateTime.convertTimeZone jpTZ)
 
 /--
-info: "0000-12-31T00:00:00.000000000-03:00"
+info: "0000-01-01T00:00:00.000000000-03:00"
 -/
 #guard_msgs in
 #eval
@@ -202,3 +202,31 @@ info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
 #eval
     let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 PM +03:00"
     (ISO8601UTC.format ·.toDateTime) <$> t2
+
+-- 12-hour clock (`h`) without AM/PM marker: the parsed hour is used as-is (AM assumed).
+def fmtH12NoAmPm : GenericFormat .any := datespec("hh:mm:ss")
+def fmtH12NoAmPmFull : GenericFormat .any := datespec("uuuu-MM-dd hh:mm:ss")
+
+/--
+info: "0000-01-01T05:30:00.000000000Z"
+-/
+#guard_msgs in
+#eval
+  let t : ZonedDateTime := fmtH12NoAmPm.parse! "05:30:00"
+  ISO8601UTC.format t.toDateTime
+
+/--
+info: "0000-01-01T11:45:20.000000000Z"
+-/
+#guard_msgs in
+#eval
+  let t : ZonedDateTime := fmtH12NoAmPm.parse! "11:45:20"
+  ISO8601UTC.format t.toDateTime
+
+/--
+info: "2024-08-15T09:15:00.000000000Z"
+-/
+#guard_msgs in
+#eval
+  let t : ZonedDateTime := fmtH12NoAmPmFull.parse! "2024-08-15 09:15:00"
+  ISO8601UTC.format t.toDateTime

tests/elab/timeSet.lean

@@ -98,3 +98,13 @@ info: zoned("2014-06-16T10:03:03.000000002-03:00")
 -/
 #guard_msgs in
 #eval date₁.withNanoseconds 2
+
+-- PlainTime.withMilliseconds preserves microseconds (uses emod 1000000, not emod 1000).
+-- nanosecond=123456789 → 123 ms + 456 µs + 789 ns; setting millis=5 → 5456789 ns.
+/--
+info: 5456789
+-/
+#guard_msgs in
+#eval
+  let t := PlainTime.ofHourMinuteSecondsNano 10 30 ⟨0, by decide⟩ ⟨123456789, by decide⟩
+  (t.withMilliseconds ⟨5, by decide⟩).nanosecond.val

tests/elab/timeSub.lean

@@ -53,3 +53,48 @@ info: true
 -/
 #guard_msgs in
 #eval (t + dur - dur) == t
+
+-- Duration.toMilliseconds uses truncation division (consistent with ofNanoseconds).
+-- Negative sub-millisecond values round toward zero, not toward negative infinity.
+
+/--
+info: 0
+-/
+#guard_msgs in
+#eval (Duration.ofNanoseconds (-999999)).toMilliseconds.val
+
+/--
+info: 0
+-/
+#guard_msgs in
+#eval (Duration.ofNanoseconds (-1)).toMilliseconds.val
+
+/--
+info: -1
+-/
+#guard_msgs in
+#eval (Duration.ofNanoseconds (-1000000)).toMilliseconds.val
+
+/--
+info: -1
+-/
+#guard_msgs in
+#eval (Duration.ofNanoseconds (-1999999)).toMilliseconds.val
+
+/--
+info: 0
+-/
+#guard_msgs in
+#eval (Duration.ofNanoseconds 999999).toMilliseconds.val
+
+/--
+info: 1
+-/
+#guard_msgs in
+#eval (Duration.ofNanoseconds 1000000).toMilliseconds.val
+
+/--
+info: 1
+-/
+#guard_msgs in
+#eval (Duration.ofNanoseconds 1999999).toMilliseconds.val

tests/elab/timeTzifParse.lean

@@ -108,3 +108,43 @@ info: zoned("2012-12-10T00:35:47.000000000-02:00")
 -/
 #guard_msgs in
 #eval ZonedDateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch 1355106947) rules
+
+-- ZoneRules.findTransitionForTimestamp: a timestamp before the first transition uses initialLocalTimeType.
+def testZoneRulesInitialLTT : TimeZone.ZoneRules :=
+  let initLTT : TimeZone.LocalTimeType := {
+    gmtOffset := .ofSeconds 3600,
+    isDst := false, abbreviation := "TST1",
+    wall := .standard, utLocal := .ut, identifier := "Test/Zone1"
+  }
+  let transLTT : TimeZone.LocalTimeType := {
+    gmtOffset := .ofSeconds 7200,
+    isDst := false, abbreviation := "TST2",
+    wall := .standard, utLocal := .ut, identifier := "Test/Zone2"
+  }
+  { initialLocalTimeType := initLTT, transitions := #[⟨100, transLTT⟩] }
+
+/--
+info: "Test/Zone1"
+-/
+#guard_msgs in
+#eval
+  let tm := Timestamp.ofSecondsSinceUnixEpoch 50
+  (ZonedDateTime.ofTimestamp tm testZoneRulesInitialLTT).timezone.name
+
+-- Transition.apply adds the GMT offset exactly once to the timestamp.
+def testTransitionApply : TimeZone.Transition :=
+  { time := 0
+    localTimeType := {
+      gmtOffset := .ofSeconds 3600,
+      isDst := false, abbreviation := "TST",
+      wall := .standard, utLocal := .ut, identifier := "Test/Zone"
+    }
+  }
+
+/--
+info: 4600
+-/
+#guard_msgs in
+#eval
+  let t := Timestamp.ofSecondsSinceUnixEpoch 1000
+  (TimeZone.Transition.apply t testTransitionApply).toSecondsSinceUnixEpoch.val