Skip to content
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.

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

Transformation of control flow into monads: support continue, break and return #96

Closed
W95Psp opened this issue May 24, 2023 · 4 comments
Assignees
Labels
engine Issue in the engine help wanted Extra attention is needed marked-unimplemented Issue refered by `Unimplemented {issue_id...}` in the engine

Comments

@W95Psp
Copy link
Collaborator

W95Psp commented May 24, 2023

No description provided.

@W95Psp
Copy link
Collaborator Author

W95Psp commented May 30, 2023

This is related to #28: causes an issue with tls_cryptolib

@lassebramer
Copy link

Ran into this error:

error[CE0001]: (Diagnostics.Context.Phase CfIntoMonads): something is not implemented yet. This is discussed in issue 96: please upvote or comment this issue if you see this error message.
               TODO: Monad for loop-related control flow
   --> pasta/src/pasta.rs:783:5
    |
783 | /     for _ in 0..loop_upper_bound {
784 | |         if check_not_zero(r.clone()) && degree_polyx(r.clone()) >= degree_polyx(d.clone()) {
785 | |             let t: Polyx = divide_leading_terms(r.clone(), d.clone());
786 | |
...   |
790 | |         }
791 | |     }
    | |_____^

Full function here:

pub fn divide_poly(n: Polyx, d: Polyx) -> (Polyx, Polyx) {
    let mut q: Polyx = Seq::<FpVesta>::create(n.len());
    let mut r: Polyx = n.clone();

    let mut loop_upper_bound = d.len();
    if q.len() > d.len() {
        loop_upper_bound = q.len();
    }
    for _ in 0..loop_upper_bound {
        if check_not_zero(r.clone()) && degree_polyx(r.clone()) >= degree_polyx(d.clone()) {
            let t: Polyx = divide_leading_terms(r.clone(), d.clone());

            q = add_polyx(q, t.clone());
            let aux_prod: Polyx = mul_polyx(d.clone(), t.clone());
            r = sub_polyx(r, aux_prod);
        }
    }

    (trim_poly(q), trim_poly(r))
}

@W95Psp
Copy link
Collaborator Author

W95Psp commented May 31, 2023

Thanks for your bug report! This for loop contains no break or continue; thus I suspect hax is not reconstructing properly a for loop. I opened #105 for tracking that specifically.

@W95Psp W95Psp added bug Something isn't working engine Issue in the engine and removed bug Something isn't working labels Jun 6, 2023
@W95Psp W95Psp changed the title Transformation of control flow into monads: support continue and break Transformation of control flow into monads: support continue, break and return Jun 16, 2023
@W95Psp W95Psp added the marked-unimplemented Issue refered by `Unimplemented {issue_id...}` in the engine label Jun 23, 2023
W95Psp added a commit that referenced this issue Jun 30, 2023
The `Break` expression constructor of the AST was gated only by the
feature `loop`. This commit introduces the feature `break` and makes
the `Break` constructor gated by the witness tuple `break * loop`.

Thanks to that, the phase `Cf_into_monads` now can remove
`Break`-nodes in a type-safe manner. (though, for now, it removes
`Break`s in favor of a runtime error, see issue #96)
bors bot added a commit that referenced this issue Jul 4, 2023
170: Introduce feature `break` r=franziskuskiefer a=W95Psp

The `Break` expression constructor of the AST was gated only by the feature `loop`. This commit introduces the feature `break` and makes the `Break` constructor gated by the witness tuple `break * loop`.

Thanks to that, the phase `Cf_into_monads` now can remove `Break`-nodes in a type-safe manner. (though, for now, it removes `Break`s in favor of a runtime error, see issue #96)

~**PR #169 should be merged before this PR**~ ✔️

Co-authored-by: Lucas Franceschino <lucas.franceschino@inria.fr>
Co-authored-by: Franziskus Kiefer <franziskuskiefer@gmail.com>
@franziskuskiefer franziskuskiefer added the help wanted Extra attention is needed label Aug 21, 2023
@W95Psp
Copy link
Collaborator Author

W95Psp commented Jan 2, 2024

Closing in favor of #15

@W95Psp W95Psp closed this as completed Jan 2, 2024
chrysn added a commit to chrysn-pull-requests/edhoc-rs that referenced this issue May 23, 2024
chrysn added a commit to chrysn-pull-requests/edhoc-rs that referenced this issue May 23, 2024
chrysn added a commit to chrysn-pull-requests/edhoc-rs that referenced this issue May 23, 2024
geonnave pushed a commit to geonnave/lakers that referenced this issue May 29, 2024
W95Psp added a commit that referenced this issue Oct 2, 2024
Issue #96 was closed in favor of #15, this commit reflects that in code.
W95Psp added a commit that referenced this issue Oct 2, 2024
Issue #96 was closed in favor of #15, this commit reflects that in code.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
engine Issue in the engine help wanted Extra attention is needed marked-unimplemented Issue refered by `Unimplemented {issue_id...}` in the engine
Projects
No open projects
Status: Done
Development

No branches or pull requests

3 participants