-- SPDX-License-Identifier: CC0-1.0
let Genode = env:DHALL_GENODE

let Prelude = Genode.Prelude

in    λ(boot : Genode.Boot.Type)
    → let child =
            { mapKey = "test", mapValue = Genode.Init.toStart boot.config }
      
      in  { config =
              Genode.Init::{
              , verbose = True
              , children =
                  toMap
                    { harness =
                        Genode.Init.Start::{
                        , binary = "sotest-harness"
                        , exitPropagate = True
                        , resources =
                            { caps = child.mapValue.resources.caps + 128
                            , ram =
                                  child.mapValue.resources.ram
                                + Genode.units.MiB 1
                            }
                        , config =
                            Some
                              ( Prelude.XML.element
                                  { name = "config"
                                  , attributes = Prelude.XML.emptyAttributes
                                  , content =
                                      [ Genode.Init.Start.toXML
                                          child.mapKey
                                          child.mapValue
                                      ]
                                  }
                              )
                        , routes =
                            [ Genode.ServiceRoute.parentLabel
                                "LOG"
                                (Some "SOTEST")
                                (Some "unlabeled")
                            ]
                        }
                    }
              }
          , rom =
              let manifest = env:MANIFEST
              
              in      Genode.Boot.toRomPaths
                        [ manifest.sotest-producer.bin.sotest-harness ]
                    # boot.rom
                  : Genode.Prelude.Map.Type Text Genode.Boot.Rom
          }