Skip to content

Porting feature #1108 and #905 from mlkem-native to mldsa-native #413

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
+195 −64
Open

Porting feature #1108 and #905 from mlkem-native to mldsa-native #413

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a244f8a
lint, autogen, format: Improve and unify UX
willieyz Aug 6, 2025
04ff52a
CBMC tests: Allow wildcard pattern in list of proofs to run
willieyz Aug 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 59 additions & 14 deletions scripts/autogen
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,44 @@ montgomery_factor = pow(2, 32, modulus)
# - header guards


# Standard color definitions
GREEN = "\033[32m"
RED = "\033[31m"
BLUE = "\033[94m"
BOLD = "\033[1m"
NORMAL = "\033[0m"


def clear_status_line():
"""Clear any existing status line by overwriting with spaces and returning to start of line"""
print(f"\r{' ' * 160}", end="", flush=True)


def status_update(task, msg):
print(f"\r{'':<140}", end="", flush=True)
print(f"\r[{task}]: {msg} ...", end="", flush=True)
clear_status_line()
print(f"\r{BLUE}[{task}]{NORMAL}: {msg} ...", end="", flush=True)


def high_level_status(msg):
clear_status_line()
print(
f"\r{GREEN}✓{NORMAL} {msg}"
) # This will end with a newline, clearing the status line


def info(msg):
clear_status_line()
print(f"\r{GREEN}info{NORMAL} {msg}")


def error(msg):
clear_status_line()
print(f"\r{RED}error{NORMAL} {msg}")


def file_updated(filename):
clear_status_line()
print(f"\r{BOLD}updated {filename}{NORMAL}")


def gen_header():
Expand Down Expand Up @@ -237,7 +272,7 @@ class CondParser:
return CondParser.print_exp(self.parse_condition(filename, exp))


def adjust_preprocessor_comments_for_filename(content, source_file):
def adjust_preprocessor_comments_for_filename(content, source_file, show_status=False):
"""Automatically add comments to large `#if ... #else ... #endif`
blocks indicating the guarding conditions.
Expand Down Expand Up @@ -267,7 +302,8 @@ def adjust_preprocessor_comments_for_filename(content, source_file):
```
"""
status_update("if-else", source_file)
if show_status:
status_update("if-else", source_file)

content = content.split("\n")
new_content = []
Expand Down Expand Up @@ -387,7 +423,9 @@ def adjust_preprocessor_comments_for_filename(content, source_file):
def gen_preprocessor_comments_for(source_file, dry_run=False):
with open(source_file, "r") as f:
content = f.read()
new_content = adjust_preprocessor_comments_for_filename(content, source_file)
new_content = adjust_preprocessor_comments_for_filename(
content, source_file, show_status=True
)
update_file(source_file, new_content, dry_run=dry_run)


Expand All @@ -399,13 +437,20 @@ def gen_preprocessor_comments(dry_run=False):
)


def update_file(filename, content, dry_run=False, force_format=False):

def update_file(
filename,
content,
dry_run=False,
force_format=False,
skip_preprocessor_comments=False,
):
if force_format is True or filename.endswith((".c", ".h", ".i")):
content = adjust_preprocessor_comments_for_filename(content, filename)
if skip_preprocessor_comments is False:
content = adjust_preprocessor_comments_for_filename(content, filename)
content = format_content(content)

if dry_run is False:
file_updated(filename)
with open(filename, "w+") as f:
f.write(content)
else:
Expand All @@ -416,11 +461,10 @@ def update_file(filename, content, dry_run=False, force_format=False):
current_content = f.read()
if current_content != content:
filename_new = f"{filename}.new"
print(
f"Autogenerated file {filename} needs updating. Have you called scripts/autogen?",
file=sys.stderr,
error(
f"Autogenerated file {filename} needs updating. Have you called scripts/autogen?"
)
print(f"Writing new version to {filename_new}", file=sys.stderr)
info(f"Writing new version to {filename_new}")
with open(filename_new, "w") as f:
f.write(content)
subprocess.run(["diff", filename, filename_new])
Expand Down Expand Up @@ -1035,10 +1079,11 @@ def _main():
gen_aarch64_rej_uniform_eta_table(args.dry_run)
gen_avx2_zeta_file(args.dry_run)
gen_avx2_rej_uniform_table(args.dry_run)
high_level_status("Generated zeta and lookup tables")
gen_header_guards(args.dry_run)
high_level_status("Generated header guards")
gen_preprocessor_comments(args.dry_run)

print()
high_level_status("Generated preprocessor comments")


if __name__ == "__main__":
Expand Down
23 changes: 16 additions & 7 deletions scripts/format
View file
Open in desktop
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see that the format script has diverged from mlkem-native.
Can we consolidate that by either fixing it in this PR, or opening an issue.
I see there is already #158 for the magic constant, but there are 3 more difference:

  • check-constracts
  • shell linting
  • copyright checking

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hello, Matthias,
Thank you for your reviewing, open issue:

Original file line number Diff line number Diff line change
Expand Up @@ -10,40 +10,49 @@ set -o pipefail
# consts
ROOT="$(realpath "$(dirname "$0")"/../)"

GREEN="$(tput setaf 2)"
NORMAL="$(tput sgr0)"
# Standard color definitions
GREEN="\033[32m"
RED="\033[31m"
BLUE="\033[94m"
BOLD="\033[1m"
NORMAL="\033[0m"

# utility
info()
{
printf "%s %b\n" "${GREEN}info" "${NORMAL}${*}"
printf "%b %b\n" "${GREEN}info" "${NORMAL}${*}"
}

error()
{
printf "%b %b\n" "${RED}error" "${NORMAL}${*}"
}

info "Formatting nix files"
if ! command -v nixpkgs-fmt 2>&1 >/dev/null; then
echo "nixpkgs-fmt not found. Are you running in a nix shell? See BUILDING.md."
error "nixpkgs-fmt not found. Are you running in a nix shell? See BUILDING.md."
exit 1
fi

nixpkgs-fmt "$ROOT"

info "Formatting shell scripts"
if ! command -v shfmt 2>&1 >/dev/null; then
echo "shfmt not found. Are you running in a nix shell? See BUILDING.md."
error "shfmt not found. Are you running in a nix shell? See BUILDING.md."
exit 1
fi
shfmt -s -w -l -i 2 -ci -fn $(shfmt -f $(git grep -l '' :/))

info "Formatting python scripts"
if ! command -v black 2>&1 >/dev/null; then
echo "black not found. Are you running in a nix shell? See BUILDING.md."
error "black not found. Are you running in a nix shell? See BUILDING.md."
exit 1
fi
black --include "(scripts/tests|scripts/simpasm|scripts/autogen|scripts/check-namespace|\.py$)" "$ROOT"

info "Formatting c files"
if ! command -v clang-format 2>&1 >/dev/null; then
echo "clang-format not found. Are you running in a nix shell? See BUILDING.md."
error "clang-format not found. Are you running in a nix shell? See BUILDING.md."
exit 1
fi

Expand Down
131 changes: 103 additions & 28 deletions scripts/lint
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,29 @@ set -o pipefail
ROOT="$(realpath "$(dirname "$0")"/../)"
GITHUB_STEP_SUMMARY=${GITHUB_STEP_SUMMARY:-/dev/stdout}

# Check if we're in GitHub context
IN_GITHUB_CONTEXT=false
if [[ $GITHUB_STEP_SUMMARY != "/dev/stdout" ]]; then
IN_GITHUB_CONTEXT=true
fi

# Standard color definitions
GREEN="\033[32m"
RED="\033[31m"
BLUE="\033[94m"
BOLD="\033[1m"
NORMAL="\033[0m"

info()
{
printf "%b %b\n" "${GREEN}✓" "${NORMAL}${*}"
}

error()
{
printf "%b %b\n" "${RED}✗" "${NORMAL}${*}"
}

checkerr()
{
local code=$?
Expand All @@ -22,44 +45,92 @@ checkerr()
fi

if [[ ${#out} != 0 ]]; then
echo "$out" | while read -r file line; do
echo "::error file=$file,line=${line:-1},title=Format error::$file require to be formatted"
done
if $IN_GITHUB_CONTEXT; then
echo "$out" | while read -r file line; do
echo "::error file=$file,line=${line:-1},title=Format error::$file require to be formatted"
done
fi
success=false
fi

if $success; then
echo ":white_check_mark: $title" >>"$GITHUB_STEP_SUMMARY"
info "$title"
gh_summary_success "$title"
else
error "$title"
SUCCESS=false
echo ":x: $title" >>"$GITHUB_STEP_SUMMARY"
gh_summary_failure "$title"
fi
}

gh_group_start()
{
if $IN_GITHUB_CONTEXT; then
echo "::group::$1"
fi
}

gh_group_end()
{
if $IN_GITHUB_CONTEXT; then
echo "::endgroup::"
fi
}

gh_summary_success()
{
if $IN_GITHUB_CONTEXT; then
echo ":white_check_mark: $1" >>"$GITHUB_STEP_SUMMARY"
fi
}

gh_summary_failure()
{
if $IN_GITHUB_CONTEXT; then
echo ":x: $1" >>"$GITHUB_STEP_SUMMARY"
fi
}

gh_error()
{
if $IN_GITHUB_CONTEXT; then
echo "::error file=$1,line=${2:-1},title=$3::$4"
fi
}

gh_error_simple()
{
if $IN_GITHUB_CONTEXT; then
echo "::error title=$1::$2"
fi
}

# Formatting
SUCCESS=true

echo "::group::Linting nix files with nixpkgs-fmt"
gh_group_start "Linting nix files with nixpkgs-fmt"
checkerr "Lint nix" "$(nixpkgs-fmt --check "$ROOT")"
echo "::endgroup::"
gh_group_end

#echo "::group::Linting shell scripts with shfmt"
#gh_group_start "Linting shell scripts with shfmt"
#checkerr "Lint shell" "$(shfmt -s -l -i 2 -ci -fn $(shfmt -f $(git grep -l '' :/)))"
#echo "::endgroup::"
#gh_group_end

echo "::group::Linting python scripts with black"
gh_group_start "Linting python scripts with black"
if ! diff=$(black --check --diff -q --include "(scripts/tests|scripts/simpasm|scripts/autogen|scripts/check-namespace|\.py$)" "$ROOT"); then
echo "::error title=Format error::$diff"
gh_error_simple "Format error" "$diff"
error "Lint python"
SUCCESS=false
echo ":x: Lint python" >>"$GITHUB_STEP_SUMMARY"
gh_summary_failure "Lint python"
else
echo ":white_check_mark: Lint Python" >>"$GITHUB_STEP_SUMMARY"
info "Lint Python"
gh_summary_success "Lint Python"
fi
echo "::endgroup::"
gh_group_end

echo "::group::Linting c files with clang-format"
gh_group_start "Linting c files with clang-format"
checkerr "Lint C" "$(clang-format $(git ls-files ":/*.c" ":/*.h") --Werror --dry-run 2>&1 | grep "error:" | cut -d ':' -f 1,2 | tr ':' ' ')"
echo "::endgroup::"
gh_group_end

check-eol-dry-run()
{
Expand All @@ -71,52 +142,56 @@ check-eol-dry-run()
fi
done
}
echo "::group::Checking eol"
gh_group_start "Checking eol"
checkerr "Check eol" "$(check-eol-dry-run)"
echo "::endgroup::"
gh_group_end

check-spdx()
{
local success=true
for file in $(git ls-files -- ":/" ":/!:*.json" ":/!:*.png" ":/!:*LICENSE*" ":/!:.git*" ":/!:flake.lock"); do
# Ignore symlinks
if [[ ! -L $file && $(grep "SPDX-License-Identifier:" $file | wc -l) == 0 ]]; then
echo "::error file=$file,line=${line:-1},title=Missing license header error::$file is missing SPDX License header"
gh_error "$file" "${line:-1}" "Missing license header error" "$file is missing SPDX License header"
success=false
fi
done
for file in $(git ls-files -- "*.[chsS]" "*.py" ":/!proofs/cbmc/*.py"); do
# Ignore symlinks
if [[ ! -L $file && $(grep "Copyright (c) The mldsa-native project authors" $file | wc -l) == 0 ]]; then
echo "::error file=$file,line=${line:-1},title=Missing copyright header error::$file is missing copyright header"
gh_error "$file" "${line:-1}" "Missing copyright header error" "$file is missing copyright header"
success=false
fi
done

if $success; then
echo ":white_check_mark: Check SPDX + Copyright" >>"$GITHUB_STEP_SUMMARY"
info "Check SPDX + Copyright"
gh_summary_success "Check SPDX + Copyright"
else
error "Check SPDX + Copyright"
SUCCESS=false
echo ":x: Check SPDX + Copyright" >>"$GITHUB_STEP_SUMMARY"
gh_summary_failure "Check SPDX + Copyright"
fi
}
echo "::group::Checking SPDX + Copyright headers"
gh_group_start "Checking SPDX + Copyright headers"
check-spdx
echo "::endgroup::"
gh_group_end

check-autogenerated-files()
{
if python3 $ROOT/scripts/autogen --dry-run; then
echo ":white_check_mark: Check native auto-generated files" >>"$GITHUB_STEP_SUMMARY"
info "Check native auto-generated files"
gh_summary_success "Check native auto-generated files"
else
echo ":x: Check native auto-generated files" >>"$GITHUB_STEP_SUMMARY"
error "Check native auto-generated files"
gh_summary_failure "Check native auto-generated files"
SUCCESS=false
fi
}

echo "::group::Check native auto-generated files"
gh_group_start "Check native auto-generated files"
check-autogenerated-files
echo "::endgroup::"
gh_group_end

if ! $SUCCESS; then
exit 1
Expand Down
Loading
Loading