Function entry_basename 

pub fn entry_basename(ctx: &CodegenContext) -> String

Basename for the entry file emitted by Lean / Dafny. Prefer the source-declared module name (module Foo → Foo) so the entry file’s name matches what the user wrote; fall back to a capitalised project name when no module declaration is present. Lake’s path-as-module-name convention forces this for Lean — Dafny doesn’t strictly need it but the same basename keeps the two backends aligned (no more playground.dfy vs OracleTrace.lean).