Merge pull request #151 from project-everest/nik_3d_perf

Optimize validation of arrays
project-everest · Oct 22, 2024 · 50ddf78 · 50ddf78
2 parents 444a1d6 + 68b73d1
commit 50ddf78
Show file tree

Hide file tree

Showing 34 changed files with 1,093 additions and 1,518 deletions.
diff --git a/.github/workflows/linux-x64.yaml b/.github/workflows/linux-x64.yaml
@@ -1,4 +1,4 @@
-name: Build and test EverParse based on a FStar image
+name: Linux build
 on:
   push:
     branches-ignore:

diff --git a/.github/workflows/windows.yaml b/.github/workflows/windows.yaml
@@ -1,4 +1,4 @@
-name: Build and test EverParse
+name: Windows package build
 on:
   pull_request:
   workflow_dispatch:

diff --git a/EverParse.fst.config.json b/EverParse.fst.config.json
@@ -5,7 +5,8 @@
       "--max_fuel", "2",
       "--initial_ifuel", "2",
       "--max_ifuel", "2",
-      "--initial_ifuel", "2"
+      "--initial_ifuel", "2",
+      "--ext", "context_pruning"
     ],
     "include_dirs": [
       "./src/lowparse",

diff --git a/doc/3d-snapshot/Base.c b/doc/3d-snapshot/Base.c
@@ -65,66 +65,14 @@ BaseValidatePair(
   uint64_t StartPosition
 )
 {
-  /* Validating field first */
-  /* Checking that we have enough space for a UINT32, i.e., 4 bytes */
-  BOOLEAN hasBytes0 = 4ULL <= (InputLength - StartPosition);
-  uint64_t positionAfterPair;
-  if (hasBytes0)
-  {
-    positionAfterPair = StartPosition + 4ULL;
-  }
-  else
-  {
-    positionAfterPair =
-      EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
-        StartPosition);
-  }
-  uint64_t res;
-  if (EverParseIsSuccess(positionAfterPair))
-  {
-    res = positionAfterPair;
-  }
-  else
-  {
-    ErrorHandlerFn("_Pair",
-      "first",
-      EverParseErrorReasonOfResult(positionAfterPair),
-      EverParseGetValidatorErrorKind(positionAfterPair),
-      Ctxt,
-      Input,
-      StartPosition);
-    res = positionAfterPair;
-  }
-  uint64_t positionAfterfirst = res;
-  if (EverParseIsError(positionAfterfirst))
-  {
-    return positionAfterfirst;
-  }
-  /* Validating field second */
-  /* Checking that we have enough space for a UINT32, i.e., 4 bytes */
-  BOOLEAN hasBytes = 4ULL <= (InputLength - positionAfterfirst);
-  uint64_t positionAfterPair0;
+  KRML_MAYBE_UNUSED_VAR(Ctxt);
+  KRML_MAYBE_UNUSED_VAR(ErrorHandlerFn);
+  KRML_MAYBE_UNUSED_VAR(Input);
+  BOOLEAN hasBytes = 8ULL <= (InputLength - StartPosition);
   if (hasBytes)
   {
-    positionAfterPair0 = positionAfterfirst + 4ULL;
-  }
-  else
-  {
-    positionAfterPair0 =
-      EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
-        positionAfterfirst);
-  }
-  if (EverParseIsSuccess(positionAfterPair0))
-  {
-    return positionAfterPair0;
+    return StartPosition + 8ULL;
   }
-  ErrorHandlerFn("_Pair",
-    "second",
-    EverParseErrorReasonOfResult(positionAfterPair0),
-    EverParseGetValidatorErrorKind(positionAfterPair0),
-    Ctxt,
-    Input,
-    positionAfterfirst);
-  return positionAfterPair0;
+  return EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition);
 }
 
diff --git a/doc/3d-snapshot/Color.c b/doc/3d-snapshot/Color.c
@@ -74,66 +74,13 @@ ColorValidateColoredPoint(
   {
     return positionAftercol_refinement0;
   }
-  /* Validating field x */
-  /* Checking that we have enough space for a UINT32, i.e., 4 bytes */
-  BOOLEAN hasBytes1 = 4ULL <= (InputLength - positionAftercol_refinement0);
-  uint64_t positionAfterColoredPoint0;
-  if (hasBytes1)
-  {
-    positionAfterColoredPoint0 = positionAftercol_refinement0 + 4ULL;
-  }
-  else
-  {
-    positionAfterColoredPoint0 =
-      EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
-        positionAftercol_refinement0);
-  }
-  uint64_t res;
-  if (EverParseIsSuccess(positionAfterColoredPoint0))
-  {
-    res = positionAfterColoredPoint0;
-  }
-  else
-  {
-    ErrorHandlerFn("_coloredPoint",
-      "x",
-      EverParseErrorReasonOfResult(positionAfterColoredPoint0),
-      EverParseGetValidatorErrorKind(positionAfterColoredPoint0),
-      Ctxt,
-      Input,
-      positionAftercol_refinement0);
-    res = positionAfterColoredPoint0;
-  }
-  uint64_t positionAfterx = res;
-  if (EverParseIsError(positionAfterx))
-  {
-    return positionAfterx;
-  }
-  /* Validating field y */
-  /* Checking that we have enough space for a UINT32, i.e., 4 bytes */
-  BOOLEAN hasBytes = 4ULL <= (InputLength - positionAfterx);
-  uint64_t positionAfterColoredPoint1;
+  BOOLEAN hasBytes = 8ULL <= (InputLength - positionAftercol_refinement0);
   if (hasBytes)
   {
-    positionAfterColoredPoint1 = positionAfterx + 4ULL;
+    return positionAftercol_refinement0 + 8ULL;
   }
-  else
-  {
-    positionAfterColoredPoint1 =
-      EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
-        positionAfterx);
-  }
-  if (EverParseIsSuccess(positionAfterColoredPoint1))
-  {
-    return positionAfterColoredPoint1;
-  }
-  ErrorHandlerFn("_coloredPoint",
-    "y",
-    EverParseErrorReasonOfResult(positionAfterColoredPoint1),
-    EverParseGetValidatorErrorKind(positionAfterColoredPoint1),
-    Ctxt,
-    Input,
-    positionAfterx);
-  return positionAfterColoredPoint1;
+  return
+    EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
+      positionAftercol_refinement0);
 }
 
diff --git a/doc/3d-snapshot/ColoredPoint.c b/doc/3d-snapshot/ColoredPoint.c
@@ -2,87 +2,6 @@
 
 #include "ColoredPoint.h"
 
-static inline uint64_t
-ValidatePoint(
-  uint8_t *Ctxt,
-  void
-  (*ErrorHandlerFn)(
-    EVERPARSE_STRING x0,
-    EVERPARSE_STRING x1,
-    EVERPARSE_STRING x2,
-    uint64_t x3,
-    uint8_t *x4,
-    uint8_t *x5,
-    uint64_t x6
-  ),
-  uint8_t *Input,
-  uint64_t InputLength,
-  uint64_t StartPosition
-)
-{
-  /* Validating field x */
-  /* Checking that we have enough space for a UINT16, i.e., 2 bytes */
-  BOOLEAN hasBytes0 = 2ULL <= (InputLength - StartPosition);
-  uint64_t positionAfterPoint;
-  if (hasBytes0)
-  {
-    positionAfterPoint = StartPosition + 2ULL;
-  }
-  else
-  {
-    positionAfterPoint =
-      EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
-        StartPosition);
-  }
-  uint64_t res;
-  if (EverParseIsSuccess(positionAfterPoint))
-  {
-    res = positionAfterPoint;
-  }
-  else
-  {
-    ErrorHandlerFn("_point",
-      "x",
-      EverParseErrorReasonOfResult(positionAfterPoint),
-      EverParseGetValidatorErrorKind(positionAfterPoint),
-      Ctxt,
-      Input,
-      StartPosition);
-    res = positionAfterPoint;
-  }
-  uint64_t positionAfterx = res;
-  if (EverParseIsError(positionAfterx))
-  {
-    return positionAfterx;
-  }
-  /* Validating field y */
-  /* Checking that we have enough space for a UINT16, i.e., 2 bytes */
-  BOOLEAN hasBytes = 2ULL <= (InputLength - positionAfterx);
-  uint64_t positionAfterPoint0;
-  if (hasBytes)
-  {
-    positionAfterPoint0 = positionAfterx + 2ULL;
-  }
-  else
-  {
-    positionAfterPoint0 =
-      EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
-        positionAfterx);
-  }
-  if (EverParseIsSuccess(positionAfterPoint0))
-  {
-    return positionAfterPoint0;
-  }
-  ErrorHandlerFn("_point",
-    "y",
-    EverParseErrorReasonOfResult(positionAfterPoint0),
-    EverParseGetValidatorErrorKind(positionAfterPoint0),
-    Ctxt,
-    Input,
-    positionAfterx);
-  return positionAfterPoint0;
-}
-
 uint64_t
 ColoredPointValidateColoredPoint1(
   uint8_t *Ctxt,
@@ -101,61 +20,15 @@ ColoredPointValidateColoredPoint1(
   uint64_t StartPosition
 )
 {
-  /* Validating field color */
-  /* Checking that we have enough space for a UINT8, i.e., 1 byte */
-  BOOLEAN hasBytes = 1ULL <= (InputLength - StartPosition);
-  uint64_t positionAfterColoredPoint1;
+  KRML_MAYBE_UNUSED_VAR(Ctxt);
+  KRML_MAYBE_UNUSED_VAR(ErrorHandlerFn);
+  KRML_MAYBE_UNUSED_VAR(Input);
+  BOOLEAN hasBytes = 5ULL <= (InputLength - StartPosition);
   if (hasBytes)
   {
-    positionAfterColoredPoint1 = StartPosition + 1ULL;
+    return StartPosition + 5ULL;
   }
-  else
-  {
-    positionAfterColoredPoint1 =
-      EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
-        StartPosition);
-  }
-  uint64_t res;
-  if (EverParseIsSuccess(positionAfterColoredPoint1))
-  {
-    res = positionAfterColoredPoint1;
-  }
-  else
-  {
-    ErrorHandlerFn("_coloredPoint1",
-      "color",
-      EverParseErrorReasonOfResult(positionAfterColoredPoint1),
-      EverParseGetValidatorErrorKind(positionAfterColoredPoint1),
-      Ctxt,
-      Input,
-      StartPosition);
-    res = positionAfterColoredPoint1;
-  }
-  uint64_t positionAftercolor = res;
-  if (EverParseIsError(positionAftercolor))
-  {
-    return positionAftercolor;
-  }
-  /* Validating field pt */
-  uint64_t
-  positionAfterColoredPoint10 =
-    ValidatePoint(Ctxt,
-      ErrorHandlerFn,
-      Input,
-      InputLength,
-      positionAftercolor);
-  if (EverParseIsSuccess(positionAfterColoredPoint10))
-  {
-    return positionAfterColoredPoint10;
-  }
-  ErrorHandlerFn("_coloredPoint1",
-    "pt",
-    EverParseErrorReasonOfResult(positionAfterColoredPoint10),
-    EverParseGetValidatorErrorKind(positionAfterColoredPoint10),
-    Ctxt,
-    Input,
-    positionAftercolor);
-  return positionAfterColoredPoint10;
+  return EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition);
 }
 
 uint64_t
@@ -176,59 +49,14 @@ ColoredPointValidateColoredPoint2(
   uint64_t StartPosition
 )
 {
-  /* Validating field pt */
-  uint64_t
-  positionAfterColoredPoint2 =
-    ValidatePoint(Ctxt,
-      ErrorHandlerFn,
-      Input,
-      InputLength,
-      StartPosition);
-  uint64_t positionAfterpt;
-  if (EverParseIsSuccess(positionAfterColoredPoint2))
-  {
-    positionAfterpt = positionAfterColoredPoint2;
-  }
-  else
-  {
-    ErrorHandlerFn("_coloredPoint2",
-      "pt",
-      EverParseErrorReasonOfResult(positionAfterColoredPoint2),
-      EverParseGetValidatorErrorKind(positionAfterColoredPoint2),
-      Ctxt,
-      Input,
-      StartPosition);
-    positionAfterpt = positionAfterColoredPoint2;
-  }
-  if (EverParseIsError(positionAfterpt))
-  {
-    return positionAfterpt;
-  }
-  /* Validating field color */
-  /* Checking that we have enough space for a UINT8, i.e., 1 byte */
-  BOOLEAN hasBytes = 1ULL <= (InputLength - positionAfterpt);
-  uint64_t positionAfterColoredPoint20;
+  KRML_MAYBE_UNUSED_VAR(Ctxt);
+  KRML_MAYBE_UNUSED_VAR(ErrorHandlerFn);
+  KRML_MAYBE_UNUSED_VAR(Input);
+  BOOLEAN hasBytes = 5ULL <= (InputLength - StartPosition);
   if (hasBytes)
   {
-    positionAfterColoredPoint20 = positionAfterpt + 1ULL;
-  }
-  else
-  {
-    positionAfterColoredPoint20 =
-      EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA,
-        positionAfterpt);
-  }
-  if (EverParseIsSuccess(positionAfterColoredPoint20))
-  {
-    return positionAfterColoredPoint20;
+    return StartPosition + 5ULL;
   }
-  ErrorHandlerFn("_coloredPoint2",
-    "color",
-    EverParseErrorReasonOfResult(positionAfterColoredPoint20),
-    EverParseGetValidatorErrorKind(positionAfterColoredPoint20),
-    Ctxt,
-    Input,
-    positionAfterpt);
-  return positionAfterColoredPoint20;
+  return EverParseSetValidatorErrorPos(EVERPARSE_VALIDATOR_ERROR_NOT_ENOUGH_DATA, StartPosition);
 }