Removing old TODOs

esa · Apr 15, 2024 · 8cc5cb6 · 8cc5cb6
1 parent 86d1591
commit 8cc5cb6
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 14 deletions.
diff --git a/FrontEndAst/DAst.fs b/FrontEndAst/DAst.fs
@@ -336,7 +336,6 @@ with
         | S32 -> 32
         | S64 -> 64
 
-// TODO: Find a better name
 type IntegerEndianness =
     | Byte
     | Unbounded
@@ -363,18 +362,18 @@ type Asn1IntegerEncodingType =
     | Unconstrained
 
 type TypeEncodingKind =
-    | Asn1IntegerEncodingType of Asn1IntegerEncodingType option // None si range min = max
+    | Asn1IntegerEncodingType of Asn1IntegerEncodingType option // None if range min = max
     | Asn1RealEncodingType of Asn1AcnAst.RealClass
     | AcnIntegerEncodingType of AcnIntegerEncodingType
     | AcnRealEncodingType of AcnRealEncodingType
     | AcnBooleanEncodingType of AcnBooleanEncoding option
     | AcnNullEncodingType of PATTERN_PROP_VALUE option
     | AcnStringEncodingType of Asn1AcnAst.StringAcnEncodingClass
-    | AcnOctetStringEncodingType of Asn1AcnAst.SizeableAcnEncodingClass // TODO: ACN?
-    | AcnBitStringEncodingType of Asn1AcnAst.SizeableAcnEncodingClass // TODO: ACN?
-    | SequenceOfEncodingType of TypeEncodingKind * Asn1AcnAst.SizeableAcnEncodingClass // TODO: Quid uper?
-    | SequenceEncodingType of TypeEncodingKind option list // TODO: Quid des None?
-    | ChoiceEncodingType of TypeEncodingKind option list // TODO: Quid des None?
+    | AcnOctetStringEncodingType of Asn1AcnAst.SizeableAcnEncodingClass
+    | AcnBitStringEncodingType of Asn1AcnAst.SizeableAcnEncodingClass
+    | SequenceOfEncodingType of TypeEncodingKind * Asn1AcnAst.SizeableAcnEncodingClass
+    | SequenceEncodingType of TypeEncodingKind option list
+    | ChoiceEncodingType of TypeEncodingKind option list
     | ReferenceEncodingType of string
     | OptionEncodingType of TypeEncodingKind
     | Placeholder

diff --git a/FrontEndAst/Language.fs b/FrontEndAst/Language.fs
@@ -92,7 +92,6 @@ type SequenceProofGen = {
     uperSiblingMaxSize: bigint option
     children: SequenceChildProps list
 } with
-    // TODO: What about padding?
 
     member this.siblingMaxSize (enc: Asn1Encoding): bigint option =
         match enc with
@@ -181,7 +180,7 @@ type SequenceOfLikeProofGen = {
     acnMaxOffset: bigint
     uperMaxOffset: bigint
     typeInfo: TypeInfo
-    sel: string // Selection
+    sel: string
     ixVariable: string
 } with
     member this.outerMaxSize (enc: Asn1Encoding): bigint =

diff --git a/StgScala/ProofGen.fs b/StgScala/ProofGen.fs
@@ -66,7 +66,7 @@ let wrapEncDecStmts (enc: Asn1Encoding) (snapshots: Var list) (cdc: Var) (oldCdc
         | FullyConstrainedPositive (min, max) | FullyConstrained (min, max) ->
             // TODO: The RT library does not add 1, why?
             let call = RTFunctionCall {fn = GetBitCountUnsigned; args = [IntLit (ULong, max - min)]}
-            // TODO: Cas min = max?
+            // TODO: Case min = max?
             let nBits = if max = min then 0I else bigint (ceil ((log (double (max - min))) / (log 2.0)))
             let cond = Equals (call, IntLit (Int, nBits))
             Some cond
@@ -85,7 +85,7 @@ let wrapEncDecStmts (enc: Asn1Encoding) (snapshots: Var list) (cdc: Var) (oldCdc
 
   let wrap (ix: int, (snap: Var, child: SequenceChildProps, stmt: string option)) (offsetAcc: bigint, rest: Expr): bigint * Expr =
     let sz = child.typeInfo.maxSize enc
-    //assert (thisMaxSize <= (pg.siblingMaxSize enc |> Option.defaultValue thisMaxSize))
+    //assert (thisMaxSize <= (pg.siblingMaxSize enc |> Option.defaultValue thisMaxSize)) // TODO: Somehow does not always hold with UPER?
     let relativeOffset = offsetAcc - (pg.maxOffset enc)
     let offsetCheckOverall = Check (Leq (callBitIndex (Var cdc), Plus ((callBitIndex (Var oldCdc)), (IntLit (Long, offsetAcc)))))
     let offsetCheckNested =
@@ -191,9 +191,6 @@ let generateSequenceOfLikeProof (enc: Asn1Encoding) (sqf: SequenceOfLike) (pg: S
     })
   let postSerde =
     Ghost (mkBlock [
-      // Assert (Equals (IntLit (Long, pg.outerMaxSize enc), IntLit (Long, pg.outerMaxSize enc)))
-      // Assert (Equals (IntLit (Long, sqfMaxSizeInBits), IntLit (Long, sqfMaxSizeInBits)))
-      // Assert (Equals (IntLit (Long, pg.maxOffset enc), IntLit (Long, pg.maxOffset enc)))
       Check (Equals (
         Mult (elemSzExpr, Plus (Var ix, IntLit (Int, 1I))),
         Plus (Mult (elemSzExpr, Var ix), elemSzExpr)