https://github.com/EasyCrypt/easycrypt
Revision dab7c477290c5f1a5a53c317edc089b63cf8e5bf authored by Cameron Low on 11 October 2021, 09:55:19 UTC, committed by GitHub on 11 October 2021, 09:55:19 UTC
Csidh group action
Tip revision: dab7c477290c5f1a5a53c317edc089b63cf8e5bf authored by Cameron Low on 11 October 2021, 09:55:19 UTC
Merge pull request #81 from Cameron-Low/csidh-group-action
Merge pull request #81 from Cameron-Low/csidh-group-action
Tip revision: dab7c47
ecPhlHiCond.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcUtils
open EcFol
open EcCoreGoal
open EcLowGoal
open EcLowPhlGoal
open EcPhlCond
(* -------------------------------------------------------------------- *)
let process_cond info tc =
let default_if (i : EcParsetree.codepos1 option) s =
ofdfl (fun _ -> Zpr.cpos (tc1_pos_last_if tc s)) i in
match info with
| `Head side ->
t_hS_or_bhS_or_eS
~th:t_hoare_cond ~tbh:t_bdhoare_cond ~te:(t_equiv_cond side) tc
| `Seq (side, (i1, i2), f) ->
let es = tc1_as_equivS tc in
let f = EcProofTyping.tc1_process_prhl_formula tc f in
let n1 = default_if i1 es.es_sl in
let n2 = default_if i2 es.es_sr in
FApi.t_seqsub (EcPhlApp.t_equiv_app (n1, n2) f)
[ t_id; t_equiv_cond side ] tc
| `SeqOne (s, i, f1, f2) ->
let es = tc1_as_equivS tc in
let n = default_if i (match s with `Left -> es.es_sl | `Right -> es.es_sr) in
let f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in
let f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in
FApi.t_seqsub
(EcPhlApp.t_equiv_app_onesided s n f1 f2)
[ t_id; t_bdhoare_cond] tc
Computing file changes ...