2.4. Artifact three: proof obligations🔗

Outputs/Decimal/soundness.lean is the write-once third artifact. It contains the format-specific facts that Triptych cannot infer from the grammar alone. These fall into two separate groups.

2.4.1. Generated parser and serializer🔗

The generated Decimal.parse needs no parser-correctness proof from the user: Decimal.parse_sound, Decimal.parse_complete, and Decimal.parse_reject were already generated and proved in Artifact 2.

Two surrounding choices still require evidence. First, the declared ofSpec and toSpec functions must be inverse on accepted specification values. For Decimal, the range constraint makes the potentially lossy Int64.ofInt conversion faithful:

theorem Decimal.toSpec_ofSpec (s : String) (v : Int) :
    Decimal.IsValid s → Decimal.computeValue s = some v → Int64.toInt (Int64.ofInt v) = v := bys:Stringv:Int⊢ IsValid s → computeValue s = some v → (Int64.ofInt v).toInt = v
  intro hvalid hvalues:Stringv:Inthvalid:IsValid shvalue:computeValue s = some v⊢ (Int64.ofInt v).toInt = v
  obtain ⟨view, hview, hvalidView⟩ := (Decimal.IsValid_view s).mp hvalids:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhvalidView:view.Valid⊢ (Int64.ofInt v).toInt = v
  have hdenotation : Decimal.View.denotation view = v := bys:Stringv:Int⊢ IsValid s → computeValue s = some v → (Int64.ofInt v).toInt = v
    rw [Decimal.computeValue_view,s:Stringv:Inthvalid:IsValid shvalue:Option.map View.denotation (decodeView s) = some vview:Viewhview:decodeView s = some viewhvalidView:view.Valid⊢ view.denotation = v hviews:Stringv:Inthvalid:IsValid sview:Viewhvalue:Option.map View.denotation (some view) = some vhview:decodeView s = some viewhvalidView:view.Valid⊢ view.denotation = v] at hvalues:Stringv:Inthvalid:IsValid sview:Viewhvalue:Option.map View.denotation (some view) = some vhview:decodeView s = some viewhvalidView:view.Valid⊢ view.denotation = v
    exact Option.some.inj hvalues:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhvalidView:view.Validhdenotation:view.denotation = v⊢ (Int64.ofInt v).toInt = v
  have hbounds :
      (-9223372036854775808 : Int) ≤ v ∧ v ≤ (9223372036854775807 : Int) := bys:Stringv:Int⊢ IsValid s → computeValue s = some v → (Int64.ofInt v).toInt = v
    unfold Decimal.View.Valid Decimal.View.Constraints Decimal.Constraints at hvalidViews:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhvalidView:-9223372036854775808 ≤ «value» view.sign view.natural view.fraction ∧
  «value» view.sign view.natural view.fraction ≤ 9223372036854775807hdenotation:view.denotation = v⊢ -9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807
    change
      (-9223372036854775808 : Int) ≤ Decimal.View.denotation view ∧
        Decimal.View.denotation view ≤ (9223372036854775807 : Int) at hvalidViews:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhdenotation:view.denotation = vhvalidView:-9223372036854775808 ≤ view.denotation ∧ view.denotation ≤ 9223372036854775807⊢ -9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807
    rw [hdenotations:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhdenotation:view.denotation = vhvalidView:-9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807⊢ -9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807] at hvalidViews:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhdenotation:view.denotation = vhvalidView:-9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807⊢ -9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807
    exact hvalidViews:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhvalidView:view.Validhdenotation:view.denotation = vhbounds:-9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807⊢ (Int64.ofInt v).toInt = v
  exact Int64.toInt_ofInt_of_le (bys:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhvalidView:view.Validhdenotation:view.denotation = vhbounds:-9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807⊢ -2 ^ 63 ≤ v omegaAll goals completed! 🐙) (bys:Stringv:Inthvalid:IsValid shvalue:computeValue s = some vview:Viewhview:decodeView s = some viewhvalidView:view.Validhdenotation:view.denotation = vhbounds:-9223372036854775808 ≤ v ∧ v ≤ 9223372036854775807⊢ v < 2 ^ 63 omegaAll goals completed! 🐙)

Second, the declared serializer decimalToStr requires one proof obligation, Decimal.encode_view. It says that serializing any Int64 produces text whose decoded view is valid and whose specification value, converted with Int64.ofInt, equals the original value:

theorem Decimal.encode_view (i : Int64) :
    ∃ v : Decimal.View,
      Decimal.decodeView (decimalToStr i) = some v ∧
      Decimal.View.Valid v ∧
      Int64.ofInt (Decimal.View.denotation v) = i := byi:Int64⊢ ∃ v, decodeView (decimalToStr i) = some v ∧ v.Valid ∧ Int64.ofInt v.denotation = i
  triptych_encode [Cedar.Thm.Decimal.parse_toString_roundtrip,
    Decimal.RuleRegistrySoundness.parser_agrees, Decimal.IsValid_view,
    Decimal.computeValue_view, Int64.ofInt_toInt i]All goals completed! 🐙

This is the single toString obligation. From it, Triptych derives acceptance, value preservation, generated-parser roundtrip, serializer injectivity, and normalization. For example:

theorem Decimal.parse_toString_roundtrip (i : Int64) :
    Decimal.parse (decimalToStr i) = some i :=
  Triptych.parse_toString_roundtrip_of_encodeView
    Decimal.parse_eq_some_iff_view Decimal.encode_view i

2.4.2. External parser🔗

The parser Cedar.Spec.Ext.Decimal.parse clause names an implementation that Triptych did not generate. Using it directly therefore requires three separate agreement proofs:

Decimal.extparse_sound: every external success is valid and has the specified value.
Decimal.extparse_complete: every valid input with that value is accepted externally.
Decimal.extparse_reject: the external parser returns Option.none exactly for invalid inputs.

The stronger Decimal.RuleRegistrySoundness.parser_agrees theorem is proved separately by decomposing Cedar's executable parser with reusable parser rules. The generated soundness obligation is then a direct projection:

theorem Decimal.extparse_sound (s : String) (d : Cedar.Spec.Ext.Decimal) :
    Cedar.Spec.Ext.Decimal.parse s = some d →
      Decimal.IsValid s ∧ Decimal.computeValue s = some (Int64.toInt d) := bys:Stringd:Cedar.Spec.Ext.Decimal⊢ Cedar.Spec.Ext.Decimal.parse s = some d → IsValid s ∧ computeValue s = some (Int64.toInt d)
  simpa only using (Decimal.RuleRegistrySoundness.parser_agrees s d).mpAll goals completed! 🐙

Once those parser obligations and the shared Decimal.encode_view serializer certificate are available, the external parser receives its own roundtrip theorem:

theorem Decimal.extparse_toString_roundtrip (i : Int64) :
    Cedar.Spec.Ext.Decimal.parse (decimalToStr i) = some i :=
  Triptych.parse_toString_roundtrip Decimal.extparse_complete Decimal.encode_accepted
    Decimal.encode_value i

This external roundtrip is derived, not a fourth external-parser obligation. It reuses the same serializer certificate that proves the generated-parser roundtrip. Reusable registry rules help prove the substantive Decimal.RuleRegistrySoundness.parser_agrees theorem, but that format-specific theorem is not itself registered. Soundness and completeness apply its two directions directly; the view theorem uses simp with the reusable optional-witness rule to compose it with generated view facts.