diff --git a/.github/workflows/linux-x64-hierarchic.yaml b/.github/workflows/linux-x64-hierarchic.yaml
index 47785c74..045bec80 100644
--- a/.github/workflows/linux-x64-hierarchic.yaml
+++ b/.github/workflows/linux-x64-hierarchic.yaml
@@ -16,7 +16,7 @@ jobs:
         run: |
           echo "CI_INITIAL_TIMESTAMP=$(date '+%s')" >> $GITHUB_ENV
       - name: Check out repo        
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: Identify the base FStar branch and the notification channel
         run: |
           echo "FSTAR_BRANCH=$(jq -c -r '.BranchName' .docker/build/config.json)" >> $GITHUB_ENV
@@ -41,7 +41,7 @@ jobs:
           DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}
       - name: Archive build log
         if: ${{ always() }}
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: log
           path: log.txt
diff --git a/lib/Bundles.ml b/lib/Bundles.ml
index eae774af..953d3468 100644
--- a/lib/Bundles.ml
+++ b/lib/Bundles.ml
@@ -217,7 +217,23 @@ let make_bundles files =
 (* A more refined version of direct_dependencies (found above), which
    distinguishes between internal and public dependencies. Keeps less dependency
    information, too, since it does not need to generate precise error messages.
-   To be used after Inlining has run. *)
+   To be used after Inlining has run.
+
+   We do not run this on the C grammar (which would presumably be simpler,
+   because by then we would have built both flavors of headers + C files),
+   because it does not distinguish between lids and ids, and also because the
+   grammar is convoluted and makes it hard to access the "name" of a
+   declaration.
+   
+   So instead, we anticipate and rely on the fact that:
+   - to compute the dependencies of the public header, one needs to visit public
+     (not internal, not private) functions and type declarations, and
+     - skip the body of functions unless they are "static header", and
+     - skip the body of type declarations marked as C abstract structs
+   - to compute the dependencies of the internal header, same deal
+   - to compute the dependencies of the C header, same deal except all bodies
+     are visited
+*)
 
 module StringSet = Set.Make(String)
 module LidSet = Idents.LidSet
@@ -227,11 +243,30 @@ type deps = {
   public: StringSet.t;
 }
 
+type all_deps = {
+  h: deps;
+  internal_h: deps;
+  c: deps;
+}
+
 let empty_deps = { internal = StringSet.empty; public = StringSet.empty }
 
 let drop_dinstinction { internal; public } =
   List.of_seq (StringSet.to_seq (StringSet.union internal public))
 
+class record_everything gen_dep = object
+  inherit [_] reduce
+  method plus { internal = i1; public = p1 } { internal = i2; public = p2 } =
+    { internal = StringSet.union i1 i2; public = StringSet.union p1 p2 }
+  method zero = empty_deps
+  method! visit_EQualified _ lid =
+    gen_dep lid
+  method! visit_TQualified _ lid =
+    gen_dep lid
+  method! visit_TApp () lid _ =
+    gen_dep lid
+end
+
 let direct_dependencies_with_internal files file_of =
   (* Set of decls marked as internal *)
   let internal = List.fold_left (fun set (_, decls) ->
@@ -247,29 +282,61 @@ let direct_dependencies_with_internal files file_of =
     let gen_dep (callee: lident) =
       match file_of callee with
       | Some f when f <> fst file && not (Helpers.is_primitive callee) ->
-          (* KPrint.bprintf "In file %s, reference to %a (in file %s)\n" *)
-          (*   (fst file) PrintAst.plid callee f; *)
-          if LidSet.mem callee internal then
+          let is_internal = LidSet.mem callee internal in
+          KPrint.bprintf "In file %s, reference to %a (in %sheader %s)\n"
+            (fst file) PrintAst.plid callee (if is_internal then "internal " else "") f;
+          if is_internal then
             { empty_deps with internal = StringSet.singleton f }
           else
             { empty_deps with public = StringSet.singleton f }
       | _ ->
           empty_deps
     in
-    let deps =
-      (object
-        inherit [_] reduce
-        method plus { internal = i1; public = p1 } { internal = i2; public = p2 } =
-          { internal = StringSet.union i1 i2; public = StringSet.union p1 p2 }
-        method zero = empty_deps
-        method! visit_EQualified _ lid =
-          gen_dep lid
-        method! visit_TQualified _ lid =
-          gen_dep lid
-        method! visit_TApp _ lid _ =
-          gen_dep lid
-      end)#visit_file () file
-    in
+    let is_inline_static lid = List.exists (fun p -> Bundle.pattern_matches_lid p lid) !Options.static_header in
+    let header_deps which = object
+      inherit (record_everything gen_dep) as super
+
+      method! visit_DFunction env cc flags n_cgs n ret name binders body =
+        let concerns_us =
+          match which with
+          | `Public -> not (List.mem Common.Internal flags) && not (List.mem Common.Private flags)
+          | `Internal ->  List.mem Common.Internal flags
+        in
+        if concerns_us then
+          if is_inline_static name then
+            super#visit_DFunction env cc flags n_cgs n ret name binders body
+          else
+            (* ill-typed, but convenient *)
+            super#visit_DFunction env cc flags n_cgs n ret name binders Helpers.eunit
+        else
+          super#zero
+
+      method! visit_DType env name flags n_cgs n def =
+        let concerns_us =
+          match which with
+          | `Public -> not (List.mem Common.Internal flags) && not (List.mem Common.Private flags)
+          | `Internal ->  List.mem Common.Internal flags
+        in
+        let is_c_abstract_struct = List.mem Common.AbstractStruct flags in
+        if concerns_us then
+          if is_c_abstract_struct then
+            super#visit_DType env name flags n_cgs n (Abbrev TUnit)
+          else
+            super#visit_DType env name flags n_cgs n def
+        else
+          super#zero
+    end in
+    let deps = {
+      h = (KPrint.bprintf "PUBLIC %s\n" (fst file); header_deps `Public)#visit_file () file;
+      internal_h = (KPrint.bprintf "INTERNAL %s\n" (fst file); header_deps `Internal)#visit_file () file;
+      c = (KPrint.bprintf "C %s\n" (fst file); new record_everything gen_dep)#visit_file () file;
+    } in
+
+    if not (StringSet.is_empty deps.h.internal) then
+      Warn.fatal_error "Unexpected: %s depends on some internal headers: %s\n"
+        (fst file)
+        (String.concat ", " (List.of_seq (StringSet.to_seq deps.h.internal)));
+       
     StringMap.add (fst file) deps by_file
   ) StringMap.empty files
 
diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml
index f8c9cf9b..f4545166 100644
--- a/lib/CStarToC11.ml
+++ b/lib/CStarToC11.ml
@@ -1522,19 +1522,18 @@ let mk_headers (map: GlobalNames.mapping)
   ) [] files in
   List.rev headers
 
-let drop_empty_headers deps headers: Bundles.deps Bundles.StringMap.t =
+let drop_empty_headers deps headers: Bundles.all_deps Bundles.StringMap.t =
   let open Bundles in
   (* Refine dependencies to ignore now-gone empty headers. *)
-  let not_dropped_internal f = List.exists (function
-    | (name, C.Internal _) when f = name -> true
-    | _ -> false
-  ) headers in
-  let not_dropped_public f = List.exists (function
-    | (name, Public _) when f = name -> true
-    | _ -> false
-  ) headers in
-  StringMap.map (fun { internal; public } -> {
+  let kept_internal = List.filter_map (function (name, C.Internal _) -> Some name | _ -> None) headers in
+  let kept_public = List.filter_map (function (name, C.Public _) -> Some name | _ -> None) headers in
+  let not_dropped_internal f = List.mem f kept_internal in
+  let not_dropped_public f = List.mem f kept_public in
+  let filter_dep { internal; public } = {
     internal = StringSet.filter not_dropped_internal internal;
     public = StringSet.filter not_dropped_public public
-  }) deps
+  } in
+  StringMap.map (fun { h; internal_h; c } ->
+    { h = filter_dep h; internal_h = filter_dep internal_h; c = filter_dep c }
+  ) deps
 
diff --git a/lib/Output.ml b/lib/Output.ml
index 0ae20222..47eb9b26 100644
--- a/lib/Output.ml
+++ b/lib/Output.ml
@@ -140,14 +140,15 @@ let maybe_create_internal_dir h =
   if List.exists (function (_, C11.Internal _) -> true | _ -> false) h then
     create_subdir "internal"
 
-let write_c files internal_headers deps =
+let write_c files internal_headers (deps: Bundles.all_deps Bundles.StringMap.t) =
   Driver.detect_fstar_if ();
   Driver.detect_karamel_if ();
   List.map (fun file ->
     let name, program = file in
-    let deps = Bundles.StringMap.find name deps in
-    let deps = List.of_seq (Bundles.StringSet.to_seq deps.Bundles.internal) in
-    let deps = List.map (fun f -> "internal/" ^ f) deps in
+    let all_deps = Bundles.StringMap.find name deps in
+    let internal_deps = List.of_seq (Bundles.StringSet.to_seq all_deps.Bundles.c.Bundles.internal) in
+    let public_deps = List.of_seq (Bundles.StringSet.to_seq all_deps.Bundles.c.Bundles.public) in
+    let deps = List.map (fun f -> "internal/" ^ f) internal_deps @ public_deps in
     let includes = includes_for ~is_c:true name deps in
     let header = string (header ()) ^^ hardline ^^ hardline in
     let internal = if Bundles.StringSet.mem name internal_headers then "internal/" else "" in
@@ -170,10 +171,14 @@ let write_c files internal_headers deps =
     name
   ) files
 
-let write_h files public_headers deps =
+let write_h files public_headers (deps: Bundles.all_deps Bundles.StringMap.t) =
   List.map (fun file ->
     let name, program = file in
-    let { Bundles.public; internal } = Bundles.StringMap.find name deps in
+    let all_deps = Bundles.StringMap.find name deps in
+    let { Bundles.public; internal } = match program with
+      | C11.Internal _ -> all_deps.Bundles.internal_h
+      | C11.Public _ -> all_deps.Bundles.h
+    in
     let public = List.of_seq (Bundles.StringSet.to_seq public) in
     let internal = List.of_seq (Bundles.StringSet.to_seq internal) in
     let original_name = name in