Merge branch 'master' into getopt

project-everest · Oct 23, 2024 · cd8344c · cd8344c
2 parents 44f6296 + b93322f
commit cd8344c
Show file tree

Hide file tree

Showing 94 changed files with 8,889 additions and 1,537 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
@@ -1,16 +1,20 @@
 {
     "fstar_exe": "fstar.exe",
     "options": [
-      "--max_fuel", "0",
+      "--initial_fuel", "0",
+      "--max_fuel", "2",
+      "--initial_ifuel", "2",
       "--max_ifuel", "2",
-      "--initial_ifuel", "2"
+      "--initial_ifuel", "2",
+      "--ext", "context_pruning"
     ],
     "include_dirs": [
-      "./src/lowparse", 
+      "./src/lowparse",
       "${KRML_HOME}/krmllib",
       "${KRML_HOME}/krmllib/obj",
       "./src/3d",
-      "./src/3d/prelude"
+      "./src/3d/prelude",
+      "./src/ASN1"
     ]
   }
 
diff --git a/Makefile b/Makefile
@@ -1,11 +1,14 @@
-all: quackyducky lowparse 3d
+all: quackyducky lowparse 3d asn1
 
 lowparse:
 	+$(MAKE) -C src/lowparse
 
 3d: lowparse
 	+$(MAKE) -C src/3d
 
+asn1: lowparse
+	+$(MAKE) -C src/ASN1 verify
+
 quackyducky:
 	+$(MAKE) -C src/qd
 
@@ -25,6 +28,9 @@ lowparse-unit-test: lowparse
 
 3d-test: 3d-unit-test 3d-doc-test
 
+asn1-test: asn1
+	+$(MAKE) -C src/ASN1 test
+
 lowparse-bitfields-test: lowparse
 	+$(MAKE) -C tests/bitfields
 
@@ -44,7 +50,7 @@ quackyducky-sample0-test: quackyducky lowparse
 
 quackyducky-test: quackyducky-unit-test quackyducky-sample-test quackyducky-sample0-test quackyducky-sample-low-test
 
-test: all lowparse-test quackyducky-test 3d-test
+test: all lowparse-test quackyducky-test 3d-test asn1-test
 
 ci: test
 
@@ -60,7 +66,7 @@ clean-quackyducky:
 clean: clean-3d clean-lowparse clean-quackyducky
 	rm -rf bin
 
-.PHONY: all gen verify test gen-test clean quackyducky lowparse lowparse-test quackyducky-test lowparse-fstar-test quackyducky-sample-test quackyducky-sample0-test quackyducky-unit-test package 3d 3d-test lowparse-unit-test lowparse-bitfields-test release everparse 3d-unit-test 3d-doc-test ci clean-3d clean-lowparse clean-quackyducky
+.PHONY: all gen verify test gen-test clean quackyducky lowparse lowparse-test quackyducky-test lowparse-fstar-test quackyducky-sample-test quackyducky-sample0-test quackyducky-unit-test package 3d 3d-test lowparse-unit-test lowparse-bitfields-test release everparse 3d-unit-test 3d-doc-test ci clean-3d clean-lowparse clean-quackyducky asn1 asn1-test
 
 release:
 	+src/package/release.sh

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);
 }