1  /-
  2    Cornell - Verified Binary Format DSL
  3    
  4    "Cornell boxes... the man made these things. Boxes with things inside them."
  5    
  6    A box is a bidirectional codec with machine-checked round-trip correctness.
  7    
  8    This module re-exports verified boxes from Cornell.Proofs.
  9    All boxes have complete proofs - no sorry, no axiom, no partial.
 10  -/
 11  
 12  import Cornell.Proofs
 13  
 14  namespace Cornell
 15  
 16  -- ═══════════════════════════════════════════════════════════════════════════════
 17  -- RE-EXPORTS FROM PROOFS
 18  -- All of these have complete, machine-checked proofs.
 19  -- ═══════════════════════════════════════════════════════════════════════════════
 20  
 21  -- Core types
 22  export Cornell.Proofs (Bytes ParseResult Box)
 23  
 24  -- Verified primitive boxes
 25  export Cornell.Proofs (unit u8 u64leBitVec u32leBitVec)
 26  
 27  -- Verified combinators  
 28  export Cornell.Proofs (seq isoBox)
 29  
 30  -- ═══════════════════════════════════════════════════════════════════════════════
 31  -- BYTES UTILITIES (convenience functions)
 32  -- ═══════════════════════════════════════════════════════════════════════════════
 33  
 34  instance : Repr Bytes where
 35    reprPrec bs _ := 
 36      let hex := bs.toList.map fun b => 
 37        let hi := b.toNat / 16
 38        let lo := b.toNat % 16
 39        let toHex := fun n => if n < 10 then Char.ofNat (48 + n) else Char.ofNat (87 + n)
 40        s!"{toHex hi}{toHex lo}"
 41      Std.Format.text s!"⟨{String.intercalate " " hex}⟩"
 42  
 43  def Bytes.empty : Bytes := ByteArray.empty
 44  
 45  def Bytes.length (bs : Bytes) : Nat := bs.size
 46  
 47  def Bytes.append (a b : Bytes) : Bytes := a ++ b
 48  
 49  instance : Append Bytes := ⟨Bytes.append⟩
 50  
 51  -- ═══════════════════════════════════════════════════════════════════════════════
 52  -- PARSERESULT UTILITIES
 53  -- ═══════════════════════════════════════════════════════════════════════════════
 54  
 55  open Cornell.Proofs in
 56  instance [Repr α] : Repr (ParseResult α) where
 57    reprPrec
 58      | .ok a _, n => Repr.addAppParen ("ParseResult.ok " ++ reprArg a ++ " <bytes>") n
 59      | .fail, _ => "ParseResult.fail"
 60  
 61  open Cornell.Proofs in
 62  def ParseResult.isOk : ParseResult α → Bool
 63    | .ok _ _ => true
 64    | .fail => false
 65  
 66  open Cornell.Proofs in
 67  def ParseResult.toOption : ParseResult α → Option (α × Bytes)
 68    | .ok a rest => some (a, rest)
 69    | .fail => none
 70  
 71  -- ═══════════════════════════════════════════════════════════════════════════════
 72  -- UINTXX BOXES (via isoBox from BitVec)
 73  -- These use the verified BitVec boxes and convert via isomorphism
 74  -- ═══════════════════════════════════════════════════════════════════════════════
 75  
 76  open Cornell.Proofs in
 77  /-- Little-endian u64 (verified via isoBox from u64leBitVec) -/
 78  def u64le : Box UInt64 := 
 79    isoBox u64leBitVec 
 80      UInt64.ofBitVec 
 81      UInt64.toBitVec
 82      (fun _ => rfl)
 83      (fun _ => rfl)
 84  
 85  open Cornell.Proofs in
 86  /-- Little-endian u32 (verified via isoBox from u32leBitVec) -/
 87  def u32le : Box UInt32 := 
 88    isoBox u32leBitVec 
 89      UInt32.ofBitVec 
 90      UInt32.toBitVec
 91      (fun _ => rfl)
 92      (fun _ => rfl)
 93  
 94  open Cornell.Proofs in
 95  /-- Boolean as u64 (Nix style): 0 = false, nonzero = true 
 96      
 97      Note: This is a lossy encoding (many u64 values map to true).
 98      The roundtrip property still holds: parse(serialize(b)) = b
 99  -/
100  def bool64 : Box Bool where
101    parse bs := (u64le.parse bs).map (· != 0)
102    serialize b := u64le.serialize (if b then 1 else 0)
103    roundtrip b := by
104      simp only [u64le, isoBox, ParseResult.map]
105      cases b
106      · -- false case: serialize gives 0, parse gives 0, (0 != 0) = false
107        rw [u64leBitVec.roundtrip]; rfl
108      · -- true case: serialize gives 1, parse gives 1, (1 != 0) = true  
109        rw [u64leBitVec.roundtrip]; rfl
110    consumption b extra := by
111      simp only [u64le, isoBox, ParseResult.map]
112      cases b
113      · rw [u64leBitVec.consumption]; rfl
114      · rw [u64leBitVec.consumption]; rfl
115  
116  -- ═══════════════════════════════════════════════════════════════════════════════
117  -- CONVENIENCE COMBINATORS
118  -- ═══════════════════════════════════════════════════════════════════════════════
119  
120  open Cornell.Proofs in
121  /-- Map a box through an isomorphism (alias for isoBox) -/
122  def isoMap (box : Box α) (f : α → β) (g : β → α) 
123      (iso_fg : ∀ b, f (g b) = b) (iso_gf : ∀ a, g (f a) = a) : Box β := 
124    isoBox box f g iso_fg iso_gf
125  
126  end Cornell