How does the Fμω lambda calculus use C?

Question

While poking around in the repositories I wondered how the sha2_256 algorithm was implemented in the PlutusTx module. I followed all the imports and got the following path

1. The sha2_256 function in PlutusTx.Builtins is defined at (1). In this module it is imported from a internal module with import name BI.

{-# INLINABLE sha2_256 #-}
-- | The SHA2-256 hash of a 'ByteString'
sha2_256 :: BuiltinByteString -> BuiltinByteString
sha2_256 = BI.sha2_256

2. This BI.sha2_256 function in the PlutusTx.Builtins.Internal is defined at (2). Here the function is wrapped in the BuiltinByteString type. A function is imported from the the Hash module.

{-# NOINLINE sha2_256 #-}
sha2_256 :: BuiltinByteString -> BuiltinByteString
sha2_256 (BuiltinByteString b) = BuiltinByteString $ Hash.sha2 b

3. This Hash.sha2 function in the Data.ByteString.Hash is defined at (3). Here it gets a bit more complicated. A cryptographic hash function takes an arbitrary block of data and calculates a fixed-size bit string (the digest). Since there may be other hash function (like the SHA3_256 version in PlutusTx) the function is abstracted to a general hash function where the type inferred by the type application @SHA256). This data type and its instance of a hash algorithm is imported from Cardano.Crypto.Hash.SHA256.

-- | Hash a [[BSL.ByteString]] using the SHA-256 hash function.
sha2 :: BS.ByteString -> BS.ByteString
sha2 = digest (Proxy @SHA256)

4. In this cardano-base package the module Cardano.Crypto.Hash.SHA256 defines the data type SHA256 and its instance of a hash algorithm at (4). The function sha256_libsodium is also defined there. This function uses another function called c_crypto_hash_sha256, this is where it gets interesting imported from the module Libsodium.C.

data SHA256

instance HashAlgorithm SHA256 where
  type SizeHash SHA256 = 32
  hashAlgorithmName _ = "sha256"
  digest _ = sha256_libsodium

5. The function c_crypto_hash_sha256 in Cardano.Crypto.Libsodium.C (like many other cryothographic derivatives used in cardano) is defined in (5). Here this function is actually import from the package Libsodium which is a library for encryption, decryption, signatures, password hashing and more written in C.

Now my question is, how is this lower level C function get used in the lower level Fμω lambda calculus onchain? Does each node just invoke/inject the C function once the lambda calculus references it?