cryspen/hax

`while let .. = .. {}`

Open

#113 opened on Jun 2, 2023

View on GitHubContributor guide
 (1 comment) (0 reactions) (0 assignees)OCaml (61 forks)auto 404
enginegood first issuehelp wantedkeep-openunsupported-rust

Repository metrics

Stars
 (456 stars)
PR merge metrics
 (PR metrics pending)

Description

Early in the pipeline, the Rust compiler expands every kind of loops (while, while let, for) as plain loops. Thus, what we see in the engine are only loops.

Loops in the AST of hax are designed to be flexible: either we deal with plain loops, or with specific loop kinds. ASTs can allow or disable (by type) any loop kind.

For for loops, we have two different possible special handlings. Loops that look like for loops can be reshaped into proper iterator-based fors or into range-based fors.

  • reconstruct while let loops.

(see https://github.com/hacspec/hax/issues/522 for simple whiles)

Contributor guide

Research direction
Examine the AST definition for loop kinds in engine/lib/ast.ml, understand how loops are currently handled for 'while', and implement the reconstruction of 'while let' loops by following a similar pattern. Look at how 'for' loops are reshaped for reference.
Tech stack
rust
Domain
compilerstooling
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
OCamlRustAST manipulation
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30